Editing Combinatory logic (section)

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