18

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?

Community
  • 1
Petr
  • 2,601
  • 15
  • 28

2 Answers2

21

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.

Neel Krishnaswami
  • 32,528
  • 1
  • 100
  • 165
12

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

cody
  • 13,861
  • 1
  • 49
  • 103