Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting

Authors Joerg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, Vincent van Oostrom

Thumbnail PDF


  • Filesize: 234 kB
  • 18 pages

Document Identifiers

Author Details

Joerg Endrullis
Clemens Grabmayer
Dimitri Hendriks
Jan Willem Klop
Vincent van Oostrom

Cite AsGet BibTex

Joerg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom. Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 85-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property (UNinf) fails by a simple example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that UNinf also fails for the infinitary lambda-beta-eta-calculus. As positive results we obtain the following: Infinitary confluence, and hence UNinf, holds for weakly orthogonal TRSs that do not contain collapsing rules. To this end we refine the compression lemma. Furthermore, we consider the triangle and diamond properties for infinitary developments in weakly orthogonal TRSs, by refining an earlier cluster-analysis for the finite case.
  • Weakly orthogonal term rewrite systems
  • unique normal form property
  • infinitary rewriting
  • infinitary lambda-beta-eta-calculus,


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail