# Do combinatory logic bases need a function of 3 variables?

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*}

• it has 4 nested lambdas, so let's call it 4. Feb 3, 2022 at 21:11
• @LSpice: The definition I’m familiar with, used e.g. in the Legrand paper Peter Taylor’s answer and mine are based on, is that a combinator of rank $n$ is one with a reduction rule $C x_1 \ldots x_n \to E$ where $E$ is formed just from $x_1,\ldots,x_n$ and application. So more complex combinators like the universal $\iota$ don’t fit that form. It would be nice to have a more general definition of rank that extended Legrand’s result to cover $\iota$ and similar, but I’ve not come across such a definition. Feb 4, 2022 at 11:17
• I learned that a very similar result was proved for lambda calculus; see cstheory.stackexchange.com/questions/36276/… Feb 7, 2022 at 17:48
• Thanks to @JohnTromp for linking the related cstheory question from here and vice versa. I did not know about Remi Legrand's paper. Indeed, Rick Statman also has a self-contained paper "Two variables are not enough" (dl.acm.org/citation.cfm?id=2100917) proving a slightly stronger result, that any complete basis of closed lambda terms must contain a term with at least 3 distinct bound variables. The idea of the proof is contained in his earlier 1988 tech report on "Combinators hereditarily of order two" (doi.org/10.1184/R1/6477068.v1). Feb 23, 2022 at 10:05
• Just a comment about generalizing the definition of "rank" of a combinator (@PeterLeFanuLumsdaine). As per the papers by Statman, considering a combinator as a closed lambda term, one can talk about the minimum number of distinct bound variables needed to represent it. And as per my cstheory answer, that can be equivalently (but I find slightly more cleanly) expressed as the maximum number of free variables in any subterm of the combinator. Under either of those equivalent definitions of "rank" (or "hereditary rank"), the $\iota$ combinator has rank 4, as per @JohnTromp's suggestion. Feb 23, 2022 at 10:13

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

@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
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 35, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}