SKI combinator calculus


The SKI combinator calculus is a combinatory logic, a computational system that may be perceived as a reduced version of the untyped lambda calculus. It can be thought of as a computer programming language, though it is not convenient for writing software. Instead, it is important in the mathematical theory of algorithms because it is an extremely simple Turing complete language. It was introduced by Moses Schönfinkel and Haskell Curry.
All operations in lambda calculus can be encoded via abstraction elimination into the SKI calculus as binary trees whose leaves are one of the three symbols S, K, and I.
Although the most formal representation of the objects in this system requires binary trees, they are usually represented, for typesetability, as parenthesized expressions, either with all the subtrees parenthesized, or only the right-side children subtrees parenthesized. So, the tree whose left subtree is the tree KS and whose right subtree is the tree SK is usually typed as ), or more simply as KS, instead of being fully drawn as a tree. Parenthesizing only the right subtree makes this notation left-associative: ISK means.
I is redundant, as it behaves the same as SKK, but is included for convenience.

Informal description

Informally, and using programming language jargon, a tree can be thought of as a "function" x applied to an
"argument" y. When "evaluated", the tree "returns a value", i.e., transforms into another tree. Of course, all three of the "function", the "argument" and the "value" are either combinators, or binary trees, and if they are binary trees they too may be thought of as functions whenever the need arises.
The evaluation operation is defined as follows:
:
I returns its argument:
K, when applied to any argument x, yields a one-argument constant function Kx, which, when applied to any argument, returns x:
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:
Example computation: SKSK evaluates to KK by the S-rule. Then if we evaluate KK, we get K by the K-rule. As no further rule can be applied, the computation halts here.
For all trees x and all trees y, SKxy will always evaluate to y in two steps, Ky = y, so the ultimate result of evaluating SKxy will always equal the result of evaluating y. We say that SKx and I are "functionally equivalent" because they always yield the same result when applied to any y.
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 all occurrences of I in any expression can be replaced by or or and the resulting expression will yield the same result. So the "I" is merely syntactic sugar.
It is possible to define a complete system using only one combinator. An example is Chris Barker's iota combinator, which can be expressed in terms of S and K as follows:
It is possible to reconstruct S, K, and I from the iota combinator. Applying ι to itself gives ιι = ιSK = SSKK = SK which is functionally equivalent to I. K can be constructed by applying ι twice to I : ι = ι = ι = ι = SKSK = K. Applying ι one more time gives ι = ιK = KSK = S.

Formal definition

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. S, K, and I are terms.
  2. If τ1 and τ2 are terms, then 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 :
  1. If Δ is a derivation ending in an expression of the form αι, then Δ followed by the term αβι is a derivation.
  2. If Δ is a derivation ending in an expression of the form αι, then Δ followed by the term αβι is a derivation.
  3. If Δ is a derivation ending in an expression of the form αδ)ι, then Δ followed by the term α)ι is a derivation.
Assuming a sequence is a valid derivation to begin with, it can be extended using these rules.

Recursive parameter passing and quoting

;K=λq.λi.q : quotes q and ignores i
;S=λx.λy.λz.) : forms a binary tree that parameters can flow from root to branches and be read by identityFunc= or read a quoted lambda q using Kq.

SKI expressions

Self-application and recursion

SII is an expression that takes an argument and applies that argument to itself:
One interesting property of this is that it makes the expression SII irreducible:
Another thing that results from this is that it allows you to write a function that applies something to the self application of something else:
This function can be used to achieve recursion. If β is the function that applies α to the self application of something else, then self-applying β performs α recursively on ββ. More clearly, if:
then:

The reversal expression

SK reverses the following two terms:

Boolean logic

SKI combinator calculus can also implement Boolean logic in the form of an if-then-else structure. An if-then-else structure consists of a Boolean expression that is either true or false and two arguments, such that:
and
The key is in defining the two Boolean expressions. The first works just like one of our basic combinators:
The second is also fairly simple:
Once true and false are defined, all Boolean logic can be implemented in terms of if-then-else structures.
Boolean NOT works the same as the if-then-else structure, with F and T as the second and third values, so it can be implemented as a postfix operation:
If this is put in an if-then-else structure, it can be shown that this has the expected result
Boolean OR works the same as an if-then-else structure with T as the second value, so it can be implemented as an infix operation:
If this is put in an if-then-else structure, it can be shown that this has the expected result:
Boolean AND works the same as an if-then-else structure with F as the third value, so it can be implemented as a postfix operation:
If this is put in an if-then-else structure, it can be shown that this has the expected result:
Because this defines T, F, NOT, OR, and AND in terms of SKI notation, this proves that the SKI system can fully express Boolean logic.

Connection to intuitionistic logic

The combinators K and S correspond to two well-known axioms of sentential logic:
Function application corresponds to the rule modus ponens:
The axioms AK and AS, and the rule MP are complete for the implicational fragment of intuitionistic logic. In order for combinatory logic to have as a model:
This connection between the types of combinators and the corresponding logical axioms is an instance of the Curry–Howard isomorphism.