Dual Identity Combinators :: Combinatory Logic Math Papers

Dual Identity Combinators Combinatory logic has been invented independently by M. Schà ¶nfinkel and H.B. Curry in the 20s of this century (Cf. Schà ¶nfinkel 1924, Curry 1930.). The impetus was to reduce the number of primitive notions needed for a logical system, in particular, for first-order logic. Schà ¶nfinkel used functions to provide a translation for a closed first-order formula into a functional expression, thereby eliminating bound variables of first-order logic. About the success of this attempt cf. Curry & Feys 1968: beyond this primarily intended connection between first-order logic and (illative) combinatory logic there is another connection between the two, the so called Curry-Howard isomorphism (Curry & Feys 1968, Howard 1980). This relates combinators to implicational formulae. It is just a small step from the Curry-Howard isomorphism to put combinatory bases (which are possibly combinatorially non-complete) into correspondence with logical systems. It is well-known, e.g., that the relevant system R ® corresponds in the above sense to the combinatory base {B, C, W, I}. Of course, such combinatory bases are not unique just as axiomatizations are not unique. For instance, the combinatory base {B’, C, S, I} is equally suitable. (Cf. Dunn 1986.) 1. Dual combinators. Pure combinators operate on left associated sequences of objects. The result of an application of a combinator is a sequence made out of some of the objects on the left (possibly with repetitions) and parentheses scattered across: ( . . . ( ( Q x1 ) . . . ) xn )  º ( xi 1 . . . xi m ) where any xi j (1 £ j  £ m) is xk (1 £ k  £ n) for some k , and the sequence on the right might be associated arbitrarily. The parentheses on the left of the identity are frequently dropped, since left association is taken to be the default. To recall the most familiar combinators as an illustration of the above general statement we have: Sxyz  º xz(yz), Kxy  º x, Ix  º x, Bxyz  º x(yz), Cxyz  º xzy, Wxy  º xyy. Using the combinatory axioms above we can define the notions of one-step reduction (4 1), of reduction (4 ), and of weak equality (=w) as usual. (For an introduction to combinatory logic see e.g., Hindley & Seldin 1986.) In case where one is interested in a combinatory base which is not combinatorially complete it might be useful to emphasize that the above notions are restricted to the particular combinatory base.