<p>As far as I know, showing that this direction is the <em>hard</em> part of Wells proof! At least this is what Pawel (Urzyczyn) explained to me a few years back.</p>
<p>Apparently it is not too hard to show that type checking is undecidable; the hard part is showing that this implies undecidability of type reconstruction! Indeed there are some cases in which the first is undecidable and the second decidable: see e.g. <a href="https://doi.org/10.1007/BFb0037103" rel="nofollow noreferrer">Dowek 1993.</a></p>
<hr />
<p>Added 5/9/23:</p>
<p>The example I hint at in the Dowek paper is very simple, so it might be worth outlining it here:</p>
<p>In a calculus with dependent types but no polymorphism (essentially MLTT without inductives or universes), typability of un-annotated terms is somewhat trivial: since the &quot;dependent&quot; part of dependent types can be erased, it suffices to check that the term can be given a simple type!</p>
<p>In contrast, type checking is undecidable, because the dependent types can introduce complex constraints on the inputs of functions.</p>

CC BY-SA 4.0
2012-11-19T17:40:26.697Z
2023-05-09T17:28:13.953Z
2023-05-09T17:28:13.953Z
cody
<p>Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a proof due to Malecki 1989 that type checking implies typability. This is because </p>

<blockquote>
  <p>exists $\sigma$ such that $M:\sigma$</p>
</blockquote>

<p>is equivalent to</p>

<blockquote>
  <p>$(\lambda xy.y)M : (\alpha\rightarrow\alpha)$</p>
</blockquote>

<p>(This is because if a term is typable in System F then all its subterms are.)</p>

<p>Is there a simple proof the other way around? That is, <strong>a proof that typability implies type checking in System F?</strong></p>

<lo.logic><computability><type-theory><lambda-calculus><type-inference>
A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?
Petr
# A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

(Asked by: username_0 on 2012-11-18)

Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a proof due to Malecki 1989 that type checking implies typability. This is because

> exists $\sigma$ such that $M:\sigma$

is equivalent to

> $(\lambda xy.y)M : (\alpha\rightarrow\alpha)$

(This is because if a term is typable in System F then all its subterms are.)

Is there a simple proof the other way around? That is, **a proof that typability implies type checking in System F?**

**Tags:** lo.logic, computability, type-theory, lambda-calculus, type-inference


---

## 1 answers

### Answer by username_1 on 2012-11-19. Score: 6 | Accepted answer

As far as I know, showing that this direction is the *hard* part of Wells proof! At least this is what Pawel (Urzyczyn) explained to me a few years back.

Apparently it is not too hard to show that type checking is undecidable; the hard part is showing that this implies undecidability of type reconstruction! Indeed there are some cases in which the first is undecidable and the second decidable: see e.g. [Dowek 1993.](https://doi.org/10.1007/BFb0037103)

---

Added 5/9/23:

The example I hint at in the Dowek paper is very simple, so it might be worth outlining it here:

In a calculus with dependent types but no polymorphism (essentially MLTT without inductives or universes), typability of un-annotated terms is somewhat trivial: since the "dependent" part of dependent types can be erased, it suffices to check that the term can be given a simple type!

In contrast, type checking is undecidable, because the dependent types can introduce complex constraints on the inputs of functions.


---

