18
$\begingroup$

I know that's impossible to decide $\beta$-equivalence for untyped lambda calculus. Quoting Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984).:

If A and B are disjoint, nonempty sets of lambda terms which are closed under equality, then A and B are recursively inseparable. It follows that if A is a nontrivial set of lambda terms closed under equality, then A is not recursive. So, we cannot decide the problem "M=x?" for any particular M. Also, it follows that Lambda has no recursive models.

If we have a normalizing system, such as System F, then we can decide $\beta$-equivalence "from outside" by reducing the two given terms and comparing if their normal forms are the same or not. However, can we do it "from inside"? Is there a System-F combinator $E$ such that for two combinators $M$ and $N$ we have $E M N = \mbox{true}$ if $M$ and $N$ have the same normal form, and $E M N = \mbox{false}$ otherwise? Or can this be done at least for some $M$s? To construct a combinator $E_M$ such that $E_M N$ is true iff $N\equiv_\beta M$? If not, why?

$\endgroup$
19
$\begingroup$

No, it's not possible. Consider the following two inhabitants of the type $(A \to B) \to (A \to B)$.

$$ \begin{array}{l} M = \lambda f.\;f \\ N = \lambda f.\;\lambda a.\; f\;a \end{array} $$

These are distinct $\beta$-normal forms, but cannot be distinguished by a lambda-term, since $N$ is an $\eta$-expansion of $M$, and $\eta$-expansion preserves observational equivalence in a pure typed lambda calculus.

Cody asked what happens if we mod out by $\eta$-equivalence, also. The answer is still negative, because of parametricity. Consider the following two terms at the type $(\forall \alpha.\;\alpha \to \alpha) \to (\forall \alpha.\;\alpha \to \alpha)$:

$$ \begin{array}{lcl} M & = & \lambda f:(\forall \alpha.\;\alpha \to \alpha).\;\Lambda \alpha.\lambda x:\alpha.\;f \;[\forall \alpha.\;\alpha \to \alpha]\;(\Lambda \beta.\lambda y:\beta.\;y)\;[\alpha]\;x\\ N & = & \lambda f:(\forall \alpha.\;\alpha \to \alpha).\;\Lambda \alpha.\lambda x:\alpha.\;f\;[\alpha]\;x \end{array} $$

They are distinct $\beta$-normal, $\eta$-long form, but are observationally equivalent. In fact, all functions of this type are equivalent, since $\forall \alpha.\;\alpha \to \alpha$ is the encoding of the unit type, and so all functions of the type $(\forall \alpha.\;\alpha \to \alpha) \to (\forall \alpha.\;\alpha \to \alpha)$ must be extensionally equivalent.

$\endgroup$
  • 2
    $\begingroup$ Ok, same question with $\beta,\eta$-equivalence :) $\endgroup$ – cody Nov 1 '12 at 22:13
11
$\begingroup$

Another possible answer to Neel's perfectly correct one: Suppose that there is a combinator $E$, well-typed in system F such that the above condition holds. The type of $E$ is:

$$ E : \forall \alpha.\alpha\rightarrow \alpha\rightarrow {\bf bool}$$

It turns out that there is a theorem for free that expresses that such a term is necessarily constant:

$$ \forall T,\ t,u,t',u':T,\ E\ T\ t\ u = E\ T\ t'\ u'$$

In particular, $E$ is the constantly true function or the constantly false function, and can not possibly be an "equality decider".

$\endgroup$

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.