On the Finite Church-Rosser Property of Nonlinear Term Rewriting Systems(Preliminary report)
Mizuhito Ogawa, Satoshi Ono · Institutional Repositories DataBase (IRDB) · 1989
This paper proves that an infinitely nonoverlapping (possibly nonlinear) $TRS$ is finitely Church-Rosser.The condition infinitely nonoverlapping is a nonoverlapping condition under unification with infinite terms.The property finitely Church-Rosser is equivalent to uniquely normalizing with respect to equality (i.e.$x=y\Rightarrow x\equiv y$ for any normal forms $x,$ $y$ ), and is an intermidiate property between Church-Rosser and uniquely normalizing with respect to reduction.