Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting


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 (UN infinity) fails by a simple example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that UN infinity also fails for the infinitary lambda beta eta-calculus. As positive results we obtain the following: Infinitary confluence, and hence UN-infinity, 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 inŽnitary multi-steps (complete developments) in weakly orthogonal TRSs, by refining an earlier cluster-analysis for the Žnite case.