eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2010-07-06
85
102
10.4230/LIPIcs.RTA.2010.85
article
Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting
Endrullis, Joerg
Grabmayer, Clemens
Hendriks, Dimitri
Klop, Jan Willem
van Oostrom, Vincent
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol006-rta2010/LIPIcs.RTA.2010.85/LIPIcs.RTA.2010.85.pdf
Weakly orthogonal term rewrite systems
unique normal form property
infinitary rewriting
infinitary lambda-beta-eta-calculus,