J. B. Wells

Typability and type checking in System F are equivalent and undecidable

Ann. Pure Appl. Logic, 98(1-3):111-156, 1999

Girard and Reynolds independently invented System F (a.k.a. the second-order polymorphically typed lambda calculus) to handle problems in logic and computer programming language design, respectively. Viewing F in the Curry style, which associates types with untyped lambda terms, raises the questions of typability and type checking. Typability asks for a term whether there exists some type it can be given. Type checking asks, for a particular term and type, whether the term can be given that type. The decidability of these problems has been settled for restrictions and extensions of F and related systems and complexity lower-bounds have been determined for typability in F, but this report is the first to resolve whether these problems are decidable for System F.

This report proves that type checking in F is undecidable, by a reduction from semi-unification, and that typability in F is undecidable, by a reduction from type checking. Because there is an easy reduction from typability to type checking, the two problems are equivalent. The reduction from type checking to typability uses a novel method of constructing lambda terms that simulate arbitrarily chosen type environments. All of the results also hold for the lambda I-calculus.

[ bib | .ps.gz | .html ]


This file has been generated by bibtex2html 1.61

Copyright notice: The documents contained in these pages are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

If you experience problems downloading any of the files above, it is most likely because your browser does not handle compressed files correctly.

In particular, Netscape might save the file in the compressed gz-format with extension .ps or .pdf (indicating postscript or PDF, resp.). You can work around this by saving the file, renaming it to .ps.gz or .pdf.gz, and then uncrompress it.

This page is maintained by Peter Møller Neergaard. Autogenerated on Monday August 20 2007.