An algebraic semantics for busy (data-driven) and lazy (demand-driven) evaluation and its application to a functional language

  • Bernhard Möller
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)


The method of algebraic specification, when extended to inductive continuous algebras, is a convenient tool for defining and describing domains with nonstrict operations and with limit points. This replies to a number of remarks in [8] on the “restrictiveness” of algebraic specifications. Moreover, our approach has the advantage that the characteristic properties define the semantic domains, whereas in [8] they have to be proved.

Our main aim was to show how correct operational semantics can be derived from a mathematical semantics in terms of operative continuous algebras. Such algebras are defined by equations of a certain restricted form which provide a reduction calculus for the evaluation of terms over the algebras. By organizing the application of the rules suitably various operational realizations (here lazy and busy evaluation) of the mathematical semantics can be obtained.

Further research should concern techniques for implementing continuous algebras specified by more general kinds of axioms (e.g. conditional equations, see [16]) in terms of operative ones. In this way a first specification could be free of operational details which should only be introduced in a later stage of the development process.


Normal Form Operational Semantic Recursive Definition Operation Symbol Critical Argument 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    J.A.Goguen, J.W.Thatcher, E.G.Wagner, J.B.Wright: Initial algebra semantics and continuous algebras. JACM 24, 68–95 (1977)Google Scholar
  2. [2]
    J.B.Wright, E.G.Wagner, J.W.Thatcher: A uniform approach to inductive posets and inductive closure. MFCS 1977. LNCS 53. Berlin: Springer 1977, 192–212Google Scholar
  3. [3]
    J.Backus: Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. CACH 21, 613–641 (1978)Google Scholar
  4. [4]
    F.L.Bauer: Detailization and lazy evaluation, infinite objects and pointer representation. In: F.L.Bauer, M.Broy (eds.): Program construction. LNCS 69. Berlin: Springer 1979. 406–420Google Scholar
  5. [5]
    F.L.Bauer, H.Wössner: Algorithmic language and program development. Berlin: Springer 1982Google Scholar
  6. [6]
    S.L.Bloom: Varieties of ordered algebras. JCSS 13, 200–212 (1976)Google Scholar
  7. [7]
    M.Broy: Transformation parallel ablaufender Programme. Fakultät für Mathematik der TU München, Dissertation, 1980. Institut für Informatik der TU München, TUM-I8001, 1980Google Scholar
  8. [8]
    R.Cartwright, J.Donahue: The semantics of lazy (and industrious) evaluation. Conf. Record of the 1982 ACM Symposium on LISP and Functional Programming, 253–261Google Scholar
  9. [9]
    B.Courcelle, M.Nivat: Algebraic families of interpretations. 17th FOCS 1976, 137–146Google Scholar
  10. [10]
    D.P.Friedman, D.S.Wise: CONS should not evaluate its arguments. In: S.Michaelson, R.Milner (eds.): Automata, languages and programming. Edinburgh: Edinburgh University Press 1976, 257–285Google Scholar
  11. [11]
    J.V.Guttag: The specification and application to programming of abstract data types. Ph.D. Thesis, University of Toronto, Dept. of Computer Science, Rep. CSRG-59, 1975Google Scholar
  12. [12]
    P.Henderson, J.H.Morris: A lazy evaluator. 3rd POPL 1976, 95–103Google Scholar
  13. [13]
    G.Huet, J.-M.Hullot: Proofs by induction in equational theories with constructors. 21st FOCS 1980, 96–107Google Scholar
  14. [11]
    S.C.Kleene: Introduction to metamathematics. New York: Van Nostrand 1952Google Scholar
  15. [15]
    Z.Manna: Mathematical theory of computation. New York: McGraw-Hill 1974Google Scholar
  16. [16]
    B.Möller: Unendliche Objekte und Geflechte. Fakultät für Mathematik und Informatik der TU München, Dissertation, 1982. Institut für Informatik der TU München, TUH-I8213, 1982Google Scholar
  17. [17]
    M.Nivat: On the interpretation of recursive polyadic program schemes. Istituto Nazionale di Alta Matematica, Symposia Mathematica XV. London: Academic Press 1975, 255–281Google Scholar
  18. [18]
    P.C.Treleaven, D.R.Brownbridge, R.P.Hopkins: Data-driven and demand-driven computer architecture. Computing Surveys 14, 93–143 (1982)Google Scholar
  19. [19]
    J.Vuillemin: Correct and optimal implementations of recursion in a simple programming language. JCSS 9, 332–354 (1974)Google Scholar
  20. [20]
    J.Vuillemin: Syntaxe, semantique et axiomatique d'une langage de programmation simple. Basel: Birkhäuser 1975Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Bernhard Möller
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMünchen 2Fed. Rep. Germany

Personalised recommendations