Combinatory logic

:This article is about a topic in mathematical logic and theoretical computer science, and is not to be confused with combinatorial logic, a topic in electronics.

((S λx.E1 λx.E2) a)

By extensional equality,

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

λx.(E1 E2) = (S λx.E1 λx.E2)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Therefore, to find a combinator equivalent to λx.(E1 E2), it is

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

sufficient to find a combinator equivalent to (S λx.E1 λx.E2), and

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

(S T T)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

evidently fits the bill. E1 and E2 each contain strictly fewer

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

applications than (E1 E2), 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 transformation can be made

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

smaller if we take into account the η-reduction rule:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

T = T (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:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

T

~ ~ ~ ~ ~ ~ ~ ~ ~ ~