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.
  67. This leads to:
  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

Raw Paste


Login or Register to edit or fork this paste. It's free.