# Incomplete basis of combinators

This is inspired by this question. Let $\mathcal{C}$ be the collection of all combinators which only have two bound variables. Is $\mathcal{C}$ combinatorially complete?

I believe the answer is negative, however I was not able to find a reference for this. I would also be interested in references for proofs of combinatorial incompleteness of sets of combinators (I can see why the set $\mathcal{D}$ consisting of combinators with only one bound variable is incomplete, so these sets ought to contain more than just elements of $\mathcal{D}$).

• Could you clarify what you mean by the number of bound variables of a combinator (= closed lambda term)? Total number of lambda abstractions? – Noam Zeilberger Jul 27 '16 at 19:02
• Yes, this is what I meant. – tci Jul 27 '16 at 19:08
• Actually, maybe that's not exactly what you meant...perhaps rather you mean the total number of distinct variables used in lambda abstractions, so that for example $(\lambda x.x(\lambda y.y))(\lambda x.\lambda y.x y)$ has two distinct bound variables, despite having four lambda abstractions? In that case, it appears that Rick Statman answered exactly this question (negatively), in "Two variables are not enough". – Noam Zeilberger Jul 27 '16 at 21:23
• Right. I think this is the answer I was looking for, and I definitely expected it to be a result of Statman's. I haven't checked yet, but I think this would also give a negative answer to the question that I mentioned. If you would post it as an answer, I would gladly accept it. – tci Aug 1 '16 at 0:15

[Expanding the comment into an answer.]

First, just a clarification about counting bound variables in a combinator (= closed term) $t$. I interpret the question as asking about $$\text{the total number of distinct bound variable names in }t$$ so that for example the term $t = (\lambda x.x(\lambda y.y))(\lambda x.\lambda y.yx)$ counts as having two bound variables, despite having four binders (i.e., lambda abstractions). This way of counting was initially a bit strange to me since it is not invariant under $\alpha$-conversion: for example, $t$ is $\alpha$-equivalent to $t' = (\lambda x.x(\lambda y.y))(\lambda a.\lambda b.ba)$, but $t'$ has four distinct bound variable names. However, this is not really a problem, because the minimum number of distinct bound variable names needed to write a closed term $t$ is equal to $$\text{the maximum number of free variables in a subterm of }t$$ and the latter notion is invariant under $\alpha$-conversion.

So, let $\mathcal{C}$ be the collection of all combinators which can be written using at most two distinct bound variables, or equivalently the collection of all combinators whose subterms have at most two free variables.

Theorem (Statman): $\mathcal{C}$ is not combinatorially complete.

It seems that the original proof of this is contained in a tech report by Rick Statman:

• Combinators Hereditarily of Order Two. Carnegie Mellon Math Department Technical Report 88-33, August 1988. (pdf)

Statman defines an essentially isomorphic collection of combinators which he calls "HOT", for "hereditarily of order two". The tech report actually shows that the word problem (i.e., $\beta$-equality) for HOT is still undecidable, despite the fact that it is not combinatorially complete. Statman later wrote a short self-contained paper with the proof that HOT is not combinatorially complete in:

• Two variables are not enough. Proceedings of the 9th Italian conference on Theoretical Computer Science, pp. 406-409, 2005. (acm)

In any case, as glossed in the abstract of the original tech report, the idea of the proof is to show that HOT is a "hierarchy by definitional level". That is, he defines a notion of rank for a HOT combinator, and a family of combinators $Hn$, such that each $Hn$ has rank $n+1$ and is not $\beta$-equivalent to any combination of HOT combinators of rank $n$. This implies that HOT is not combinatorially complete, because if the $S = \lambda x.\lambda y.\lambda z.(xz)(yz)$ combinator could be derived from a combination of HOT combinators of rank $n$ for some $n$, then so could any other combinator, in particular the combinator $Hn$ of rank $n+1$.