A combinator expression (let's say in the SK basis) can be thought of as a function that maps combinator calculus expressions to combinator calculus expressions. That is, one can think of an expression $X$ as a function $X:L \to L,ドル where $L$ is the set of all syntactically valid combinator expressions in the SK basis. This mapping is performed by applying the input to the expression, and then reducing to normal form to get the output.
Since the SK basis is Turing complete, one might naïvely think that there exists a an SK expression $X$ that implements any computable function from $L$ to $L$. However, this clearly isn't the case, since the result of reduction will always be in normal form. This means there is no way for an expression to have an output that isn't in normal form.
So instead, I could think of SK calculus expressions as mapping $L'$ to $L',ドル where $L'$ is the set of SK expressions in normal form. Is it the case that, for any computable map $f:L'\to L',ドル there is an SK expression $X$ that implements this map? Or are there further restrictions on the set of functions that can be computed by combinator calculus expressions in this way?
1 Answer 1
To get the ball rolling, and in hopes of other people giving deeper and more detailed answers on the structure of the $\lambda$-definable functions $L'\to L',ドル let me cite Corollary 20.3.3 from Barendregts' The Lambda Calculus, Its Syntax and Semantics (aka "the bible").
Corollary 20.3.3: The function $\delta:L'^2\to L',ドル defined by $$ \delta(M, N) = \cases{\mathrm{True}\mbox{ if }M=_{\beta\eta}N\\ \mathrm{False}\mbox{ otherwise}}$$ is not definable in the untyped $\lambda$-calculus, i.e. there is no term $D$ such that $$D\ M\ N =_{\beta\eta} \delta(M,N)$$ for all $M,N\in L'$.
The proof involves considerations on Böhm trees which give a rather strong characterization of the possible "actions" of arbitrary lambda terms on normal forms. In particular, for any non-constant closed term $F,ドル on can find $n\in\mathbb{N}$ and $P_1,\ldots,P_n$ such that $$ F\ x\ P_1\ldots P_n =_{\beta\eta} x\ Q_1\ldots Q_k$$
For some $k,ドル $Q_1,\ldots,Q_k$. This drastically constrains the possible forms of a hypothetical $D$ that implements $\delta,ドル showing with a little work that such a $D$ cannot exist.