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.

:T] (by 5)

: = T T)] (by 6)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: = T)] (by 4)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: = T (by 3)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: = (S T T) (by 6)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: = (S (K (S I)) T) (by 3)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: = (S (K (S I)) (S T T)) (by 6)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: = (S (K (S I)) (S (K K) T)) (by 3)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: = (S (K (S I)) (S (K K) I)) (by 4)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

If we apply this combinator to any two terms x and y, 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 construction may expand a lambda

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

term of length n to a combinatorial term of length

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Θ(3n).

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Explanation of the T transformation

The T 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 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's 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.(E1 E2) is a function which takes an argument, say a, and

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

substitutes it into the lambda term (E1 E2) in place of x,

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

yielding (E1 E2). But substituting a into (E1 E2) in place

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

of x is just the same as substituting it into both E1 and E2, so

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

(E1 E2) = (E1 E2)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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

~ ~ ~ ~ ~ ~ ~ ~ ~ ~