Editing SKI combinator calculus (section)

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