Chapter 6: Minimal Calculus

Lambda Calculus

All functions in lambda calculus could be reduced into following minimal functions, or combinators:

$$\lambda x.x\\ \lambda x.c\\ \lambda x.yz$$

The first one returns its parameter unchanged. The second one returns a free variable captured from outer scope, which is considered as constant to the inner function itself. The third one provokes an application.

SKI Calculus

But there is a more famous set of combinators, called SKI Caculus.

$$\begin{array}{} \text{let}&\left\{ \begin{array}{} I&=&\lambda x.x \\ K&=&\lambda xy.x \\ S&=&\lambda xyz.xz(yz)\\ \end{array}\right.\\ \text{then}&\left\{ \begin{array}{} \lambda x.x &=& I\\ \lambda x.c &=& Kc\\ \lambda x.yz &=& S (\lambda x.y) (\lambda x.z)\\ \end{array}\right.\\ \end{array}$$

Then we can learn calculus again.

$$T=K\\ F=SK\\ \text{not}=S(SI(KF))(KT)\\ \text{and}=SS(K(KF))\\ \text{or}=SI(KT)\\ \vdots$$

Don't wanna enumerate more. You may try it by yourself.

SK Calculus

However, $I$ is actually not primitive. It could still be rewritten as:

$$I=SKK=SKS$$

Then we get SK Calculus! Can go dive deeper into this? Sure!

Iota Calculus

Don't close your mouth while watching this magic.

$$\begin{array}{} \text{let}&\space\space\space \iota=\lambda f.fSK\\ \text{then}&\left\{ \begin{array}{} I &&&=& \iota\iota\\ K &=& \iota(\iota I) &=& \iota(\iota(\iota\iota))\\ S &=& \iota(K) &=& \iota(\iota(\iota(\iota\iota)))\\ \end{array}\right.\\ \end{array}$$

Don't verify these equations by hand. 会变得不幸。别问我怎么知道的。

Yes, it reach the top of minimalism! Only one combinator! Since iota calculus is so minimal, it is possible to transform it into a kind of binary tree, with iota as leaf node and application order (by functionality of parentheses) as internal node. Furthermore, the tree could be then encoded as pre-order, i. e.

iota := "1" | "0" iota iota

Which means an iota expression should be either 1 or 0, 1 stands for iota itself and 0 is followed by another two iota expressions. For example 0011011 denotes $((\iota \iota )(\iota \iota ))$, and 0101011 denotes $\iota (\iota (\iota \iota ))$.

Long long ago you might have been told that computer programs are all stored in binary form in computers. Well, now binary is here, where were you?

BCKW System

And yes, alternative system exists, such as BCKW system:

$$\begin{array}{} \text{let}&\left\{ \begin{array}{} B&=&\lambda xyz.x(yz) \\ C&=&\lambda xyz.xzy \\ K&=&\lambda xy.x\\ W&=&\lambda xy.xyy \end{array}\right.\\ \text{then}&\left\{ \begin{array}{} B&=&S(KS)K\\ C&=&S(S(K(S(KS)K))S)(K K)\\ K&=&K\\ W&=&SS(SK) \end{array}\right.\\ \text{and}&\left\{ \begin{array}{} I&=&WK\\ K&=&K\\ S&=&B(B(BW)C)(BB)&=&B(B W)(BBC)\\ \end{array}\right.\\ \end{array}$$