Editing SKI combinator calculus

{{Short description|Simple Turing complete logic}}
The '''SKI combinator calculus''' is a [[combinatory logic|combinatory logic system]] and a [[model of computation|computational system]]. It can be thought of as a computer programming language, though it is not convenient for writing software.{{Citation needed|date=May 2025}} Instead, it is important in the mathematical theory of [[algorithm]]s because it is an extremely simple [[Turing complete]] language. It can be likened to a reduced version of the untyped [[lambda calculus]]. It was introduced by [[Moses Schönfinkel]]<ref>{{cite journal |first=M. |last=Schönfinkel |date=1924 |title=Über die Bausteine der mathematischen Logik |journal=Mathematische Annalen |volume=92 |issue=3–4 |pages=305–316 |doi=10.1007/BF01448013|s2cid=118507515 }} Translated by Stefan Bauer-Mengelberg as {{cite book |chapter=On the building blocks of mathematical logic |chapter-url=https://books.google.com/books?id=v4tBTBlU05sC&pg=PA355 |editor-link=Jean van Heijenoort |editor-first=Jean |editor-last=van Heijenoort |orig-year=1967 |title=A Source Book in Mathematical Logic 1879–1931 |publisher=Harvard University Press |pages=355–366 |date=2002 |isbn=9780674324497}}</ref> and [[Haskell Curry]].<ref>{{cite journal|last=Curry|first=Haskell Brooks|title=Grundlagen der Kombinatorischen Logik|journal=American Journal of Mathematics|year=1930|volume=52|issue=3|pages=509–536|authorlink=Haskell Curry|trans-title=Foundations of combinatorial logic|publisher=Johns Hopkins University Press|language=German|doi=10.2307/2370619|jstor=2370619}}</ref>

All operations in lambda calculus can be encoded via [[Combinatory logic#Completeness of the S-K basis|abstraction elimination]] into the SKI calculus as [[binary tree]]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 ''y'', 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" for any ''x''  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''' ''x'') for any ''x'', 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 and Jot|iota]] combinator, which can be expressed in terms of '''S''' and '''K''' as follows:
: ι''x'' = ''x'''''SK''' = '''S'''(λ''x''.''x'''''S''')(λ''x''.'''K''') = '''S'''('''S'''(λx.x)(λx.'''S'''))('''KK''') = '''S'''('''SI'''('''KS'''))('''KK''')
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'''.

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'''.

==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 τ<sub>1</sub> and τ<sub>2</sub> are terms, then (τ<sub>1</sub>τ<sub>2</sub>) 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. All derivations of length 1 are valid derivations.

==Converting lambda calculus expressions into SKI combinator calculus expressions==
An expression in the lambda calculus can be converted into an SKI combinator calculus expression in accordance with the following rules:
# λ''x''. ''x'' = '''I'''
# λ''x''. c = '''K'''c (provided that c does not depend on ''x'')
# λ''x''. ''f'' ''x'' = ''f''
# λ''x''. ''y'' ''z'' = '''S'''(λ''x''.''y'')(λ''x''.''z'')

==SKI expressions==

===Self-application and recursion===
'''SII''' is an expression that takes an argument and applies that argument to itself:
: '''SII'''α = '''I'''α('''I'''α) = αα

This is also known as '''U''' combinator, '''U'''''x'' = ''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 get '''U''' '''U''' = '''U''' '''U'''.

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, '''H'''''xy'' = ''x''(''yy'').

This function can be used to achieve [[recursion]].  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'''β = ββ = α(ββ) = α(α(ββ)) = <math>\ldots</math>
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 using ''the 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 us [[Fixed-point_combinator#Other_fixed-point_combinators|one possible encoding]] of the '''Y''' combinator. A shorter variation replaces its two leading subterms with just '''SSI''', since '''H'''α('''H'''α) = '''SHH'''α = '''SSIH'''α.

This becomes much shorter with the use of the [[B, C, K, W system|'''B,C,W''' combinators]], as [[B, C, K, W system#Connection_to_other_combinators|the equivalent]]

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

<!-- or, directly using the '''H''' combinator definition,

: '''H'''gx = g(xx) = '''B'''g'''U'''x = '''CBU'''gx = '''SB(KU)'''gx , or '''B'''gxx = '''W'''('''B'''g)x = '''BWB'''gx = '''S(KW)B'''gx 
: '''Y'''g = '''H'''g('''H'''g) = '''U'''('''H'''g) = '''BUH'''g, or '''SHH'''g = '''WSH'''g = '''SSIH'''g  -->
<!--
Yα = S(K(SII))(S(S(KS)K)(K(SII))) α = SSI(S(S(KS)K)(K(SII))) α
Yα = S(KU)(SB(KU))α = U(BαU) = BU(CBU)α = SSI(CBU)α = SSI(BWB) α
-->
And with a pseudo-[[Haskell (programming language)|Haskell]] syntax it becomes the exceptionally short '''Y''' = '''U''' . (. '''U''').

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

* This '''Y''', by [[Haskell Curry]]:
: '''H'''''gx'' = ''g''(''xx'') ; '''Y'''''g'' = '''H'''''g''('''H'''''g'') ; '''Y = SSI(SB(KU)) = SSI(S(S(KS)K)(K(SII)))'''
* Turing's '''Θ''':
: '''H'''''hg'' = ''g''(''hhg'') ; '''Θ'''''g'' = '''HH'''''g'' ; '''Θ = U(B(SI)U) = SII(S(K(SI))(SII))'''
* '''Y'''' (with SK-encoding by [[John Tromp]]<ref>https://tromp.github.io/</ref>):
: '''H'''''gh'' = ''g''(''hgh'') ; '''Y''''''g'' = '''H'''''g'''''H''' ; '''Y' = WC(SB(C(WC))) = SSK(S(K(SS(S(SSK))))K)'''
* '''Θ₄''' by R.Statman:<ref>{{cite journal|first1=William McCune|last1=Larry Wos|author1-link=|title=Searching for Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report|website=Argonne National Laboratory|date=September 1988|url=https://inis.iaea.org/collection/NCLCollectionStore/_Public/20/016/20016944.pdf|editor1-first=|editor1-last=|edition=|access-date=December 12, 2024}}, p.9</ref>
: '''H'''''gyz'' = ''g''(''yyz'') ; '''Θ₄'''''g'' = '''H'''''g''('''H'''''g'')('''H'''''g'') ; '''Θ₄ = B(WW)(BW(BBB))'''
* or in general,
: '''H'''''something'' = ''g''(''hsomething'') ; '''Y'''<sub><sub>H</sub></sub>&thinsp;''g'' = '''H'''_____'''H'''__&thinsp;''g''
:  (where anything goes instead of "_") or any other intermediary '''H''' combinator's definition, with its correspondent '''Y''' definition to jump-start it correctly. In particular,<ref>"A construction due to Klop 2007" https://ncatlab.org/nlab/show/fixed-point+combinator</ref>
: '''L'''''abcdefghijklmnopqstuvwxyzr'' = ''r''(''thisisafixedpointcombinator'') ; '''Y = LLLLLLLLLLLLLLLLLLLLLLLLLL''' 
<!--
      Hgh = g(hgh)
 Yg = HgH
 &nbsp;
      Hhg = g(hhg)
 Yg = HHg
 &nbsp;
      Hsomething = g(hsomething)
 Yg = H_____H__g
-->

In a [[strict programming language]] the [[Fixed-point combinator|Y combinator]] will expand until [[stack overflow]], or never halt in case of [[tail call optimization]].<ref>{{cite web |last1=Bene |first1=Adam |title=Fixed-Point Combinators in JavaScript |url=https://blog.benestudio.co/fixed-point-combinators-in-javascript-c214c15ff2f6 |website=Bene Studio |publisher=Medium |access-date=2 August 2020 |language=en |date=17 August 2017}}</ref> The [[Z combinator]] will work in [[Strict programming language|strict languages]] (also called eager languages, where applicative evaluation order is applied).

: <math>\begin{align}
Z & = \lambda f. (\lambda x. f (\lambda v. x x v))(\lambda x. f (\lambda v. x x v)) \\
& = \lambda f. U (\lambda x. f (\lambda v. U x v)) \\
& = S(\lambda f. U)(\lambda f. \lambda x. f (\lambda v. U x v)) \\
& = S(KU)(\lambda f. S(\lambda x. f)(\lambda x. \lambda v. U x v)) \\
& = S(KU)(\lambda f. S(K f)(\lambda x. \lambda v. U x v)) \\
& = S(KU)(S(\lambda f. S(K f))(\lambda f. \lambda x. \lambda v. U x v)) \\
& = S(KU)(S(S(\lambda f. S)(\lambda f. K f))(K(\lambda x. \lambda v. U x v))) \\
& = S(KU)(S(S(KS)K)(K(\lambda x. \lambda v. U x v))) \\
& = S(KU)(S(S(KS)K)(K(\lambda x. S({\color{Red}\lambda v. U x})(\lambda v. v)))) \\
& = S(KU)(S(S(KS)K)(K(\lambda x. S(S(\lambda v. U)(\lambda v. x))I))) \\
& = S(KU)(S(S(KS)K)(K(\lambda x. S(S(KU)(Kx))I))) \\
& = S(KU)(S(S(KS)K)(K(S(\lambda x. S(S(KU)(Kx)))(\lambda x. I)))) \\
& = S(KU)(S(S(KS)K)(K(S(S(\lambda x. S)(\lambda x. S(KU)(Kx)))(KI)))) \\
& = S(KU)(S(S(KS)K)(K(S(S(KS)(S(\lambda x. S(KU))(\lambda x. Kx)))(KI)))) \\
& = S(KU)(S(S(KS)K)(K(S(S(KS)(S(K(S(KU)))K))(KI)))) \\
\end{align}</math>

===The reversal expression===
'''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 to '''CI'''. And in general, '''S'''('''K'''('''S'''''f''))'''K''' is equivalent to '''C'''''f'', for any ''f''.

===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 ('''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''' = λb.b ('''F''')('''T''') = λb.b ('''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 [[Combinatory logic#Completeness of the S-K basis|complete]], 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]]:

:{{math|'''AK''': ''A'' &rarr; (''B'' &rarr; ''A'')}},
:{{math|'''AS''': (''A'' &rarr; (''B'' &rarr; ''C'')) &rarr; ((''A'' &rarr; ''B'') &rarr; (''A'' &rarr; ''C''))}}.

Function application corresponds to the rule [[modus ponens]]:

:{{math|'''MP'''}}: from {{mvar|A}} and {{math|''A'' &rarr; ''B''}}, infer {{mvar|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 propositional calculus|implicational fragment]] of [[classical logic]], would require the combinatory analog to the [[law of excluded middle]], ''i.e.'', [[Peirce's law]];
*[[sentential logic|Complete classical logic]], would require the combinatory analog to the sentential axiom {{math|'''F''' &rarr; ''A''}}.

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

== Examples of reduction ==

There may be multiple ways to do a reduction. All are equivalent, as long as you don't break order of operations

* <math>\mathsf{SKI(KIS)}</math>
** <math>\mathsf{SKI(KIS)} \Rightarrow \mathsf{K(KIS)(I(KIS))} \Rightarrow \mathsf{KIS} \Rightarrow \mathsf{I}</math>
** <math>\mathsf{SKI(KIS)} \Rightarrow \mathsf{SKII} \Rightarrow \mathsf{KI(II)} \Rightarrow \mathsf{KII} \Rightarrow \mathsf{I}</math>
* <math>\mathsf{KS(I(SKSI))}</math>
** <math>\mathsf{KS(I(SKSI))} \Rightarrow \mathsf{KS(I(KI(SI)))} \Rightarrow \mathsf{KS(I(I))} \Rightarrow \mathsf{KS(II)} \Rightarrow \mathsf{KSI} \Rightarrow \mathsf{S}</math>
** <math>\mathsf{KS(I(SKSI))} \Rightarrow \mathsf{S}</math>
* <math>\mathsf{SKIK} \Rightarrow \mathsf{KK(IK)} \Rightarrow \mathsf{KKK} \Rightarrow \mathsf{K}</math>

== See also ==
* [[Combinatory logic]]
* [[B, C, K, W system]]
* [[Fixed point combinator]]
* [[Lambda calculus]]
* [[Functional programming]]
* [[Unlambda]] programming language
* The [[Iota and Jot]] programming languages, designed to be even simpler than SKI. 
* ''[[To Mock a Mockingbird]]''

==References ==
{{Reflist}}
{{refbegin}}
*{{cite book |author-link=Raymond Smullyan |last=Smullyan |first=Raymond |date=1985 |title=To Mock a Mockingbird |title-link=To Mock a Mockingbird |publisher=Knopf |isbn=0-394-53491-3}} A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors.
*{{cite book |author-mask=1 |author-link=Raymond Smullyan |last=Smullyan |first=Raymond |date=1994 |title=Diagonalization and Self-Reference |publisher=Oxford University Press |chapter=Ch. 17–20 |isbn=9780198534501 |oclc=473553893}} are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
{{refend}}

==External links==
* O'Donnell, Mike "[http://people.cs.uchicago.edu/~odonnell/Teacher/Lectures/Formal_Organization_of_Knowledge/Examples/combinator_calculus/ The SKI Combinator Calculus as a Universal System.]"
* Keenan, David C. (2001) "[http://dkeenan.com/Lambda/index.htm To Dissect a Mockingbird.]"
* Rathman, Chris, "[https://www.angelfire.com/tx4/cus/combinator/birds.html Combinator Birds.]"
* "[https://web.archive.org/web/20081029051502/http://cstein.kings.cam.ac.uk/~chris/combinators.html "Drag 'n' Drop Combinators (Java Applet).]"
* [http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-85/ A Calculus of Mobile Processes, Part I] (PostScript) (by Milner, Parrow, and Walker) shows a scheme for ''combinator [[graph reduction]]'' for the SKI calculus in pages 25–28.
* the [https://web.archive.org/web/20131014210033/http://www.urbit.org/2013/08/22/Chapter-2-nock.html Nock 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.

[[Category:Lambda calculus]]
[[Category:Combinatory logic]]