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^{[1]} and Haskell Curry.^{[2][3]}

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** (called *combinators*).

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 ((**KS**)(**SK**)), or more simply as **KS**(**SK**), instead of being fully drawn as a tree (as formality and readability would require). Parenthesizing only the right subtree makes this notation left-associative: **ISK** means ((**IS**)**K**).

**I** is redundant, as it behaves the same as **SKK**,^{[4]} but is included for convenience.

Informal description

Informally, and using programming language jargon, a tree (*xy*) can be thought of as a “function” *x* applied to an “argument” *y*. When “evaluated” (*i.e.*, when the function is “applied” to the argument), 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:

(*x*, *y*, and *z* represent expressions made from the functions **S**, **K**, and **I**, and set values):

**I** returns its argument:^{[4]}

**I***x* = *x*

**K**, when applied to any argument *x*, yields a one-argument constant function **K***x*, which, when applied to any argument, returns *x*:^{[4]}

**K***xy* = *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.^{[4]} More clearly:

**S***xyz* = *xz*(*yz*)

Example computation: **SKSK** evaluates to **KK**(**SK**) by the **S**-rule. Then if we evaluate **KK**(**SK**), 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*, **SK***xy* will always evaluate to *y* in two steps, **K***y*(*xy*) = *y*, so the ultimate result of evaluating **SK***xy* will always equal the result of evaluating *y*. We say that **SK***x* and **I** are “functionally equivalent” because they always yield the same result when applied to any *y*.^{[4]}

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 (**SKK**) or (**SKS**) or (**SK** whatever)^{[4]} and the resulting expression will yield the same result. So the “**I**” is merely syntactic sugar. Since **I** is optional, the system is also referred as SK calculus or SK combinator calculus.

It is possible to define a complete system using only one (improper) combinator. An example is Chris Barker’s iota combinator, which can be expressed in terms of **S** and **K** as follows:

ι*x* = *x***SK**

It is possible to reconstruct **S**, **K**, and **I** from the iota combinator. Applying ι to itself gives ιι = ι**SK** = **SSKK** = **SK**(**KK**) which is functionally equivalent to **I**. **K** can be constructed by applying ι twice to **I** (which is equivalent to application of ι to itself): ι(ι(ιι)) = ι(ιι**SK**) = ι(**ISK**) = ι(**SK**) = **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.

**S**,**K**, and**I**are terms.- If τ
_{1}and τ_{2}are terms, then (τ_{1}τ_{2}) is a term. - 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 α and ι are words over the alphabet {**S**, **K**, **I**, (, )} while β, γ and δ are terms):

- If Δ is a derivation ending in an expression of the form α(
**I**β)ι, then Δ followed by the term αβι is a derivation. - If Δ is a derivation ending in an expression of the form α((
**K**β)γ)ι, then Δ followed by the term αβι is a derivation. - If Δ is a derivation ending in an expression of the form α(((
**S**β)γ)δ)ι, 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. [1]

nnection to intuitionistic logic[edit]

The combinators **K** and **S** correspond to two well-known axioms of sentential logic:

**AK**: *A* → (*B* → *A*),

**AS**: (*A* → (*B* → *C*)) → ((*A* → *B*) → (*A* → *C*)).

Function application corresponds to the rule modus ponens:

**MP**: from *A* and *A* → *B*, infer *B*.

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:

- The implicational fragmentof classical logic, would require the combinatory analog to the law of excluded middle,
*e.*, Peirce’s law; - Complete classical logic, would require the combinatory analog to the sentential axiom
**F**→*A*.

This connection between the types of combinators and the corresponding logical axioms is an instance of the Curry–Howard isomorphism.

See also[edit]

- Combinatory logic
- B, C, K, W system
- Fixed point combinator
- Lambda calculus
- Functional programming
- Unlambdaprogramming language
- The Iota and Jotprogramming languages, designed to be even simpler than SKI.
*To Mock a Mockingbird*

References[edit]

**^**“Über die Bausteine der mathematischen Logik”,*Mathematische Annalen***92**, pp. 305–316. Translated by Stefan Bauer-Mengelberg as “On the building blocks of mathematical logic” in Jean van Heijenoort, 1967.*A Source Book in Mathematical Logic, 1879–1931*. Harvard Univ. Press: 355–66.**^***Curry, Haskell Brooks**(1930). “Grundlagen der Kombinatorischen Logik” [Foundations of combinatorial logic]. American Journal of Mathematics (in German). The Johns Hopkins University Press.***52**(3): 509–536.*doi**:**2307/2370619**.**JSTOR**2370619**.***^***Wolfram, Stephen.**“History of Symbolic Systems”**. A New Kind of Science Online. Retrieved 2019-06-17.*- ^ Jump up to:
^{a}^{b}^{c}^{d}^{e}^{f}*Wolfram, Stephen.**“Combinators”**. A New Kind of Science Online. Retrieved 2019-06-17.*

- Smullyan, Raymond, 1985.
*To Mock a Mockingbird*. Knopf. ISBN0-394-53491-3. A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors. - ——–, 1994.
*Diagonalization and Self-Reference*. Oxford Univ. Press. Chpts. 17-20 are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.