Bounded quantification is undecidable

ABSTRACT

F≤ is a typed &lgr;-calculus with subtyping and bounded second-order polymorphism. First proposed by Cardelli and Wegner, it has been widely studied as a core calculus for type systems with subtyping. Curien and Ghelli proved the partial correctness of a recursive procedure for computing minimal types of F≤ terms and showed that the termination of this procedure is equivalent to the termination of this procedure is equivalent to the termination of its major component, a procedure for checking the subtype relation between F≤ types. This procedure was thought to terminate on all inputs, but the discovery of a subtle bug in a purported proof of this claim recently reopened the question of the decidability of subtyping, and hence of typechecking. This question is settled here in the negative, using a reduction from the halting problem for two-counter Turing machines to show that the subtype relation of F≤ is undecidable.

REFERENCES

• 1: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
• 2: Kim B. Bruce, The Equivalence of Two Semantic Definitions for Inheritance in Object-Oriented Languages, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.102-124, March 25-28, 1991
• 3: Kim Bruce and Giuseppe Longo. A modest model of records, inheritance, and bounded quantification. In Proceedings of the IEEE Symposium on Logic in Computer Science, pages 38-50, 1988.
• 4: P. S. Canning , W. R. Cook , W. L. Hill , W. G. Olthoff, Interfaces for strongly-typed object-oriented programming, Conference proceedings on Object-oriented programming systems, languages and applications, p.457-467, October 02-06, 1989, New Orleans, Louisiana, United States
• 5: Peter Canning , William Cook , Walter Hill , Walter Olthoff , John C. Mitchell, F-bounded polymorphism for object-oriented programming, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.273-280, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99392]
• 6: Peter Canning, Walt Hill, and Walter Olthoff. A kernel language for object-oriented programruing. Technical Report STL-88-21, Hewlett- Packard Labs, 1988.
• 7: Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
• 8: Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
• 9: L. Cardelli, Structural subtyping and the notion of power type, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-79, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73566]
• 10: Luca Cardelli. Typeful programming. Research Report 45, Digital Equipment Corporation, Systems Research Center, Palo Alto, California, February 1989.
• 11: Luca Cardelli, 1991. Personal Communication.
• 12: Luca Cardelli. Extensible records in a pure calculus of subtyping. To appear, 1991.
• 13: Luca Cardelli , Giuseppe Longo, A semantic basis for quest, Proceedings of the 1990 ACM conference on LISP and functional programming, p.30-43, June 27-29, 1990, Nice, France [doi>10.1145/91556.91586]
• 14: Luca Cardelli , Simone Martini , John C. Mitchell , Andre Scedrov, An Extension of System F with Subtyping, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.750-770, September 24-27, 1991
• 15: Luca Cardelli , John C. Mitchell, Operations on records, Proceedings of the fifth international conference on Mathematical foundations of programming semantics, p.22-52, July 1990, New Orleans, Louisiana, United States
• 16: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 17: Felice Cardone, Relational Semantics for Recursive Types and Bounded Quantification, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.164-178, July 11-15, 1989
• 18: William R. Cook , Walter Hill , Peter S. Canning, Inheritance is not subtyping, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.125-135, December 1989, San Francisco, California, United States [doi>10.1145/96709.96721]
• 19: M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and lambda calculus semantics. In To H. B. Curry" Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 535-560, New York, 1980. Academic Press.
• 20: Pierre-Louis Curien and Giorgio Ghetli. Coherence of subsumption. Mathematical Structures in Computer Science, 1991. To appear.
• 21: Pierre-Louis Curien , Giorgio Ghelli, Subtyping + Extensionality: Confluence of beta-eta-top reduction in F<=, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.731-749, September 24-27, 1991
• 22: Nicolas G. de Bruijn. Lambda-calculus notation with nameless dummies" a tool for automatic formula manipulation with application to the Church- Rosser theorem. Indag. Math., 34(5):381-392, 1972.
• 23: Giorgio Ghelli. Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism. PhD thesis, UniversitS~ di Pisa, March 1990. Technical report TD-6/90, Dipartimento di Informatica, Universit~ di Pisa.
• 24: Giorgio Ghelli, 1991. Personal Communication.
• 25: Jean-Yves Girard. Interpretation fonctionelle et (limination des coupures de l'arithm~lique d'ordre supdrieur. PhD thesis, Universit~ Paris VII, 1972.
• 26: Carl Gunter, 1990. Personal Communication.
• 27: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 28: Proceedings of the international conference on Theoretical aspects of computer software, June 1991
• 29: Simon Martini, Bounded quantifiers have interval models, Proceedings of the 1988 ACM conference on LISP and functional programming, p.164-173, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62699]
• 30: John C. Mitchell, Polymorphic type inference and containment, Information and Computation, v.76 n.2-3, p.211-249, February/March 1988 [doi>10.1016/0890-5401(88)90009-0]
• 31: Benjamin C. Pierce. Bounded quantification is undecidable. Technical Report CMU-CS-91-161, Carnegie Mellon University, July 1991.
• 32: Benjamin Crawford Pierce, Programming with intersection types and bounded polymorphism, Carnegie Mellon University, Pittsburgh, PA, 1992
• 33: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 34: john C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Languages