SKI combinator calculus

SKI combinator calculus is a computational system that is a reduced, untyped version of Lambda calculus. The system states that all operations in Lambda calculus can be expressed in terms of the three combinators $\mathbf {S}$, $\mathbf {K}$, and $\mathbf {I}$.

All functions in this system can be expressed using the alphabet of only $\mathbf {S}$, $\mathbf {K}$, $\mathbf {I}$, and parentheses (used as grouping symbols). Although the most formal representation of this system requires fully balanced parentheses, it is usually simplified for readability by leaving out parentheses on the left (those that do not effect order of operations), as expressions are evaluated left to right.

The SKI combinators

($x$, $y$, and $z$ represent expressions made frome the functions $\mathbf {S}$, $\mathbf {K}$, and $\mathbf {I}$, and set values)

$\mathbf {I}$ takes one argument and returns it:

$(\mathbf {I} x)\qquad \to \qquad x$

$\mathbf {K}$ takes two arguments, throws away the second, and returns the first:

$(\mathbf {K} xy)\qquad \to \qquad x$

$\mathbf {S}$ is a substitution operator. It takes three arguments and then returns the first argument applied to the third, which is then applied to the result of the second argument applied to the third. More clearly:

$(\mathbf {S} xyz)\qquad \to \qquad (xz(yz))$

[1]

Note that from these definitions it can be shown that SKI calculus is not the minimum system that can fully perform the computations of Lambda calculus, as $\mathbf {I}$ can be expressed in terms of $\mathbf {S}$ and $\mathbf {K}$:

1. $(\mathbf {SKK} x)\qquad \to \qquad (\mathbf {K} x(\mathbf {K} x))\qquad \to \qquad x\qquad \gets \qquad (\mathbf {I} x)$

Formal expression of the SKI combinators

The terms and derivations in this system can also be more formally defined.

Terms: The set $T$ of terms is defined recursively by the following rules.

1. $\mathbf {S}$, $\mathbf {K}$, and $\mathbf {I}$ are terms.
2. If $\tau _{1}$ and $\tau _{2}$ are terms, then $(\tau _{1}\tau _{2})$ is a term.
3. Nothing is a term if not required to be so by the first two rules.

Derivations: A derivation is a finite sequence of terms defined recursively by the following rules (where all Greek letters represent valid terms or expressions with fully balanced parentheses):

1. If $\Delta$ is a derivation of the form $\alpha (\mathbf {I} \beta )\iota$, then $\Delta$ can also be expressed as the derivation $\alpha \beta \iota$.
2. If $\Delta$ is a derivation of the form $\alpha ((\mathbf {K} \beta )\gamma )\iota$, then $\Delta$ can also be expressed as the derivation $\alpha \beta \iota$.
3. If $\Delta$ is a derivation of the form $\alpha (((\mathbf {S} \beta )\gamma )\delta )\iota$, then $\Delta$ can also be expressed as the derivation $\alpha ((\beta \delta )(\gamma \delta ))\iota$.

Assuming a sequence is a valid derivation to begin with, it can be evaluated using these rules. [2]

External links

• S and K Combinators
• The SKI Combinator Calculus as a Universal System