Dual Identity Combinators :: Combinatory Logic Math Papers

Dual Identity CombinatorsCombinatory logic has been invented independently by M. Schnfinkel and H.B. Curry in the 20s of this century (Cf. Schnfinkel 1924, Curry 1930.). The impetus was to reduce the result of primitive nonions needed for a logical system, in particular, for first-order logic. Schnfinkel 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) combinative 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 by chance 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 odd field 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 relation we haveSxyz xz(yz), Kxy x, Ix x, Bxyz x(yz), Cxyz xzy, Wxy xyy.Using the combinatory axioms a bove 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 utilitarian to emphasize that the above notions are restricted to the particular combinatory base.