5
$\begingroup$

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?

$\endgroup$
10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I guess technically the way that I phrased the question, no $f$ exists so $f x$ always normalizes because if $M$ is unsolvable, then (assuming call-by-value) $f M$ is unsolvable. $\endgroup$ – while1fork Mar 11 at 14:24
  • $\begingroup$ @while1fork In CBV that's trivial, but note that the genericity lemma does not assume any evaluation strategy. It also holds in CBN, for instance. $\endgroup$ – chi Mar 11 at 15:31
0
$\begingroup$

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$.

$\endgroup$
  • 2
    $\begingroup$ This term only evaluates to a boolean if the input is a church numeral. In my question, I specified that it must evaluate to a boolean for ANY term. For example, if you plug in $\lambda a b . (\lambda x . x)$ into your term, then it evaluates to $\lambda x.x$ which is not a boolean value. $\endgroup$ – while1fork Mar 11 at 14:03
  • $\begingroup$ In this case I misunderstood you. I hardly think it is possible to construct a term that makes a systematic distinction between inputs (outputs true for some and false for others) but doesn't come along with any restriction on the type of the input. Usually, functions that are not completely trivial and actually do a computation on the input are defined over a particular type of arguments. So if you really want a combinator that works on any term but does more than something trivial like a constant function, I suppose the answer is no. $\endgroup$ – lemontree Mar 11 at 14:11
  • $\begingroup$ Exactly. The point is that I don't know how to prove that its not possible, so I am asking the question here. $\endgroup$ – while1fork Mar 11 at 14:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.