The SKI combinator calculus is a
combinatory logic system and a
computational system. 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
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
s because it is an extremely simple
Turing complete
Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical com ...
language. It can be likened to a reduced version of the untyped
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
. It was introduced by
Moses Schönfinkel
Moses Ilyich Schönfinkel (russian: Моисей Исаевич Шейнфинкель, translit=Moisei Isai'evich Sheinfinkel; 29 September 1888 – 1942) was a logician and mathematician, known for the invention of combinatory logic.
Life
Mose ...
and
Haskell Curry
Haskell Brooks Curry (; September 12, 1900 – September 1, 1982) was an American mathematician and logician. Curry is best known for his work in combinatory logic. While the initial concept of combinatory logic was based on a single paper by ...
.
All operations in lambda calculus can be encoded via
abstraction elimination
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of comput ...
into the SKI calculus as
binary tree
In computer science, a binary tree is a k-ary k = 2 tree data structure in which each node has at most two children, which are referred to as the ' and the '. A recursive definition using just set theory notions is that a (non-empty) binary t ...
s whose leaves are one of the three symbols S, K, and I (called ''combinators'').
Notation
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 tree KS and whose right subtree is the tree SK can be written as KS(SK). If more explicitness is desired, the implied parentheses can be included as well: ((KS)(SK)).
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. The "function", "argument" and the "value" are either combinators or binary trees. If they are binary trees, they may be thought of as functions too, if needed.
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:
: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'':
: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. 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''.
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) and the resulting expression will yield the same result. So the "I" is merely
syntactic sugar
In computer science, syntactic sugar is syntax within a programming language that is designed to make things easier to read or to express. It makes the language "sweeter" for human use: things can be expressed more clearly, more concisely, or in an ...
. 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
Iota (; uppercase: Ι, lowercase: ι; ) is the ninth letter of the Greek alphabet. It was derived from the Phoenician letter Yodh. Letters that arose from this letter include the Latin alphabet, Latin I and J, the Cyrillic І (І, і), Yi (Cy ...
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 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. All derivations of length 1 are valid derivations.
Recursive parameter passing and quoting
; : quotes q and ignores i
; : forms a binary tree that parameters can flow from root to branches and be read by identityFunc=((SK)K) 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:
: SIIα = Iα(Iα) = αα
One interesting property of this is that it makes the expression SII(SII) irreducible:
: SII(SII) = I(SII)(I(SII)) = I(SII)(SII) = SII(SII)
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:
: (S(Kα)(SII))β = Kαβ(SIIβ) = α(SIIβ) = α(ββ)
This function can be used to achieve
recursion
Recursion (adjective: ''recursive'') occurs when a thing is defined in terms of itself or of its type. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in mathematics ...
. If β is the function that applies α to the self application of something else, then self-applying β performs α recursively on ββ. More clearly, if:
: β = S(Kα)(SII)
then:
: SIIβ = ββ = α(ββ) = α(α(ββ)) =
The reversal expression
S(K(SI))K reverses the following two terms:
: S(K(SI))Kαβ →
: K(SI)α(Kα)β →
: SI(Kα)β →
: Iβ(Kαβ) →
: Iβα →
: βα
Boolean logic
SKI combinator calculus can also implement
Boolean logic
In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variable (mathematics), variables are the truth values ''true'' and ''false'', usually denote ...
in the form of an ''if-then-else'' structure. An ''if-then-else'' structure consists of a Boolean expression that is either true (T) or false (F) and two arguments, such that:
: T''xy'' = ''x''
and
: F''xy'' = ''y''
The key is in defining the two Boolean expressions. The first works just like one of our basic combinators:
: T = K
: K''xy'' = ''x''
The second is also fairly simple:
: F = SK
: SK''xy'' = K''y(xy)'' = y
Once true and false are defined, all Boolean logic can be implemented in terms of ''if-then-else'' structures.
Boolean NOT (which returns the opposite of a given Boolean) 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:
: NOT = (F)(T) = (SK)(K)
If this is put in an ''if-then-else'' structure, it can be shown that this has the expected result
: (T)NOT = T(F)(T) = F
: (F)NOT = F(F)(T) = T
Boolean OR (which returns T if either of the two Boolean values surrounding it is T) works the same as an ''if-then-else'' structure with T as the second value, so it can be implemented as an infix operation:
: OR = T = K
If this is put in an ''if-then-else'' structure, it can be shown that this has the expected result:
: (T)OR(T) = T(T)(T) = T
: (T)OR(F) = T(T)(F) = T
: (F)OR(T) = F(T)(T) = T
: (F)OR(F) = F(T)(F) = F
Boolean AND (which returns T if both of the two Boolean values surrounding it are T) works the same as an ''if-then-else'' structure with F as the third value, so it can be implemented as a postfix operation:
: AND = F = SK
If this is put in an ''if-then-else'' structure, it can be shown that this has the expected result:
: (T)(T)AND = T(T)(F) = T
: (T)(F)AND = T(F)(F) = F
: (F)(T)AND = F(T)(F) = F
: (F)(F)AND = F(F)(F) = F
Because this defines T, F, NOT (as a postfix operator), OR (as an infix operator), and AND (as a postfix operator) in terms of SKI notation, this proves that the SKI system can fully express Boolean logic.
As the SKI calculus is
complete
Complete may refer to:
Logic
* Completeness (logic)
* Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable
Mathematics
* The completeness of the real numbers, which implies t ...
, it is also possible to express NOT, OR and AND as prefix operators:
: NOT = S(SI(KF))(KT) (as S(SI(KF))(KT)''x'' = SI(KF)''x''(KT''x'') = I''x''(KF''x'')T = ''x''FT)
: OR = SI(KT) (as SI(KT)''xy'' = I''x''(KT''x'')''y'' = ''x''T''y'')
: AND = SS(K(KF)) (as SS(K(KF))''xy'' = S''x''(K(KF)''x'')''y'' = ''xy''(KF''y'') = ''xy''F)
Connection to intuitionistic logic
The combinators K and S correspond to two well-known axioms of
sentential logic
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
:
:,
:.
Function application corresponds to the rule
modus ponens
In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. ...
:
:: from and , infer .
The axioms AK and AS, and the rule MP are complete for the implicational fragment of
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
. In order for combinatory logic to have as a model:
*The
implicational fragment of
classical logic
Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this class ...
, would require the combinatory analog to the
law of excluded middle
In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradic ...
, ''i.e.'',
Peirce's law
In logic, Peirce's law is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic. It can be thought of as the law of excluded middle written in a form that i ...
;
*
Complete classical logic, would require the combinatory analog to the sentential axiom .
This connection between the types of combinators and the corresponding logical axioms is an instance of the
Curry–Howard isomorphism.
Examples of reduction
*
*
*
See also
*
Combinatory logic
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of comput ...
*
B, C, K, W system
The B, C, K, W system is a variant of combinatory logic that takes as primitive the combinators B, C, K, and W. This system was discovered by Haskell Curry in his doctoral thesis ''Grundlagen der kombinatorischen Logik'', whose results are set out ...
*
Fixed point combinator
In mathematics and computer science in general, a '' fixed point'' of a function is a value that is mapped to itself by the function.
In combinatory logic for computer science, a fixed-point combinator (or fixpoint combinator) is a higher-order f ...
*
Lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
*
Functional programming
In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declar ...
*
Unlambda
Unlambda is a minimal, "nearly pure" functional programming language invented by David Madore. It is based on combinatory logic, an expression system without the lambda operator or free variables. It relies mainly on two built-in functions (s a ...
programming language
* The
Iota and Jot
In formal language theory and computer science, Iota and Jot (from Greek iota ι, Hebrew yodh י, the smallest letters in those two alphabets) are languages, extremely minimalist formal systems, designed to be even simpler than other more popular ...
programming languages, designed to be even simpler than SKI.
* ''
To Mock a Mockingbird
''To Mock a Mockingbird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic'' (1985, {{isbn, 0-19-280142-2) is a book by the mathematician and logician Raymond Smullyan. It contains many nontrivial recreational puzzles ...
''
References
* A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors.
* are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
{{refend
External links
* O'Donnell, Mike
The SKI Combinator Calculus as a Universal System.
* Keenan, David C. (2001)
* Rathman, Chris,
*
A Calculus of Mobile Processes, Part I(PostScript) (by Milner, Parrow, and Walker) shows a scheme for ''combinator
graph reduction
In computer science, graph reduction implements an efficient version of non-strict evaluation, an evaluation strategy where the arguments to a function are not immediately evaluated. This form of non-strict evaluation is also known as lazy evaluati ...
'' for the SKI calculus in pages 25–28.
* th
Nock programming languagemay 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