The complexity of parameter passing in polymorphic procedures

ABSTRACT

Our subject is at the confluence of two foundational research areas: formal independence results, and higher order data types. A central problem with polymorphism is the impact of involved polymorphic types on termination of program executions and on the complexity of types occurring therein. It is known thattermination of chains of procedure calls is guaranteed for all polymorphic procedures [5]; however, M. O'Donnell [16] and S. Fortune [4] have independently shown that this statement cannot be proved in usual (Peano's) first-order arithmetic, attesting to the potentially complex effect of polymorphic types. Our main result is that termination of polymorphic argument-passing is a statement that cannot be proved even in full (impredicative) second order arithmetic, a theory whose exceeding strength is briefly illustrated.

REFERENCES

• 1: A. Demers & J. Donahue, Revised report on Russell; Report TR 79-389, Computer Science Department, Cornell University, 1979.
• 2: Richard A. DeMillo , Richard J. Lipton, Some connections between mathematical logic and complexity theory, Proceedings of the eleventh annual ACM symposium on Theory of computing, p.153-159, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804408]
• 3: Richard A. DeMillo , Richard J. Lipton, The consistency of "P = NP" and related problems with fragments of number theory, Proceedings of the twelfth annual ACM symposium on Theory of computing, p.45-57, April 28-30, 1980, Los Angeles, California, United States [doi>10.1145/800141.804652]
• 4: S. Fortune, Topics in Complexity Theory; PhD Dissertation; Cornell University, 1979.
• 5: S. Fortune, D. Leivant & M. O'Donnell, The expressiveness of simple and second order type structures; IBM Research Report # (to appear elsewhere).
• 6: H. Friedman, PhD Dissertation; M.I.T., 1967.
• 7: H. Friedman, Borel Diagonalization and the incompleteness phenomena (preliminary report); The Ohio State university, 1980.
• 8: J.-Y. Girard, These de Doctorat d'Etat; Universite Paris VII, 1972.
• 9: W. A. Howard, The formula as type notion of construction; mimeographed notes, 1969.
• 10: Robert T. Johnson , James B. Morris, Abstract data types in the Model programming language, Proceedings of the 1976 conference on Data : Abstraction, definition and structure, p.36-46, March 22-24, 1976, Salt Lake City, Utah, United States
• 11: J. Hartmanis , J. E. Hopcroft, Independence results in computer science, ACM SIGACT News, v.8 n.4, p.13-24, October-December 1976 [doi>10.1145/1008335.1008336]
• 12: G. Kreisel & A. Levy, Reflection principles and their use in establishing the complexity of axiomatic systems; Zeitschrift fur Math. Logik 14, 1968, 97-124.
• 13: D. Leivant, Unprovability of theorems of complexity theory in weak number theories; to appear in Theoretical Computer Science.
• 14: R.J. Lipton, Model theoretic aspects of complexity theory; Proceedings of the Nineteenth Symposium on the Foundations of Computer Science, (1978) 176-188.
• 15: B. Liskov , R. R. Atkinson , T. Bloom , E. B. Moss , R. Schaffert , A. Snyder, CLU REFERENCE MANUAL, Massachusetts Institute of Technology, Cambridge, MA, 1979
• 16: Michael O'Donnell, A programming language theorem which is independent of Peano Arithmetic, Proceedings of the eleventh annual ACM symposium on Theory of computing, p.176-188, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804411]
• 17: D. Prawitz, Natural Deduction; Uppsala, 1965.
• 18: R. Statman, PhD Dissertation; Stanford University, 1974.
• 19: G. Takeuti, Proof Theory; Amsterdam, 1975.
• 20: W. Wulf, R.L. London and M. Shaw, Abstraction and verification in ALPHARD—Introduction to language and methodology; Tech. Report, Carnegie-Mellon University, 1976.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures; Procedures, functions, and subroutines

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory