10
$\begingroup$

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?

$\endgroup$

1 Answer 1

6
$\begingroup$

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.


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.

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.