Selection terms in the untyped lambda calculus

Question

In the untyped $\lambda$-calculus, are there terms $S$ and $T$ such that for any $n$ and any terms $t_1, \dotsc, t_n$, $$S(T(t_1)\dots(t_n)) \twoheadrightarrow_{\beta} t_1$$ Of course, if $n$ is fixed or known in advance, then such terms $S$ and $T$ can easily be constructed. The question is whether there are terms $S$ and $T$ that work for all $n$.

Answer 1

No such terms can exist. Here's a proof, way too convoluted for my tastes, but I don't have time to find a better one.

The proof uses a lot the so-called Genericity Lemma, a standard result the proof of which may be found, for example, in Barendregt's monograph. Here is a statement. Say that a term $F$ is constant if there exists a term $c$ such that $FX\to^\ast c$ for every term $X$.

Genericity Lemma. Let $\Omega$ be an unsolvable term. If $F\Omega\to^\ast N$ with $N$ normal, then $FX\to^\ast N$ for every term $X$. In particular, $F$ is constant.

On to the proof. Suppose there are terms $S$ and $T$ as required. It is obvious from the property defining it that $S$ is not constant. We also observe that $T$ is solvable: if it were unsolvable, then so would be $TN$ for any normal term $N$, but $S(TN)\to^\ast N$, so the Genericity Lemma tells us that $S$ is constant, contradiction.

Since $T$ is solvable, it has a head normal form:

$$T\to^\ast \lambda x_1\ldots x_m.yM_1\ldots M_k,$$

for some natural numbers $m,k$ and some terms $M_1,\ldots,M_k$. I claim that $y$ must be among one of the $x_i$. Suppose that it is not, that is, that $y$ is free in $T$. Let $K_k$ be a term which is constant on $k$ arguments, that is, there exists a term $c$ such that, for any $t_1,\ldots,t_k$,

$$K_kt_1\ldots t_k\to^\ast c.$$

Such a $K_k$ obviously exists. Let $S':=S[K_k/y]$, let $t_1,\ldots,t_m$ be arbitrary terms in which $y$ does not appear free and let, for all $1\leq i\leq k$, $M_i':=M_i[K_k/y][t_1/x_1]\cdots[t_m/x_m]$. We have

$$(\lambda y.S(Tt_1\ldots t_m))K_k \to S'(T[K_k/y]t_1\ldots t_m)\to^\ast S'(K_kM_1'\ldots M_k') \to^\ast S'c.$$

On the other hand, by the defining property of $S$ and $T$, we must also have

$$(\lambda y.S(Tt_1\ldots t_m))K_k \to^\ast (\lambda y.t_1)K_k \to t_1.$$

Now, apart from the fact that it does not contain $y$, $t_1$ is completely arbitrary, in particular we may choose it to be not $\beta$-equivalent to $S'c$, contradicting confluence.

So we actually have

$$T\to^\ast \lambda x_1\ldots x_m.x_iM_1\ldots M_k$$

for some $1\leq i\leq m$ and, in particular, $m>0$. The proof now splits in two cases: either $i=1$, or $i>1$. In both cases, we will derive a final contradiction, showing that $S$ and $T$ cannot exist.

Let us start with $i>1$. Let $t_1,\ldots,t_m$ be arbitrary, except that $t_1$ is normal and $t_i:=\Omega$ (an unsolvable term), and let $M_i'$ be defined as above. We have

$$S(Tt_1\ldots t_m)\to^\ast S(\Omega M_1'\ldots M_k').$$

However, we must also have

$$S(Tt_1\ldots t_m)\to^\ast t_1$$

and, since $t_1$ is normal, by confluence we obtain

$$S(\Omega M_1'\ldots M_k') \to^\ast t_1.$$

But $\Omega M_1'\ldots M_k'$ is unsolvable, and $t_1$ is normal, so by the Genericity Lemma $S$ is constant, contradiction.

Let now $i=1$. Take $t_2,\ldots,t_m$ arbitrary, let

$$t_1:=\lambda y_1\ldots y_ky_{k+1}.y_{k+1}$$

and $\Omega$ be unsolvable. We have

$$S(Tt_1\ldots t_m\Omega)\to^\ast S(t_1M_1'\ldots M_k'\Omega) \to S\Omega,$$

and again by the property of $S$ and $T$, confluence and the fact that $t_1$ is normal, we also have $S\Omega\to^\ast t_1$, which, again, by the Genericity Lemma, implies that $S$ is constant, contradiction.