Editing Combinatory logic (section)

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