Chapter 135Optional

Defunctionalization, Refunctionalization, and Abstract Machines

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Krivine’s abstract machine is usually presented as a finished object: a set of states and four transitions. With de Bruijn terms $t ::= n ∣ λ . t ∣ t_{0} t_{1}$ , thunks $θ = (t, ρ)$ , environments $ρ$ and stacks $π$ both lists of thunks, the states are triples $⟨ t, ρ, π ⟩$ and the transitions are $\begin{aligned} ⟨ n, ρ, π ⟩ & ⟶ ⟨ t^{'}, ρ^{'}, π ⟩ & where ρ_{n} = (t^{'}, ρ^{'}), \\ ⟨ t_{0} t_{1}, ρ, π ⟩ & ⟶ ⟨ t_{0}, ρ, (t_{1}, ρ) :: π ⟩, \\ ⟨ λ . t, ρ, θ :: π ⟩ & ⟶ ⟨ t, θ :: ρ, π ⟩ . \end{aligned}$ A reader can check that this machine runs. A reader cannot say why it has three components rather than two or four, why the stack holds thunks rather than values, why the abstraction rule pops the stack onto the environment, or what evaluation order it implements. Those facts are not recoverable from the table.

They are recoverable from a program. The claim of this chapter is that the machine above is what a particular evaluator becomes after three mechanical transformations, that each transformation has a correctness statement, and that the transformations can be run backwards. The evaluator exhibits the reduction strategy; the machine exhibits the steps. The development follows Ager, Biernacki, Danvy and Midtgaard (2003), and the two transformations it composes are Reynolds’s defunctionalization (1972) and its left inverse, studied by Danvy and Millikin (2009).

The evaluator

Definition 135.1 — The higher-order call-by-name evaluator ¶

Denotable and expressible values are $D_{0} = {Th (f) ∣ f : 1 \to E_{0}}, E_{0} = {Fn (g) ∣ g : D_{0} \to E_{0}},$ and the evaluator $E_{0}$ takes a term and an environment $ρ \in D_{0}^{*}$ : $\begin{aligned} E_{0} (n, ρ) & = f () where ρ_{n} = Th (f), \\ E_{0} (λ . t, ρ) & = Fn (λ v . E_{0} (t, v :: ρ)), \\ E_{0} (t_{0} t_{1}, ρ) & = g (Th (λ () . E_{0} (t_{1}, ρ))) where E_{0} (t_{0}, ρ) = Fn (g) . \end{aligned}$ A program is a closed term, evaluated in the empty environment.

Referenced from 10 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Two properties of definition 135.1 determine everything below. It is compositional: the meaning of a term is built from the meanings of its immediate subterms and nothing else. And it is higher order: both value sets contain functions of the metalanguage. Call by name is visible in one place — the argument of an application is wrapped in a thunk rather than evaluated — and that is the only place a reader must look to see the strategy.

Because a program may diverge, the equations of definition 135.1 define a partial function. Write $E_{0} (t, ρ) ⇓ v$ for the least relation closed under the three clauses, read as: the evaluator, run on $t$ and $ρ$ , terminates with $v$ . Every statement below is about that relation, so that each induction is an induction on a derivation and not on a number of steps.

Closure conversion

The function spaces of $D_{0}$ and $E_{0}$ are not arbitrary. Only two abstractions of the metalanguage ever inhabit them: $λ v . E_{0} (t, v :: ρ)$ in the meaning of an abstraction, and $λ () . E_{0} (t_{1}, ρ)$ in the meaning of an application. Each has exactly two free variables, a term and an environment. So each function space can be replaced by a pair.

Definition 135.2 — The closure-converted evaluator ¶

$D_{1} = {Th (t, ρ)}$ , $E_{1} = {Fn (t, ρ)}$ , and $\begin{aligned} E_{1} (n, ρ) & = E_{1} (t^{'}, ρ^{'}) where ρ_{n} = Th (t^{'}, ρ^{'}), \\ E_{1} (λ . t, ρ) & = Fn (t, ρ), \\ E_{1} (t_{0} t_{1}, ρ) & = E_{1} (t, Th (t_{1}, ρ) :: ρ^{'}) where E_{1} (t_{0}, ρ) = Fn (t, ρ^{'}) . \end{aligned}$

Referenced from 7 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Proposition 135.3 — Closure conversion is correct ¶

Define relations $R_{D} \subseteq D_{0} \times D_{1}$ and $R_{E} \subseteq E_{0} \times E_{1}$ coinductively by $\begin{aligned} Th (f) & R_{D} Th (t, ρ) iff f () ⇓ v_{0} exactly when E_{1} (t, ρ) ⇓ v_{1}, \\ and then v_{0} R_{E} v_{1}; \\ Fn (g) & R_{E} Fn (t, ρ) iff, for all d_{0} R_{D} d_{1}, \\ g (d_{0}) ⇓ v_{0} exactly when E_{1} (t, d_{1} :: ρ) ⇓ v_{1}, \\ and then v_{0} R_{E} v_{1}, \end{aligned}$ and extend $R_{D}$ pointwise to environments. Then for all $t$ and all $ρ_{0} R_{D}^{*} ρ_{1}$ , $E_{0} (t, ρ_{0}) ⇓ v_{0}$ if and only if $E_{1} (t, ρ_{1}) ⇓ v_{1}$ , and then $v_{0} R_{E} v_{1}$ .

Referenced from 5 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Proof of Proposition 135.3 — Closure conversion is correct

Proof. Forwards, by induction on the derivation of $E_{0} (t, ρ_{0}) ⇓ v_{0}$ .

Index. $ρ_{0, n} = Th (f)$ and $ρ_{1, n} = Th (t^{'}, ρ^{'})$ are related, so the definition of $R_{D}$ gives the conclusion directly from the premise $f () ⇓ v_{0}$ .

Abstraction. Both sides terminate immediately, with $Fn (λ v . E_{0} (t, v :: ρ_{0}))$ and $Fn (t, ρ_{1})$ . To relate them, take $d_{0} R_{D} d_{1}$ ; the two evaluations to compare are $E_{0} (t, d_{0} :: ρ_{0})$ and $E_{1} (t, d_{1} :: ρ_{1})$ , and the environments are related because $R_{D}^{*}$ is pointwise. This is exactly the statement of the proposition at the smaller term $t$ , which is available as a coinduction hypothesis: the relations $R_{D}, R_{E}$ are defined coinductively because the values they relate are functions whose behaviour is only observable when applied.

Application. The premise gives $E_{0} (t_{0}, ρ_{0}) ⇓ Fn (g)$ together with $g (Th (λ () . E_{0} (t_{1}, ρ_{0}))) ⇓ v_{0} .$ By the induction hypothesis at $t_{0}$ , $E_{1} (t_{0}, ρ_{1}) ⇓ Fn (t, ρ^{'})$ with the two function values related. The thunk $Th (λ () . E_{0} (t_{1}, ρ_{0}))$ is related to $Th (t_{1}, ρ_{1})$ by the induction hypothesis at $t_{1}$ . Unfolding $R_{E}$ at those two related arguments gives $E_{1} (t, Th (t_{1}, ρ_{1}) :: ρ^{'}) ⇓ v_{1}$ with $v_{0} R_{E} v_{1}$ , which is the conclusion.

Backwards, the same three cases with the two sides exchanged; the relations are symmetric in the sense that each clause is an “if and only if”. ◻

Definition 135.2 is first order in its data: no value contains a metalanguage function. It is still higher order in its control, because the recursive call in the application clause is not a tail call.

Continuation-passing style

Definition 135.4 — The continuation-passing evaluator ¶

$\begin{aligned} E_{2} (n, ρ, κ) & = E_{2} (t^{'}, ρ^{'}, κ) where ρ_{n} = Th (t^{'}, ρ^{'}), \\ E_{2} (λ . t, ρ, κ) & = κ (Fn (t, ρ)), \\ E_{2} (t_{0} t_{1}, ρ, κ) & = E_{2} (t_{0}, ρ, λ Fn (t, ρ^{'}) . E_{2} (t, Th (t_{1}, ρ) :: ρ^{'}, κ)) . \end{aligned}$ The top level is $E_{2} (t, ε, λ v . v)$ .

Referenced from 11 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Every call is now a tail call, which is what makes the next step possible.

Proposition 135.5 — The transformation is correct ¶

For all $t$ , $ρ$ , $κ$ and $w$ , $E_{2} (t, ρ, κ) ⇓ w if and only if E_{1} (t, ρ) ⇓ v and κ (v) ⇓ w for some v .$

Referenced from 5 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Proof of Proposition 135.5 — The transformation is correct

Proof. Both directions by induction on the respective derivations.

Index. Both clauses recur on $t^{'}$ and $ρ^{'}$ with the same $κ$ ; the statement at $t^{'}$ is the statement at $n$ .

Abstraction. $E_{1} (λ . t, ρ) ⇓ Fn (t, ρ)$ in one step, and the right-hand side reduces to $κ (Fn (t, ρ))$ , which is the left-hand side by definition 135.4.

Application. Write $κ^{'}$ for the continuation built in the application clause. Then Numbering the four justifications

definition 135.4;
the hypothesis at $t_{0}$ ;
the definition of $κ^{'}$ ;
the hypothesis at $t$ ;

the calculation is $\begin{aligned} E_{2} (t_{0} t_{1}, ρ, κ) ⇓ w & \overset{(1)}{⟺} E_{2} (t_{0}, ρ, κ^{'}) ⇓ w \\ \overset{(2)}{⟺} E_{1} (t_{0}, ρ) ⇓ u and κ^{'} (u) ⇓ w \\ \overset{(3)}{⟺} u = Fn (t, ρ^{'}) and E_{2} (t, Th (t_{1}, ρ) :: ρ^{'}, κ) ⇓ w \\ \overset{(4)}{⟺} E_{1} (t, Th (t_{1}, ρ) :: ρ^{'}) ⇓ v and κ (v) ⇓ w, \end{aligned}$ and the last line is $E_{1} (t_{0} t_{1}, ρ) ⇓ v$ with $κ (v) ⇓ w$ by definition 135.2. The hypothesis is applied at $t$ , the body of the abstraction returned by $t_{0}$ , which is not a subterm of $t_{0} t_{1}$ ; the induction is therefore on the derivation, not on the term. ◻

Defunctionalizing the continuation

The continuation space of definition 135.4 is inhabited by two abstractions: $λ v . v$ at the top level, with no free variables, and the one built in the application clause, with three free variables $t_{1}$ , $ρ$ and $κ$ . Replace the space by a data type with two constructors, and add the function that interprets them.

Definition 135.6 — The defunctionalized evaluator ¶

$K ::= K_{0} ∣ K_{1} (t, ρ, K)$ , and $\begin{aligned} E_{3} (n, ρ, κ) & = E_{3} (t^{'}, ρ^{'}, κ) where ρ_{n} = Th (t^{'}, ρ^{'}), \\ E_{3} (λ . t, ρ, κ) & = A (κ, Fn (t, ρ)), \\ E_{3} (t_{0} t_{1}, ρ, κ) & = E_{3} (t_{0}, ρ, K_{1} (t_{1}, ρ, κ)), \\ A (K_{0}, v) & = v, \\ A (K_{1} (t_{1}, ρ, κ), Fn (t, ρ^{'})) & = E_{3} (t, Th (t_{1}, ρ) :: ρ^{'}, κ) . \end{aligned}$

Referenced from 7 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Proposition 135.7 — Defunctionalization is correct ¶

Interpret continuation data by $[[K_{0}]] = λ v . v$ and $[[K_{1} (t_{1}, ρ, κ)]] = λ Fn (t, ρ^{'}) . E_{2} (t, Th (t_{1}, ρ) :: ρ^{'}, [[κ]])$ . Then for all $t$ , $ρ$ , $κ$ and $w$ , $E_{3} (t, ρ, κ) ⇓ w$ if and only if $E_{2} (t, ρ, [[κ]]) ⇓ w$ ; and $A (κ, v) ⇓ w$ if and only if $[[κ]] (v) ⇓ w$ .

Referenced from 8 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Proof of Proposition 135.7 — Defunctionalization is correct

Proof. Simultaneous induction on the two derivations. The interpretation $[[\cdot]]$ was chosen so that each clause of definition 135.6 maps to the corresponding clause of definition 135.4: the index and application clauses are literally the same after substituting $[[K_{1} (t_{1}, ρ, κ)]]$ for the abstraction built in definition 135.4, and the abstraction clause becomes $[[κ]] (Fn (t, ρ))$ by the second half of the statement. The second half is immediate at $K_{0}$ and, at $K_{1}$ , is the first half at the smaller derivation.

The step this proof depends on is that no other abstraction inhabits the continuation space: definition 135.4 builds continuations in exactly two places. If a third were added, the data type would need a third constructor and $[[\cdot]]$ a third clause; if a continuation were built by a function not in the enumerated set, $[[\cdot]]$ would not be defined on it. ◻

Remark 135.8 — The continuation is a stack ¶

The data type $K$ of definition 135.6 has one nullary constructor and one constructor carrying a term, an environment and a $K$ . That is a list whose elements are pairs $(t_{1}, ρ)$ — that is, a stack of thunks. Nothing in the derivation chose that representation: it is what defunctionalizing this particular continuation space produces.

Referenced from 2 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Theorem 135.9 — The derived machine is Krivine's ¶

Identify $Fn (t, ρ)$ with $Th (t, ρ)$ , write the continuation as a list $π$ of thunks, and inline $A$ . The resulting transition system on triples $⟨ t, ρ, π ⟩$ is exactly the three transitions of the opening display, with final states $⟨ λ . t, ρ, ε ⟩$ . Consequently, for a closed $t$ , $⟨ t, ε, ε ⟩ ⟶^{*} ⟨ λ . t^{'}, ρ^{'}, ε ⟩ if and only if E_{0} (t, ε) ⇓ Fn (g)$ for some $g$ with $Fn (g) R_{E} Fn (t^{'}, ρ^{'})$ .

Referenced from 5 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Proof of Theorem 135.9 — The derived machine is Krivine's

Proof. For the identification: inlining $A$ into definition 135.6 replaces the abstraction clause by a case analysis on $κ$ , giving the final state when $κ = K_{0}$ and the third transition when $κ = K_{1} (t_{1}, ρ_{1}, κ^{'})$ ; the index and application clauses are the first two transitions. Since $Fn$ and $Th$ carry the same data, dropping the distinction changes no state.

For the displayed equivalence, compose proposition 135.3, proposition 135.5, proposition 135.7: the first relates $E_{0}$ and $E_{1}$ , the second relates $E_{1}$ and $E_{2}$ at the identity continuation, the third relates $E_{2}$ and $E_{3}$ at $K_{0}$ , whose interpretation is the identity, and the machine is $E_{3}$ . ◻

The four questions the opening asked are now answered by the derivation. Three components, because the evaluator has a term, an environment and a continuation. Thunks on the stack, because call by name wraps the argument. The abstraction rule pops onto the environment, because that is the application clause of definition 135.2. And the strategy is call by name, because that is the strategy of definition 135.1.

Exercise 135.1 ¶

★★☆ Change one clause of definition 135.1 so that the argument of an application is evaluated before the call, and rerun the three transformations. Give the resulting machine’s states and transitions, and say which of them differ from Krivine’s. (Half a page; the continuation space acquires one more inhabiting abstraction.)

Referenced from 2 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Exercise 135.2 ¶

★★☆ Add a constant $c$ and a unary primitive to the source language, extending definition 135.1 in the obvious way. Recompute the set of abstractions inhabiting the continuation space of definition 135.4, and give the resulting data type $K$ and $A$ . Then say which clause of the proof of proposition 135.7 you had to extend.

Referenced from 2 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Defunctionalization in general

Construction 135.10 — Defunctionalization ¶

Fix a set $S = {λ x . M_{i} ∣ 1 \leq i \leq n}$ of abstractions of one type $τ \to τ^{'}$ , where $λ x . M_{i}$ has free variables $x_{1}^{i} : τ_{1}^{i}, \dots, x_{m_{i}}^{i} : τ_{m_{i}}^{i}$ . Then

introduce a data type with one constructor per abstraction, $C_{i} : τ_{1}^{i} \times \dots \times τ_{m_{i}}^{i} \to Arr$ ;
introduce $A (C_{i} ({\vec{x}}^{i}), x) = M_{i}$ , dispatching on the constructor;
replace each $λ x . M_{i}$ by $C_{i} ({\vec{x}}^{i})$ ;
replace each application $f a$ of a value of the function type by $A (f, a)$ .

Referenced from 8 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Convention 135.11 — The closure condition ¶

$S$ must be closed under data flow to call sites: if some element of $S$ can be called at a call site, then every function that can be called at that site is in $S$ .

Referenced from 4 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Convention 135.11 is the hypothesis that makes step 4 well defined, and it is the one that a reader is most likely to skip. Its role is visible in the proof of proposition 135.7: the interpretation $[[\cdot]]$ is a function from the data type onto $S$ , and the correctness argument needs it to be onto.

Proposition 135.12 — The condition is not automatic ¶

There is a program with two abstractions of one type, one call site, and a choice of $S$ containing exactly one of them, for which construction 135.10 produces a program that is not equivalent to the original.

Referenced from 3 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Proof of Proposition 135.12 — The condition is not automatic

Proof. Take $h (b) = (if b then λ x . x else λ x . x + 1) (0)$ and $S = {λ x . x}$ . Construction 135.10 gives $Arr = {C_{1}}$ and $A (C_{1}, x) = x$ , and rewrites the call site to $A (if b then C_{1} else λ x . x + 1, 0)$ , in which $A$ is applied to an abstraction. Either the result does not typecheck, or — in an untyped setting — $A$ has no clause for that argument and the program is stuck at $b = false$ , where the original returns $1$ . ◻

Refunctionalization

Defunctionalization has a left inverse. Applying it to an arbitrary first-order program is not possible; applying it to a program in the image of construction 135.10 is mechanical.

Definition 135.13 — Defunctionalized form ¶

A program is in defunctionalized form with respect to a data type $Arr$ when

exactly one function $A$ of the program eliminates values of $Arr$ , and it does so by a case analysis on the constructor;
every other occurrence of $Arr$ in the program builds a value of it or passes one on; and
$A$ takes a value of $Arr$ and one further argument, and every call of $A$ is saturated.

Referenced from 7 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Construction 135.14 — Refunctionalization ¶

Given a program in defunctionalized form, replace $Arr$ by the function type of $A$ ’s remaining argument and result; replace each $C_{i} (\vec{a})$ by $λ x . M_{i} [\vec{a} / {\vec{x}}^{i}]$ , where $M_{i}$ is the right-hand side of $A$ ’s $i$ th clause; replace each $A (f, a)$ by $f a$ ; and delete $A$ .

Referenced from 6 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Theorem 135.15 — Round trip ¶

Let $P$ be a program and $S$ a set of abstractions satisfying convention 135.11, and let $P^{'}$ be the result of construction 135.10. Then $P^{'}$ is in defunctionalized form with respect to the introduced data type, and construction 135.14 applied to $P^{'}$ returns $P$ up to renaming of bound variables.

Referenced from 4 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Proof of Theorem 135.15 — Round trip

Proof. $P^{'}$ satisfies clause 1 of definition 135.13 because step 2 of construction 135.10 introduces $A$ and step 4 rewrites every application of a value of the function type into a call of $A$ ; no other elimination of $Arr$ is introduced. It satisfies clause 2 because step 3 replaces abstractions by constructor applications and nothing else touches values of $Arr$ . Clause 3 holds because step 4 supplies both arguments.

For the round trip, follow the three replacements. Refunctionalization sends $C_{i} (\vec{a})$ to $λ x . M_{i} [\vec{a} / {\vec{x}}^{i}]$ ; step 3 of construction 135.10 produced $C_{i} ({\vec{x}}^{i})$ at the site of $λ x . M_{i}$ , so the substitution is the identity and the abstraction returns. It sends $A (f, a)$ to $f a$ ; step 4 produced $A (f, a)$ at the site of $f a$ . And it deletes $A$ , which step 2 introduced. Nothing else in $P$ was changed. ◻

The converse composition is not the identity: refunctionalizing a program in defunctionalized form and defunctionalizing the result recovers the program only if the set $S$ chosen the second time is the set of abstractions produced the first time. This is why construction 135.14 is called the left inverse.

Remark 135.16 — Two repairs for a machine that is almost in defunctionalized form ¶

Most published abstract machines are not literally in defunctionalized form, and two syntactic changes usually suffice. Disentangling splits a single transition function that dispatches on several components at once into one function per mode of the machine, so that the component playing the role of the continuation is eliminated in one place; this restores clause 1 of definition 135.13. Merging apply functions replaces several functions that each eliminate the same data type by one, restoring clause 1 when disentangling has produced two eliminators for one type. Neither changes the machine’s transitions; both change which function performs them.

Referenced from 5 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Example 135.17 — Refunctionalizing a machine ¶

Take the call-by-value machine on terms with names, with states $⟨ t, ρ, κ ⟩$ and $⟨ κ, v ⟩$ , values $v = Cl (x, t, ρ)$ , and continuations $κ ::= K_{0} ∣ K_{ar} (t, ρ, κ) ∣ K_{fn} (v, κ)$ . Its two state forms are already disentangled: one function steps a term, the other applies a continuation. The continuation data type is eliminated only by the second, by case analysis, and built in three places, so definition 135.13 holds. Construction 135.14 therefore applies and returns a continuation-passing, closure-converted evaluator; undoing the transformations of section 135.2, section 135.3 returns an ordinary call-by-value evaluator, which differs from definition 135.1 in exactly one clause.

Referenced from 3 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Remark 135.18 — Refunctionalizing always yields a continuation-passing program ¶

The observation of example 135.17 is general for abstract machines: the component being refunctionalized is the one that says what to do next, so the function it becomes is applied in tail position, and the resulting program is in continuation-passing style. That is a statement about the shape of the output, not a theorem about every machine: a machine whose control component is not in defunctionalized form after the repairs of remark 135.16 is not refunctionalized at all.

Referenced from 2 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Exercise 135.3 ¶

★★☆ Give an abstract machine with a single transition function that dispatches simultaneously on the term and on the continuation, and show that it fails clause 1 of definition 135.13. Then disentangle it and check that the result satisfies all three clauses.

Referenced from 2 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Exercise 135.4 ¶

★★☆ Exhibit a first-order program in defunctionalized form whose refunctionalization, when defunctionalized again with a different choice of $S$ , is not the original program. Conclude that construction 135.14 is a left and not a two-sided inverse.

Referenced from 2 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Limits and seminar

The frozen sources are Reynolds (1972) for defunctionalization, Ager, Biernacki, Danvy and Midtgaard (2003) for the correspondence between evaluators and abstract machines, and Danvy and Millikin (2009) for refunctionalization and the two repairs of remark 135.16. The four evaluators of definition 135.1, definition 135.2, definition 135.4, definition 135.6 and the transition system of theorem 135.9 are theirs. Proposition 135.3, Proposition 135.5, Proposition 135.7 are stated in those papers as corollaries of general correctness results for closure conversion, the continuation-passing transformation and defunctionalization; the proofs written here are local, for the selected evaluator only, and are inductions on the big-step derivations of section 135.1. Proposition 135.12, Theorem 135.15 are local.

Four boundaries. First, nothing here is a general correctness theorem for defunctionalization: proposition 135.7 is about one continuation space with two inhabiting abstractions, and theorem 135.15 is a syntactic round-trip statement, not a semantic one. Second, the source language is the pure untyped lambda calculus; laziness with sharing, mutable state, control operators and data types are all absent, and each changes the derived machine. Third, the correspondence is between an evaluator and a machine, not between a machine and a reduction strategy: no theorem here says that Krivine’s machine implements a named reduction relation on terms. Fourth, a machine that distinguishes an instruction set from the terms it runs — a virtual machine — is outside the correspondence as stated; the derivation produces machines that operate on source terms directly.

[4]

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 135.5, then complete exercise 135.8.

Exercise 135.5 ¶

★★★ Landin’s machine has four components: a stack, an environment, a control and a dump. Disentangle its transition function into one function per component in control, identify which component is the defunctionalized continuation, and refunctionalize it. State the evaluator you obtain and say in one sentence why it is a continuation-passing program.

Referenced from 3 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Exercise 135.6 ¶

★★☆ The naive fringe comparison, which flattens both trees and compares the lists, and the iterative one, which walks both trees with an explicit stack, are defunctionalized and refunctionalized counterparts. Write both, exhibit the data type and the apply function that connect them, and check definition 135.13 on the iterative version.

Referenced from 2 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Exercise 135.7 ¶

★★★ Extend definition 135.1 with a single mutable cell, threading a store through the evaluator. Rerun the three transformations and give the resulting machine. Then identify the one degree of freedom in the evaluator — the order in which the store and the continuation are threaded — and give the two different machines it produces.

Referenced from 2 locations

Defunctionalization, Refunctionalization, and Abstract Machines

Exercise 135.8 — Practical: derive the machine ¶

★★★ Practical project.defun-derivation Complete project defun-derivation. Implement the evaluators of definition 135.2, definition 135.6 together with the transition system of theorem 135.9, for the de Bruijn source language of this chapter, and a checker that runs a fixed list of closed terms through all three and compares the results. Implement also the two maps between the data type $K$ and a stack of thunks, and check that their composite is the identity. The invariant the implementation must maintain is proposition 135.7 together with theorem 135.9: on every input the three must agree. If the implementation language is total, note where definition 135.4 cannot be written in it: a function that applies a continuation received as a parameter makes a call to an unknown function, and no syntactic termination check can bound it. That obstruction is itself the reason defunctionalization is worth performing. The named cases print

identity: agree
church-two-succ-zero: agree
call-by-name-discards: agree
krivine-steps: 7
cont-is-stack: ok

The checker is independent evidence on the named inputs. It does not prove proposition 135.3 or proposition 135.5, which relate the two evaluators the implementation does not contain, and it does not implement refunctionalization or the repairs of remark 135.16.

Referenced from 3 locations