An algebraic semantics for busy (data-driven) and lazy (demand-driven) evaluation and its application to a functional language
- 95 Downloads
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  on the “restrictiveness” of algebraic specifications. Moreover, our approach has the advantage that the characteristic properties define the semantic domains, whereas in  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 ) 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.
KeywordsNormal Form Operational Semantic Recursive Definition Operation Symbol Critical Argument
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 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
- F.L.Bauer, H.Wössner: Algorithmic language and program development. Berlin: Springer 1982Google Scholar
- S.L.Bloom: Varieties of ordered algebras. JCSS 13, 200–212 (1976)Google Scholar
- 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
- 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
- B.Courcelle, M.Nivat: Algebraic families of interpretations. 17th FOCS 1976, 137–146Google Scholar
- 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
- 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
- P.Henderson, J.H.Morris: A lazy evaluator. 3rd POPL 1976, 95–103Google Scholar
- G.Huet, J.-M.Hullot: Proofs by induction in equational theories with constructors. 21st FOCS 1980, 96–107Google Scholar
- S.C.Kleene: Introduction to metamathematics. New York: Van Nostrand 1952Google Scholar
- Z.Manna: Mathematical theory of computation. New York: McGraw-Hill 1974Google Scholar
- 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
- 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
- P.C.Treleaven, D.R.Brownbridge, R.P.Hopkins: Data-driven and demand-driven computer architecture. Computing Surveys 14, 93–143 (1982)Google Scholar
- J.Vuillemin: Correct and optimal implementations of recursion in a simple programming language. JCSS 9, 332–354 (1974)Google Scholar
- J.Vuillemin: Syntaxe, semantique et axiomatique d'une langage de programmation simple. Basel: Birkhäuser 1975Google Scholar