Rewrite, rewrite, rewrite, rewrite, rewrite...
Nachum Dershowitz, Stéphane Kaplan · 1989
We study properties of rewrite systems that are not necessarily terminating, but allow instead for transfinite derivations that have a limit.In particular, we give conditions for the existence of a limit and for its uniqueness and relate the operational and algebraic semantics of infinitary theories.We also consider sufficient completeness of hierarchical systems.