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

<p>$$ E : \forall \alpha.\alpha\rightarrow \alpha\rightarrow {\bf bool}$$</p>

<p>It turns out that there is a <a href="http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875" rel="noreferrer">theorem for free</a> that expresses that such a term is necessarily <strong>constant</strong>:</p>

<p>$$ \forall T,\ t,u,t',u':T,\ E\ T\ t\ u = E\ T\ t'\ u'$$</p>

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

CC BY-SA 3.0
2012-11-02T14:59:14.790Z
2012-11-05T19:25:04.033Z
2012-11-05T19:25:04.033Z
cody
<p>No, it's not possible. Consider the following two inhabitants of the type $(A \to B) \to (A \to B)$. </p>

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

<p>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. </p>

<p>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)$:</p>

<p>$$
\begin{array}{lcl}
M &amp; = &amp; \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 &amp; = &amp; \lambda f:(\forall \alpha.\;\alpha \to \alpha).\;\Lambda \alpha.\lambda x:\alpha.\;f\;[\alpha]\;x
\end{array}
$$</p>

<p>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. </p>

CC BY-SA 3.0
2012-11-01T22:13:03.180Z
Ok, same question with $\beta,\eta$-equivalence :)
cody
CC BY-SA 3.0
2012-11-01T07:09:05.970Z
2012-11-02T07:40:13.423Z
2012-11-02T07:40:13.423Z
Neel Krishnaswami
<p>I know that's impossible to decide $\beta$-equivalence for untyped lambda calculus. Quoting <a href="http://mathgate.info/cebrown/notes/barendregt.php">Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984).</a>:</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>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"? <strong>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?</strong> 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?</p>

<lo.logic><computability><lambda-calculus><normalization><decidability>
Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)?
Petr
# Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)?

(Asked by: username_0 on 2012-10-31)

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).](http://mathgate.info/cebrown/notes/barendregt.php):

> 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?

**Tags:** lo.logic, computability, lambda-calculus, normalization, decidability

---

## 2 answers

### Answer by username_2 on 2012-11-01. Score: 21 | Accepted answer

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.

> **Comments:**
> **username_1**: Ok, same question with $\beta,\eta$-equivalence :)  

---

### Answer by username_1 on 2012-11-02. Score: 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](http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875) 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".


---

