Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
up vote 4 down vote accepted

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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