Lambda calculus function with unrestricted domain and nontrivial finite range?

76 Views Asked by At

In the untyped lambda calculus, one of the first encountered expressions is:

$F = Const(I) = \lambda x.\lambda y.y$

It is easily seen that a property of this expression is that the set of possible evaluation "results" - the normal / non-reducible forms belonging to the equivalence classes under beta reduction of $Fz$ for arbitrary $z$ - is finite and consists of a single element $I = \lambda y.y$. In this simple case every equivalence class (just one!) has a normal form, ie. evaluation of every $Fz$ terminates, every $Fz => I$.

Is there an expression $G$ for which the set of possible results of evaluation of the $Gz$, with unrestricted $z$, is finite, non-empty, and contains at least two elements? Can it be proven that this expression does not exist?

1

There are 1 best solutions below

4
On

EDIT: As discussed in the comments following this answer, there is a problem in the proof.

I have been literally reading about lambda calculus for two-three months, so please help me correct any mistakes.

I am targeting at the case where the ultimate result set has 2 terms.

Now let $z_1$ and $z_2$ be two terms such that $Gz_1$ is not equivalent to $Gz_2$. Now take $A$ and $B$ as the beta-closed sets that contain $z_1$ and $z_2$ respectively.

Now using the Scott Curry theorem, $A$ and $B$ should be recursively inseparable. But we can use the $G$ function to separate them, which is a contradiction.

We can extend this to higher sized result sets too, I think.

Is my logic reasonable?