A Confluent Rewriting System Having No Computable, One-Step, Normalizing Strategy
Jakob Grue Simonsen · ACM Transactions on Computational Logic · 2015
A full and finitely generated Church-Rosser term rewriting system is presented that has no computable one-step, normalizing strategy; the system is both left- and right-linear. The result provides a negative answer to a question posed by Kennaway in 1989: Number 10 on the List of Open Problems in Rewriting.