Abstract

Symmetic combinatory logic with the symmetric analogue of a combinatorially complete base (in the form of symmetric λ-calculus) is known to lack the Church-Rosser property. We prove a muchstrongertheorem that no symmetric combinatory logic that containsat least two proper symmetric combinatoryhas the Church-Rosser property. Although the statement of the result looks similar to an earlier one concerning dual combinatory logic,the proof is differentbecause symmetric combinators may form redexes in both left and right associated terms. Perhaps surprisingly, we are also able to show that certain symmetric combinatory logics that include justone particular constantare not confluent. This result (beyond other differences) clearly sets apart symmetric combinatory logic from dual combinatory logic, since all dual combinatory systems with a single combinator or a single dual combinator are Church-Rosser. Lastly, we prove that a symmetric combinatory logic that contains the fixed point and the one-place identity combinator has the Church-Rosser property.