Denotational semantics and rewrite rules for FP

ABSTRACT

We consider languages whose operational semantics is given by a set of rewrite rules. For such languages, it is important to be able to determine that there are enough rules to completely reduce all meaningful expressions, but not so many that the system of rules is inconsistent. We develop a formal framework in which to give a precise treatment of these soundness and completeness issues. We believe our approach to be novel in that we make heavy use of denotational semantics in our proof of completeness. The particular language for which we answer these questions is an extended version of the functional programming language FP; however the applicability of these techniques extends beyond the realm of FP rewriting systems.

REFERENCES

• 1: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 2: [Bi67] Birkhoff, G., Lattice Theory, American Math. Society Colloquium Publications, vol. 23, Third edition (1967).
• 3: R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
• 4: Walter Dosch , Bernhard Möller>, Busy and lazy FP with infinite objects, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.282-292, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802045]
• 5: [En71] Engeler, E., "Algebras and combinators", Algebra Universalis 13 (1971), pp. 389-392.
• 6: Steven Fortune , Daniel Leivant , Michael O'Donnell, The Expressiveness of Simple and Second-Order Type Structures, Journal of the ACM (JACM), v.30 n.1, p.151-185, Jan. 1983 [doi>10.1145/322358.322370]
• 7: [FW76] Friedman, D. and D. Wise, "Cons should not evaluate its arguments", Third International Colloquium on Automata, Languages, and Programming (1976) pp. 257-284.
• 8: [GMP82] Goguen, J., J. Meseguer. and D. Plaisted, "Programming with parameterized abstract objects in OBJ", in Theory and Practice of Software Technology, North-Holland (1982).
• 9: [HW³84] Halpern, J. Y., J. H. Williams, E. L. Wimmers, and T. C. Winkler, "Denotational semantics and rewrite rules for FP", to appear as an IBM Research Report (1984).
• 10: Peter Henderson , James H. Morris, Jr., A lazy evaluator, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.95-103, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811543]
• 11: Christoph M. Hoffmann , Michael J. O`Donnell, Implementation of an interpreter for abstract equations, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.111-121, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800522]
• 12: [Me82] Meyer, A. R., "What is a model of the ¿-calculus?", Information and Control 52, (1982) pp. 87-122.
• 13: Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
• 14: Hartley Rogers, Jr., Theory of recursive functions and effective computability, MIT Press, Cambridge, MA, 1987
• 15: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 16: [Tu79] Turner, D. A., "A new implementation technique for applicative languages", Sofware practice and Experience 9 (1979). pp. 31-49.
• 17: John H. Williams, Formal Representations for Recursively Defined Functional Programs, Proceedings of the International Colloquium on Formalization of Programming Concepts, p.460-470, April 19-25, 1981
• 18: John H. Williams, On the Development of the Algebra of Functional Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.4, p.733-757, Oct. 1982 [doi>10.1145/69622.357193]

INDEX TERMS

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

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

          Nouns: FP

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
          Subjects: Parallel rewriting systems (e.g., developmental systems, L-systems)

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