Term Rewriting and All That

2. Abstract Reduction Systems

Abstract Reduction System is

• a pair $(A,\to )$, where the reduction is a binary relation on the set A, i.e. $\to \subseteq A\times A$. Instead of $(a,b)\in \to$ we write $a\to b$.
• If you want it terminate, well-founded relation is necessary.

2.1 Equivalence and reduction

Reduction is

1. a directed computation, which, starting from some point $a_0$, tries to reach a normal form by following the reduction $a0\to a1\to ...$ . This corresponds to the idea of program evaluation.
2. a description of $\stackrel{\star }{\leftrightarrow }$, where $a\stackrel{\star }{\leftrightarrow }b$ means that there is a path between a and b where the arrow can be traversed in both directions

Equivalent is

• If two elements a and b are equivalent , i.e. if $a\stackrel{\star }{\leftrightarrow }b$ holds.

The central themes of this book is termination and confluence of reduction.

2.1.1 Basic definitions

A reduction is called

• Church-Rosser: iff $x\stackrel{\star }{\leftrightarrow }y\Rightarrow x\downarrow y$.
• confluent: iff $y_1\stackrel{\star }{\leftarrow }x\stackrel{\star }{\to }{y}_2{y}_1\downarrow y_2$.
• terminating: iff there is no infinite descending chain $a_0\to a_1\to ...$
• normalizing: iff every element has a normal form.
• convergent: iff it is both confluent and terminating.

2.1.2 Basic Results

Church-Rosser, confluent, semi-confluent are equivalent.

2.2. Well-Founded induction

2.3 Proving Termination

2.4 Lexicographic orders

2.5 Multiset orders

2.6 Orders in ML

2.7 Proving confluence

3. Universal Algebra