Do combinatory logic bases need a function of 3 variables?

Question

All the known bases of combinatory logic, such as $\{S,K\}$, or $\{K,W,B,C\}$, have one or more combinators using 3 variables: \begin{align*} S ={} & \lambda x\lambda y\lambda z. x z(y z), \\ B ={} & \lambda x\lambda y\lambda z. x (y z), \\ C ={} & \lambda x\lambda y\lambda z. x z y. \end{align*} This raises the question whether we can make a basis with functions of only 2 variables. Surely if such a thing were possible, it would be a most interesting result and it would be well-known. But as far as I can tell, no such thing is known. Thus it seems nobody believes such a thing to be possible.

But has this been proven anywhere?

How do we know that $\{K,W,2,O,T,D\}$ is not a basis, where \begin{align*} K ={} & \lambda x\lambda y. x, \\ W ={} & \lambda x\lambda y. x y y, \\ 2 ={} & \lambda f\lambda x. f(f x), \\ O ={} & \lambda x\lambda y. y(x y), \\ T ={} & \lambda x\lambda y. y x, \\ D ={} & \lambda x. x x? \end{align*}

Answer 1

A Basis Result in Combinatory Logic, Remi Legrand, J. Symb. Logic 53.4 (1988), pp. 1224-1226.

The aim of this article is to show that a basis for combinatory logic must contain at least one combinator with rank strictly greater than two.

Answer 2

@PeterTaylor’s excellent answer points to exactly the result wanted. But the proof there can be streamlined a bit, and may be paywalled for some readers, so I’ll write it out here for accessibility.

Theorem. Let $\newcommand{\B}{\mathbf{B}}\B$ be any set of combinators of rank ≤2. Then there is no $\B$-expression $T$ such that $\newcommand{\reddto}{\twoheadrightarrow}Tabc \reddto cab$.

Proof. Fix such $\B$ throughout. The idea is (unsurprisingly) to find an invariant of $Tabc$ that is sufficiently closed under reduction, and not satisfied by $cab$. Say that an expression is bad if it is of the form $E[F[a,b],c]$, where $E$ and $F$ are each $\B$-expressions of 2 variables. Then we have:

Lemma. Any bad expression is either normal, or else has a reduction chain to another bad expression, including at least one leftmost reduction.

Proof of lemma. If a bad expression $E[F[a,b],c]$ is not stuck, consider its leftmost redex. There are three possible cases:

1. The head combinator of the redex is not in an occurrence of $F$. Then each occurrence of $F$ is either outside the redex, or inside an argument of the head combinator; so the reduct is of the form $E'[F[a,b],c]$.

2. The whole redex is inside an occurrence of $F$. Then by reducing it in every occurrence of $F$, we have $E[F[a,b],c] \reddto E[F'[a,b],c]$, and this includes the leftmost redex.

3. The head combinator $H$ is iside an occurrence of $F$, but not the whole redex. Then $H$ must be of rank ≥1. If $H$ is of rank 1, then $F$ is just $H$, so $x,y$ don’t occur, and the whole expression (both before and after reduction) is of the form $E'[c]$, so is still bad. If the head combinator is of rank 2, then we must have $F[a,b] \equiv HF'[a,b]$, so by re-parsing as $E[F[a,b],c] \equiv E'[F'[a,b],c]$, case 1 applies.

This proves the lemma. It follows that any bad expression either reduces to a bad normal form, or has an infinite quasi-leftmost reduction sequence. So by the quasi-leftmost-reduction theorem (Hindley–Seldin 2008, Thm 3.22), any normal form of a bad expression is bad; and so the bad expression $Tabc$ cannot reduce to the normal, non-bad expression $cab$. □

References:

• Rémi Legrand, A Basis Result in Combinatory Logic, J. Symb. Logic 1988; jstor full text
• J. Roger Hindley, Jonathan P. Seldin, Lambda-Calculus and Combinators, an Introduction, CUP 2008