Operational and axiomatic semantics of PCF

ABSTRACT

PCF, as considered in this paper, is a lazy typed lambda calculus with functions, pairing, fixed-point operators and arbitrary algebraic data types. The natural equational axioms for PCF include &eegr;-equivalence and the so-called “surjective pairing” axiom for pairs. However, the reduction system pcf&eegr;,sp defined by directing each equational axiom is not confluent, for virtually any choice of algebraic data types. Moreover, neither &eegr;-reduction nor surjective pairing seems to have a counterpart in ordinary execution. Therefore, we consider a smaller reduction system pcf without &eegr;-reduction or surjective pairing. The system pcf is confluent when combined with any linear, confluent algebraic rewrite rules. The system is also computationally adequate, in the sense that whenever a closed term of “observable” type has a pcf&eegr;,sp normal form, this is also the unique pcf normal form. Moreover, the equational axioms for PCF, including (&eegr;) and surjective pairing, are sound for pcf observational equivalence. These results suggest that if we take the equational axioms as defining the language, the smaller reduction system gives an appropriate operational semantics.

REFERENCES

• Bar84: H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.
• BT88: V. Breazu-Tannen. Combining algebra and higher-order types. In Third IEEE Syrnp. Logic in Computer Science, pages 82-90, 1988.
• BTG89: Val Breazu-Tannen , Jean Gallier, Polymorphic rewriting conserves algebraic strong normalization, Selected papers of the 16th international colloquium on Automata, languages, and programming, p.3-28, June 1991, Stresa, Italy
• Chu41: A. Church. The Calculi of Larnbda Conversion. Princeton Univ. Press, 1941. Reprinted 1963 by University Microfilms Inc., Ann Arbor, MI.
• Hen80: Peter Henderson, Functional Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1980
• HWWW85: Joseph Y. Halpern , John H. Williams , Edward L. Wimmers , Timothy C. Winkler, Denotational semantics and rewrite rules for FP, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.108-120, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318623]
• Kd89: J. W. Klop , R. C. de Vrijer, Unique normal forms for Lambda calculus with surjective pairing, Information and Computation, v.80 n.2, p.97-113, Feb. 1989 [doi>10.1016/0890-5401(89)90014-X]
• Klo80: J.W. Klop. Combinatory Reduction Systems. PhD thesis, University of Utrecht, 1980. Published as Mathematical Centei Tract 129.
• Mit90: John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• Nes89: D. Nesmith. The Church-Rosser property in higher-order rewrite systems. Manuscript, 1989.
• Pey87: Simon L. Peyton Jones, The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
• Plo77: G.D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1977.
• Pot81: G. Porringer. The Church-Rosser theorem for typed A-calculus with surjective pairing. Notre Dame Journal of Formal Logic, 22(3):264-268, 1981.
• Sco69: D.S. Scott. A type-theoretic alternative to CUCH, ISWIM, OWHY. Manuscript, 1969.
• Tur85: D. A. Turner, Miranda: a non-strict functional language with polymorphic types, Proc. of a conference on Functional programming languages and computer architecture, p.1-16, January 1985, Nancy, France

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:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Algorithms, Languages