Complete proof systems for algebraic simply-typed terms

ABSTRACT

We show that reasoning by case analysis (on whether subprograms diverge or converge) is complete for proving PCF observational congruences of algebraic terms. The latter are applicative combinations of first-order variables and a constant &OHgr; denoting a diverging program of base type. A restricted version of the logic is complete for proving equality of algebraic terms in the full continuous type hierarchy (equivalently, observational congruence in PCF with parallel conditional). We show that the provability in the latter logic is in co-NP. We also give complete equational proof systems for a subclass of algebraic terms; provability in these systems is in linear time.

REFERENCES

• 1: Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic. North-Holland, 1981. Revised Edition, }984.
• 2: G. Berry, and P.-L. Curien. SequentiM algorithms on concrete d~t~ $tructurc~. ThcorcticM Computer Science 20, 1982.
• 3: G Berry , P L Curien , J J Lévy, Full abstraction for sequential algorithms: the state of the art, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 4: Robert Cartwright , Matthias Felleisen, Observable sequentiality and full abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.328-342, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143232]
• 5: Harvey Friedman. Equality between functionals. In Rohit Parikh, editor, Logic Colloquium '73, volume 453 of Lect. Notes in Math., pages 22-37. Springer-Verlag, 1975.
• 6: Michael J.C. Gordon, Robin Milner, and C.P. Wadsworth. Edinburgh LCF: A Mechanical Logic of Computation, volume 78 of Lect. Notes in Computer Sci. Springer- Verlag, 1979.
• 7: Robin Milner. Fully abstract models of the typed lambda calculus. Theoretical Computer Sci., 4:1-22, 1977.
• 8: Gordon D. Plotkin. )~~definability and logical relations. Technical Report SAI-RM-4, University of Edinburgh, School of Artificial Intelligence, 1973.
• 9: Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Sci., 5:223-257, 1977.
• 10: Gordon D. Plotkin. Notes on completeness of the full continuous type hierarchy. Unpublished manuscript, MiT, November 1982.
• 11: V.Yu. Sazonov. Expressibility of functions in D. Scott's LCF language. Algebra i Logika, 15:308-330, 1976. (Russian).
• 12: Richard Statman. Completeness, invariance and lambda-definability. J. Symbolic Logic, 47:17-~6, 1982.
• 13: Richard Statman. Equality between fuuctionals revisited. In L.A. Harrington, et al., editor, Harvey Friedman's Research on the Foundations of Mathematics, volume 117 of Studies in Logic, pages 331--338. North- Holland, 1985.
• 14: Ramesh Subrahmanyam, Dan Dougherty. Completeness theorem for the set-theoretic coproduct model. Manuscript, 1993.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

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

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION

General Terms:
Languages, Theory, Verification