2026-07-22T10:45:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2646 2024-03-06T10:33:28Z ddc:004 open_access

Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting Endrullis, Joerg Grabmayer, Clemens Hendriks, Dimitri Klop, Jan Willem van Oostrom, Vincent Weakly orthogonal term rewrite systems unique normal form property infinitary rewriting infinitary lambda-beta-eta-calculus, 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Joerg Endrullis and Clemens Grabmayer and Dimitri Hendriks and Jan Willem Klop and Vincent van Oostrom 2010 Is Part Of LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2010.85 urn:nbn:de:0030-drops-26469 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.85 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode