×

zbMATH — the first resource for mathematics

Typability and type checking in System F are equivalent and undecidable. (English) Zbl 0932.03017
Summary: 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.

MSC:
03B40 Combinatory logic and lambda calculus
03B25 Decidability of theories and sets of sentences
Software:
Automath; Haskell; Miranda; ML
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barendregt, H.P., The lambda calculus: its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[2] Barendregt, H.P., Lambda calculi with types, (), 117-309, chapter 2
[3] Boehm, H.-J., Partial polymorphic type inference is undecidable, (), 339-345
[4] Also DEC SRC Research Report 45.
[5] Giannini, P.; Honsell, F.; Rocca, S.Ronchi Della, A strongly normalizable term having no type in the system F (second order λ-calculus), ()
[6] Giannini, P.; Honsell, F.; Rocca, S.Ronchi Della, Type inference: some results, some problems, Fund. inform., 19, 1/2, 87-125, (1993) · Zbl 0797.68026
[7] Girard, J.-Y., Interprétation fonctionnelle et elimination des coupures de l’arithmétique d’ordre supérieur, ()
[8] Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and types, ()
[9] Goldfarb, W.D., Undecidability of the second-order unification problem, Theoret. comput. sci., 13, 225-230, (1981) · Zbl 0457.03006
[10] Giannini, P.; Rocca, S.Ronchi Della, Characterization of typings in polymorphic type discipline, (), 61-70
[11] Giannini, P.; Rocca, S.Ronchi Della, Type inference in polymorphic type discipline, (), 18-37
[12] Henglein, F.; Mairson, H.G., The complexity of type inference for higher-order typed lambda calculi, (), 119-130, An expanded version appeared as [13]
[13] Henglein, F.; Mairson, H.G., The complexity of type inference for higher-order typed lambda calculi, J. funct. prog., 4, 4, 435-477, (1994), First appeared as [12] · Zbl 0827.03005
[14] Hindley, R., The principal type scheme of an object in combinatory logic, Trans. AMS, (1969) · Zbl 0196.01501
[15] Hooper, P.K., The undecidability of the Turing machine immortality problem, J. symbolic logic, 31, 2, 219-234, (1966) · Zbl 0173.01201
[16] Hudak, P.; Wadler, P.L., Report on the functional programming language Haskell, ()
[17] Jim, T., Type inference in system F plus subtyping, (Dec. 1995), Manuscript
[18] Kfoury, A.J.; Tiuryn, J., Type reconstruction in finite-rank fragments of the second-order λ-calculus, Inform. and comput., 98, 2, 228-257, (1992) · Zbl 0753.68022
[19] Kfoury, A.J.; Tiuryn, J.; Urzyczyn, P., The undecidability of the semi-unification problem, Inform and comput., 102, 1, 83-101, (1993) · Zbl 0769.68059
[20] Kfoury, A.J.; Wells, J.B., A direct algorithm for type inference in the rank-2 fragment of the second-order λ-calculus, () · Zbl 1070.68021
[21] Leivant, D., Polymorphic type inference, (), 88-98
[22] Leivant, D., Finitely stratified polymorphism, Inform and comput., 93, 1, 93-113, (1991) · Zbl 0799.68041
[23] MacQueen, D.; Sethi, R., A semantic model of types for applicative languages, (), 243-252
[24] McCracken, N., The typechecking of programs with implicit type structure, (), 301-315
[25] Milner, R.; Tofte, M.; Harper, R., The definition of standard ML, (1990), MIT Press Cambridge, MA
[26] Minsky, M., Recursive unsolvability of Post’s problem of ‘tag’ and other topics in the theory of Turing machines, Ann. math., 74, 3, 437-455, (1961) · Zbl 0105.00802
[27] Mitchell, J.C., Polymorphic type inference and containment, Inform and comput., 76, 2/3, 211-249, (1988) · Zbl 0656.68023
[28] Pfenning, F., On the undecidability of partial polymorphic type reconstruction, Fund. inform., 19, 1-2, 185-199, (1993) · Zbl 0789.03017
[29] Pfenning, F.; Lee, P., LEAP: a language with eval and polymorphism, ()
[30] Prawitz, D., Natural deduction; A proof-theoretical study, (), No. 3 · Zbl 0173.00205
[31] ()
[32] Pudlák, P., On a unification problem related to Kreisel’s conjecture, Commentationes mathematicae universitatis carolinae, 29, 3, 551-556, (1988), Prague, Czechoslovakia · Zbl 0664.03037
[33] Reynolds, J.C., Towards a theory of type structure, (), 408-425
[34] Schubert, A., Second-order unification and type inference for church-style polymorphism, ()
[35] Tiuryn, J.; Urzyczyn, P., The subtyping problem for second-order types is undecidable, () · Zbl 1049.68039
[36] Tiuryn, J.; Urzyczyn, P., The subtyping problem for second-order types is undecidable, (), Shorter Proceedings version of [35] · Zbl 1049.68039
[37] Turner, D.A., Miranda: a non-strict functional language with polymorphic types, () · Zbl 0592.68014
[38] Urzyczyn, P., The emptiness problem for intersection types, () · Zbl 0937.03022
[39] Urzyczyn, P., Type reconstruction in Fω is undecidable, (), 418-432 · Zbl 0791.68059
[40] Urzyczyn, P., The emptiness problem for intersection types, (), 300-309
[41] Urzyczyn, P., Type reconstruction in Fω, Math. struct. comput. sci., 7, 4, 329-358, (1997) · Zbl 0883.03044
[42] Wells, J.B., Typability and type checking in the second-order λ-calculus are equivalent and undecidable, () · Zbl 0932.03017
[43] Wells, J.B., The undecidability of Mitchell’s subtyping relation, ()
[44] Wells, J.B., Typability is undecidable for F + eta, () · Zbl 0932.03017
[45] Wells, J.B., Type inference for system F with and without the eta rule, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.