Undecidability of Confluence for Binary Length-Reducing Cycle Rewriting
Confluence guarantees that diverging rewrite choices can always be rejoined. For finite terminating string- and term-rewriting systems, confluence is decidable by critical-pair analysis, and in polynomial time for length-reducing strings. For finite terminating (hyper)graph transformation systems, in contrast, confluen...