We define dual and symmetric combinatory calculi (inequational and equational ones), and prove their consistency. Then, we introduce algebraic and set theoretical relational and operational - semantics, and prove soundness and completeness. We analyze the relationship between these logics, and argue that inequational dual logics are the best suited to model computation.

Dual combinators emerge 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 that no dual combinatory system possesses the Church-Rosser property. Although the lack of confluence might be problematic in some cases, it is not a problem per se. In particular, we show that no damage is inflicted upon the structurally free logics, the system in which dual combinators first appeared. (shrink)

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. (shrink)