Chew's theorem is originally proposed in his paper titled
"Unique normal forms in term rewriting systems with repeated variables"
(ACM STOC'81). The statement is "a compatible TRS is UN".
However, his proof has a serious glitch in the proof of the key lemma 6.1.
Ogawa independently investigated the UN property of nonlinear TRSs.
He proposed that "an $\omega$-nonoverlapping TRS is UN" in
"on the uniquely converging property of nonlinear term rewriting systems"
(IEICE SIGCOMP 1989), but his proof has a gap in the Main Theorem 1
and it covers only strongly nonoverlapping TRSs.
Ogawa also proposed that "a weakly compatible TRS is UN" in
"Chew's theorem revisited - uniquely normalizing property of non-linear
term rewriting systems" (ISAAC'92).
However, his proof is valid only for
weakly compatible TRSs under single-assignments (this is
an easier problem than Chew's theorem),
which is incomparable with compatible TRSs.
For instance, {d(x,x,a) -> x, d(a,a,y) -> y} is compatible but not
weakly compatible under single assignments, and
{p(if(z,x,x)) -> p(x), if(T,x,y) -> x, if(F,x,y) -> y}
is weakly compatible under single-assignments but not compatible.
In "a new proof of Chew's theorem"
(RIMS symposium 1995, submitted to journal 1997),
Mano and Ogawa firstly gave the correct proof of Chew's theorem.
There are still remaining many conjectures related to Chew's theorem,
such as
The first conjecture is true for simple-right-linear TRSs (i.e.,
right-linear and no nonlinear variables appear in the rhs) by Ooyamaguchi,
et.al but false for nonduplicating TRSs.
The counter example by Gramrich is as follows:
Let R = {b -> g(b,b), f(x,x) -> a, g(x,x) -> f(x,g(b,x))}.
It is not difficult to see b -*-> a. Thus g(b,b) -*-> a, f(a,g(a,a))
which are not joinable.
See bibliography.
Last Modified 98/08/24