and inlinerefocusaux:
EContext0: E[ ] ::= [ ]|E[[ ] (e, s)]|E[q[ ]]
Value0 : v ::= b|(λe, ρ) evalTLLF : Exp→Value0 evalTLLF = refocus(t, •, [ ]) refocus(b, s, [ ]) = b
refocus(λe, s, [ ]) = (λe, s)
refocus(i, (e1, s1)· · ·(ei, si)· · ·(ej, sj), E[ ]) = refocus(ei, si, E[ ]) refocus(λe, s, E[[ ] (e0, s0)]) = refocus(e, (e0, s0)·s, E[ ])
refocus(e e0, s, E[ ]) = refocus(e, s, E[[ ] (e0, s)]) refocus(q, s, E[[ ] (e, s0)]) = refocus(e, s0, E[q[ ]])
refocus(l, s, E[q[ ]]) = refocus(capp(q, l), s, E[ ])
Removing the first and the last two clauses ofrefocus, the abstract machine is the Krivine machine [13], which is the standard abstract machine that performs call-by-name evaluation of pureλ-terms. The extra three rules exclusively cope with basic constants.
The above derivation illustrates the syntactic correspondence but also demonstrates that the correspondence directly applies to applied λ-calculi. In later chapters we give more examples.
Relating the abstract machine and the reduction semantics for TLLF Starting with the re-duction semantics for the programming language TLLF we via the syntactic correspondence derived an abstract machine. A comparison with the abstract machine specified on page 53 defining the semantics for TLLF shows that inliningrefocusaux yields that machine: The only difference is the stack of the abstract machine for TLLF. But the stacks are isomorphic with the contexts used in the derived abstract machine and it is hence the same machine.
That is, the abstract machine for TLLF and the reduction semantics for TLLF are equivalent specifications:
runTLLFe=b ⇐⇒ evalTLLFe=b[s]
Considering for simplicity only basic constants as results: starting from a closed expression e the abstract machine and the reduction semantics for TLLF either both do not yield a basic constant or they both yield the same basic constant. This result is a corollary of the correctness of the applied transformations in the derivation of the abstract machine starting from the reduction semantics.
operations in the metalanguage, and the valuation function becomes an interpreter for the de-fined language depending on the semantics of the constructs of the metalanguage. The deno-tational specification become a definitional interpreter.9 Reynolds investigated the relationship between the defined language and the metalanguage in such definitional interpreters in his seminal paper Definitional Interpreters for Higher-Order Programming Languages [61] and intro-duced relevant transformations. It is now standard to introduce various language constructs via definitional interpreters. For example, Friedman, Wand, and Haynes use Scheme [43] as metalanguage in Essentials of Programming Languages [34].
Danvy et al. have systematically investigated the transformations Reynolds employed.
The research has among other things given rise to several papers on a derivational approach to the relationship between semantic artifacts [2–5] pioneered by Reynolds. The approach has been dubbed a functional correspondence.
5.3.1 A definitional interpreter
The denotational semantics for TLLF on page 49 becomes a definitional interpreter when de-ciding on a semantics for the metalanguage used. We assume a call-by-name metalanguage.
In the extension of the environment we inline the construction of the pair and switch to the list notation used in this text. For closed expressions, looking up a variableiis identified to taking thei-th element of a list. Evaluation starts with the empty environment•:
ExpVal = Int+Prim+ (DenVal→ExpVal) DenVal = ExpVal
eval : Exp×DenVal list→ExpVal eval(i, d1· · ·di· · ·dj) = di
eval(λe, ρ) = λd.eval(e, d·ρ) eval(e e0, ρ) = caseeval(e, ρ)of
f→f(eval(e0, ρ)) q→caseeval(e0, ρ) of
l→capp(q, l) eval(b, ρ) = b
evaluate : Exp→ExpVal evaluatee = eval(e, •)
Instead of introducing some kind of error mechanism, the interpreter is left partial. Several of the constructs in the defined language are interpreted via a similar construct in the met-alanguage. In such a setting the reader must be familiar with higher-order languages and have in-depth understanding of the metalanguage to understand the defined language. In the following we briefly introduce Reynolds’s ideas to separate the defined language from the metalanguage.
5.3.2 Closure conversion
Closure conversion eliminates the use of the function space in the values by introducing clo-sures: Evaluating an abstraction then results in a pair composed of the body of the
abstrac-9A definitional interpreter is an implementation of a big-step operational semantics.
tion and the current environment. This pair represents the evaluation of the body with the environment extended.10
5.3.3 Continuation-passing-style/direct-style transformations
Reynolds points out how the evaluation order of the defined language depends on the eval-uation order of the metalanguage in a direct style interpreter.11 To eliminate this evaluation-order dependency Reynolds applies a continuation-passing-style (CPS) transformation to the interpreter. In a (higher-order) program in CPS all functions take an extra argument, the continuation, a functional representation of the rest of the computation. Instead of returning a value directly, all functions apply the current continuation to the value. All intermediate results are named, and all calls are tail-calls. In other words, the computation has been se-quentialized: in the interpreter no implicit control-flow remains, which otherwise depend on the evaluation order of the metalanguage. Plotkin has formally proved the evaluation-order independency of programs in CPS by simulations of call-by-value in a call-by-name evaluation order and visa versa [59].12
The interpreter for TLLF given above relies on a call-by-name evaluation order of the metalanguage. That is, to define TLLF evaluation-order independent we would apply a call-by-name-CPS transformation to the interpreter.
The left-inverses of CPS transformations maps programs in CPS into corresponding pro-grams in direct style. Danvy has formulated these direct-style transformations [19].
5.3.4 Defunctionalization/refunctionalization
After the CPS transformation the interpreter is higher-order: continuations are functions from intermediate results to final answers. Reynolds introduced Defunctionalization as the mechanism to translate higher-order programs into first-order: For the function space of continuations we identify the (finite number of) inhabitants occurring in the program and create a sum space with one injection for each of these inhabitants. Each member holds the free variables of the function it represents. Continuation constructions become injections.
Eliminations (applications of continuations) become calls to an apply function which (1) dis-patches on the first-order continuation representation, and (2) performs the corresponding evaluation.
The left-inverse of defunctionalization transforms programs in defunctionalized form, i.e., in the image of defunctionalization, into corresponding higher-order programs. Danvy and Millikin have investigated this refunctionalization [26].
5.3.5 Relating interpreters and abstract machines
Reynolds used the transformations on a definitional interpreter to disconnect the defined language from the metalanguage. The result is a sequentialized, first-order specification.
10The term ‘closure’ in this context is due to Landin [50].
11Because TLLF is a pure functional language referential transparency holds. That is, if the metalanguage used call-by-value evaluation order the semantics of the language would only change in case of non-terminating evaluation of argument expressions in applications.
12It is noted that the notion of CPS and CPS-transformations does not originate in Reynolds work on defi-nitional interpreters. Reynolds has (like Landin [52]) later published a paper on the discoveries of continua-tions [62].
Danvy et al. have observed that an interpreter after the transformations implements a state-transition system, i.e., an abstract machine. Danvy et al. have systematically applied the transformations to a wide range of interpreters and have showed that well-known abstract machines functionally correspond to well-known interpreters [3–5]. Especially they have shown that the above interpreter (without support for basic constants) closure-converted on the one hand corresponds to the Krivine machine when applying a call-by-name-CPS transfor-mation,13 and on the other hand corresponds to the CEK machine when applying a call-by-value-CPS transformation, when followed by defunctionalization [22]. Nothing changes with the introduction of basic constants. The interpreter for TLLF thus functionally corre-sponds to the abstract machine for TLLF specified on page 53.