The Church-Rosser property in dual combinatory logic

Abstract Dual combinatorsemerge from the aim of assigning formulas containing ← as types to combinators. This paper investigates formally some of the properties of combinatory systems that include both combinators and dual combinators. Although the addition of dual combinators to a combinatory system does not affect the unique decomposition of terms, it turns out that some terms might be redexes in two ways (with a combinator as its head, and with a dual combinator as its head). We prove a general theorem stating thatno dual combinatory system possesses the Church-Rosser property. Although the lack of confluence might be problematic in some cases, it is not a problemper se. In particular, we show that no damage is inflicted upon thestructurally free logics, the system in which dual combinators first appeared.