Difference between revisions of "Term Rewriting"

From Termination-Portal.org
Jump to navigationJump to search
 
(12 intermediate revisions by 2 users not shown)
Line 1: Line 1:
−
We use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format]. Our format differs from the formt used at COCO as follows:
+
== General ==
 +
 
 +
We use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format], so TRSs are represented as S-Expressions (see [https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf here, Sec. 3.1]). Our format differs from the format used at CoCo as follows:
  
 
* We do not impose any variable conditions, so a rewrite rule is a pair of arbitrary terms.
 
* We do not impose any variable conditions, so a rewrite rule is a pair of arbitrary terms.
−
* Identifiers (i.e., names of variables or function symbols) must be valid [https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf SMT-LIB symbols], whereas COCO uses a more liberal definition. Both simple and quoted symbols are allowed.
+
* Identifiers must be valid SMT-LIB symbols (see [https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf here, Sec. 3.2]), whereas CoCo uses a more liberal definition. Both simple and quoted symbols are allowed. As in SMT-LIB, simple symbols must not be equal to reserved words. In our case, the reserved words are: <pre>fun, rule, format, sort, theory, define-fun, prule, -></pre> To ease parsing, we impose the following additional restrictions:
−
* Rules are annotated with optional costs, which are natural numbers. So rules are defined as follows:
+
** Quoted identifiers must be non-empty.
−
<code>
+
** Quoted identifiers must not contain whitespace, parantheses, or semicolons.
−
rule ::= ( rule term term cost?)
+
** All occurrences of the same identifier must be either quoted or unquoted. So <pre>(rule |a| |a|)</pre> is valid, but <pre>(rule a |a|)</pre> is invalid.
−
cond ::= :cost number
+
** Use sane identifiers. For example, <pre>a->a</pre> is a valid identifier, but it will cause confusion, so using it is a bad idea.
−
</code>
+
* Rules are annotated with optional costs, which are natural numbers. This allows, e.g., to model relative rewriting (by setting the cost of relative rules to 0). Categories may disallow costs. So rules are defined as follows:
 +
<pre>
 +
rule ::= ( rule term term cost? )
 +
cost ::= :cost number
 +
</pre>
 +
 
 +
In contrast to the former XTC format, the goal of the analysis is implicitly specified by the category.
 +
 
 +
== Termination ==
 +
 
 +
All termination categories consider termination w.r.t. arbitrary start terms.
 +
 
 +
=== Relative Termination ===
 +
 
 +
All categories for relative termination consider full rewriting.
 +
See [https://project-coco.uibk.ac.at/ARI/trs.php here] for the format of all categories for relative termination.
 +
 
 +
==== TRS Relative ====
 +
 
 +
* no further restrictions
 +
 
 +
==== SRS Relative ====
 +
 
 +
* just unary function symbols
 +
 
 +
=== Non-Relative Termination ===
 +
 
 +
All categories for non-relative termination disallow costs.
 +
 
 +
==== TRS Standard ====
 +
 
 +
* full rewriting
 +
* see [https://project-coco.uibk.ac.at/ARI/trs.php here]
 +
 
 +
==== SRS Standard ====
 +
 
 +
* full rewriting
 +
* just unary function symbols
 +
* see [https://project-coco.uibk.ac.at/ARI/trs.php here]
 +
 
 +
==== TRS Contextsensitive ====
 +
 
 +
* context-sensitive rewriting
 +
* see [https://project-coco.uibk.ac.at/ARI/cstrs.php here]
 +
 
 +
==== TRS Equational ====
 +
 
 +
Here, a ''theory'' may be added to declarations of function symbols.
 +
 
 +
<pre>
 +
fun ::= ( fun identifier number theory? )
 +
theory ::= :theory [A | C | AC]
 +
</pre>
 +
 
 +
* full rewriting modulo associativity / commutativity / associativity and commutativity
 +
 
 +
==== TRS Innermost ====
 +
 
 +
* innermost rewriting
 +
* see [https://project-coco.uibk.ac.at/ARI/trs.php here]
 +
 
 +
==== TRS Outermost ====
 +
 
 +
* outermost rewriting
 +
* see [https://project-coco.uibk.ac.at/ARI/trs.php here]
 +
 
 +
==== TRS Conditional ====
 +
 
 +
* full conditional rewriting
 +
* see [https://project-coco.uibk.ac.at/ARI/ctrs.php here]
 +
* currently, we only support the condition-type ''oriented''
 +
 
 +
==== TRS Conditional - Operational Termination ====
 +
 
 +
* TODO clarify the difference to ''TRS Conditional''
 +
* see [https://project-coco.uibk.ac.at/ARI/ctrs.php here]
 +
* currently, we only support the condition-type ''oriented''
 +
 
 +
== Complexity ==
 +
 
 +
See [https://project-coco.uibk.ac.at/ARI/trs.php here] for all complexity categories.
 +
 
 +
=== Runtime Complexity ===
 +
 
 +
All categories for runtime complexity consider basic start terms only.
 +
 
 +
==== Runtime Complexity Innermost ====
 +
 
 +
* innermost rewriting
 +
 
 +
==== Runtime Complexity Full ====
 +
 
 +
* full rewriting
 +
 
 +
=== Derivational Complexity ===
 +
 
 +
All categories for derivational complexity consider arbitrary start terms.
 +
 
 +
==== Derivational Complexity Innermost ====
 +
 
 +
* innermost rewriting
 +
 
 +
==== Derivational Complexity Full ====
 +
 
 +
* full rewriting

Latest revision as of 07:37, 15 July 2024

General

We use an adaption of the ARI format, so TRSs are represented as S-Expressions (see here, Sec. 3.1). Our format differs from the format used at CoCo as follows:

  • We do not impose any variable conditions, so a rewrite rule is a pair of arbitrary terms.
  • Identifiers must be valid SMT-LIB symbols (see here, Sec. 3.2), whereas CoCo uses a more liberal definition. Both simple and quoted symbols are allowed. As in SMT-LIB, simple symbols must not be equal to reserved words. In our case, the reserved words are: 
    fun, rule, format, sort, theory, define-fun, prule, ->
    To ease parsing, we impose the following additional restrictions:
    • Quoted identifiers must be non-empty.
    • Quoted identifiers must not contain whitespace, parantheses, or semicolons.
    • All occurrences of the same identifier must be either quoted or unquoted. So 
      (rule |a| |a|)
      is valid, but 
      (rule a |a|)
      is invalid.
    • Use sane identifiers. For example, 
      a->a
      is a valid identifier, but it will cause confusion, so using it is a bad idea.
  • Rules are annotated with optional costs, which are natural numbers. This allows, e.g., to model relative rewriting (by setting the cost of relative rules to 0). Categories may disallow costs. So rules are defined as follows:
rule ::= ( rule term term cost? )
cost ::= :cost number

In contrast to the former XTC format, the goal of the analysis is implicitly specified by the category.

Termination

All termination categories consider termination w.r.t. arbitrary start terms.

Relative Termination

All categories for relative termination consider full rewriting. See here for the format of all categories for relative termination.

TRS Relative

  • no further restrictions

SRS Relative

  • just unary function symbols

Non-Relative Termination

All categories for non-relative termination disallow costs.

TRS Standard

  • full rewriting
  • see here

SRS Standard

  • full rewriting
  • just unary function symbols
  • see here

TRS Contextsensitive

  • context-sensitive rewriting
  • see here

TRS Equational

Here, a theory may be added to declarations of function symbols. 

fun ::= ( fun identifier number theory? )
theory ::= :theory [A | C | AC]
  • full rewriting modulo associativity / commutativity / associativity and commutativity

TRS Innermost

  • innermost rewriting
  • see here

TRS Outermost

  • outermost rewriting
  • see here

TRS Conditional

  • full conditional rewriting
  • see here
  • currently, we only support the condition-type oriented

TRS Conditional - Operational Termination

  • TODO clarify the difference to TRS Conditional
  • see here
  • currently, we only support the condition-type oriented

Complexity

See here for all complexity categories.

Runtime Complexity

All categories for runtime complexity consider basic start terms only.

Runtime Complexity Innermost

  • innermost rewriting

Runtime Complexity Full

  • full rewriting

Derivational Complexity

All categories for derivational complexity consider arbitrary start terms.

Derivational Complexity Innermost

  • innermost rewriting

Derivational Complexity Full

  • full rewriting
Retrieved from "http://termination-portal.org/mediawiki/index.php?title=Term_Rewriting&oldid=2006"