TheSKI combinator calculus is acombinatory logic system and acomputational system. It can be thought of as a computer programming language, though it is not convenient for writing software.^{[citation needed]} Instead, it is important in the mathematical theory ofalgorithms because it is an extremely simpleTuring complete language. It can be likened to a reduced version of the untypedlambda calculus. It was introduced byMoses Schönfinkel^[1] andHaskell Curry.^[2]

All operations in lambda calculus can be encoded viaabstraction elimination into the SKI calculus asbinary trees whose leaves are one of the three symbolsS,K, andI (calledcombinators).

Although the most formal representation of the objects in this system requires binary trees, for simpler typesetting they are often represented as parenthesized expressions, as a shorthand for the tree they represent. Any subtrees may be parenthesized, but often only the right-side subtrees are parenthesized, with left associativity implied for any unparenthesized applications. For example,ISK means ((IS)K). Using this notation, a tree whose left subtree is the treeKS and whose right subtree is the treeSK can be written asKS(SK). If more explicitness is desired, the implied parentheses can be included as well: ((KS)(SK)).

Informally, and using programming language jargon, a tree (xy) can be thought of as an application of the functionx to an argumenty. When evaluated (i.e., when the "function" is "applied" to the argument), the tree "returns a value",i.e., transforms into another tree. The "function", "argument" and the "value" are either combinators or binary trees with application nodes. If they are binary trees, they may be thought of as functions too, if needed.

Theevaluation operation is defined as follows:

(x,y, andz represent expressions made from the combinatorsS,K, andI, and possibly variables standing for some as yet unspecifiedSKI expressions):

I returns its argument:

Ix =x

K, when applied to any argumentx, yields a one-argument constant functionKx, which, when applied to any argumenty, returnsx:

Kxy =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:

Sxyz =xz(yz)

Example computation:SKSK evaluates toKK(SK) by theS-rule. Then if we evaluateKK(SK), we getK by theK-rule. As no further rule can be applied, the computation halts here.

For all treesx and all treesy,SKxy will always evaluate toy in two steps,Ky(xy) =y, so the ultimate result of evaluatingSKxy will always be the same as the result of evaluatingy. We say thatSKx andI are "functionally equivalent" for anyx, because they always yield the same result when applied to anyy.

From these definitions it can be shown that SKI calculus, while being a minimalistic system, can fully perform any computations of the lambda calculus. All occurrences ofI in any expression can be replaced by (SKK) or (SKS) or (SKx) for anyx, and the resulting expression will yield the same result. So the "I" is merelysyntactic sugar. SinceI is optional, the system is also referred to asSK calculus orSK combinator calculus.

It is possible to define a complete system using only one (improper) combinator. An example is Chris Barker'siota combinator, which can be expressed in terms ofS andK as follows:

ιx =xSK =S(λx.xS)(λx.K)x =S(S(λx.x)(λx.S))(KK)x =S(SI(KS))(KK)x

It is possible to reconstructS,K, andI from the iota combinator. Applying ι to itself gives ιι = ιSK =SSKK =SK(KK) which is functionally equivalent toI.K can be constructed by applying ι twice toI (which is equivalent to application of ι to itself): ι(ι(ιι)) = ι(ιιSK) = ι(ISK) = ι(SK) =SKSK =K. Applying ι one more time gives ι(ι(ι(ιι))) = ιK =KSK =S.

The simplest possible term forming a basis is X = λf.f (λxyz.x z (y z)) (λxyz.x), which satisfies X X =K, and X (X X) =S.

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

Terms:The setT of terms is defined recursively by the following rules.

1. S,K, andI are terms.
2. If τ₁ and τ₂ 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 (where α and ι are words over the alphabet {S,K,I, (, )} while β, γ and δ are terms):

1. If Δ is a derivation ending in an expression of the form α(Iβ)ι, then Δ followed by the term αβι is a derivation.
2. If Δ is a derivation ending in an expression of the form α((Kβ)γ)ι, then Δ followed by the term αβι is a derivation.
3. 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. All derivations of length 1 are valid derivations.

An expression in the lambda calculus can be converted into an SKI combinator calculus expression in accordance with the following rules:

1. λx.x =I
2. λx. c =Kc (provided that c does not depend onx)
3. λx. cx = c (provided that c does not depend onx)
4. λx.yz =S(λx.y)(λx.z)

SII is an expression that takes an argument and applies that argument to itself:

SIIα =Iα(Iα) = αα

This is also known asU combinator,Ux =xx. One interesting property of it is that its self-application is irreducible:

SII(SII) =I(SII)(I(SII)) =SII(I(SII)) =SII(SII)

Or, using the equation as its definition directly, we immediately getUU =UU.

Another thing is that it allows one to write a function that applies one thing to the self application of another thing:

(S(Kα)(SII))β =Kαβ(SIIβ) = α(Iβ(Iβ)) = α(ββ)

or it can be seen as defining yet another combinator directly,Hxy =x(yy).

This function can be used to achieverecursion. If β is the function that applies α to the self application of something else,

β =Hα =S(Kα)(SII)

then the self-application of this β is the fixed point of that α:

SIIβ = ββ = α(ββ) = α(α(ββ)) =${\displaystyle \dots }$

Or, directly again from the derived definition,Hα(Hα) = α(Hα(Hα)).

If α expresses a "computational step" computed by αρν for some ρ and ν, that assumes ρν' expresses "the rest of the computation" (for some ν' that α will "compute" from ν), then its fixed point ββ expresses the whole recursive computation, since usingthe same function ββ for the "rest of computation" call (with ββν = α(ββ)ν) is the very definition of recursion: ρν' = ββν' = α(ββ)ν' = ... . α will have to employ some kind of conditional to stop at some "base case" and not make the recursive call then, to avoid divergence.

This can be formalized, with

β =Hα =S(Kα)(SII) =S(KS)Kα(SII) =S(S(KS)K)(K(SII)) α

as

Yα =SIIβ =SII(Hα) =S(K(SII))H α =S(K(SII))(S(S(KS)K)(K(SII))) α

which gives usone possible encoding of theY combinator. A shorter variation replaces its two leading subterms with justSSI, sinceHα(Hα) =SHHα =SSIHα.

This becomes much shorter with the use of theB,C,W combinators, asthe equivalent

Yα =S(KU)(SB(KU))α =U(BαU) =BU(CBU)α =SSI(CBU)α

And with a pseudo-Haskell syntax it becomes the exceptionally shortY =U . (.U).

Following this approach, other fixpoint combinator definitions are possible. Thus,

• ThisY, byHaskell Curry:

Hgx =g(xx) ;Yg =Hg(Hg) ;Y = S(KU)(SB(KU)) = SS(S(S(KS)K))(K(SII))

• Turing'sΘ:

Hhg =g(hhg) ;Θg =HHg ;Θ = U(B(SI)U) = SII(S(K(SI))(SII))

• Y' (with SK-encoding byJohn Tromp^[3]):

Hgh =g(hgh) ;Y'g =HgH ;Y' = WC(SB(C(WC))) = SSK(S(K(SS(S(SSK))))K)

• Θ₄ by R.Statman:^[4]

Hgyz =g(yyz) ;Θ₄g =Hg(Hg)(Hg) ;Θ₄ = B(WW)(BW(BBB))

• or in general,

Hsomething =g(hsomething) ;Y_H g =H_____H__ g

(where anything goes instead of "_") or any other intermediaryH combinator's definition, with its correspondentY definition to jump-start it correctly. In particular,^[5]

Labcdefghijklmnopqstuvwxyzr =r(thisisafixedpointcombinator) ;Y_K =LLLLLLLLLLLLLLLLLLLLLLLLLL

In astrict programming language theY combinator will expand untilstack overflow, or never halt in case oftail call optimization.^[6] TheZ combinator will work instrict languages (also called eager languages), where the applicative evaluation order is in effect.

Its difference from theY combinator is that it is using${\displaystyle Qx=B(Ux)I=S(K(Ux))I=S(BS(BKU))(KI)x}$ as the${\displaystyle \eta }$-expanded form ofY's plain${\displaystyle Ux}$. WhereasY =BU(CBU), we haveZ =BU(CBQ) =S(KU)(SB(KQ)):

S(K(SI))K reverses the two terms following it:

S(K(SI))Kαβ →

K(SI)α(Kα)β →

SI(Kα)β →

Iβ(Kαβ) →

Iβα →

βα

It is thus equivalent toCI. And in general,S(K(Sf))K is equivalent toCf, for anyf.

SKI combinator calculus can also implementBoolean logic in the form of anif-then-else structure. Anif-then-else structure consists of aBoolean expression that is either true (T) or false (F) and two arguments, such that:

Txy =x

and

Fxy =y

The key is in defining the two Boolean expressions. The first works just like one of our basic combinators:

T =K

Kxy =x

The second is also fairly simple:

F =SK

SKxy =Ky(xy) =y

Once true and false are defined, all Boolean logic can be implemented in terms of Booleans acting asif-then-else structures.

BooleanNOT (which returns the opposite of a given Boolean) works the same as theif-then-else structure, withF andT as the second and third values:

NOTb =bFT =S(SI(KF))(KT)b

If this is put in anif-then-else structure, it has the expected result:

NOT(T) = (T)FT =F

NOT(F) = (F)FT =T

BooleanOR (which returnsT if either of its two Boolean argument values isT) works the same as anif-then-else structure withT as the second value:

ORab =aTb =SI(KT)ab

If this is put in anif-then-else structure, it has the expected result:

OR(T)(T) = (T)T(T) =T

OR(T)(F) = (T)T(F) =T

OR(F)(T) = (F)T(T) =T

OR(F)(F) = (F)T(F) =F

BooleanAND (which returnsT if both its Boolean argument values areT) works the same as anif-then-else structure withF as the third value:

ANDab =abF =Sa(KF)b =SS(K(KF))ab

If this is put in anif-then-else structure, it has the expected result:

AND(T)(T) = (T)(T)F =T

AND(T)(F) = (T)(F)F =F

AND(F)(T) = (F)(T)F =F

AND(F)(F) = (F)(F)F =F

This proves that the SKI system can fully express Boolean logic.

SKI calculus iscomplete, so any other logical combinator can be expressed in it as well, like, e.g.,

XORab =OR (ANDa (NOTb)) (AND (NOTa)b)

so that

XORabxy = (a(bFT)F)T((aFT)bF)xy =a(byx)(bxy)

as well as

NOTbxy =bFTxy =b(Fxy)(Txy) =byx

ORabxy =aTbxy =a(Txy)(bxy) =ax(bxy)

ANDabxy =abFxy =a(bxy)(Fxy) =a(bxy)y

The combinatorsK andS correspond to two well-known axioms ofsentential logic:

AK:A → (B →A),

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

Function application corresponds to the rulemodus ponens:

MP: fromA andA →B, inferB.

The axiomsAK andAS, and the ruleMP are complete for the implicational fragment ofintuitionistic logic. In order for combinatory logic to have as a model:

• Theimplicational fragment ofclassical logic, would require the combinatory analog to thelaw of excluded middle,i.e.,Peirce's law;
• Complete classical logic, would require the combinatory analog to the sentential axiomF →A.

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

There usually are multiple ways to do a reduction. If the term has the normal form, it is unique, hence the same result will be reached in such a case whatever theorder of operations.

• ${\displaystyle \mathsf{S}\mathsf{K}\mathsf{I}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{S}\mathsf{)}}$
  • ${\displaystyle \mathsf{S}\mathsf{K}\mathsf{I}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{S}\mathsf{)}\Rightarrow \mathsf{K}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{S}\mathsf{)}\mathsf{(}\mathsf{I}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{S}\mathsf{)}\mathsf{)}\Rightarrow \mathsf{K}\mathsf{I}\mathsf{(}\mathsf{I}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{S}\mathsf{)}\mathsf{)}\Rightarrow \mathsf{I}}$
  • ${\displaystyle \mathsf{S}\mathsf{K}\mathsf{I}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{S}\mathsf{)}\Rightarrow \mathsf{K}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{S}\mathsf{)}\mathsf{(}\mathsf{I}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{S}\mathsf{)}\mathsf{)}\Rightarrow \mathsf{K}\mathsf{I}\mathsf{S}\Rightarrow \mathsf{I}}$
  • ${\displaystyle \mathsf{S}\mathsf{K}\mathsf{I}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{S}\mathsf{)}\Rightarrow \mathsf{S}\mathsf{K}\mathsf{I}\mathsf{I}\Rightarrow \mathsf{K}\mathsf{I}\mathsf{(}\mathsf{I}\mathsf{I}\mathsf{)}\Rightarrow \mathsf{I}}$
• ${\displaystyle \mathsf{K}\mathsf{S}\mathsf{(}\mathsf{I}\mathsf{(}\mathsf{S}\mathsf{K}\mathsf{S}\mathsf{I}\mathsf{)}\mathsf{)}}$
  • ${\displaystyle \mathsf{K}\mathsf{S}\mathsf{(}\mathsf{I}\mathsf{(}\mathsf{S}\mathsf{K}\mathsf{S}\mathsf{I}\mathsf{)}\mathsf{)}\Rightarrow \mathsf{K}\mathsf{S}\mathsf{(}\mathsf{I}\mathsf{(}\mathsf{K}\mathsf{I}\mathsf{(}\mathsf{S}\mathsf{I}\mathsf{)}\mathsf{)}\mathsf{)}\Rightarrow \mathsf{K}\mathsf{S}\mathsf{(}\mathsf{I}\mathsf{(}\mathsf{I}\mathsf{)}\mathsf{)}\Rightarrow \mathsf{K}\mathsf{S}\mathsf{(}\mathsf{I}\mathsf{I}\mathsf{)}\Rightarrow \mathsf{K}\mathsf{S}\mathsf{I}\Rightarrow \mathsf{S}}$
  • ${\displaystyle \mathsf{K}\mathsf{S}\mathsf{(}\mathsf{I}\mathsf{(}\mathsf{S}\mathsf{K}\mathsf{S}\mathsf{I}\mathsf{)}\mathsf{)}\Rightarrow \mathsf{S}}$
• ${\displaystyle \mathsf{S}\mathsf{K}\mathsf{I}\mathsf{K}}$
  • ${\displaystyle \mathsf{S}\mathsf{K}\mathsf{I}\mathsf{K}\Rightarrow \mathsf{K}\mathsf{K}\mathsf{(}\mathsf{I}\mathsf{K}\mathsf{)}\Rightarrow \mathsf{K}\mathsf{K}\mathsf{K}\Rightarrow \mathsf{K}}$
  • ${\displaystyle \mathsf{S}\mathsf{K}\mathsf{I}\mathsf{K}\Rightarrow \mathsf{K}\mathsf{K}\mathsf{(}\mathsf{I}\mathsf{K}\mathsf{)}\Rightarrow \mathsf{K}}$

• Combinatory logic
• B, C, K, W system
• Fixed point combinator
• Lambda calculus
• Functional programming
• Unlambda programming language
• TheIota and Jot programming languages, designed to be even simpler than SKI.
• To Mock a Mockingbird

• O'Donnell, Mike "The SKI Combinator Calculus as a Universal System."
• Keenan, David C. (2001) "To Dissect a Mockingbird."
• Rathman, Chris, "Combinator Birds."
• ""Drag 'n' Drop Combinators (Java Applet)."
• A Calculus of Mobile Processes, Part I (PostScript) (by Milner, Parrow, and Walker) shows a scheme forcombinatorgraph reduction for the SKI calculus in pages 25–28.
• theNock programming language may be seen as an assembly language based on SK combinator calculus in the same way that traditional assembly language is based on Turing machines. Nock instruction 2 (the "Nock operator") is the S combinator and Nock instruction 1 is the K combinator. The other primitive instructions in Nock (instructions 0,3,4,5, and the pseudo-instruction "implicit cons") are not necessary for universal computation, but make programming more convenient by providing facilities for dealing with binary tree data structures and arithmetic; Nock also provides 5 more instructions (6,7,8,9,10) that could have been built out of these primitives.

• Lambda calculus
• Combinatory logic

• CS1 German-language sources (de)
• Articles with short description
• Short description is different from Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from May 2025