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.

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:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• v
• P
• (E1 E2)

where v is a variable, P is one of the primitive functions, and E1 and E2 are combinatory terms. The primitive functions themselves are combinators, or functions that contain no free variables.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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 same convention for

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

multiple application as in the lambda-calculus,

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:(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.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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 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 capture the notion of

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

intensional equality of functions: that two functions are 'equal'

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

only if they have identical implementations. 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.

Related Topics:
Fixed point combinator - Recursion

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Completeness of the S-K basis

It is a perhaps astonishing fact that 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,

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

T, which converts an arbitrary lambda term into an equivalent

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

combinator.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

T may be defined as follows:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• T => V
• T => (T T)
• T => (K T) (if x is not free in E)
• T => I
• T => T] (if x is free in E)
• T => (S T T)

Conversion of a lambda term to an equivalent combinatorial term

For example, we will convert the lambda term λx.λy.(y x) to a

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

combinator:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:T

~ ~ ~ ~ ~ ~ ~ ~ ~ ~