Term rewriting system

The Term Rewriting Systems ( TES ) is a formal calculation model in theoretical computer science . In particular, they form the basis of logic and functional programming . They also play an important role in the word problem and termination analysis .

Term replacement systems are sets of term replacement rules . These sets can be thought of as systems of equations between terms , in which the equations can only be applied from left to right.

example

   plus(0, y)  →  y
   plus(succ(x), y)  →   succ(plus(x, y))

The above rules form a term replacement system, which can be understood as the addition of two natural numbers. This requires that you represent the number 0 with the term 0, the number 1 with the term succ (0), the number 2 with the term succ (succ (0)) and so on. The rules state that, for example, every occurrence of in a term can be replaced by. It can itself be any term, so it does not have to represent a natural number. ${\displaystyle \operatorname {plus} (0,y)}$ ${\displaystyle y}$ ${\displaystyle y}$

Term rewriting systems are Turing-complete , so, in terms of computational strength , they are in no way inferior to other formalisms such as the Turing machines , the lambda calculus or register machines . Since they have a comparatively simple structure and can be handled easily by computers, term rewriting systems are an important tool in the computer-aided analysis of algorithms.

Definitions

In order to set up a term replacement system, you first need a clear idea of ​​the underlying terms.

Terms

For a set of function symbols and an (infinite) set of variables , the set of terms is defined inductively as follows: ${\displaystyle \Sigma }$ ${\displaystyle {\mathcal {V}}}$ ${\displaystyle {\mathcal {T}}(\Sigma ,{\mathcal {V}})}$

• Each variable and zero-digit function symbol (i.e., constant) is a term.
• Are terms and is an n-place function symbol, is also a term. ${\displaystyle t_{1},\dots ,t_{n}}$ ${\displaystyle f}$ ${\displaystyle f(t_{1},\dots ,t_{n})}$

Note that this definition corresponds exactly to the definition of a mathematical term .

Without a formal definition, the following terms should also be mentioned:

• A substitution assigns new terms to some variables. A substitution acts on a term by replacing each occurrence of a variable with the term specified by the substitution. For example , if the substitution is and is a term, then is the term that results from applying to . ${\displaystyle \sigma =\{x/f(x,y)\}}$ ${\displaystyle t=g(x)}$ ${\displaystyle t\sigma =g(f(x,y))}$ ${\displaystyle \sigma }$ ${\displaystyle t}$
• A term matches a term if there is a substitution such that it holds. For example, matches the term . ${\displaystyle t}$ ${\displaystyle s}$ ${\displaystyle \sigma }$ ${\displaystyle t\sigma =s}$ ${\displaystyle g(x)}$ ${\displaystyle g(f(x,y))}$

Term replacement rules

A term replacement rule is a pair of two terms , where there must be no variable and no variable that does not also appear in . The reason for this restriction is related to the termination of a term replacement system and is explained in more detail in the relevant section. ${\displaystyle l\rightarrow r}$ ${\displaystyle l,r}$ ${\displaystyle l}$ ${\displaystyle r}$ ${\displaystyle l}$

The term replacement relation

The "functionality" of a term rewriting system is defined by the term rewriting relation . ${\displaystyle \rightarrow _{\mathcal {R}}}$

Clear description

If the left side of a rule matches a term or a sub-term of the rule, this left side can be replaced by the right side of the corresponding rule and a new term is thus obtained. This should be shown with a few examples. For this we consider the simple term rewriting system ${\displaystyle s}$ ${\displaystyle s}$ ${\displaystyle s}$ ${\displaystyle t}$

   f(x,y) → x

• The term can be evaluated with this rule . ${\displaystyle f(s(y),g(x))}$ ${\displaystyle s(y)}$
• ${\displaystyle g(f(a,b))}$one can evaluate. ${\displaystyle g(a)}$
• ${\displaystyle f(f(a,b),c)}$can be both to and to evaluate in one step . ${\displaystyle f(a,c)}$ ${\displaystyle f(a,b)}$

Formal definition

A term evaluates to , written if the following applies: ${\displaystyle s}$ ${\displaystyle t}$ ${\displaystyle s\rightarrow _{\mathcal {R}}t}$

• There is a substitution and ${\displaystyle \sigma }$
• a rule in such that ${\displaystyle l\rightarrow _{\mathcal {R}}r}$ ${\displaystyle {\mathcal {R}}}$
• ${\displaystyle s}$contains the term and ${\displaystyle l\sigma }$
• ${\displaystyle t}$contains the term in the same place , but otherwise matches. ${\displaystyle r\sigma }$ ${\displaystyle s}$

Questions

Depending on the area of ​​application of a term rewriting system, there are several questions that are of interest. These are among others:

Termination

The question arises whether there are terms for a term rewriting system that allow an infinite chain of evaluations , or whether all derivatives of all terms are always finite. If the latter is the case, it is also called terminating or well-founded. ${\displaystyle {\mathcal {R}}}$ ${\displaystyle s\rightarrow _{\mathcal {R}}s_{1}\rightarrow _{\mathcal {R}}s_{2}\rightarrow _{\mathcal {R}}\dots }$ ${\displaystyle {\mathcal {R}}}$

The question of termination is undecidable in every Turing-complete calculation system . However, there are a number of advanced techniques that can be used to automatically detect the termination of many term rewriting systems. A general approach is an educated order to find, so for all rules applies the TES. In addition, this order must be preserved when substituting substitutions for and (the order must be stable ) or when and appear as partial terms of another term (the order must be monotonic ). Numerous other methods exist. The terms can be interpreted as polynomials or matrices , for example , and a more detailed analysis of the interdependencies of the function symbols can be carried out. For this, please refer to the further literature. ${\displaystyle \succ }$ ${\displaystyle \rightarrow _{\mathcal {R}}\subseteq \succ }$ ${\displaystyle l\succ r}$ ${\displaystyle l\rightarrow _{\mathcal {R}}r}$ ${\displaystyle l}$ ${\displaystyle r}$ ${\displaystyle l}$ ${\displaystyle r}$

Confluence

There can be several possible derivatives starting from a term. With confluence refers to the property of a term rewriting system is that two terms that result in multiple steps in different ways from one output term can always be recombined into a term. A related question is whether the calculation described by a term rewriting system always produces the same result (unique normal form ) for the same input . Confluence is generally just as undecidable as termination.

A term rewriting system that is terminated and confluent is also called convergent . For such systems there is a unique normal form for each term. It can be decided whether a terminating term replacement system is confluent.

Applications

As a mathematically relatively easy to handle construct, term rewriting systems are suitable for the computer-aided treatment of problems from theoretical computer science. Some uses are:

Decision procedure for the word problem

A term equation system is a set of equations between terms. The word problem for means the question of whether an equation is true, provided that the equations are true. As an example one could code in the group axioms : ${\displaystyle {\mathcal {E}}}$ ${\displaystyle {\mathcal {E}}}$ ${\displaystyle s=t}$ ${\displaystyle {\mathcal {E}}}$ ${\displaystyle {\mathcal {E}}}$

   f(x, f(y,z))  =  f(f(x,y), z)
   f(x, e)       =  x
   f(x, i(x))    =  e

The two-digit function symbol stands for the group link, the single-digit function supplies the inverse elements, and the constant denotes the neutral element; , and are variables. One is now looking for a method to automatically check equations such as or for their truth content. ${\displaystyle f}$ ${\displaystyle i}$ ${\displaystyle e}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle z}$ ${\displaystyle i(e)=e}$ ${\displaystyle i(i(x))=x}$

For this purpose one constructs an equivalent and convergent term replacement system for the equation system . Equivalent here means that if and only if . The notation means that the term replacement relation can be used here as often as required and in both directions. ${\displaystyle {\mathcal {E}}}$ ${\displaystyle {\mathcal {R}}}$ ${\displaystyle s=t}$ ${\displaystyle s\leftrightarrow _{\mathcal {R}}^{*}t}$ ${\displaystyle \leftrightarrow _{\mathcal {R}}^{*}}$

If one has now given such a convergent TES, the word problem can be solved by evaluating simply and using in any way until no further evaluation is possible. Since the TES is convergent according to the assumption, there is no infinite evaluation. The procedure itself terminates. Since the TES is also confluent, it does not matter which of the possible evaluations you choose. If the evaluation of the two terms leads to one and the same term, then applies to the equations of . ${\displaystyle s=t}$ ${\displaystyle s}$ ${\displaystyle t}$ ${\displaystyle \rightarrow _{\mathcal {R}}}$ ${\displaystyle s=t}$ ${\displaystyle {\mathcal {E}}}$

Since the word problem is undecidable, it is not always possible to find a convergent term rewriting system that makes the word problem decidable for the corresponding system of equations. One method for constructing convergent term rewriting systems is the Knuth-Bendix completion method. If successful, it calculates an equivalent and convergent term replacement system for a given set of equations and a well-founded term order. However, neither the termination nor the success of the Knuth-Bendix completion procedure is guaranteed. For the case of the group axioms above, the Knuth-Bendix completion method calculates e.g. B. the following convergent term rewriting system:

   f(x, e)          ->  x
   f(e, x)          ->  x
   f(x, i(x))       ->  e
   f(i(x), x)       ->  e
   f(f(x,y), z)     ->  f(x, f(y,z))
   f(x, f(i(x),y))  ->  y
   f(i(x), f(x,y))  ->  y
   i(e)             ->  e
   i(i(x))          ->  x
   i(f(x, y))       ->  f(i(y), i(x))

Termination analysis

Since there are so many powerful techniques for term rewriting systems that can prove termination, programs of high-level programming languages ​​are transformed into term rewriting systems and these techniques are applied to them. The tool AProvE , which is being developed at RWTH Aachen University , has so far implemented this for the programming languages Prolog and Haskell .

The treatment of imperative and object-oriented languages, such as Java , is the subject of current research.

literature

• F. Baader , T. Nipkow: Term Rewriting and All That . Cambridge University Press, 1999.
• J. Avenhaus: Reduction Systems . Springer-Verlag, 1995, ISBN 3-540-58559-1 .
• R. Bündgen: Term rewriting systems theory, implementation, application . Vieweg 1998, ISBN 3-528-05652-5 ; PostScript , PDF
• TeReSe. Term rewriting systems . Cambridge University Press, 2003, ISBN 0-521-39115-6

Web links

• IFIP Working Group 1.6
• Tool which, among other things, can automatically prove the termination of term replacement systems as well as Prolog and Haskell programs.
• Portal page of the termination community

Individual evidence

1. ↑ ^{a b} D. E. Knuth, PB Bendix: Simple word problems in universal algebra . In: Computational Problems in Abstract Algebra . Pergamon Press, 1970.