TEXT   72

# term-rewriting.txt

Guest on 2nd September 2021 02:08:22 AM

1. Term Rewriting
2.
3.   "The best writing is rewriting." - E. B. Whites
4.
5. Problem Statement
6.   and a plan by Term Rewriting
7. Ensuring Termination
8.   Lexicographical Path Order
9.   Knuth-Bendix Order
10. Detecting Non-Confluence
11.   Critical Pairs
12. Completion: Fixing Non-Confluence
13.   Knuth-Bendix Completion
14.
15. Problem Statement
16.
17. Have constant and function symbols (arities known), variables,
18. equational axioms (finitely many) (variables implicitly ∀),
19. two terms.
20. Are the two terms equal according to the axioms?
21.
22. Example.
23.
24. This problem is arbitrarily hard. Example: Combinatory Logic.
25. This constitutes a Turing-complete programming language. You
26. don't even need to use any variable! So equality in this language
27. (even without variables) is as hard as program equivalence.
28.
29. One way (not the only one):
30. Use axioms as rewrite rules. Keep rewriting both terms:
31.   instantiate a rule so one side matches a subterm,
32.   replace by the other side
33.
34. Example again.
35.
36. Two things can go wrong:
37.   goes on forever
38.   non-deterministic choice ⇒ non-deterministic answer
39.
40. The rest is devoted to avoiding these two problems
41. (or declare failure otherwise). Thus:
42.
43. If this process is terminating:
44.   Every chain of rewrites gets stuck
45. And confluent:
46.   ∀s. t0 <--rewrite*-- s --rewrite*--> t1
47.       ⇒ ∃u.
48.       t0 --rewrite*--> u <--rewrite*-- t1
49.   (draw picture)
50. Then: the two terms are equal according to the axioms
51.       =
52.       rewrite both until stuck, get (syntactically) equal terms
53.
54. (The converse does not hold. Use some other approach.)
55.
56. The rest is devoted to ensuring termination and confluence
57. (or die trying).
58.
59.
60. Ensuring Termination
61.
62. Absence of infinite rewrite chains
63. =
64. Single-step rewrite, viewed as a relation, is a well-founded order.
65.
66. Seek well-founded order over terms, compatible with rewriting.
68.
69. ">" is a reduction order :=
70.   well-founded order
71. ∧ compatible with function sysmbols ("functions are monotonic"):
72.     s>t ⇒ f(...s...) > f(...t...)
73. ∧ all substitutions are monotonic:
74.     s>t ⇒ σs>σt
75.
76. Use each axiom a=b in only one direction: make it into rule a->b only if a>b.
77.
78. Theorem: Rewriting is terminating
79.          =
80.          ∃ reduction order ">" . ∀ rule l->r . l>r
81.
82. The next step is imposing a stronger restriction:
83.
84. ">" is a simplification order :=
85.   each term > all its proper subterms
86. ∧ compatible with function sysmbols ("functions are monotonic"):
87.     s>t ⇒ f(...s...) > f(...t...)
88. ∧ all substitutions are monotonic:
89.     s>t ⇒ σs>σt
90.
91. The condition
92.   each term > all its proper subterms
93. can be verified with the simpler
94.   ∀f. ∀ variables. ∀i. f(v1 ... vn) > vi
95.
96. So the latest definition loses power but gains ease.
97.
98. We now show two famous examples of simplification orders.
99.
100. Lexicographical Path Order (LPO)
101.
102. Given ">" over function symbols. (Does not need to be total. Just need
103. to be total enough for the rewrite rules.)
104.
105. Extend to all terms: s>t :=
106.   t variable ∧ s≠t
107. ∨ s=f(s1...sm) ∧ t=g(t1...tn) ∧ (
108.     ∃i. si > g(t1...tn)
109.   ∨ f>g ∧ ∀i. f(s1...sm)>ti
110.   ∨ f=g ∧ (s1...sm)>(t1...tm) lexicographically
111.   )
112.
113. Example.
114.
115. Since LPO is generated by ordering the function symbols, you can try
116. all possible orders of function symbols, then see if any one can oriented
117. your axioms. In other words you can always find out whether LPO works for
118. you or not.
119.
120. Knuth-Bendix Order (KBO)
121.
122. Given ">" over function symbols,
123. weight function w: fun ∪ var -> nonneg real,
124.   ∃w0>0.   ∀v:var. wv=w0
125.          ∧ ∀c:const. wc≥w0
126.   ∀f:fun. f unary ∧ wf=0 ⇒ ∀g:fun. f≥g
127.
128. The last condition is weird. It is a funny hack inspired by practice.
129.
130. Extend w to terms: Sum up weights of all symbols seen in the term.
131. E.g., w( f(x,g(x,a)) ) = wf + wx + wg + wx + wa
132.
133. Extend to all terms: s>t :=
134.   (∀v:var. #occ(v,s) ≥ #occ(v,t)) ∧ ws>wt
135. ∨ (∀v:var. #occ(v,s) ≥ #occ(v,t)) ∧ ws=wt ∧ (
136.     s=f^n(v), t=v, v:var
137.   ∨ s=f(...) ∧ t=g(...) ∧ f>g
138.   ∨ s=f(s1...sm) ∧ t=f(t1...tm) ∧ (s1...sm)>(t1...tm) lexicographically
139.
140. Example.
141.
142. As before, you can try all possible orders over function symbols.
143. How to choose weights? Solve for them instead:
144. Try also all possible orientations of axioms.
145. Each requirement l>r comes down to something like wl>wr
146. (or wl=wr plus more inequalities); but note it is linear.
147. So the