Editing Combinatory logic (section)

=== Completeness of the S-K basis ===

'''S''' and '''K''' can be composed to produce combinators that are extensionally equal to ''any'' lambda term, and therefore, by Church's thesis, to any computable function whatsoever. The proof is to present a transformation, {{nowrap|''T''[&nbsp;]}}, which converts an arbitrary lambda term into an equivalent combinator.

{{nowrap|''T''[&nbsp;]}} may be defined as follows:

#      {{nowrap| ''T''[''x'']          ⇒ ''x''}}
#      {{nowrap| ''T''[(''E''{{sub|1}} ''E''{{sub|2}})]    ⇒ (''T''[''E''{{sub|1}}] ''T''[''E''{{sub|2}}])}}
#      {{nowrap| ''T''[''λx''.''E'']       ⇒ ('''K''' ''T''[''E''])}}         (if ''x'' does not occur free in ''E'')
#      {{nowrap| ''T''[''λx''.''x'']       ⇒ '''I'''}}
#      {{nowrap| ''T''[''λx''.''λy''.''E'']    ⇒ ''T''{{!(}}''λx''.''T''{{!(}}''λy''.''E''{{))!}}}} (if ''x'' occurs free in ''E'')
#      {{nowrap| ''T''[''λx''.(''E''{{sub|1}} ''E''{{sub|2}})] ⇒ ('''S''' ''T''[''λx''.''E''{{sub|1}}] ''T''[''λx''.''E''{{sub|2}}])}} (if ''x'' occurs free in ''E''{{sub|1}} or ''E''{{sub|2}})

Note that ''T''[&nbsp;] as given is not a well-typed mathematical function, but rather a term rewriter: Although it eventually yields a combinator, the transformation may generate intermediary expressions that are neither lambda terms nor combinators, via rule (5).

This process is also known as ''abstraction elimination''. This definition is exhaustive: any lambda expression will be subject to exactly one of these rules (see [[Combinatory logic#Summary of lambda calculus|Summary of lambda calculus]] above).

It is related to the process of ''bracket abstraction'', which takes an expression ''E'' built from variables and application and produces a combinator expression [x]E in which the variable x is not free, such that [''x'']''E x'' = ''E'' holds. A very simple algorithm for bracket abstraction is defined by induction on the structure of expressions as follows:{{sfn|Turner|1979}}
# [''x'']''y'' := '''K''' ''y''
# [''x'']''x'' := '''I'''
# [''x''](''E''{{sub|1}} ''E''{{sub|2}}) := '''S'''([''x'']''E''{{sub|1}})([''x'']''E''{{sub|2}})
Bracket abstraction induces a translation from lambda terms to combinator expressions, by interpreting lambda-abstractions using the bracket abstraction algorithm.

==== Conversion of a lambda term to an equivalent combinatorial term ====

For example, we will convert the lambda term ''λx''.''λy''.(''y'' ''x'') to a combinatorial term:

:''T''[''λx''.''λy''.(''y'' ''x'')]
::        = ''T''{{!(}}''λx''.''T''{{!(}}''λy''.(''y'' ''x''){{))!}} (by 5)
::        = ''T''[''λx''.('''S''' ''T''[''λy''.''y''] ''T''[''λy''.''x''])] (by 6)
::        = ''T''[''λx''.('''S I'''       ''T''[''λy''.''x''])] (by 4)
::        = ''T''[''λx''.('''S I'''       ('''K''' ''T''[''x'']))] (by 3)
::        = ''T''[''λx''.('''S I'''       ('''K''' ''x''))] (by 1)
::        = ('''S''' ''T''[''λx''.('''S I''')] ''T''[''λx''.('''K''' ''x'')]) (by 6)
::        = ('''S''' ('''K''' ('''S I'''))   ''T''[''λx''.('''K''' ''x'')]) (by 3)
::        = ('''S''' ('''K''' ('''S I'''))   ('''S''' ''T''[''λx''.'''K'''] ''T''[''λx''.''x''])) (by 6)
::        = ('''S''' ('''K''' ('''S I'''))   ('''S''' ('''K K''') ''T''[''λx''.''x''])) (by 3)
::        = ('''S''' ('''K''' ('''S I'''))   ('''S''' ('''K K''') '''I''')) (by 4)

If we apply this combinatorial term to any two terms ''x'' and ''y'' (by feeding them in a queue-like fashion into the combinator 'from the right'), it reduces as follows:

:          ('''S''' ('''K''' ('''S''' '''I''')) ('''S''' ('''K''' '''K''') '''I''') x y)
::        = ('''K''' ('''S''' '''I''') x  ('''S''' ('''K''' '''K''')   '''I''' x) y)
::        = ('''S''' '''I''' ('''S''' ('''K''' '''K''')   '''I''' x) y)
::        = ('''I''' y ('''S''' ('''K''' '''K''')   '''I''' x y))
::        = (y ('''S''' ('''K''' '''K''')   '''I''' x y))
::        = (y ('''K''' '''K''' x ('''I''' x) y))
::        = (y ('''K''' ('''I''' x) y))
::        = (y ('''I''' x))
::        = (y x)

The combinatory representation, ('''S''' ('''K''' ('''S I''')) ('''S''' ('''K K''') '''I''')) is much longer than the representation as a lambda term, ''λx''.''λy''.(y x).  This is typical. In general, the ''T''[&nbsp;] construction may expand a lambda term of length ''n'' to a combinatorial term of length [[Big O notation|Θ]](''n''<sup>3</sup>).{{sfn|Lachowski |2018}}

==== Explanation of the ''T''[&nbsp;] transformation ====

The ''T''[&nbsp;] transformation is motivated by a desire to eliminate abstraction. Two special cases, rules 3 and 4, are trivial: ''λx''.''x'' is clearly equivalent to '''I''', and ''λx''.''E'' is clearly equivalent to ('''K''' ''T''[''E'']) if ''x'' does not appear free in ''E''.

The first two rules are also simple: Variables convert to themselves, and applications, which are allowed in combinatory terms, are converted to combinators simply by converting the applicand and the argument to combinators.

It is rules 5 and 6 that are of interest.  Rule 5 simply says that to convert a complex abstraction to a combinator, we must first convert its body to a combinator, and then eliminate the abstraction.  Rule 6 actually eliminates the abstraction.

''λx''.(''E''{{sub|1}} ''E''{{sub|2}}) is a function which takes an argument, say ''a'', and substitutes it into the lambda term (''E''{{sub|1}} ''E''{{sub|2}}) in place of ''x'', yielding (''E''{{sub|1}} ''E''{{sub|2}})[''x'' : = ''a'']. But substituting ''a'' into (''E''{{sub|1}} ''E''{{sub|2}}) in place of ''x'' is just the same as substituting it into both ''E''{{sub|1}} and ''E''{{sub|2}}, so

:(''E''{{sub|1}} ''E''{{sub|2}})[''x'' := ''a''] = (''E''{{sub|1}}[''x'' := ''a''] ''E''{{sub|2}}[''x'' := ''a''])

:(''λx''.(''E''{{sub|1}} ''E''{{sub|2}}) ''a'') = ((''λx''.''E''{{sub|1}} ''a'') (''λx''.''E''{{sub|2}} ''a''))
:::::= ('''S''' ''λx''.''E''{{sub|1}} ''λx''.''E''{{sub|2}} ''a'')
:::::= (('''S''' ''λx''.''E''{{sub|1}} ''λx''.''E''{{sub|2}}) ''a'')

By extensional equality,

:''λx''.(''E''{{sub|1}} ''E''{{sub|2}})     = ('''S''' ''λx''.''E''{{sub|1}} ''λx''.''E''{{sub|2}})

Therefore, to  find  a combinator equivalent to ''λx''.(''E''{{sub|1}} ''E''{{sub|2}}), it is sufficient to find a combinator equivalent to ('''S''' ''λx''.''E''{{sub|1}} ''λx''.''E''{{sub|2}}), and

:('''S''' ''T''[''λx''.''E''{{sub|1}}] ''T''[''λx''.''E''{{sub|2}}])

evidently fits the bill.  ''E''{{sub|1}} and ''E''{{sub|2}} each contain strictly fewer applications than (''E''{{sub|1}} ''E''{{sub|2}}), so the recursion must terminate in a lambda term with no applications at all—either a variable, or a term of the
form ''λx''.''E''.