Deciding ML typability is complete for deterministic exponential time

ABSTRACT

A well known but incorrect piece of functional programming folklore is that ML expressions can be efficiently typed in polynomial time. In probing the truth of that folklore, various researchers, including Wand, Buneman, Kanellakis, and Mitchell, constructed simple counterexamples consisting of typable ML programs having length n, with principal types having &OHgr;(2cn) distinct type variables and length &OHgr;(22cn). When the types associated with these ML constructions were represented as directed acyclic graphs, their sizes grew as &OHgr;(2cn). The folklore was even more strongly contradicted by the recent result of Kanellakis and Mitchell that simply deciding whether or not an ML expression is typable is PSPACE-hard. We improve the latter result, showing that deciding ML typability is DEXPTIME-hard. As Kanellakis and Mitchell have shown containment in DEXPTIME, the problem is DEXPTIME-complete. The proof of DEXPTIME-hardness is carried out via a generic reduction: it consists of a very straightforward simulation of any deterministic one-tape Turing machine M with input &khgr; running in &Ogr;(c|&khgr;|) time by a polynomial-sized ML formula &PHgr;M,&khgr;, such that M accepts &khgr; iff &PHgr;M,&khgr; is typable. The simulation of the transition function &dgr; of the Turing Machine is realized uniquely through terms in the lambda calculus without the use of the polymorphic let construct. We use let for two purposes only: to generate an exponential amount of blank tape for the Turing Machine simulation to begin, and to compose an exponential number of applications of the ML formula simulating state transition. It is purely the expressive power of ML polymorphism to succinctly express function composition which results in a proof of DEXPTIME-hardness. We conjecture that lower bounds on deciding typability for extensions to the typed lambda calculus can be regarded precisely in terms of this expressive capacity for succinct function composition. To further understand this lower bound, we relate it to the problem of proving equality of type variables in a system of type equations generated from an ML expression with let-polymorphism. We show that given an oracle for solving this problem, deciding typability would be in PSPACE, as would be the actual computation of the principal type of the expression, were it indeed typable.

REFERENCES

• AS85: Harold Abelson , Gerald J. Sussman, Structure and Interpretation of Computer Programs, MIT Press, Cambridge, MA, 1996
• AHU74: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• DKM84: Cynthia Dwork , Paris C. Kanellakis , John C. Mitchell, On the sequential nature of unification, Journal of Logic Programming, v.1 n.1, p.35-50, June 1984 [doi>10.1016/0743-1066(84)90022-0]
• GLT89: Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
• HMM86: Robert Harper, David MacQueen, and Robin Milner, Standard ML. Research Report ECS- LFCS-86-2, Computer Science Department, University of Edinburgh, March 1986.
• HU79: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• Hu73: Harry B. Hunt, The equivalence problem for regular expressions with intersection is not polynomial in tape. TR 73-156, Computer Science Department, Cornell University, 1973.
• Ka: Paris Kanellakis, personal communication.
• KM89: P. C. Kanellakis , J. C. Mitchell, Polymorphic unification and ML typing, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-115, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75286]
• Kf: Dennis Kfoury, personal communication.
• KTU89a: Dennis Kfoury, Jerzy Tiuryn, and Pavel Urzyczyn, An anMysis of ML typability. Preprint.
• KTU89b: Dennis Kfoury, Jerzy Tiuryn, and Pavel Urzyczyn, Undecidability of the semi-unification problem. Preprint.
• Mi78: Robin Milner, A theory of type polymorphism in programming, JCSS 17 (1978), pp. 348- 375.
• Sa70: Walter Savitch, Relationship between nondeterministic and deterministic tape complexities, JCSS 4:2 (1970), pp. 177-192.
• Pf88: Frank Pfenning, Partial polymorphic type inference and higher-order unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.153-163, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62697]
• W87: Mitch Wand, A simple algorithm and proof for type inference. Fundamenta Informaticae 10 (1987).

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Bounded-action devices (e.g., Turing machines, random access machines)
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs; Type structure

General Terms:
Algorithms, Languages, Performance, Theory, Verification