Are there lambda-calculus functions which always output booleans, but are not constant functions?

Question

In labmda calculus, true = $\lambda x,y.x$ and false = $\lambda x,y.y$.

Is there a term $f$ such that for any other term $x$, $f x$ normalizes to true or false BUT $f$ does not have the same output for all inputs?

Answer 1

That is not possible. By the "genericity lemma" (Barendregt book, lemma 14.3.24), if $C[M] = N$ with $M$ unsolvable, and $N$ normal form, then $C[L] = N$ for any term $L$.

So, if $x$ is an unsolvable term (like $\Omega=(\lambda w.ww)(\lambda w.ww)$) and $f x = {\sf true}$ (normal form), then $f y = {\sf true}$ for any term $y$. The same holds for $\sf false$ or any other normal form.

The intuition here is that an unsolvable subterm will make the whole term diverge as soon as it is needed for the computation, much like while (true) {} hangs the program in imperative programming as soon as the loop is executed.

Answer 2

Yes, there is. Take, for example, the combinator

$iszero := \lambda xyz. z((\lambda xy.x)y)x$

which has the following behavior:

$iszero\ P\ Q\ 0 =_\beta P\\ iszero\ P\ Q\ k+1 =_\beta Q$

i.e. the operator expresses "If $n=0$ then $P$ else $Q$".

This definition presupposes an encoding of natural numbers as Church numerals: For any n, $n = \lambda xy.x^ny$, where $M^0N$ = $N$ and $M^{n+1}N = M(M^nN)$, i.e. $n$-fold application of $M$: $M(M(M(...N)))$.
So $0 = \lambda xy.y; 1 = \lambda xy.xy; 2 = \lambda xy.x(xy); 3 = \lambda xy.x(x(xy)); ...$.

Now construct the following $\lambda$ term:

$iszero (true) (false)\\ = (\lambda xyz.(z((\lambda xy.x)y))x)(true)(false)\\ =_\beta (\lambda z. (z((\lambda xy.x)false))true)\\ =_\beta (\lambda z. (z(\lambda y.false))true)$

This operator will always return a boolean value ($true$ or $false$), but different values depending on the input.

Input $k = 0$:
$ (\lambda z. (z(\lambda y.false))true)(0)\\ =_\beta (0(\lambda y.false))true\\ = ((\lambda xy.y)(\lambda y.false))true\\ =_\beta (\lambda y.y)(true)\\ =_\beta true$

Input $k > 0$, e.g. $k=1$:
$ (\lambda z. (z(\lambda y.false))true)(1)\\ =_\beta (1(\lambda y.false))true\\ = ((\lambda xy.xy)(\lambda y.false))true\\ =_\beta (\lambda y.(\lambda y.false)y)true\\ =_\beta (\lambda y.false)true\\ =_\beta false$

So the term $iszero (true) (false)$ will always return one out of $true$ or $false$, but the former output only for inputs $=0$ and the latter for inputs $k>0$.