Lecture Notes on Term Rewriting and Computational Complexity
Harvey M. Friedman · 2001
Abstract. The main powerful method for establishing termination of term rewriting systems was discovered by Nachum Dershowitz through the introduction of certain natural well founded orderings (lexicographic path orderings). This leads to natural decision problems which may be of the highest computational complexity of any decidable problems appearing in a natural established computer science context. 1. TERM REWRITING. A signature S is a finite set of function symbols (arities ≥ 0). V is the set of variables x 1,x 2,.... T(S,V) is the set of all terms using elements of S » V. T(S) is the restriction to closed terms (i.e., with no variables). A rewrite rule in T(S,V) is an expression l Æ r