Editing Combinatory logic (section)

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