Combinators

Overview

Assume that there is given an infinite sequence of expressions called variables and a finite or infinite sequence of expressions called atomic constants, different from the variables. Included in the atomic constants are some basic combinators. The set of expressions called $CL$-terms is defined inductively as follows:

• all variables and atomic constants are $CL$-terms;
• if $X$ and $Y$ are $CL$-terms, then so is $(XY)$.

An atom is a variable or atomic constant. A non-redex constant is any atomic constant other than the basic combinators. A non-redex atom is a variable or non-redex constant. A closed term is a term containing no variables. A combinator is a closed term containing no atomic constants other than the basic combinators.

If the sequence of atomic constants is empty (besides the basic combinators), the system is called pure. Otherwise it is called applied.

Basic Combinators

The combinatory logic is a notation that eliminate the need for quantified variables. We start with basis $\mathbf{S}$, $\mathbf{K}$, and $\mathbf{I}$. These basic combinators are defined as:

• $\mathbf{S}$ (the starling); $(\mathbf{S}(f,g))(x)=f(x,g(x))$
• $\mathbf{K}$ (the kestrel); $(\mathbf{K}(a))(x)=a$
• $\mathbf{I}$ (the idiot bird); $\mathbf{I}(f)=f$

Length

The length of a $CL$-term (denoted $lgh$) is equal to the number of atoms in the term:

• $lgh(a)=1$
• $lgh(MN)=lgh(M)+lgh(N)$

Occurrence

For $CL$-terms $P$ and $Q$, the relation $P$ occurs in $Q$ is defined by induction on $Q$ as:

• $P$ occurs in $P$;
• if $P$ occurs in $M$ or in $N$, then $P$ occurs in $(MN)$;

Free Variables

$FV(P)$ denotes all the variables of $P$. Note in $CL$-terms, all occurrences of variables are free because there is no $\lambda$ to bind them.

Substitution

For any $M$, $N$, and $x$, define $[N/x]M$ to be the result of substituting $N$ for every occurrence of $x$ in $M$.