4.5 Semantics
4.5.2 Abstract machines
The SECD machine To define the semantics of applicative expressions (AE), Landin de-signed the SECD machine [50]. As Landin later points out [51, page 159] the abstract lan-guage ISWIM (If you See What I Mean) is AE with ‘syntactic sugar’. That is, AE is the
‘kernel’ of ISWIM: Every construct of ISWIM can be expressed in AE.
At any point in time the SECD machine’s state or configuration is a four-tuple:(S, E, C, D).
This machine performs evaluation of applicative expressions by looking at the four com-ponents and deterministically determining the four comcom-ponents of the next configuration.
Iteratively performing this mapping from configuration to configuration (possibly) obtain-ing a configuration, which cannot be mapped to another configuration, defines evaluation of applicative expressions via the SECD machine. That is, the SECD machine defines the semantics of applicative expressions, via an abstract specification of configurations and a definition of transitions from configurations to configurations. In that respect, this approach is a small-step operational semantics.5
Variations of the SECD machine The SECD machine is mostly important because it is the first abstract machine defined as a definitional semantics for a programming language.
The original specification is not properly tail-recursive [12] and Danvy et al. show that the dump component D (which is isomorphic to a stack of(S, E, C)-triples) is an unnecessary artifact [3].
Directly simplified or extended versions also exist. For example, without support for basic constants or with support for non-local control operators [3, 25]. Hannan and Miller define such a version without support for basic functions [39]. That machine differs from the original version in a more subtle way: In the evaluation of applications the operator subex-pression is evaluated before the operand subexsubex-pression resulting in left-to-right applicative evaluation order whereas the original has right-to-left applicative evaluation order. The ma-chine also operates on expressions with de Bruijn indices instead of named variables.
Landin’s original version operates directly on applicative expressions. Felleisen and Flatt have a version where such expressions must be compiled into a language of instructions before running the machine [31, Section 8.1].
Plotkin allows closures involving expressions in general instead of only abstractions [59, page 120]. Plotkin has this more general notion of closures to easily define a call-by-name version of the SECD machine.
Other machines Felleisen and Friedman designed another machine called the CEK ma-chine [32]; a simple mama-chine inspired by the SECD mama-chine but with roots in Reynolds’s work on definitional interpreters [32, Section 2] [61]. Several variants of the CEK machine have been presented [31]. One of these variants is the CESK machine which was presented in Felleisen’s PhD-dissertation as a specification of the semantics of what he calls Idealized Scheme [30]. The added component S represents a store needed to model the language: Ide-alized Scheme is essentially applicative expressions extended with imperative constructs for side-effecting variables and a non-local control operator.
A wide range of machines has been presented in the literature. Some other machines are Hannan and Miller’s CLS machine, the VEC machine, which was presented as an imple-mentation for a denotational semantics [65], the never published Krivine machine [13], and the CAM with origin in categorical combinators [16].
Abstract machines and virtual machines Ager et al. distinguish between abstract machines and virtual machines [2]. According to their definition a machine is a virtual machine if and
5Reynolds refers to semantics of this kind by transition semantics [64, Chapter 6].
only if it operates on compiled terms. In that respect, e.g., Felleisen and Flatt’s version of the SECD machine, the VEC-machine and the CAM are virtual machines and the SECD machine and the Krivine machine are abstract machines. We follow the distinction suggested by Ager et al. and concentrate on machines operating directly on abstract syntax.
Our notion of an abstract machine An abstract machineMis a state-transition system. It has a set of states (or configurations) partitioned into the terminal configurations (TerminalM) and the non-terminal configurations (NonTerminalM). It has a transition relation (σM) that de-cides the next configuration for a given non-terminal configuration. The transition relation is iterated until (possibly) a terminal configuration is obtained.
Following Plotkin [60] we have restrictedσMto be a (total) function such that the ma-chine is deterministic. We restrictσMfurther by only allowing elementary operations. This restriction makes the evaluation steps explicit. For example, a recursive traversal on a term is then not allowed in one transition.6
A total functionloadMis specified to map a term into a corresponding start configuration ofM. Likewise, a partial functionunloadMis specified to extract the result from a terminal configuration. Running an abstract machine is then defined as the composition of loading, iterating the transition function, and possibly unloading the final result:
TerminalM a
NonTerminalM n
ConfigurationM c ::= a|n
loadM : Term→ConfigurationM
σM : NonTerminalM→ConfigurationM
unloadM : TerminalM→Val
iterateM : ConfigurationM→TerminalM
iterateMa = a
iterateMn = iterateM(σMn) runM : Term→Val
runM = unloadM◦iterateM◦loadM
Here Val is the set of result values. If an abstract machine M on term t never reaches a terminal configuration, the machine is said to diverge ont. If a terminal configurationa is reached butunloadMis not defined ona,Mis said to be stuck ina.
The above specification implies that an abstract machine Mis completely specified by defining the possible terminal and nonterminal configurations and the three functions:loadM, σMandunloadM.
As defined above an abstract machine may operate directly on terms by letting terms be part of each configuration. But there is no constraint implying that such an explicit use of terms is always the case. For example, by letting the load function be a compiler the result is a virtual machine. For that reason we restrict loading and unloading as well to only perform elementary operations.
6Felleisen and Flatt do not restrict the transition relation to be a function and they also do not restrict that function by only allowing elementary operations. For example, the CC machine performs a recursive descent on certain terms in one transition [31, Chapter 6].
An abstract machine for TLLF
A configuration of the abstract machine consists of three parts: (1) an expression from the source language, (2) an environment mapping lexical offsets to closures, and (3) a stack where each element is either a closure or a basic function:
Closure c ::= (e, ρ) Env ρ ::= •|c·ρ Stack s ::= •|c·s|q·s Val v ::= b|(λe, ρ)
Configuration = Exp×Env×Stack
Loading the machine is defined as forming the configuration of the initial expression and the empty environment and the empty stack. Unloading consists of extracting the expres-sion part when the stack is empty. If the expresexpres-sion is an abstraction it is paired with the environment which binds the free indices of the body of the abstraction:
loadTLLF : Exp→Configuration loadTLLFe = (e, •, •)
unloadTLLF : Configuration→Val unloadTLLF(b, ρ, •) = b
unloadTLLF(λe, ρ, •) = (λe, ρ)
The transition function from (non-terminal) configurations to configurations reads:
σTLLF : Configuration→Configuration σTLLF(i, c1· · ·(ei, ρi)· · ·cj, s) = (ei, ρi, s)
σTLLF(λe, ρ, c·s) = (e, c·ρ, s) σTLLF(e e0, ρ, s) = (e, ρ, (e0, ρ)·s) σTLLF(q, ρ, (e, ρ0)·s) = (e, ρ0, q·s)
σTLLF(l, ρ, q·s) = (capp(q, l), ρ, s)
Because programs are closed terms a variable can always find a corresponding binding to a closure in the environment. In case of a match, the expression and the associated environ-ment is used for evaluation. Closures are shifted from the stack to the environenviron-ment when the term-part is an abstraction. The associated environment is the application-time environment and is associated an unevaluated expression. The call-by-name application mechanism and static scope of bindings is hence achieved. When the left sub-expression of an application is evaluated to a basic function, the argument expression must be evaluated to a literal.
The definition of σTLLF defines the set of terminal configurations. BecauseunloadTLLF is partially defined on this set the machine can get stuck. Stuck configurations correspond to situations where the left subexpression of an application evaluates to a literal, or a basic function is applied to a literal wherecappis not defined. The machine can diverge because of self-application.
The above abstract machine gives the semantics for TLLF. The machine is a direct exten-sion of a well-known abstract machine: the Krivine machine. The Krivine machine performs call-by-name evaluation of pure de Bruijn-indexedλ-terms. The extension thus consists in the support for basic constants: The first rules ofunloadTLLFand the last two rules ofσTLLF are not part of the Krivine machine.
Adjusted representation By (lightweight) fusing the iterating function with the transition function another useful representation of abstract machines is achieved. The fusion consists in letting the transition function call itself after each single transition. Inlining the unload function lets the machine directly unload the result from a terminal configuration. The aux-iliary structures remain unchanged, and running the extended Krivine machine from above is equivalently expressed:
σTLLF : Configuration→Val σTLLF(b, ρ, •) = b
σTLLF(λe, ρ, •) = (λe, ρ)
σTLLF(i, c1· · ·(ei, ρi)· · ·cj, s) = σTLLF(ei, ρi, s) σTLLF(λe, ρ, c·s) = σTLLF(e, c·ρ, s)
σTLLF(e e0, ρ, s) = σTLLF(e, ρ, (e0, ρ)·s) σTLLF(q, ρ, (e, ρ0)·s) = σTLLF(e, ρ0, q·s)
σTLLF(l, ρ, q·s) = σTLLF(capp(q, l), ρ, s) runTLLF : Exp→Val
runTLLFe = σTLLF(e, •, •)
In the following we will often use this alternative representation of abstract machines. In each situation it will be a straightforward exercise to translate to the other representation.
Danvy and Millikin go into details [18].