Editing Combinatory logic (section)

== Combinatory calculi ==

Since abstraction is the only way to manufacture functions in the lambda calculus, something must replace it in the combinatory calculus. Instead of abstraction, combinatory calculus provides a limited set of primitive functions out of which other functions may be built.

=== Combinatory terms ===

A combinatory term has one of the following forms:

{| class="wikitable"
|-
! Syntax !! Name !! Description
|-
| x || Variable || A character or string representing a combinatory term.
|-
| P || Primitive function || One of the combinator symbols '''I''', '''K''', '''S'''.
|-
| (M N) || Application || Applying a function to an argument. M and N are combinatory terms. 
|}

The primitive functions are ''combinators'', or functions that, when seen as lambda terms, contain no [[free variable]]s.

To shorten the notations, a general convention is that {{tmath|(E_1 E_2 E_3 ... E_n)}}, or even {{tmath|E_1 E_2 E_3... E_n}}, denotes the term {{tmath|(...((E_1 E_2) E_3)... E_n)}}. This is the same general convention (left-associativity) as for multiple application in lambda calculus.

=== Reduction in combinatory logic ===

In combinatory logic, each primitive combinator comes with a reduction rule of the form

:{{math|1=(''P'' ''x''<sub>1</sub> ... ''x<sub>n</sub>'') = ''E''}}

where ''E'' is a term mentioning only variables from the set {{math|{{mset|''x''<sub>1</sub> ... ''x<sub>n</sub>''}}}}. It is in this way that primitive combinators behave as functions.

=== Examples of combinators ===

The simplest example of a combinator is '''I''', the identity combinator, defined by

:('''I''' ''x'') = ''x''

for all terms ''x''.  Another simple combinator is '''K''', which manufactures constant functions:  ('''K''' ''x'') is the function which, for any argument, returns ''x'', so we say

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

for all terms ''x'' and ''y''.  Or, following the convention for multiple application,

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

A third combinator is '''S''', which is a generalized version of application:

:('''S''' ''x y z'') = (''x z'' (''y z''))

'''S''' applies ''x'' to ''y'' after first substituting ''z'' into
each of them. Or put another way, ''x'' is applied to ''y'' inside the environment ''z''.

Given '''S''' and '''K''', '''I''' itself is unnecessary, since it can be built from the other two:

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

for any term ''x''.  Note that although (('''S K K''')
''x'') = ('''I''' ''x'') for any ''x'', ('''S K K''')
itself is not equal to '''I'''.  We say the terms are [[extensional equality|extensionally equal]].  Extensional equality captures the mathematical notion of the equality of functions: that two functions are ''equal'' if they always produce the same results for the same arguments.  In contrast, the terms themselves, together with the reduction of primitive combinators, capture the notion of ''intensional equality'' of functions: that two functions are ''equal'' only if they have identical implementations [[up to]] the expansion of primitive combinators.  There are many ways to implement an identity function; ('''S K K''') and '''I''' are among these ways.  ('''S K S''') is yet another. We will use the word ''equivalent'' to indicate extensional equality, reserving ''equal'' for identical combinatorial terms.

A more interesting combinator is the [[fixed point combinator]] or '''Y''' combinator, which can be used to implement [[recursion]].

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

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

=== Reverse conversion ===

The conversion ''L''[&nbsp;] from combinatorial terms to lambda terms is trivial:

:''L''['''I'''] = ''λx''.''x''
:''L''['''K'''] = ''λx''.''λy''.''x''
:''L''['''C'''] = ''λx''.''λy''.''λz''.(''x'' ''z'' ''y'')
:''L''['''B'''] = ''λx''.''λy''.''λz''.(''x'' (''y'' ''z''))
:''L''['''S'''] = ''λx''.''λy''.''λz''.(''x'' ''z'' (''y'' ''z''))
:''L''[(''E''{{sub|1}} ''E''{{sub|2}})] = (''L''[''E''{{sub|1}}] ''L''[''E''{{sub|2}}])

Note, however, that this transformation is not the inverse
transformation of any of the versions of ''T''[&nbsp;] that we have seen.