Term Rewriting

  "The best writing is rewriting." - E. B. Whites

Problem Statement
  and a plan by Term Rewriting
Ensuring Termination
  Lexicographical Path Order
  Knuth-Bendix Order
Detecting Non-Confluence
  Critical Pairs
Completion: Fixing Non-Confluence
  Knuth-Bendix Completion

Problem Statement

Have constant and function symbols (arities known), variables,
equational axioms (finitely many) (variables implicitly ∀),
two terms.
Are the two terms equal according to the axioms?

Example.

This problem is arbitrarily hard. Example: Combinatory Logic.
This constitutes a Turing-complete programming language. You
don't even need to use any variable! So equality in this language
(even without variables) is as hard as program equivalence.

One way (not the only one):
Use axioms as rewrite rules. Keep rewriting both terms:
  instantiate a rule so one side matches a subterm,
  replace by the other side

Example again.

Two things can go wrong:
  goes on forever
  non-deterministic choice ⇒ non-deterministic answer

The rest is devoted to avoiding these two problems
(or declare failure otherwise). Thus:

If this process is terminating:
  Every chain of rewrites gets stuck
And confluent:
  ∀s. t0 <--rewrite*-- s --rewrite*--> t1
      ⇒ ∃u. 
      t0 --rewrite*--> u <--rewrite*-- t1
  (draw picture)
Then: the two terms are equal according to the axioms
      =
      rewrite both until stuck, get (syntactically) equal terms

(The converse does not hold. Use some other approach.)

The rest is devoted to ensuring termination and confluence
(or die trying).


Ensuring Termination

Absence of infinite rewrite chains
=
Single-step rewrite, viewed as a relation, is a well-founded order.

Seek well-founded order over terms, compatible with rewriting.
This leads to:

">" is a reduction order := 
  well-founded order
∧ compatible with function sysmbols ("functions are monotonic"):
    s>t ⇒ f(...s...) > f(...t...)
∧ all substitutions are monotonic:
    s>t ⇒ σs>σt

Use each axiom a=b in only one direction: make it into rule a->b only if a>b.

Theorem: Rewriting is terminating
         =
         ∃ reduction order ">" . ∀ rule l->r . l>r

The next step is imposing a stronger restriction:

">" is a simplification order :=
  each term > all its proper subterms
∧ compatible with function sysmbols ("functions are monotonic"):
    s>t ⇒ f(...s...) > f(...t...)
∧ all substitutions are monotonic:
    s>t ⇒ σs>σt

The condition
  each term > all its proper subterms
can be verified with the simpler
  ∀f. ∀ variables. ∀i. f(v1 ... vn) > vi

So the latest definition loses power but gains ease.

We now show two famous examples of simplification orders.

Lexicographical Path Order (LPO)

Given ">" over function symbols. (Does not need to be total. Just need
to be total enough for the rewrite rules.)

Extend to all terms: s>t :=
  t variable ∧ s≠t
∨ s=f(s1...sm) ∧ t=g(t1...tn) ∧ (
    ∃i. si > g(t1...tn)
  ∨ f>g ∧ ∀i. f(s1...sm)>ti
  ∨ f=g ∧ (s1...sm)>(t1...tm) lexicographically
  )

Example.

Since LPO is generated by ordering the function symbols, you can try
all possible orders of function symbols, then see if any one can oriented
your axioms. In other words you can always find out whether LPO works for
you or not.

Knuth-Bendix Order (KBO)

Given ">" over function symbols,
weight function w: fun ∪ var -> nonneg real,
  ∃w0>0.   ∀v:var. wv=w0
         ∧ ∀c:const. wc≥w0
  ∀f:fun. f unary ∧ wf=0 ⇒ ∀g:fun. f≥g

The last condition is weird. It is a funny hack inspired by practice.

Extend w to terms: Sum up weights of all symbols seen in the term.
E.g., w( f(x,g(x,a)) ) = wf + wx + wg + wx + wa

Extend to all terms: s>t :=
  (∀v:var. #occ(v,s) ≥ #occ(v,t)) ∧ ws>wt
∨ (∀v:var. #occ(v,s) ≥ #occ(v,t)) ∧ ws=wt ∧ (
    s=f^n(v), t=v, v:var
  ∨ s=f(...) ∧ t=g(...) ∧ f>g
  ∨ s=f(s1...sm) ∧ t=f(t1...tm) ∧ (s1...sm)>(t1...tm) lexicographically

Example.

As before, you can try all possible orders over function symbols.
How to choose weights? Solve for them instead:
Try also all possible orientations of axioms.
Each requirement l>r comes down to something like wl>wr
(or wl=wr plus more inequalities); but note it is linear.
So the problem is just linear programming.
Therefore, again, you can always find out whether KBO works for you or not.