Editing Combinatory logic (section)

=== Simplifications of the transformation ===

==== η-reduction ====

The combinators generated by the ''T''[&nbsp;] transformation can be made smaller if we take into account the ''η-reduction'' rule:

:''T''[''λx''.(''E'' ''x'')] = ''T''[''E'']   (if ''x'' is not free in ''E'')

''λx''.(''E'' x) is the function which takes an argument, ''x'', and applies the function ''E'' to it; this is extensionally equal to the function ''E'' itself. It is therefore sufficient to convert ''E'' to combinatorial form.

Taking this simplification into account, the example above becomes:

:{{spaces|2}}''T''[''λx''.''λy''.(''y'' ''x'')]
:= ...
:= ('''S''' ('''K''' ('''S I'''))   ''T''[''λx''.('''K''' ''x'')])
:= ('''S''' ('''K''' ('''S I'''))   '''K''')                 (by η-reduction)

This combinator is equivalent to the earlier, longer one:

:{{spaces|2}}('''S''' ('''K''' ('''S I'''))   '''K''' ''x y'')
:= ('''K''' ('''S I''') ''x'' ('''K''' ''x'') ''y'')
:= ('''S I''' ('''K''' ''x'') ''y'')
:= ('''I''' ''y'' ('''K''' ''x y''))
:= (''y'' ('''K''' ''x y''))
:= (''y x'')

Similarly, the original version of the ''T''[&nbsp;] transformation transformed the identity function ''λf''.''λx''.(''f'' ''x'') into ('''S''' ('''S''' ('''K S''') ('''S''' ('''K K''') '''I''')) ('''K I''')).  With the η-reduction rule, ''λf''.''λx''.(''f'' ''x'') is
transformed into '''I'''.

==== One-point basis ====

There are one-point bases from which every combinator can be composed extensionally equal to ''any'' lambda term. A simple example of such a basis is {'''X'''} where:

:'''X''' ≡ ''λx''.((x'''S''')'''K''')

It is not difficult to verify that:
:'''X''' ('''X''' ('''X''' '''X''')) =<sup>β</sup> '''K''' and
:'''X''' ('''X''' ('''X''' ('''X''' '''X'''))) =<sup>β</sup> '''S'''.

Since {'''K''', '''S'''} is a basis, it follows that {'''X'''} is a basis too. The [[Iota and Jot|Iota]] programming language uses '''X''' as its sole combinator.

Another simple example of a one-point basis is:

:'''X'''' ≡ ''λx''.(x '''K''' '''S''' '''K''') with
:('''X'''' '''X'''') '''X'''' =<sup>β</sup> '''K''' and
:'''X'''' ('''X'''' '''X'''') =<sup>β</sup> '''S'''

The simplest known one-point basis is a slight modification of '''S''':

:'''S'''' ≡ ''λxλyλz''. (x z) (y (λw. z))) with
:'''S'''' ('''S'''' '''S'''') ('''S'''' ('''S'''' '''S'''') '''S'''' '''S'''' '''S'''' '''S'''' '''S'''') = <sup>β</sup> '''K''' and
:'''S'''' ('''S'''' ('''S'''' '''S'''' ('''S'''' '''S'''' ('''S'''' '''S''''))('''S'''' ('''S'''' ('''S'''' '''S'''' ('''S'''' '''S'''')))))) '''S'''' '''S'''' = <sup>β</sup> '''S'''.

In fact, there exist infinitely many such bases.{{sfn|Goldberg|2004}}

==== Combinators B, C ====

In addition to '''S''' and '''K''', {{harvtxt|Schönfinkel|1924}} included two combinators which are now called '''B''' and '''C''', with the following reductions:

:('''C''' ''f'' ''g'' ''x'') = ((''f'' ''x'') ''g'')
:('''B''' ''f'' ''g'' ''x'') = (''f'' (''g'' ''x''))

He also explains how they in turn can be expressed using only '''S''' and '''K''':

:'''B''' = ('''S''' ('''K S''') '''K''') 
:'''C''' = ('''S''' ('''S''' ('''K''' ('''S''' ('''K S''') '''K''')) '''S''') ('''K K'''))

These combinators are extremely useful when translating predicate logic or lambda calculus into combinator expressions. They were also used by [[Haskell Curry|Curry]], and much later by [[David Turner (computer scientist)|David Turner]], whose name has been associated with their computational use. Using them, we can extend the rules for the transformation 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'' is not free in ''E'')
#{{nowrap|''T''[''λx''.''x'']       ⇒ '''I'''}}
#{{nowrap|''T''[''λx''.''λy''.''E'']    ⇒ ''T''{{!(}}''λx''.''T''{{!(}}''λy''.''E''{{))!}}}} (if ''x'' is 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'' is free in both ''E''{{sub|1}} and ''E''{{sub|2}})
#{{nowrap|''T''[''λx''.(''E''{{sub|1}} ''E''{{sub|2}})] ⇒ ('''C''' ''T''[''λx''.''E''{{sub|1}}] ''T''[''E''{{sub|2}}])}} (if ''x'' is free in ''E''{{sub|1}} but not ''E''{{sub|2}})
#{{nowrap|''T''[''λx''.(''E''{{sub|1}} ''E''{{sub|2}})] ⇒ ('''B''' ''T''[''E''{{sub|1}}] ''T''[''λx''.''E''{{sub|2}}])}} (if ''x'' is free in ''E''{{sub|2}} but not ''E''{{sub|1}})

Using '''B''' and '''C''' combinators, the transformation of ''λx''.''λy''.(''y'' ''x'') looks like this:

:{{spaces|2}}{{nowrap|1=''T''[''λx''.''λy''.(''y'' ''x'')]}}
:{{nowrap|1== ''T''{{!(}}''λx''.''T''{{!(}}''λy''.(''y'' ''x''){{))!}}}}
:{{nowrap|1== ''T''[''λx''.('''C''' ''T''[''λy''.''y''] ''x'')]}}     (by rule 7)
:{{nowrap|1== ''T''[''λx''.('''C''' '''I''' ''x'')]}}
:{{nowrap|1== ('''C''' '''I''')}} (η-reduction)
:<math>= \mathsf{C}_{*}</math> (traditional canonical notation: <math>\mathsf{X}_{*} = \mathsf{X I}</math>)
:<math>= \mathsf{I}'</math> (traditional canonical notation: <math>\mathsf{X}' = \mathsf{C X}</math>)

And indeed, ('''C''' '''I''' ''x'' ''y'') does reduce to (''y'' ''x''):

:{{spaces|2}}('''C''' '''I''' ''x'' ''y'')
:= ('''I''' ''y'' ''x'')
:= (''y'' ''x'')

The motivation here is that '''B''' and '''C''' are limited versions of '''S'''. Whereas '''S''' takes a value and substitutes it into both the applicand and its argument before performing the application, '''C''' performs the
substitution only in the applicand, and '''B''' only in the argument.

The modern names for the combinators come from [[Haskell Curry]]'s doctoral thesis of 1930 (see [[B, C, K, W System]]). In [[Moses Schönfinkel|Schönfinkel]]'s original paper, what we now call  '''S''', '''K''', '''I''', '''B''' and '''C''' were called '''S''', '''C''', '''I''', '''Z''', and '''T''' respectively.

The reduction in combinator size that results from the new transformation rules can also be achieved without introducing '''B''' and '''C''', as demonstrated in Section 3.2 of {{harvtxt|Tromp|2008}}.

===== CL<sub>K</sub> versus CL<sub>I</sub> calculus =====
A distinction must be made between the '''CL'''<sub>K</sub> as described in this article and the '''CL'''<sub>I</sub> calculus. The distinction corresponds to that between the λ<sub>K</sub> and the λ<sub>I</sub> calculus. Unlike the λ<sub>K</sub> calculus, the λ<sub>I</sub> calculus restricts abstractions to:
::''λx''.''E'' where ''x'' has at least one free occurrence in ''E''.
As a consequence, combinator '''K''' is not present in the λ<sub>I</sub> calculus nor in the '''CL'''<sub>I</sub> calculus. The constants of '''CL'''<sub>I</sub> are: '''I''', '''B''', '''C''' and '''S''', which form a basis from which all '''CL'''<sub>I</sub> terms can be composed (modulo equality). Every λ<sub>I</sub> term can be converted into an equal '''CL'''<sub>I</sub> combinator according to rules similar to those presented above for the conversion of λ<sub>K</sub> terms into '''CL'''<sub>K</sub> combinators. See chapter 9 in Barendregt (1984).