Title: Typability and Type Checking in the Second-Order Lambda-Calculus Are Equivalent and Undecidable
Author: J. B. Wells,Boston University
Date: September 1993
Abstract:
We consider the problems of typability and type checking in the
Girard/Reynolds second-order polymorphic typed lambda calculus, for which
we use the short name ``System F'' and which we use in the ``Curry style''
where types are assigned to pure lambda terms. These problems have been
considered and proven to be decidable or undecidable for various
restrictions and extensions of System F and other related systems, and
lower-bound complexity results for System F have been achieved, but they
have remained ``embarrassing open problems'' for System F itself. We
first prove that type checking in System F is undecidable by a reduction
from semi-unification. We then prove typability in System F is
undecidable by a reduction from type checking. Since the reverse
reduction is already known, this implies the two problems are equivalent.
The second reduction uses a novel method of constructing lambda terms such
that in all type derivations, specific bound variables must always be
assigned a specific type. Using this technique, we can require that
specific subterms must be typable using a specific, fixed type assignment
in order for the entire term to be typable at all. Any desired type
assignment may be simulated. We develop this method, which we call
``constants for free'', for both the lambda-K and lambda-I calculi.