Higher-Order and Symbolic Computation

, Volume 20, Issue 3, pp 319–332 | Cite as

State-transition machines for lambda-calculus expressions

  • David A. Schmidt


The process of compiler generation from lambda-calculus definitions is studied. The compiling schemes developed utilize as their object language the set of state transition machines (STMs): automata-like transition sets using first-order arguments. An intermediate definition form, the STM-interpreter, is treated as central to the formulation of STMs. Three compiling schemes are presented: one derived directly from an STM-interpreter for the lambda-calculus; one formulated from an STM-interpreter variant of Landin’s SECD-machine; and one defined through meaning-preserving transformations upon a denotational definition of the lambda-calculus. The results are compared and some tentative conclusions are made regarding the utility of compiler generation with the STM forms.


Lambda calculus State transition machine SECD-machine Weak-normal form Defunctionalization Continuations Denotational semantics 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Church, A.: The Calculi of Lambda-Conversion. Annals of Mathematical Studies, vol. 6. Princeton Univ. Press, Princeton (1951) Google Scholar
  2. 2.
    Curry, H., Feys, R.: Combinatory Logic, vol. 1. North-Holland, Amsterdam (1958) Google Scholar
  3. 3.
    Ershov, A.: On the essence of compilation. In: Neuhold, E. (ed.) Formal Description of Programming Concepts, pp. 391–420. North-Holland, Amsterdam (1978) Google Scholar
  4. 4.
    Jones, N., Schmidt, D.: Compiler generation from denotational semantics. In: Jones, N. (ed.) Semantics-Directed Compiler Generation. Lecture Notes in Computer Science, vol. 94, pp. 70–93. Springer, New York (1980) Google Scholar
  5. 5.
    Landin, P.: The mechanical evaluation of expressions. Comput. J. 6(4), 308–320 (1964) MATHGoogle Scholar
  6. 6.
    Plotkin, G.: Call-by-name, call-by-value and the λ-calculus. Theor. Comput. Sci. 1, 125–159 (1975) MATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Reynolds, J.: Definitional interpreters for higher-order programming languages. In: Proc. 25th ACM National Conference, Boston, pp. 717–740 (1972) Google Scholar
  8. 8.
    Reynolds, J.: On the relation between direct and continuation semantics. In: Proc. 2d Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science, pp. 141–156. Springer, New York (1974) Google Scholar
  9. 9.
    Schmidt, D.: Compiler generation from lambda-calculus definitions of programming languages. Ph.D. Thesis, Kansas State University, Manhattan, KS (1981) Google Scholar
  10. 10.
    Scott, D.: Data types as lattices. SIAM J. Comput. 5, 522–587 (1976) MATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Stoy, J.: Denotational Semantics. MIT Press, Cambridge (1997) Google Scholar
  12. 12.
    Strachey, C., Wadsworth, C.: Continuations—a mathematical semantics for handling full jumps. Technical Report PRG-11, Programming Research Group, Oxford University (1974) Google Scholar
  13. 13.
    Wadsworth, C.: The relation between computational and denotational properties for Scott’s models of the lambda-calculus. SIAM J. Comput. 5, 488–521 (1976) MATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Watt, D., Madsen, O.: Extended attribute grammars. Technical Report 10, University of Glasgow (1977). Revised version: On defining semantics by means of extended attribute grammars. In: Jones, N.D. (ed.) Semantics-Directed Compiler Generation. Lecture Notes in Computer Science, vol. 94. Springer (1980) Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2007

Authors and Affiliations

  1. 1.Computer Science DepartmentAarhus UniversityAarhusDenmark

Personalised recommendations