Type-Free Combinatory Calculi (c)

Pure Combinatory Logic

Pure combinatory logic is a simple language of combinators. The terms of the language, each of which denotes a function, are formed from variables and constants by a single construction, function application. In the pure system there is a small set of constants all of which are themselves pure combinators, usually the primitive combinators are named S, K and I, though I is in fact definable in terms of S and K.

The intended meaning of these constants can be described simply by showing a corresponding transformation or reduction which the constant may be thought of as effecting.

The transformations are as follows:

I x	=	x
K x y	=	x
S f g x	=	(f x)(g x)

This set of combinators has the property of combinatory completeness which means that for any function definition of the form: f x = combinatory expression involving x

There exists an expression E in S,K and I such that:

f = E

This property establishes the close relationship between Pure Combinatory Logic and the Pure lambda Calculus, in which a special notation for functional abstraction is available. It shows that the notation for functional abstraction, though a great convenience, adds no expressiveness to the language.

As well as having combinatorial completeness, Pure Combinatory Logic is able to express all effectively computable functions over natural numbers appropriately represented as combinators.

Pure Combinatory Logic can be extended by moving along any of The Axes of The Cube.

created 1995/12/9 modified 1999/9/19