Difference between revisions of "Term Rewriting"

Revision as of 07:48, 17 April 2024

General

We use an adaption of the ARI format. 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, whereas COCO uses a more liberal definition. Both simple and quoted symbols are allowed. To ease parsing, we impose the following additional restrictions:
- 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.
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? )
cond ::= :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

@@ Line 4: / Line 4: @@
 * We do not impose any variable conditions, so a rewrite rule is a pair of arbitrary terms.
-* Identifiers 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 [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. To ease parsing, we impose the following additional restrictions:
+** Quoted identifiers must not contain whitespace, parantheses, or semicolons.
+** 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.
 * 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>