Remix.run Logo
momentoftop 6 hours ago

Combinators were an attempt to do logic (and computation falls out) without having to mess around with variables and variable substitution, which is annoying and inelegant because you have to worry about syntax issues like variable capture. Combinators were an attempt to do logic with a much simpler and cleaner syntax.

So combinator logic starts with a really simple language, based on a small alphabet of primitive combinators. You can see a bunch listed on the webpage:

   I, K, W, C, B, Q, ....
These are the primitive bits of syntax. The only other feature in the language is the ability to apply one combinator to another combinator. You write an application of a combinator "x" to another combinator "y" as "x y", and for convenience, you treat these applications as left associative, so "x y z" means "(x y) z": that is, first apply y to x, and then apply z to the resulting combinator.

Two typical combinators are K and S, with which you can form more complex combinators like

   K K
   S K
   K K K
   K (K K)
   K (S K)
...

Combinators generally come with simplification rules, and the ones for K and S are:

   K x y = x
   S f g x = f x (g x)
With these, we can start doing interesting reductions like:

   S K K x = K x (K x) = x
Now the weird fact: we're suddenly Turing Complete. It turns out that every possible computation is expressible just by building a big combinator out of K and S and applying those two simplification rules. No other machinery is needed.

K and S are not the only combinators with this property, and others form an adequate Turing Complete basis.

If you've heard of the Curry-Howard correspondence (Curry was responsible for combinatory logic), then combinators provide probably the simplest example of it, since if you give combinators types, you realise you are working with what's called a "Hilbert style" deduction system for propositional logic, which is the simplest sort of formal logical system. Indeed:

   1. Hilbert's first two axioms for his version of the calculus are exactly the types for K and S above
   2. K and S are invocations of these axioms
   3. Application is modus ponens
   4. The combinator S K K above corresponds to the proof that p → p.
   5. The simplification of S K K x is proof normalisation (if you ever see the proof S K K x for some proof x, you should simplify it to just the proof x).