Graph-based operational semantics of a lazy functional language
Kristoffer H. Rose · 1993
Machine [Car83], the G-machine [Joh84, BPJR88], Clean [BvEvLP87, KSvEP91], and DACTL [Ken88, GKS89]. All of these can be perceived as notations for algorithms that describe how graphs may be used to model the evaluation of the implemented language. Such notations have the advantage that they are directly executable. However, they are often not very readable since all the details of the implementation have to be present in the specification. On the other hand, the idea has also been used in attempts to build models of functional languages and to prove properties of such models directly. Again starting from [Wad71] such attempts are naturally focused on models of the -calculus---a 2 We will use the traditional word "redex" (reducible expression) rather than some abbreviation of "reducible subgraph" even though we will always refer to the latter. GRAPH-BASED OPERATIONAL SEMANTICS OF A LAZY FUNCTIONAL LANGUAGE 239 rather large are of research, so we will just mention [Sta78] and [Lam90...