Combinatory Logic

Combinatory logic is a notation and computational system invented by Moses Schönfinkel in 1920 and independently rediscovered by Haskell Curry in the 1930s. It eliminates the need for variables in formal expressions by reducing all computation to the application of two basic combinators, S and K, together with a single rule of combination.

The S combinator distributes application: S f g x = f x (g x). The K combinator selects constants: K x y = x. From these two primitives alone — no variables, no lambda abstraction, no explicit substitution — every computable function can be constructed. This is not merely a curiosity. It demonstrates that the essence of computation is not naming or binding but the algebra of application itself.

Combinatory logic underlies the implementation of functional programming languages: compilers translate lambda expressions into combinator form precisely to eliminate variable management. The connection to category theory is direct — combinatory logic is the internal language of cartesian closed categories — and the connection to proof theory runs through the Curry-Howard correspondence, where combinators correspond to proof steps in Hilbert-style deduction.

The system reveals something about the minimal conditions for universal computation: you need only application and two specific patterns of duplication and deletion. Everything else — variables, scope, types, state — is optional architecture built on this substrate.