From operational semantics to abstract machines: preliminary results

ABSTRACT

The operational semantics of functional programming languages is frequently presented using inference rules within simple meta-logics. Such presentations of semantics can be high-level and perspicuous since meta-logics often handle numerous syntactic details in a declarative fashion. This is particularly true of the meta-logic we consider here, which includes simply typed &lgr;-terms, quantification at higher types, and &bgr;-conversion. Evaluation of functional programming languages is also often presented using low-level descriptions based on abstract machines: simple term rewriting systems in which few high-level features are present. In this paper, we illustrate how a high-level description of evaluation using inference rules can be systematically transformed into a low-level abstract machine by removing dependencies on high-level features of the meta-logic until the resulting inference rules are so simple that they can be immediately identified as specifying an abstract machine. In particular, we present in detail the transformation of two inference rules specifying call-by-name evaluation of the untyped &lgr;-calculus into the Krivine machine, a stack-based abstract machine that implements such evaluation. The initial specification uses the meta-logic's &bgr;-conversion to perform substitutions. The resulting machine uses de Bruijn numerals and closures instead of formal substitution. We also comment on a similar construction of a simplified SECD machine implementing call-by-value evaluation. This approach to abstract machine construction provides a semantics-directed method for motivating, proving correct, and extending such abstract machines.

REFERENCES

• 1: Rod M. Burstall , Furio Honsell, A Natural Deduction treatment of Operational Semantics, Proceedings of the Eighth Conference on Foundations of Software Technology and Theoretical Computer Science, p.250-269, December 21-23, 1988
• 2: Luca Cardelli, Compiling a functional language, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.208-217, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802037]
• 3: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 4: CURIEN, P. The )~p-calculus: An Abstract Framework for Environment Machines. Tech. Rep., LIENS, 1988.
• 5: Amy P. Felty , Dale Miller, Specifying and implementing theorem provers in a higher-order logic programming language, 1989
• 6: J. Hannan , D. Miller, A meta-logic for functional programming, Meta-programming in logic programming, MIT Press, Cambridge, MA, 1989
• 7: HARPER, R., HONSELL, F., AND PLOTKIN, G. A framework for defining logics. In Symposium on Logic in Computer Science (1987), pp. 194-204.
• 8: L. Hascoët, Partial evaluation with inference rules, New Generation Computing, v.6 n.2-3, p.187-209, March-April 1988 [doi>10.1007/BF03037137]
• 9: HUET, G., AND OPPEN, D. Equations and rewrite rules: a survey. In Formal Language Theory: Perspectives and Open Problems, R. Book, Ed., Academic Press, 1980, pp. 349--405.
• 10: Jo HN SSO N, T. Compiling Lazy Functional Languages. PhD thesis, Chalmers University of Technology, 1987.
• 11: Neil D. Jones, Semantics-Directed Compiler Generation: Proceedings, Springer-Verlag New York, Inc., Secaucus, NJ, 1980
• 12: Neil D. Jones , Peter Sestoft , Harald Sondergaard, An experiment in partial evaluation: the generation of a compiler generator, Proc. of the first international conference on Rewriting techniques and applications, p.124-140, December 1985, Dijon, France
• 13: G. Kahn, Natural semantics, 4th Annual Symposium on Theoretical Aspects of Computer Sciences on STACS 87, p.22-39, February 1987, Passau, Germany
• 14: LANDIN, P. J. The mechanical evaluation of expressions. Computer Journal 6, 5 (1964), 308-320.
• 15: NADATHUR, G., AND MILLER, D. An overview of )~Prolog. in Fibh International Conference and Symposium on Logic Programming (1988), K. Bowen and R. Kowalski, Eds., MIT Press.
• 16: Frank G. Pagan, Converting interpreters into compilers, Software—Practice & Experience, v.18 n.6, p.509-527, June, 1988 [doi>10.1002/spe.4380180603]
• 17: L. C. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, v.5 n.3, p.363-397, September 1989 [doi>10.1007/BF00248324]
• 18: Mitchell. Wand, From interpreter to compiler: a representational derivation, on Programs as data objects, p.306-324, April 1986, Copenhagen, Denmark

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages
      D.3.4 Processors
          Subjects: Compilers; Interpreters

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

General Terms:
Algorithms, Languages