A programming language theorem which is independent of Peano Arithmetic

ABSTRACT

Strongly typed programming languages contain a natural subrecursive part consisting of programs with no loops and no explicitly recursive (circular) function definitions. For languages with polymorphic type structure, such as Model, the termination of all loop-free nonrecursive programs is independent of Peano Arithmetic. An attempt to apply the same techniques to prove independence of the P@@@@NP problem can succeed only if NP complete problems have almost polynomial complexity.

REFERENCES

• 1: Curry, H.B. and Feys, R., Combinatory Logic, North-Holland Amsterdam (1958).
• 2: Feferman, S. Transfinite Recursive Progressions of Axiomatic Theories. Journal of Symbolic Logic. v. 27 no. 3 (1962) 259-316.
• 3: Fortune, S. The Polymorphic Lambda Calculus. Cornell University Dept. of Computer Science Technical Report, in preparation.
• 4: Grzegorczyk, A. Some Classes of Recursive Functions. Rozprawy matematyczne No. 4, Instytut Matematyczny Polskiej Akademie Naak, Warsaw (1953).
• 5: J. Hartmanis, Relations between diagonalization, proof systems, and complexity gaps, Proceedings of the ninth annual ACM symposium on Theory of computing, p.223-227, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803412]
• 6: 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]
• 7: Hilbert, D. Über das Unendliche. Mathematische Annalen v. 95(1926) 161-190. Translation: On The Infinite. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 van Heijenoont, ed. Harvard University Press Cambridge, Massachusetts (1967) 367-392.
• 8: 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
• 9: Levin, L.A. Universal Enumeration Problems Problemi Peredaci Informacii, Tom IX(1972) 115-116.
• 10: Lipton, R.J. Model Theoretic Aspects of Computational Complexity. 19th Annual Symposium on Foundations of Computer Science (1978) 193-200.
• 11: Löb, M.H., Cut Elimination in Type Theory (abstract), Journal of Symbolic Logic, v. 29 (1964), p. 220.
• 12: O'Donnell, M. A Programming Language T Theorem which is Independent of Peano Arithmetic. Purdue University Dept. of Computer Sciences Technical Report #299 (1979)
• 13: Paris, J.B., Some Independence Results for Peano Arithmetic Using Inner Models, to appear.
• 14: Paris, J. and L. Harrington. A Mathematical Incompleteness in Peano Arithmetic. Handbook of Mathematical Logic, J. Barwise, ed. North-Holland, New York (1977) 1133-1142.
• 15: Prawitz, D., Natural Deduction. Almquist and Wiksell, Stockholm (1965).
• 16: Prawitz, D., Some results for intuitionistic logic with second order quantification rules. Intuitionism and Proof Theory Conference, Buffalo, NY, North-Holland, Amsterdam (1970), pp. 259-270.
• 17: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 18: Schnorr, C.P. Optimal Algorithms for Self-Reducible Problems. Automata Languages and Programming. Edinburgh University Press (1976) 322-337.
• 19: Sierpinski, W. Cardinal and Ordinal Numbers. Drukarnia Uniwersytetu Jagiellońskiego w Krakowie, Warsaw (1958)
• 20: Statman, R. The Typed &lgr;-Calculus is not Elementary Recursive, 18th Annual Symposium on Foundations of Computer Science (1977) 90-94.
• 21: Stenlund, S., Combinators, Lambda Terms and Proof Theory, D. Reidel, Dordrecht, Holland (1972).
• 22: Takeuti, G. Proof Theory. Studies in Logic and the Foundations of Mathematics, v. 81, North-Holland, American Elsevier New York (1975).
• 23: Tennent, R.D., PASQUAL: A Proposed Generalization of PASCAL, Technical Report 75-32, Dept. of Computing and Information Science, Queen's University.
• 24: Wainer, S.S. A Classification of the Ordinal Recursive Functions. Archiv Fur Mathematische Logik Und Grundlagen Forschung, v. 13, no. 3-4 (1970).
• 25: Ben Wegbreit, The treatment of data types in EL1, Communications of the ACM, v.17 n.5, p.251-264, May 1974 [doi>10.1145/360980.360992]
• 26: Wulf, W., London, R., and Shaw, M., An Informal Definition of Alphard, CMO-CS-78-105, Carnegie-Mellon University (1978).
• 27: Wulf, W., London, R., and Shaw, M., An Introduction to the Construction and Verification of Alphard Programs, IEEE Transactions on Software Engineering, V. SE-2, No. 4, Dec. 1976.
• 28: Paul Young, Optimization Among Provably Equivalent Programs, Journal of the ACM (JACM), v.24 n.4, p.693-700, Oct. 1977 [doi>10.1145/322033.322046]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.0 General

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

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Recursive function theory

General Terms:
Languages, Theory