Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting

Joerg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop & Vincent Van Oostrom
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...