Faithfulness of the VLISP Operational Semantics

William M. Farmer  Joshua D. Guttman  Leonard G. Monk
John D. Ramsdell  Vipin Swarup

The MITRE Corporation^{1} M92B093 September 1992

1This work was supported by Rome Laboratories of the United States Air Force, contract No. F19628-89-C-0001. Authors’ address: The MITRE Corporation, 202 Burlington Road, Bedford MA, 01730-1420. \begin{matrix}c \\ ◯ \end{matrix}1992 The MITRE Corporation. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the MITRE copyright notice and the title of the publication and its date appear, and notice in given that copying is by permission of the MITRE Corporation.

Abstract

The Verified Programming Language Implementation project has developed a formally verified implementation of the Scheme programming language. This report provides a detailed proof that the operational semantics for the highest-level interpreter (virtual machine) is faithful to the denotational semantics used in the byte-code compiler proof.

Contents

1 Introduction 1 2 Denotational Answers 1 3 Operational Answers 3 4 Normal States and Faithfulness 4 5 The Faithfulness Theorem 4 6 Proof of Lemma 5.3 7 7 Proof of Lemma 5.4 34 References 36

1 Introduction

The vlisp project employs two kinds of semantics: one denotational and the other operational. This paper shows that the operational semantics is faithful to the denotational semantics. (The precise definition of faithfulness is given in section 4.) The two semantics are compared at the Tabular Byte Code (tbc) level, since tbc is assigned both kinds of semantics. (tbc is defined in [2].) The denotational semantics for tbc is presented as a set of equations in [1], and the operational semantics for tbc is defined by a state machine in [2]. This paper assumes familiarity with both [1] and [2].

The Augmented Byte Code (abc) is an expansion of tbc defined in [2]. An abc state is a finite sequence Σ of the form

⟨t, b, v, a, u, k, s⟩,

with the abuse of notation that b is allowed to be ⟨⟩. We assign each abc state a denotational answer a ∈ A such that a : R or a = ⊥_{A}. We also assign each abc state an operational answer a′ ∈ A with a′ : R, provided the state has a correctly terminating program run (in the operational semantics). Faithfulness is defined in terms of the denotational and operational answers assigned to well-structured abc states—so-called “normal” states.

We will not consider the two semantics in detail for vectors and strings since their semantics is not essentially different from the semantics for pairs.

2 Denotational Answers

We define in this section the notion of a denotational answer of an abc state, using some of the (denotational) semantic functions for tbc given in [1]. Our definition requires the following new semantic functions:

D_{v} : v → E

D_{a} : v^{∗} → E^{∗}

D_{u} : u → N → N → L

D_{k} : k → E → C

D_{s} : v^{∗} → E^{∗}

The definitions of the functions take two parameters:

(1) a function ρ_{G} : Ide → L known as globals, and (2) a function K′ : Con → E known as immutables such that K′ ⊆ K,

K′(p) is defined only if p has the form ⟨immutable-pair c_{1} c_{2}⟩, and K′(p) : L × L × {immutable} if K′(p) is defined.

Also, for f : A → B, f^{(∗)} : A^{∗} → B^{∗} is defined by

f^{(∗)}(⟨a_{1}, …, a_{n}⟩) = ⟨f(a_{1}), …, f(a_{n})⟩,

and f^{[∗]} : A^{∗} → B^{∗} is defined by

f^{[∗]}(⟨a_{1}, …, a_{n}⟩) = ⟨f(a_{n}), …, f(a_{1})⟩.

The semantic functions are defined by the following equations:

D_{v}[[c]] = K[[c]]. D_{v}[[⟨closure t u l⟩]] = fix(λϵ.⟨l, (λϵ^{∗}κ.T_{τ} [[t]]ρ_{G}ϵϵ^{∗}D_{u}[[u]](λϵ.κ⟨ϵ⟩))⟩) in E. D_{v}[[⟨escape k l⟩]] = ⟨l, single arg(λϵκ.D_{k}[[k]]ϵ)⟩ in E. D_{v}[[⟨mutable-pair l_{1} l_{2}⟩]] = ⟨l_{1}, l_{2}, mutable⟩ in E. D_{v}[[⟨string l^{∗}⟩]] = ⟨l^{∗}, mutable⟩ in E. D_{v}[[⟨vector l^{∗}⟩]] = ⟨l^{∗}, mutable⟩ in E. D_{v}[[not-specified]] = unspecified in E. D_{v}[[undefined]] = empty in E.

D_{a} = D_{v}^{[∗]}.

D_{u}[[empty-env]] = (λν_{1}ν_{2}.⊥). D_{u}[[⟨env u l^{∗}⟩]] = extend_{R} D_{u}[[u]](rev l^{∗}).

D_{k}[[halt]] = (λϵσ.ϵ : R → ϵ|R in A, ⊥). D_{k}[[⟨cont ⟨template b_{0} e⟩ b a u k⟩]] = λϵ.B_{τ} [[b]]eρ_{G}ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]].

D_{s} = D_{v}^{(∗)}.

Note that the following identities hold:

(1) T_{τ} [[⟨template b e⟩]] = B_{τ} [[b]]e.

(2) D_{v}[[⟨immutable-pair c_{1} c_{2}⟩]] = K′[[⟨immutable-pair c_{1} c_{2}⟩]].

The denotational answer of an abc state Σ = ⟨t, b, v, a, u, k, s⟩, denoted D[[Σ]], is the value of

B_{τ} [[b]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]].

3 Operational Answers

The operational semantics for tbc is defined by the Tabular Byte Code State Machine presented in [2]. The machine actions are specified by a set of rules called abc rules. We define in this section the notion of a operational answer of an abc state, using the abc rules.

The operational answer of an abc state Σ, denoted O[[Σ]], is defined inductively by:

(1) If b = ⟨⟩ and v ∈ R, then O[[Σ]] = D_{v}[[v]]|R in A.

(2) If b = ⟨⟩ and v ∉ R, then O[[Σ]] is undefined.

(3) If b ≠ ⟨⟩, then O[[Σ]] is the unique a ∈ A for which there is an abc rule R such that a = O[[R(Σ)]] (and is undefined if there is no such unique a).

Note that, by the definition of K on R (see [1]), if v ∈ R, then D_{v}[[v]] : R.

O′[[Σ]] is defined exactly like O[[Σ]] except that the following rule is used in place of the Make Environment abc rule:

Rule: Alternate Make Environment Domain Conditions:

b = ⟨make-env #a⟩ :: b_{1} Changes:

b′ = b_{1}

a′ = ⟨⟩

u′ = add-layer′(u, #s, #a)

s′ = s^{⌢}(rev a)

where add-layer′ is defined by:

add-layer′(u, n_{0}, n_{1}) = \{ \begin{matrix}⟨env u ⟨(n_{0} + n_{1} − 1) ⋯ n_{0}⟩⟩ & if n_{1} > 0 \\ ⟨env u ⟨⟩⟩ & if n_{1} = 0 \end{matrix}

The special rules are Alternate Make Environment and the abc rules other than Make Environment.

4 Normal States and Faithfulness

Let Σ = ⟨⟨template b_{0} e⟩, b, v, a, u, k, s⟩ be an abc state. The functions L_{glo}, L_{env}, L_{mp}, L_{ip}, which map abc states to finite sets of locations, are defined by the following equations:

L_{glo}(Σ) = ran(ρ_{G}).

L_{env}(Σ) = {env-reference(u′, n_{0}, n_{1}) : u′ occurs in Σ, n_{0}, n_{1} ∈ N,

and env-reference(u′, n_{0}, n_{1}) is defined.}.

L_{mp}(Σ) = {l_{1}, l_{2} ∈ L : ⟨mutable-pair l_{1} l_{2}⟩ occurs in Σ}.

L_{ip}(Σ) = {l_{1}, l_{2} ∈ L : p = ⟨immutable-pair c_{1} c_{2}⟩ occurs Σ and

(K′[[p]]|L × L × {immutable}) = ⟨l_{1}, l_{2}, immutable⟩}.

Σ is normal if the following conditions hold:

(1) L_{glo}(Σ) ∪ L_{env}(Σ) ∪ L_{ip}(Σ) ∪ L_{mp}(Σ) ⊆ dom(s).

(2) L_{glo}(Σ), L_{env}(Σ), L_{ip}(Σ), L_{mp}(Σ) are pairwise disjoint.

(3) For each p = ⟨immutable-pair c_{1} c_{2}⟩ occurring in Σ, there are l_{1}, l_{2} ∈ L such that (K′[[p]]|L × L × {immutable}) = ⟨l_{1}, l_{2}, immutable⟩, s(l_{1}) = c_{1}, and s(l_{2}) = c_{2}.

A initial state for a tbc template t = ⟨template b e⟩ is any normal abc state of the form

⟨t, b, not-specified, ⟨⟩, empty-env, halt, s⟩.

The operational semantics for tbc is faithful if, for all tbc templates t and all initial states Σ for t, D[[Σ]] = O[[Σ]] whenever O[[Σ]] is defined.

5 The Faithfulness Theorem

In this section, we shall prove that the operational semantics for tbc is faithful.

Lemma 5.1 If Σ is a normal abc state, R is an abc or special rule, and Σ′ = R(Σ), then Σ′ is also a normal abc state.

Proof Let Σ = ⟨t, b, v, a, u, k, s⟩ be a normal abc state, R be an abc or special rule, and Σ′ = ⟨t′, b′, v′, a′, u′, k′, s′⟩ = R(Σ). Σ′ is certainly normal if:

(1) s is a subfunction of s′ and

(2) Σ and Σ′ contain exactly the same environments, mutable pairs, and immutable pairs.

There are just seven abc or special rules which cause (1) or (2) to fail to hold: Set Global, Set Local, Make Environment, Alternate Make Environment, Make Rest List, Primitive Cons, and Primitive Set-car!.

Set Global modifies the value in s at a location in L_{glo}, but creates no new environments, mutable pairs, or immutable pairs.

Set Local modifies the value in s at a location in L_{env}, but creates no new environments, mutable pairs, or immutable pairs.

Make Environment and Alternate Make Environment both extend the store s to s′ and increases u to u′. However,

L_{env}(Σ′) \ L_{env}(Σ) = dom(s′) \ dom(s).

Also, Make Environment and Alternate Make Environment both create no new mutable pairs or immutable pairs and no other new environments.

Make Rest List extends the store s to s′ and makes new mutable pairs. However,

L_{mp}(Σ′) \ L_{mp}(Σ) ⊆ dom(s′) \ dom(s).

Also, Make Rest List creates no new immutable pairs or environments.

Primitive Cons extends the store s to s′ and sets v′ to a new mutable pair ⟨mutable-pair l_{1} l_{2}⟩. However, dom(s′)\dom(s) = {l_{1}, l_{2}}. Also, Primitive Cons creates no new environments or immutable pairs and no other mutable pairs.

Primitive Set-car! modifies the value in s at a location in L_{mp}, but creates no new environments, mutable pairs, or immutable pairs.

Therefore, Σ′ is normal when R is any one of these seven rules. □

Lemma 5.2 If Σ = ⟨t, ⟨⟩, v, a, u, k, s⟩ is a normal abc state with v ∈ R, then D[[Σ]] = D_{v}[[v]]|R in A.

Proof Let Σ = ⟨⟨template b e⟩, ⟨⟩, v, a, u, k, s⟩ be a normal abc state with v ∈ R.

D[[Σ]] = B_{τ} [[⟨⟩]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρϵϵ^{∗}ρ_{R}ψσ.ϵ : R → ϵ|R in A, ⊥)
eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D_{v}[[v]]|R in A

since v ∈ R implies D_{v}[[v]] : R.□

The proof of the following lemma is postponed until section 6.

Lemma 5.3 If Σ and Σ′ are normal abc states such that O′[[Σ]] is defined and Σ′ = R(Σ) for some special rule R, then D[[Σ]] = D[[Σ′]].

The proof of the next lemma is postponed until section 7.

Lemma 5.4 For each tbc template t and initial state Σ for t, if O[[Σ]] is defined, then O[[Σ]] = O′[[Σ]].

Theorem 5.5 The operational semantics for tbc is faithful.

Proof Let t = ⟨template b e⟩ be a tbc template, and let

Σ = ⟨t, b, not-specified, ⟨⟩, empty-env, halt, s⟩

be an initial state for t. Assume O[[Σ]] = a, and so by Lemma 5.4, O′[[Σ]] = a. We shall show that D[[Σ]] = a.

Since O′[[Σ]] is defined, there is a finite sequence Σ_{0}, …, Σ_{n} of abc states and a finite sequence R_{1}, …, R_{n} of special rules such that:

(1) Σ = Σ_{0} and 0 ≤ n.

(2) R_{i+1}(Σ_{i}) = Σ_{i+1} for all i with 0 ≤ i ≤ n − 1.

(3) Σ_{n} has the form ⟨t′, ⟨⟩, v, a, u, k, s′⟩ with (D_{v}[[v]]|R in A) = a.

Σ_{i} is normal for all i with 1 ≤ i ≤ n by Lemma 5.1, and O′[[Σ_{i}]] = a for all i with 0 ≤ i ≤ n by the definition of O′. Thus D[[Σ_{n}]] = a by Lemma 5.2, and D[[Σ_{i}]] = D[[Σ_{i+1}]] for all i with 0 ≤ i ≤ n − 1 by Lemma 5.3. Therefore, D[[Σ]] = a = O[[Σ]]. □

6 Proof of Lemma 5.3

We use in the proof of Lemma 5.3 the following easily verified facts: • #D_{a}[[a]] = #a.

• #D_{s}[[s]] = #s.

• D_{v}[[v]] = false in E iff v = false.

• single ψ⟨ϵ⟩ = ψϵ (and so λϵ.single ψ⟨ϵ⟩ = ψ).

• If l ≤ #σ, then update lϵσ = σ[ϵ/l] (and so update (new σ)ϵσ = σ[ϵ/#σ]).

The proof of Lemma 5.3 breaks down into 34 cases, one for each special rule. Let Σ and Σ′ be normal abc states such that O′[[Σ]] is defined and Σ′ = R(Σ) for some special rule R. To prove Lemma 5.3, we must show that, for each special rule R, if Σ satisfies the domain conditions of R, then D[[Σ]] = D[[Σ′]].

Case 1: R = Return-Halt. Let Σ = ⟨t, ⟨⟨return⟩⟩, v, a, u, halt, s⟩. Then R(Σ) = Σ′ = ⟨t, ⟨⟩, v, a, u, halt, s⟩.

D[[Σ]] = B_{τ} [[⟨⟨return⟩⟩]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[halt]]D_{s}[[s]]
= (λeρ.return)eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[halt]]D_{s}[[s]]
= returnD_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[halt]]D_{s}[[s]]
= (λϵϵ^{∗}ρ_{R}ψ.ψϵ)D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[halt]]D_{s}[[s]]
= D_{k}[[halt]]D_{v}[[v]]D_{s}[[s]]
= (λϵσ.ϵ : R → ϵ|R in A, ⊥)D_{v}[[v]]D_{s}[[s]]
= (λeρϵϵ^{∗}ρ_{R}ψσ.ϵ : R → ϵ|R in A, ⊥)
eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= B_{τ} [[⟨⟨⟩⟩]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[halt]]D_{s}[[s]]
= D[[Σ′]]

Case 2: R = Return. Let Σ = ⟨⟨template b e⟩, ⟨⟨return⟩⟩, v, a, u, k, s⟩, where k = ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ and t_{1} = ⟨template b′ e_{1}⟩. Then R(Σ) = Σ′ = ⟨t_{1}, b_{1}, v, a_{1}, u_{1}, k_{1}, s⟩.

D[[Σ]] = B_{τ} [[⟨⟨return⟩⟩]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.return)eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= returnD_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λϵϵ^{∗}ρ_{R}ψ.ψϵ)D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D_{k}[[k]]D_{v}[[v]]D_{s}[[s]]
= (λϵ.B_{τ} [[b_{1}]]e_{1}ρ_{G}ϵD_{a}[[a_{1}]]D_{u}[[u_{1}]]D_{k}[[k_{1}]])D_{v}[[v]]D_{s}[[s]]
= B_{τ} [[b_{1}]]e_{1}ρ_{G}D_{v}[[v]]D_{a}[[a_{1}]]D_{u}[[u_{1}]]D_{k}[[k_{1}]]D_{s}[[s]]
= D[[Σ′]]

Case 3: R = Call. Let Σ = ⟨⟨template b e⟩, ⟨⟨call #a⟩⟩, v, a, u, k, s⟩, where v = ⟨closure t_{1} u_{1} l_{1}⟩ and t_{1} = ⟨template b_{1} e_{1}⟩. Then R(Σ) = Σ′ = ⟨t_{1}, b_{1}, v, a, u_{1}, k, s⟩.

D[[Σ]] = B_{τ} [[⟨⟨call #a⟩⟩]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.call #a)eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= call #aD_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λνϵϵ^{∗}ρ_{R}ψ.#ϵ^{∗} = ν → applicate ϵϵ^{∗}(single ψ),

wrong “bad stack”)#aD_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (#D_{a}[[a]] = #a → applicate D_{v}[[v]]D_{a}[[a]](single D_{k}[[k]]),

wrong “bad stack”)D_{s}[[s]]

= applicate D_{v}[[v]]D_{a}[[a]](single D_{k}[[k]])D_{s}[[s]]
= (λϵϵ^{∗}κ.ϵ : F → ((ϵ|F)1)ϵ^{∗}κ, wrong “bad procedure”)

D_{v}[[v]]D_{a}[[a]](single D_{k}[[k]])D_{s}[[s]]

= (D_{v}[[v]] : F → ((D_{v}[[v]]|F)1)D_{a}[[a]](single D_{k}[[k]]),

wrong “bad procedure”)D_{s}[[s]]

= (λϵ^{∗}κ.T_{τ} [[t_{1}]]ρ_{G}D_{v}[[v]]ϵ^{∗}D_{u}[[u_{1}]](λϵ.κ⟨ϵ⟩))

D_{a}[[a]](single D_{k}[[k]])D_{s}[[s]]
= T_{τ} [[t_{1}]]ρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u_{1}]](λϵ.single D_{k}[[k]]⟨ϵ⟩)D_{s}[[s]]
= B_{τ} [[b_{1}]]e_{1}ρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u_{1}]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 4: R = Escape-Halt. Let Σ = ⟨t, ⟨⟨call 1⟩⟩, v, a, u, k, s⟩, where v = ⟨escape halt l⟩. Then R(Σ) = Σ′ = ⟨t, ⟨⟩, v, a, u, k, s⟩. O′[[Σ′]] is undefined since v ∉ R. Thus O′[[Σ]] is undefined, and so we do not have to consider this case.

Case 5: R = Escape. Let Σ = ⟨⟨template b e⟩, ⟨⟨call 1⟩⟩, v, ⟨v_{1}⟩, u, k, s⟩, where v = ⟨escape k′ l⟩, k′ = ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩, and t_{1} =

⟨template b′ e_{1}⟩.

Then R(Σ) = Σ′ = ⟨t_{1}, b_{1}, v_{1}, a_{1}, u_{1}, k_{1}, s⟩.

D[[Σ]] = B_{τ} [[⟨⟨call 1⟩⟩]]eρ_{G}D_{v}[[v]]D_{a}[[⟨v_{1}⟩]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.call 1)eρ_{G}D_{v}[[v]]D_{a}[[⟨v_{1}⟩]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= call 1 D_{v}[[v]]D_{a}[[⟨v_{1}⟩]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λνϵϵ^{∗}ρ_{R}ψ.#ϵ^{∗} = ν → applicate ϵϵ^{∗}(single ψ),

wrong “bad stack”) 1 D_{v}[[v]]D_{a}[[⟨v_{1}⟩]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (#D_{a}[[⟨v_{1}⟩]] = 1 → applicate D_{v}[[v]]D_{a}[[⟨v_{1}⟩]](single D_{k}[[k]]),

wrong “bad stack”)D_{s}[[s]]

= applicate D_{v}[[v]]D_{a}[[⟨v_{1}⟩]](single D_{k}[[k]])D_{s}[[s]]
= (λϵϵ^{∗}κ.ϵ : F → ((ϵ|F)1)ϵ^{∗}κ, wrong “bad procedure”)

D_{v}[[v]]D_{a}[[⟨v_{1}⟩]](single D_{k}[[k]])D_{s}[[s]]

= (D_{v}[[v]] : F → ((D_{v}[[v]]|F)1)D_{a}[[⟨v_{1}⟩]](single D_{k}[[k]]),

wrong “bad procedure”)D_{s}[[s]]

= single arg(λϵκ.D_{k}[[k′]]ϵ)D_{a}[[⟨v_{1}⟩]](single D_{k}[[k]])D_{s}[[s]]

= (λϵκ.D_{k}[[k′]]ϵ)(D_{a}[[⟨v_{1}⟩]]0)(single D_{k}[[k]])D_{s}[[s]]
= D_{k}[[k′]]D_{v}[[v_{1}]]D_{s}[[s]]
= (λϵ.B_{τ} [[b_{1}]]e_{1}ρ_{G}ϵD_{a}[[a_{1}]]D_{u}[[u_{1}]]D_{k}[[k_{1}]])D_{v}[[v_{1}]]D_{s}[[s]]
= B_{τ} [[b_{1}]]e_{1}ρ_{G}D_{v}[[v_{1}]]D_{a}[[a_{1}]]D_{u}[[u_{1}]]D_{k}[[k_{1}]]D_{s}[[s]]
= D[[Σ′]]

Case 6: R = Closed Branch/True. Let Σ = ⟨t, ⟨⟨unless-false b_{1} b_{2}⟩⟩, v, a, u, k, s⟩, where t = ⟨template b e⟩ and v ≠ false. Then R(Σ) = Σ′ = ⟨t, b_{1}, v, a, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨⟨unless-false b_{1} b_{2}⟩⟩]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.if truish(B_{τ} [[b_{1}]]eρ)(B_{τ} [[b_{2}]]eρ))eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]
D_{s}[[s]]
= if truish(B_{τ} [[b_{1}]]eρ_{G})(B_{τ} [[b_{2}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λπ_{1}π_{2}ϵϵ^{∗}ρ_{R}ψ.truish ϵ → π_{1}ϵϵ^{∗}ρ_{R}ψ, π_{2}ϵϵ^{∗}ρ_{R}ψ)
(B_{τ} [[b_{1}]]eρ_{G})(B_{τ} [[b_{2}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 7: R = Closed Branch/False. Let Σ = ⟨t, ⟨⟨unless-false b_{1} b_{2}⟩⟩, v, a, u, k, s⟩, where t = ⟨template b e⟩ and v = false. Then R(Σ) = Σ′ = ⟨t, b_{2}, v, a, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨⟨unless-false b_{1} b_{2}⟩⟩]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.if truish(B_{τ} [[b_{1}]]eρ)(B_{τ} [[b_{2}]]eρ))eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]
D_{s}[[s]]
= if truish(B_{τ} [[b_{1}]]eρ_{G})(B_{τ} [[b_{2}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λπ_{1}π_{2}ϵϵ^{∗}ρ_{R}ψ.truish ϵ → π_{1}ϵϵ^{∗}ρ_{R}ψ, π_{2}ϵϵ^{∗}ρ_{R}ψ)
(B_{τ} [[b_{1}]]eρ_{G})(B_{τ} [[b_{2}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (B_{τ} [[b_{2}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 8: R = Open Branch/True. Let Σ = ⟨t, ⟨unless-false y_{1} y_{2}⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩ and v ≠ false. Then R(Σ) = Σ′ = ⟨t, y_{1}^{⌣}b_{1}, v, a, u, k, s⟩. First, we shall show that

Y_{τ} [[y_{1}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}) = B_{τ} [[y_{1}^{⌣}b_{1}]]eρ_{G}

by induction on the structure of y_{1}. There are four cases depending on the form of y_{1}:

(1) Assume y_{1} = ⟨z⟩. Then

Y_{τ} [[y_{1}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}) = (λeρπ.Z_{τ} [[z]]eρ(Y_{τ} [[⟨⟩]]eρπ))
eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})
= Z_{τ} [[⟨z⟩]]eρ_{G}((λeρπ.π)eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}))
= Z_{τ} [[⟨z⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})
= (λeρ.Z_{τ} [[⟨z⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}
= B_{τ} [[z :: b_{1}]]eρ_{G}
= B_{τ} [[y_{1}^{⌣}b_{1}]]eρ_{G}

(2) Assume y_{1} = z :: y′. Then

Y_{τ} [[y_{1}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}) = (λeρπ.Z_{τ} [[z]]eρ(Y_{τ} [[y′]]eρπ))

eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

= Z_{τ} [[z]]eρ_{G}(Y_{τ} [[y′]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}))
= Z_{τ} [[z]]eρ_{G}(B_{τ} [[y′^{⌣}b_{1}]]eρ_{G})
= (λeρ.Z_{τ} [[z]]eρ(B_{τ} [[y′^{⌣}b_{1}]]eρ))eρ_{G}
= B_{τ} [[z :: y′^{⌣}b_{1}]]eρ_{G}
= B_{τ} [[y_{1}^{⌣}b_{1}]]eρ_{G}

(3) Assume y_{1} = ⟨make-cont ⟨⟩ n⟩ :: b′. Then

Y_{τ} [[y_{1}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}) = (λeρπ.make cont(Y_{τ} [[⟨⟩]]eρπ)n(B_{τ} [[b′]]eρ))
eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})
= make cont(Y_{τ} [[⟨⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}))
n(B_{τ} [[b′]]eρ_{G})
= make cont((λeρπ.π)eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}))
n(B_{τ} [[b′]]eρ_{G})
= make cont(B_{τ} [[b_{1}]]eρ_{G})n(B_{τ} [[b′]]eρ_{G})
= (λeρ.make cont(B_{τ} [[b_{1}]]eρ)n(B_{τ} [[b′]]eρ))eρ_{G}
= B_{τ} [[⟨make-cont b_{1} n⟩ :: b′]]eρ_{G}
= B_{τ} [[y_{1}^{⌣}b_{1}]]eρ_{G}

(4) Assume y_{1} = ⟨make-cont y′ n⟩ :: b′. Then

Y_{τ} [[y_{1}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}) = (λeρπ.make cont(Y_{τ} [[y′]]eρπ)n(B_{τ} [[b′]]eρ))
eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})
= make cont(Y_{τ} [[y′]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}))
n(B_{τ} [[b′]]eρ_{G})
= make cont(B_{τ} [[y′^{⌣}b_{1}]]eρ_{G})n(B_{τ} [[b′]]eρ_{G})
= (λeρ.make cont(B_{τ} [[y′^{⌣}b_{1}]]eρ)n(B_{τ} [[b′]]eρ))
eρ_{G}
= B_{τ} [[⟨make-cont y′^{⌣}b_{1} n⟩ :: b′]]eρ_{G}
= B_{τ} [[y_{1}^{⌣}b_{1}]]eρ_{G}

Finally,

D[[Σ]] = B_{τ} [[⟨unless-false y_{1} y_{2}⟩ :: b_{1}]]eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.Z_{τ} [[⟨unless-false y_{1} y_{2}⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨unless-false y_{1} y_{2}⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπ.if truish(Y_{τ} [[y_{1}]]eρπ)(Y_{τ} [[y_{2}]]eρπ))eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= if truish(Y_{τ} [[y_{1}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}))(Y_{τ} [[y_{2}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}))
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λπ_{1}π_{2}ϵϵ^{∗}ρ_{R}ψ.truish ϵ → π_{1}ϵϵ^{∗}ρ_{R}ψ, π_{2}ϵϵ^{∗}ρ_{R}ψ)

(Y_{τ} [[y_{1}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}))(Y_{τ} [[y_{2}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G}))

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= Y_{τ} [[y_{1}]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= B_{τ} [[y_{1}^{⌣}b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 9: R = Open Branch/False. Let Σ = ⟨t, ⟨unless-false y_{1} y_{2}⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩ and v = false. Then R(Σ) = Σ′ = ⟨t, y_{2}^{⌣}b_{1}, v, a, u, k, s⟩. The proof of this case is to the proof of Case 8 as the proof of Case 7 is to the proof of Case 6.

Case 10: R = Make Continuation. Let Σ = ⟨t, ⟨make-cont b_{1} #a⟩ :: b_{2}, v, a, u, k, s⟩, where t = ⟨template b e⟩. Then R(Σ) = Σ′ = ⟨t, b_{2}, v, ⟨⟩, u, k′, s⟩, where k′ = ⟨cont t b_{1} a u k⟩.

D[[Σ]] = B_{τ} [[⟨make-cont b_{1} #a⟩ :: b_{2}]]eρ_{G}
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.make cont(B_{τ} [[b_{1}]]eρ)#a(B_{τ} [[b_{2}]]eρ))eρ_{G}
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= make cont(B_{τ} [[b_{1}]]eρ_{G})#a(B_{τ} [[b_{2}]]eρ_{G})
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λπ′νπϵϵ^{∗}ρ_{R}ψ.#ϵ^{∗} = ν → πϵ⟨⟩ρ_{R}(λϵ.π′ϵϵ^{∗}ρ_{R}ψ),

wrong “bad stack”)(B_{τ} [[b_{1}]]eρ_{G})#a(B_{τ} [[b_{2}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (#D_{a}[[a]] = #a → B_{τ} [[b_{2}]]eρ_{G}D_{v}[[v]]⟨⟩D_{u}[[u]]

(λϵ.B_{τ} [[b_{1}]]eρ_{G}ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]]), wrong “bad stack”)D_{s}[[s]]

= B_{τ} [[b_{2}]]eρ_{G}D_{v}[[v]]⟨⟩D_{u}[[u]](λϵ.(B_{τ} [[b_{1}]]eρ_{G})ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]])

D_{s}[[s]]

= D[[Σ′]]

Case 11: R = Literal. Let Σ = ⟨t, ⟨literal n⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩ and e(n) = ⟨constant c⟩. Then R(Σ) = Σ′ = ⟨t, b_{1}, c, a, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨literal n⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨literal n⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨literal n⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.literal(K[[(e(n))(1)]])eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= literal(K[[(e(n))(1)]])(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λϵ′πϵϵ^{∗}ρ_{R}ψ.πϵ′ϵ^{∗}ρ_{R}ψ)K[[c]](B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}K[[c]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 12: R = Closure. Let Σ = ⟨t, ⟨closure n⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩ and e(n) = ⟨template b_{2} e_{2}⟩. Then R(Σ) = Σ′ = ⟨t, b_{1}, v′, a, u, k, s′⟩, where v′ = ⟨closure e(n) u #s⟩ and s′ = s^{⌢}⟨not-specified⟩.

D[[Σ]] = B_{τ} [[⟨closure n⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨closure n⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨closure n⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.closure(T_{τ} [[e(n)]]ρ))eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= closure(T_{τ} [[e(n)]]ρ_{G}))(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λπ′πϵϵ^{∗}ρ_{R}ψσ.π(fix(λϵ.⟨new σ, λϵ^{∗}κ.π′ϵϵ^{∗}ρ_{R}(λϵ.κ⟨ϵ⟩)⟩ in E))

ϵ^{∗}ρ_{R}ψ(update(new σ)(unspecified in E) σ)) (B_{τ} [[b_{2}]]e_{2}ρ_{G})(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}

(fix(λϵ.⟨new D_{s}[[s]], λϵ^{∗}κ.B_{τ} [[b_{2}]]e_{2}ρ_{G}ϵϵ^{∗}D_{u}[[u]](λϵ.κ⟨ϵ⟩)⟩ in E)) D_{a}[[a]]D_{u}[[u]]D_{k}[[k]](update(new D_{s}[[s]])(unspecified in E) D_{s}[[s]])

= B_{τ} [[b_{1}]]eρ_{G}D_{v}[[⟨closure e(n) u (new D_{s}[[s]])⟩]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]

(update(new D_{s}[[s]])(unspecified in E) D_{s}[[s]])

= B_{τ} [[b_{1}]]eρ_{G}D_{v}[[v′]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]

D_{s}[[s]][(unspecified in E)/#D_{s}[[s]]]

= D[[Σ′]]

Case 13: R = Global. Let Σ = ⟨t, ⟨global n⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩ and e(n) = ⟨global-variable i⟩, ρ_{G}(i) = l, and v_{1} = s(l) ≠ undefined. Then R(Σ) = Σ′ = ⟨t, b_{1}, v_{1}, a, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨global n⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨global n⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨global n⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.global(lookup ρ (e(n))(1)))eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= global(lookup ρ_{G} (e(n))(1))(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λαπϵϵ^{∗}ρ_{R}ψ.hold α(single(λϵ.ϵ ≠ (empty in E) → πϵϵ^{∗}ρ_{R}ψ,

wrong “undefined variable”)))

(ρ_{G}i)(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= hold l(single(λϵ.ϵ ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}

ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]], wrong “undefined variable”))D_{s}[[s]]

= (λακσ.α < #σ → send(σα)κσ, empty in E)

l(single(λϵ.ϵ ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}

ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]], wrong “undefined variable”))D_{s}[[s]]

= send(D_{s}[[s]]l)(single(λϵ.ϵ ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}

ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]], wrong “undefined variable”))D_{s}[[s]]

= (single(λϵ.ϵ ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}

ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]], wrong “undefined variable”))⟨D_{s}[[s]]l⟩D_{s}[[s]]

= (D_{s}[[s]]l ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}

(D_{s}[[s]]l)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]], wrong “undefined variable”)D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}(D_{s}[[s]]l)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 14: R = Set Global.

Let Σ = ⟨t, ⟨set-global! n⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩, e(n) = ⟨global-variable i⟩, ρ_{G}(i) = l, and l ≤ #s.

Then R(Σ) = Σ′ = ⟨t, b_{1}, not-specified, a, u, k, s′⟩, where s′ = s + {l ↦ v}.

D[[Σ]] = B_{τ} [[⟨set-global! n⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨set-global! n⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= Z_{τ} [[⟨set-global! n⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.set global(lookup ρ ((e(n))(1))))eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= set global(lookup ρ_{G} ((e(n))(1)))(B_{τ} [[b_{1}]]eρ_{G})
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λαπϵϵ^{∗}ρ_{R}ψ.assign αϵ(π (unspecified in E) ϵ^{∗}ρ_{R}ψ))
(ρ_{G}i)(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= assign lD_{v}[[v]]
(B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]])D_{s}[[s]]
= (λαϵθσ.θ(update αϵσ))

lD_{v}[[v]](B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]])D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]
(update lD_{v}[[v]]D_{s}[[s]])
= B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]
D_{s}[[s]][D_{v}[[v]]/l]
= B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s′]]
= D[[Σ′]]

Case 15: R = Local.

Let Σ = ⟨t, ⟨local n_{1} n_{2}⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩, env-reference(u, n_{1}, n_{2}) = l, and v_{1} = s(l) ≠ undefined.

Then R(Σ) = Σ′ = ⟨t, b_{1}, v_{1}, a, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨local n_{1} n_{2}⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨local n_{1} n_{2}⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨local n_{1} n_{2}⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.local n_{1}n_{2})eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= local n_{1}n_{2}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λν_{1}ν_{2}πϵϵ^{∗}ρ_{R}ψ.hold(ρ_{R}ν_{1}ν_{2})(single(λϵ.ϵ ≠ (empty in E) →

πϵϵ^{∗}ρ_{R}ψ, wrong “undefined variable”))) n_{1}n_{2}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= hold(D_{u}[[u]]n_{1}n_{2})

(single(λϵ.ϵ ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]], wrong “undefined variable”))D_{s}[[s]]

= (λακσ.α < #σ → send(σα)κσ, empty in E)l

(single(λϵ.ϵ ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]], wrong “undefined variable”))D_{s}[[s]]

= send(D_{s}[[s]]l)

(single(λϵ.ϵ ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]], wrong “undefined variable”)D_{s}[[s]]

= (λϵκ.κ⟨ϵ⟩)(D_{s}[[s]]l)

(single(λϵ.ϵ ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]], wrong “undefined variable”)D_{s}[[s]])

= (single(λϵ.ϵ ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]],

wrong “undefined variable”)⟨D_{s}[[s]]l⟩D_{s}[[s]]

= D_{s}[[s]]l ≠ (empty in E) → B_{τ} [[b_{1}]]eρ_{G}(D_{s}[[s]]l)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]],

wrong “undefined variable”)D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}(D_{s}[[s]]l)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 16: R = Set Local. Let Σ = ⟨t, ⟨set-local! n_{1} n_{2}⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩, env-reference(u, n_{1}, n_{2}) = l, and l ≤ #s. Then R(Σ) = Σ′ = ⟨t, b_{1}, not-specified, a, u, k, s′⟩, where s′ = s + {l ↦ v}.

D[[Σ]] = B_{τ} [[⟨set-local! n_{1} n_{2}⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨set-local! n_{1} n_{2}⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= Z_{τ} [[⟨set-local! n_{1} n_{2}⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.set local n_{1}n_{2})eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= set local n_{1}n_{2}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λν_{1}ν_{2}πϵϵ^{∗}ρ_{R}ψ.assign(ρ_{R}ν_{1}ν_{2})ϵ(π(unspecified in E)ϵ^{∗}ρ_{R}ψ))
n_{1}n_{2}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= assign(D_{u}[[u]]n_{1}n_{2})D_{v}[[v]](B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)
D_{a}[[a]]D_{u}[[u]]D_{k}[[k]])D_{s}[[s]]
= (λαϵθσ.θ(update αϵσ))lD_{v}[[v]](B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)
D_{a}[[a]]D_{u}[[u]]D_{k}[[k]])D_{s}[[s]]
= B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]
(update l D_{v}[[v]]D_{s}[[s]])
= B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]
D_{s}[[s]][D_{v}[[v]]/l]
= B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s′]]
= D[[Σ′]]

Case 17: R = Push. Let Σ = ⟨t, ⟨push⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩. Then R(Σ) = Σ′ = ⟨t, b_{1}, v, v :: a, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨push⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨push⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= Z_{τ} [[⟨push⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.push)eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= push(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λπϵϵ^{∗}ρ_{R}ψ.πϵ(ϵ^{∗}^{⌢}⟨ϵ⟩)ρ_{R}ψ)
(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= B_{τ} [[b_{1}]]eρ_{G}D_{v}[[v]](D_{a}[[a]]^{⌢}⟨D_{v}[[v]]⟩)D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= B_{τ} [[b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[v :: a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 18: R = Alternate Make Environment. Let Σ = ⟨t, ⟨make-env #a⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩. Then R(Σ) = Σ′ = ⟨t, b_{1}, v, ⟨⟩, u′, k, s^{⌢}(rev a)⟩, where u′ = add-layer′(u, #s, #a). If tievals aux = λν_{1}ν_{2}.⟨ν_{1} ⋯ (ν_{1} + ν_{2} − 1)⟩, then

tievals ξϵ^{∗}σ = ξ(tievals aux(#σ)(#ϵ^{∗}))(σ^{⌢}ϵ^{∗}).

Also,

extend_{R} D_{u}[[u]]⟨m ⋯ (m + n − 1)⟩ = D_{u}[[add-layer′(u, m, n)]]. These two results are used in the following derivation.

D[[Σ]] = B_{τ} [[⟨make-env #a⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨make-env #a⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= Z_{τ} [[⟨make-env #a⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.make env #a)eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= make env #a(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λνπϵϵ^{∗}ρ_{R}ψ.#ϵ^{∗} = ν →

tievals(λα^{∗}.πϵ⟨⟩(extend_{R} ρ_{R}α^{∗})ψ)ϵ^{∗}, wrong “bad stack”) #a(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (#D_{a}[[a]] = #a →

tievals(λα^{∗}.(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]⟨⟩(extend_{R} D_{u}[[u]]α^{∗})D_{k}[[k]]) D_{a}[[a]], wrong “bad stack”)D_{s}[[s]]

= tievals(λα^{∗}.(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]⟨⟩(extend_{R} D_{u}[[u]]α^{∗})D_{k}[[k]])

D_{a}[[a]]D_{s}[[s]]

= (λα^{∗}.(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]⟨⟩(extend_{R} D_{u}[[u]]α^{∗})D_{k}[[k]])

tievals aux(#D_{s}[[s]])(#D_{a}[[a]])(D_{s}[[s]]^{⌢}D_{a}[[a]])

= B_{τ} [[b_{1}]]eρ_{G}D_{v}[[v]]⟨⟩

(extend_{R} D_{u}[[u]]⟨#D_{s}[[s]] ⋯ (#D_{s}[[s]] + #D_{a}[[a]] − 1)⟩) D_{k}[[k]](D_{s}[[s]]^{⌢}D_{a}[[a]])

= B_{τ} [[b_{1}]]eρ_{G}D_{v}[[v]]⟨⟩

D_{u}[[add-layer′(u, #D_{s}[[s]], #D_{a}[[a]])]]D_{k}[[k]](D_{s}[[s]]^{⌢}D_{a}[[a]])

= D[[Σ′]]

Case 19: R = Make Rest List. Let Σ = ⟨t, ⟨make-rest-list n_{1}⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩ and #a = n_{1} + n_{2}. Then R(Σ) = Σ′ = ⟨t, b_{1}, v′, a†n_{2}, u, k, s′⟩, where v′ = mrl-value(n_{2}, null, a, s) and s′ = mrl-store(n_{2}, null, a, s). In the following derivation, we will use the fact that, if #a ≥ n, then list D_{a}[[a‡n]]κD_{s}[[s]] =

κ⟨D_{v}[[mrl-value(n, null, a, s)]]⟩D_{s}[[mrl-store(n, null, a, s)]].

D[[Σ]] = B_{τ} [[⟨make-rest-list n_{1}⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.Z_{τ} [[⟨make-rest-list n_{1}⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨make-rest-list n_{1}⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.make rest list n_{1})eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= make rest list n_{1}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λνπϵϵ^{∗}ρ_{R}ψ.#ϵ^{∗} ≥ ν →

list(ϵ^{∗}†ν)(single λϵ.πϵ(ϵ^{∗}‡ν)ρ_{R}ψ),

wrong “bad stack”)

n_{1}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (#D_{a}[[a]] ≥ n_{1} →

list(D_{a}[[a]]†n_{1})(single λϵ.B_{τ} [[b_{1}]]eρ_{G}ϵ(D_{a}[[a]]‡n_{1})D_{u}[[u]]D_{k}[[k]]), wrong “bad stack”)D_{s}[[s]]

= list(D_{a}[[a]]†n_{1})(single λϵ.B_{τ} [[b_{1}]]eρ_{G}ϵ(D_{a}[[a]]‡n_{1})D_{u}[[u]]D_{k}[[k]])

D_{s}[[s]]

= list D_{a}[[a‡n_{2}]](single λϵ.B_{τ} [[b_{1}]]eρ_{G}ϵD_{a}[[a†n_{2}]]D_{u}[[u]]D_{k}[[k]])D_{s}[[s]]
= (single λϵ.B_{τ} [[b_{1}]]eρ_{G}ϵD_{a}[[a†n_{2}]]D_{u}[[u]]D_{k}[[k]])

⟨D_{v}[[mrl-value(n_{2}, null, a, s)]]⟩D_{s}[[mrl-store(n_{2}, null, a, s)]]

= B_{τ} [[b_{1}]]eρ_{G}D_{v}[[mrl-value(n_{2}, null, a, s)]]

D_{a}[[a†n_{2}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[mrl-store(n_{2}, null, a, s)]]

= D[[Σ′]]

Case 20: R = Unspecified.

Let Σ = ⟨⟨t, ⟨unspecified⟩ :: b_{1}, v, a, u, k, s⟩, where t = template b e⟩.

Then R(Σ) = Σ′ = ⟨t, b_{1}, not-specified, a, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨unspecified⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨unspecified⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= Z_{τ} [[⟨unspecified⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.literal(unspecified in E))eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= literal (unspecified in E)(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λϵ′πϵϵ^{∗}ρ_{R}ψ.πϵ′ϵ^{∗}ρ_{R}ψ)(unspecified in E)(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (B_{τ} [[b_{1}]]eρ_{G})(unspecified in E)D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 21: R = Check Args =. Let Σ = ⟨t, ⟨checkargs= n⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩ and #a = n. Then R(Σ) = Σ′ = ⟨t, b_{1}, v, a, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨checkargs= n⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨checkargs= n⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨checkargs= n⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.check args eq n)eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= check args eq n(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λνπϵϵ^{∗}ρ_{R}ψ.#ϵ^{∗} = ν → πϵϵ^{∗}ρ_{R}ψ,

wrong “bad arg count”)n(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (#D_{a}[[a]] = n → B_{τ} [[b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]],

wrong “bad arg count”)D_{s}[[s]]

= (B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 22: R = Check Args >=.

Let Σ = ⟨t, ⟨checkargs>= n⟩ :: b_{1}, v, a, u, k, s⟩, where #a ≥ n.

Then R(Σ) = Σ′ = ⟨t, b_{1}, v, a, u, k, s⟩.

The proof of this case is essentially the same as the proof for Case 21.

Case 23: R = Primitive CWCC.

Let Σ = ⟨⟨template b e⟩, ⟨%%cwcc⟩ :: b_{1}, v, a, u, k, s⟩, where a = ⟨v_{1}⟩ and v_{1} = ⟨closure t_{1} u_{1} l_{1}⟩.

Then R(Σ) = Σ′ = ⟨t_{1}, t_{1}(1), v_{1}, a_{1}, u_{1}, k, s_{1}⟩, where a_{1} = ⟨⟨escape k #s⟩⟩ and s_{1} = s^{⌢}⟨not-specified⟩.

D[[Σ]] = B_{τ} [[⟨%%cwcc⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[⟨v_{1}⟩]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨%%cwcc⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[⟨v_{1}⟩]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨%%cwcc⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[⟨v_{1}⟩]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπϵϵ^{∗}ρ_{R}ψσ.#ϵ^{∗} = 1 →

call 1(ϵ^{∗}0)⟨make escape ψσ⟩ρ_{R}ψ (update (new σ)(unspecified in E)σ), wrong “bad arg count”σ) eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[⟨v_{1}⟩]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= #D_{a}[[⟨⟨closure t_{1} u_{1} l_{1}⟩⟩]] = 1 →

call 1(D_{a}[[⟨⟨closure t_{1} u_{1} l_{1}⟩⟩]]0) ⟨make escape D_{k}[[k]]D_{s}[[s]]⟩D_{k}[[k]]D_{u}[[u]] (update (new D_{s}[[s]])(unspecified in E)D_{s}[[s]]), wrong “bad arg count”D_{s}[[s]]

= call 1D_{v}[[⟨closure t_{1} u_{1} l_{1}⟩]]⟨make escape D_{k}[[k]]D_{s}[[s]]⟩

D_{k}[[k]]D_{u}[[u]]D_{s}[[s_{1}]]

= applicate D_{v}[[⟨closure t_{1} u_{1} l_{1}⟩]]

⟨make escape D_{k}[[k]]D_{s}[[s]]⟩(single D_{k}[[k]])D_{s}[[s_{1}]]

= (λϵ^{∗}κ.T_{τ} [[t_{1}]]ρ_{G}D_{v}[[⟨closure t_{1} u_{1} l_{1}⟩]]ϵ^{∗}D_{u}[[u_{1}]](λϵ.κ⟨ϵ⟩))

⟨make escape D_{k}[[k]]D_{s}[[s]]⟩(single D_{k}[[k]])D_{s}[[s_{1}]]

= T_{τ} [[t_{1}]]ρ_{G}D_{v}[[v_{1}]]

⟨make escape D_{k}[[k]]D_{s}[[s]]⟩ D_{u}[[u_{1}]]D_{k}[[k]]D_{s}[[s_{1}]]

= T_{τ} [[t_{1}]]ρ_{G}D_{v}[[v_{1}]]

⟨(λψσ.⟨(new σ), single arg(λϵκ.ψϵ)⟩ in E)D_{k}[[k]]D_{s}[[s]]⟩ D_{u}[[u_{1}]]D_{k}[[k]]D_{s}[[s_{1}]]

= T_{τ} [[t_{1}]]ρ_{G}D_{v}[[v_{1}]]

⟨⟨#D_{s}[[s]], single arg(λϵκ.D_{k}[[k]]ϵ)⟩ in E⟩ D_{u}[[u_{1}]]D_{k}[[k]]D_{s}[[s_{1}]]

= T_{τ} [[t_{1}]]ρ_{G}D_{v}[[v_{1}]]D_{a}[[a_{1}]]D_{u}[[u_{1}]]D_{k}[[k]]D_{s}[[s_{1}]]
= D[[Σ′]]

Case 24: R = Primitive CWCC-Escape.

Let Σ = ⟨⟨template b e⟩, ⟨%%cwcc⟩ :: b_{0}, v, a, u, k, s⟩, where a = ⟨⟨escape ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ l_{1}⟩⟩.

Then R(Σ) = Σ′ = ⟨t_{1}, b_{1}, v_{1}, a_{1}, u_{1}, k_{1}, s_{1}⟩, where t_{1} = ⟨template b′ e_{1}⟩, v_{1} = ⟨escape k #s⟩, and s_{1} = s^{⌢}⟨not-specified⟩.

D[[Σ]] = B_{τ} [[⟨%%cwcc⟩ :: b_{0}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨%%cwcc⟩]]eρ(B_{τ} [[b_{0}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨%%cwcc⟩]]eρ_{G}(B_{τ} [[b_{0}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπϵϵ^{∗}ρ_{R}ψσ.#ϵ^{∗} = 1 →

call 1(ϵ^{∗}0)⟨make escape ψσ⟩ρ_{R}ψ (update (new σ)(unspecified in E)σ), wrong “bad arg count”σ) eρ_{G}(B_{τ} [[b_{0}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= #D_{a}[[⟨⟨escape ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ l_{1}⟩⟩]] = 1 →

call 1(D_{a}[[⟨⟨escape ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ l_{1}⟩⟩]]0) ⟨make escape D_{k}[[k]]D_{s}[[s]]⟩D_{k}[[k]]D_{u}[[u]] (update (new D_{s}[[s]])(unspecified in E)D_{s}[[s]]), wrong “bad arg count”D_{s}[[s]]

= call 1D_{v}[[⟨escape ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ l_{1}⟩]]

⟨make escape D_{k}[[k]]D_{s}[[s]]⟩D_{k}[[k]]D_{u}[[u]]D_{s}[[s_{1}]]

= applicate D_{v}[[⟨escape ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ l_{1}⟩]]

⟨make escape D_{k}[[k]]D_{s}[[s]]⟩(single D_{k}[[k]])D_{s}[[s_{1}]]

= single arg(λϵκ.D_{k}[[⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩]]ϵ)

⟨make escape D_{k}[[k]]D_{s}[[s]]⟩ (single D_{k}[[k]])D_{s}[[s_{1}]]

= single arg(λϵκ.D_{k}[[⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩]]ϵ)

⟨(λψσ.⟨(new σ), single arg(λϵκ.ψϵ)⟩ in E)D_{k}[[k]]D_{s}[[s]]⟩ (single D_{k}[[k]])D_{s}[[s_{1}]]

= single arg(λϵκ.D_{k}[[⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩]]ϵ)

⟨⟨#D_{s}[[s]], single arg(λϵκ.D_{k}[[k]]ϵ)⟩ in E⟩ (single D_{k}[[k]])D_{s}[[s_{1}]]

= single arg(λϵκ.D_{k}[[⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩]]ϵ)

D_{a}[[⟨v_{1}⟩]](single D_{k}[[k]])D_{s}[[s_{1}]]

= (λϵκ.D_{k}[[⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩]]ϵ)D_{v}[[v_{1}]](single D_{k}[[k]])D_{s}[[s_{1}]]
= D_{k}[[⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩]]D_{v}[[v_{1}]]D_{s}[[s_{1}]]
= (λϵ.B_{τ} [[b_{1}]]e_{1}ρ_{G}ϵD_{a}[[a_{1}]]D_{u}[[u_{1}]]D_{k}[[k_{1}]])D_{v}[[v_{1}]]D_{s}[[s_{1}]]
= D[[Σ′]]

Case 25: R = Primitive CWCC-Escape-Halt.

Let Σ = ⟨t, ⟨%%cwcc⟩ :: b_{1}, v, a, u, k, s⟩, where a = ⟨⟨escape halt l⟩⟩.

Then R(Σ) = Σ′ = ⟨t, ⟨⟩, v′, a, u, k, s⟩, where v′ = ⟨escape k #s⟩.

O′[[Σ′]] is undefined since v′ ∉ R. Thus O′[[Σ]] is undefined, and so we do not have to consider this case.

Case 26: R = Primitive Cons.

Let Σ = ⟨t, ⟨%%cons⟩ :: b_{1}, v, ⟨v_{1} v_{2}⟩^{⌢}a_{1}, u, k, s⟩, where t = ⟨template b e⟩.

Then R(Σ) = Σ′ = ⟨t, b_{1}, v′, ⟨⟩, u, k, s^{⌢}⟨v_{2} v_{1}⟩⟩, where v′ = ⟨mutable-pair #s (1 + #s)⟩.

D[[Σ]] = B_{τ} [[⟨%%cons⟩ :: b_{1}]]eρ_{G}

D_{v}[[v]]D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.Z_{τ} [[⟨%%cons⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨%%cons⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπϵϵ^{∗}ρ_{R}ψσ.#ϵ^{∗} ≥ 2 →

(λσ′.π(⟨new σ, new σ′, mutable⟩ in E) ⟨⟩ρ_{R}ψ(update(new σ′)((rev ϵ^{∗})0)σ′)) (update(new σ)((rev ϵ^{∗})1)σ), wrong “bad arg count”σ) eρ_{G}B_{τ} [[b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= #D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]] ≥ 2 →

(λσ′.(B_{τ} [[b_{1}]]eρ_{G})(⟨new D_{s}[[s]], new σ′, mutable⟩ in E) ⟨⟩D_{u}[[u]]D_{k}[[k]](update(new σ′)((rev D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]])0)σ′)) (update(new D_{s}[[s]])(rev D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]]1), wrong “bad arg count”D_{s}[[s]]

= (λσ′.B_{τ} [[b_{1}]]eρ_{G}(⟨#D_{s}[[s]], new σ′, mutable⟩ in E)

⟨⟩D_{u}[[u]]D_{k}[[k]](update(new σ′)D_{v}[[v_{1}]]σ′))D_{s}[[s]]^{⌢}⟨D_{v}[[v_{2}]]⟩

= B_{τ} [[b_{1}]]eρ_{G}(⟨#D_{s}[[s]], (1 + #D_{s}[[s]]), mutable⟩ in E)

⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]^{⌢}⟨D_{v}[[v_{2}]] D_{v}[[v_{1}]]⟩

= D[[Σ′]]

Case 27: R = Primitive Car-Immutable Pair.

Let Σ = ⟨t, ⟨%%car⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩ and a = ⟨immutable-pair c_{1} c_{2}⟩ :: a_{1}

Then R(Σ) = Σ′ = ⟨t, b_{1}, c_{1}, ⟨⟩, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨%%car⟩ :: b_{1}]]eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.Z_{τ} [[⟨%%car⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨%%car⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπϵϵ^{∗}ρ_{R}ψσ.#ϵ^{∗} ≥ 1 →

(rev ϵ^{∗})0 : E_{p} → π(σ(((rev ϵ^{∗})0|E_{p})0))⟨⟩ρ_{R}ψσ, wrong “attempt to take car of non-pair”σ, wrong “bad arg count”σ) eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= #D_{a}[[⟨immutable-pair c_{1} c_{2}⟩ :: a_{1}]] ≥ 1 →

(rev D_{a}[[⟨immutable-pair c_{1} c_{2}⟩ :: a_{1}]])0 : E_{p} → B_{τ} [[b_{1}]]eρ_{G} (D_{s}[[s]](((rev D_{a}[[⟨immutable-pair c_{1} c_{2}⟩ :: a_{1}]])0|E_{p})0)) ⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]], wrong “attempt to take car of non-pair”D_{s}[[s]], wrong “bad arg count”D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}(D_{s}[[s]](D_{v}[[⟨immutable-pair c_{1} c_{2}⟩]]0))

⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}c_{1}⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 28: R = Primitive Car-Mutable Pair.

Let Σ = ⟨t, ⟨%%car⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩ and a = ⟨mutable-pair l_{1} l_{2}⟩ :: a_{1}

Then R(Σ) = Σ′ = ⟨t, b_{1}, s(l_{1}), ⟨⟩, u, k, s⟩.

D[[Σ]] = B_{τ} [[⟨%%car⟩ :: b_{1}]]eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.Z_{τ} [[⟨%%car⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨%%car⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπϵϵ^{∗}ρ_{R}ψσ.#ϵ^{∗} ≥ 1 →

(rev ϵ^{∗})0 : E_{p} → π(σ(((rev ϵ^{∗})0|E_{p})0))⟨⟩ρ_{R}ψσ, wrong “attempt to take car of non-pair”σ, wrong “bad arg count”σ) eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= #D_{a}[[⟨mutable-pair l_{1} l_{2}⟩ :: a_{1}]] ≥ 1 →

(rev D_{a}[[⟨mutable-pair l_{1} l_{2}⟩ :: a_{1}]])0 : E_{p} → B_{τ} [[b_{1}]]eρ_{G} (D_{s}[[s]](((rev D_{a}[[⟨mutable-pair l_{1} l_{2}⟩ :: a_{1}]])0|E_{p})0)) ⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]], wrong “attempt to take car of non-pair”D_{s}[[s]], wrong “bad arg count”D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}(D_{s}[[s]](D_{v}[[⟨mutable-pair l_{1} l_{2}⟩]]0))

⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}(D_{s}[[s]]l_{1})⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 29: R = Primitive Set-Car!.

Let Σ = ⟨t, ⟨%%set-car!⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩, a = ⟨v_{1} ⟨mutable-pair l_{1} l_{2}⟩⟩^{⌢}a_{1}, and l_{1} < #s.

Then R(Σ) = Σ′ = ⟨t, b_{1}, not-specified, ⟨⟩, u, k, s′⟩, where s′ = s + {l_{1} ↦ v_{1}}.

D[[Σ]] = B_{τ} [[⟨%%set-car!⟩ :: b_{1}]]eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρ.Z_{τ} [[⟨%%set-car!⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨%%set-car!⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπϵϵ^{∗}ρ_{R}ψ.#ϵ^{∗} ≥ 2 → (rev ϵ^{∗})1 : E_{p} →

((rev ϵ^{∗})1|E_{p})2 = mutable → assign(((rev ϵ^{∗})1|E_{p})0)((rev ϵ^{∗})0)(π(unspecified in E)⟨⟩ρ_{R}ψ), wrong “attempt to set car of immutable pair”, wrong “attempt to set car of non-pair”, wrong “bad arg count”) eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (#D_{a}[[⟨v_{1} ⟨mutable-pair l_{1} l_{2}⟩⟩^{⌢}a_{1}]] ≥ 2 →

(rev D_{a}[[⟨v_{1} ⟨mutable-pair l_{1} l_{2}⟩⟩^{⌢}a_{1}]])1 : E_{p} → ((rev D_{a}[[⟨v_{1} ⟨mutable-pair l_{1} l_{2}⟩⟩^{⌢}a_{1}]])1|E_{p})2 = mutable → assign(((rev D_{a}[[⟨v_{1} ⟨mutable-pair l_{1} l_{2}⟩⟩^{⌢}a_{1}]])1|E_{p})0) ((rev D_{a}[[⟨v_{1} ⟨mutable-pair l_{1} l_{2}⟩⟩^{⌢}a_{1}]])0) ((B_{τ} [[b_{1}]]eρ_{G})(unspecified in E)⟨⟩D_{u}[[u]]D_{k}[[k]]), wrong “attempt to set car of immutable pair”, wrong “attempt to set car of non-pair”, wrong “bad arg count”)D_{s}[[s]]

= assign l_{1}D_{v}[[v_{1}]]((B_{τ} [[b_{1}]]eρ_{G})(unspecified in E)⟨⟩D_{u}[[u]]D_{k}[[k]])

D_{s}[[s]]

= (λαϵθσ.θ(update αϵσ))

l_{1}D_{v}[[v_{1}]]((B_{τ} [[b_{1}]]eρ_{G})(unspecified in E)⟨⟩D_{u}[[u]]D_{k}[[k]])D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)⟨⟩D_{u}[[u]]D_{k}[[k]](update l_{1}D_{v}[[v_{1}]]D_{s}[[s]])
= B_{τ} [[b_{1}]]eρ_{G}(unspecified in E)⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s′]]
= D[[Σ′]]

Case 30: R = Primitive Apply-Closure.

Let Σ = ⟨⟨template b e⟩, ⟨%%apply⟩ :: b_{1}, v, a, u, k, s⟩, where a = ⟨v_{1}⟩^{⌢}a_{1}^{⌢}⟨v_{2}⟩, v_{2} = ⟨closure t_{1} u_{1} l_{1}⟩, and t_{1} =

⟨template b_{2} e_{2}⟩.

Then R(Σ) = Σ′ = ⟨t_{1}, b_{2}, v_{2}, a_{2}, u_{1}, k, s⟩, where a_{2} = app-stack(v_{1}, a_{1}, s).

In the following derivation, we use the fact that, if app-stack(v, a, s) is defined, then

app-stack(v, a, s) = list to seq D_{v}[[v]]D_{a}[[a]]D_{s}[[s]].

D[[Σ]] = B_{τ} [[⟨%%apply⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨%%apply⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨%%apply⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπϵϵ^{∗}ρ_{R}ψσ.#ϵ^{∗} ≥ 2 →

(λϵ^{∗}ϵ.call(#ϵ^{∗})ϵϵ^{∗}ρ_{R}ψσ)

(list to seq((rev ϵ^{∗})0)(((rev ϵ^{∗})†1)‡(#ϵ^{∗} − 2))σ) ((rev ϵ^{∗})(#ϵ^{∗} − 1)), wrong “bad arg count”σ) eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λϵ^{∗}ϵ.call(#ϵ^{∗})ϵϵ^{∗}D_{u}[[u]]D_{k}[[k]]D_{s}[[s]])

(list to seq D_{v}[[v_{1}]]D_{a}[[a_{1}]]D_{s}[[s]])D_{v}[[v_{2}]]

= (λϵ^{∗}ϵ.call(#ϵ^{∗})ϵϵ^{∗}D_{u}[[u]]D_{k}[[k]]D_{s}[[s]])D_{a}[[a_{2}]]D_{v}[[v_{2}]]
= call(#D_{a}[[a_{2}]])D_{v}[[v_{2}]]D_{a}[[a_{2}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= applicate D_{v}[[v_{2}]]D_{a}[[a_{2}]](single D_{k}[[k]])D_{s}[[s]]
= (λϵ^{∗}κ.T_{τ} [[t_{1}]]ρ_{G}D_{v}[[v_{2}]]ϵ^{∗}D_{u}[[u_{1}]](λϵ.κ⟨ϵ⟩))

D_{a}[[a_{2}]](single D_{k}[[k]])D_{s}[[s]]

= B_{τ} [[b_{2}]]e_{2}ρ_{G}D_{v}[[v_{2}]]D_{a}[[a_{2}]]D_{u}[[u_{1}]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

Case 31: R = Primitive Apply-Escape. Let Σ = ⟨⟨template b e⟩, ⟨%%apply⟩ :: b_{1}, v, a, u, k, s⟩, where a = ⟨v_{1}⟩^{⌢}a_{1}^{⌢}⟨v_{2}⟩, v_{2} = ⟨escape k_{1} l_{1}⟩, k_{1} = ⟨cont t_{2} b_{2} a_{2} u_{2} k_{2}⟩, t_{2} = ⟨template b_{3} e_{2}⟩, and ⟨v_{3}⟩ = app-stack(v_{1}, a_{1}, s). Then R(Σ) = Σ′ = ⟨t_{2}, b_{2}, v_{3}, a_{2}, u_{2}, k_{2}, s⟩. In the following derivation, we use the fact that, if app-stack(v, a, s) is defined, then

app-stack(v, a, s) = list to seq D_{v}[[v]]D_{a}[[a]]D_{s}[[s]].

D[[Σ]] = B_{τ} [[⟨%%apply⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨%%apply⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨%%apply⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπϵϵ^{∗}ρ_{R}ψσ.#ϵ^{∗} ≥ 2 →

(λϵ^{∗}ϵ.call(#ϵ^{∗})ϵϵ^{∗}ρ_{R}ψσ)

(list to seq((rev ϵ^{∗})0)(((rev ϵ^{∗})†1)‡(#ϵ^{∗} − 2))σ) ((rev ϵ^{∗})(#ϵ^{∗} − 1)), wrong “bad arg count”σ) eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λϵ^{∗}ϵ.call(#ϵ^{∗})ϵϵ^{∗}D_{u}[[u]]D_{k}[[k]]D_{s}[[s]])

(list to seq D_{v}[[v_{1}]]D_{a}[[a_{1}]]D_{s}[[s]])D_{v}[[v_{2}]]

= (λϵ^{∗}ϵ.call(#ϵ^{∗})ϵϵ^{∗}D_{u}[[u]]D_{k}[[k]]D_{s}[[s]])D_{a}[[⟨v_{3}⟩]]D_{v}[[v_{2}]]
= call(#D_{a}[[⟨v_{3}⟩]])D_{v}[[v_{2}]]D_{a}[[⟨v_{3}⟩]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= applicate D_{v}[[v_{2}]]D_{a}[[⟨v_{3}⟩]](single D_{k}[[k]])D_{s}[[s]]
= single arg(λϵκ.D_{k}[[k_{1}]]ϵ)D_{a}[[⟨v_{3}⟩]](single D_{k}[[k]])D_{s}[[s]]
= D_{k}[[k_{1}]]D_{v}[[v_{3}]]D_{s}[[s]]
= (λϵ.B_{τ} [[b_{2}]]e_{2}ρ_{G}ϵD_{a}[[a_{2}]]D_{u}[[u_{2}]]D_{k}[[k_{2}]])D_{v}[[v_{3}]]D_{s}[[s]]
= B_{τ} [[b_{2}]]e_{2}ρ_{G}D_{v}[[v_{3}]]D_{a}[[a_{2}]]D_{u}[[u_{2}]]D_{k}[[k_{2}]]D_{s}[[s]]
= D[[Σ′]]

Case 32: R = Primitive Apply-Escape-Halt. Let Σ = ⟨t, ⟨%%apply⟩ :: b_{1}, v, a, u, k, s⟩, where a = ⟨v_{1}⟩^{⌢}a_{1}^{⌢}⟨v_{2}⟩ and v_{2} = ⟨escape halt l_{1}⟩. Then R(Σ) = Σ′ = ⟨t, ⟨⟩, v_{2}, a, u, k, s⟩. O′[[Σ′]] is undefined since not v′ ∉ R. Thus O′[[Σ]] is undefined, and so we do not have to consider this case.

Case 33: R = Primitive Eqv. Let Σ = ⟨t, ⟨%%eqv⟩ :: b_{1}, v, ⟨v_{1} v_{2}⟩^{⌢}a_{1}, u, k, s⟩, where t = ⟨template b e⟩. Then R(Σ) = Σ′ = ⟨t, b_{1}, v′, ⟨⟩, u, k, s⟩, where v′ = ((v_{1} = v_{2}) → true, false).

D[[Σ]] = B_{τ} [[⟨%%eqv⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨%%eqv⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}

D_{v}[[v]]D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= Z_{τ} [[⟨%%eqv⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})

D_{v}[[v]]D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (λeρπϵϵ^{∗}ρ_{R}ψ.#ϵ^{∗} ≥ 2 → π

(((rev ϵ^{∗})0 = (rev ϵ^{∗})1 → true, false) in E)⟨⟩ρ_{R}ψ, wrong “bad arg count”) eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= (#D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]] ≥ 2 → B_{τ} [[b_{1}]]eρ_{G}

(((rev D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]])0 =

(rev D_{a}[[⟨v_{1} v_{2}⟩^{⌢}a_{1}]])1 → true, false) in E) ⟨⟩D_{u}[[u]]D_{k}[[k]], wrong “bad arg count”)D_{s}[[s]]

= B_{τ} [[b_{1}]]eρ_{G}((D_{v}[[v_{1}]] = D_{v}[[v_{2}]] → true, false) in E)

⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]

= D[[Σ′]]

Case 34: R = Primitive Add.

Let Σ = ⟨t, ⟨%%add⟩ :: b_{1}, v, a, u, k, s⟩, where t = ⟨template b e⟩.

Then R(Σ) = Σ′ = ⟨t, b_{1}, v′, ⟨⟩, u, k, s⟩, where v′ = n-ary-sum(a).

Notice that sum vals (rev ϵ^{∗}) = sum vals ϵ^{∗} since addition is commutative.

D[[Σ]] = B_{τ} [[⟨%%add⟩ :: b_{1}]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.Z_{τ} [[⟨%%add⟩]]eρ(B_{τ} [[b_{1}]]eρ))eρ_{G}
D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= Z_{τ} [[⟨%%add⟩]]eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρπϵϵ^{∗}ρ_{R}ψ.π(sum vals (rev ϵ^{∗}))⟨⟩ρ_{R}ψ)
eρ_{G}(B_{τ} [[b_{1}]]eρ_{G})D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= B_{τ} [[b_{1}]]eρ_{G}(sum vals D_{a}[[a]])⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= B_{τ} [[b_{1}]]eρ_{G}(fix(λfϵ^{∗}.#ϵ^{∗} = 0 → f(ϵ^{∗}†1) + ((ϵ^{∗}0)|R))D_{a}[[a]])
⟨⟩D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D[[Σ′]]

7 Proof of Lemma 5.4

Let x be an abc state value, argument stack, environment, continuation, or store. x̂ is the result of replacing each u = ⟨env u′ l^{∗}⟩ occurring in x with ⟨env u′ (rev l^{∗})⟩.

Two abc states Σ = ⟨t, b, v, a, u, k, s⟩ and Σ′ = ⟨t′, b′, v′, a′, u′, k′, s′⟩ are compatible if they are both normal, t′ = t, b′ = b, v′ = v̂, a′ = â, u′ = û, k′ = k̂, and there is a permutation p of s such that:

(1) s′ = p̂(s).

(2) For each l ∈ L_{glo}(Σ), s′(l) = ŝ(l).

(3) For each l ∈ L_{env}(Σ) with l = env-reference(u_{0}, n_{0}, n_{1}) for some u_{0} occurring in Σ and n_{0}, n_{1} ∈ N, s′(l′) = ŝ(l) where l′ = env-reference(û_{0}, n_{0}, n_{1}).

(4) For each l ∈ L_{mp}(Σ), s′(l) = ŝ(l).

(5) For each l ∈ L_{ip}(Σ), s′(l) = ŝ(l) (= s(l) since immutable pairs never contain environments).

Lemma 7.1 Let Σ and Σ′ be compatible abc states, R be an abc rule, and R′ be the corresponding special rule.

(1) R is applicable to Σ iff R′ is applicable to Σ′.

(2) If R is applicable to Σ and R′ is applicable to Σ′, then R(Σ) and R′(Σ′) are compatible.

Proof Let Σ and Σ′ be compatible abc states, R be an abc rule, and R′ be the corresponding special rule.

Case 1: R = R′, i.e., R is not Make Environment.

(1): Certainly, R is applicable to Σ iff R is applicable to Σ′ provided:

(a) The domain conditions of R do not depend on the form of any environment in Σ or Σ′.

(b) The domain conditions of R do not depend on the value of the store at a location in L_{env}(Σ).

There is just one abc rule (besides Make Environment) which violates (a) or (b): Local. The domain conditions of Local require that:

s(env-reference(u, n_{0}, n_{1})) ≠ undefined.

Since Σ and Σ′ are compatible, and hence satisfy clause 3 of the definition of compatible, Σ satisfies this condition iff Σ′ satisfies it.

(2): Assume R is applicable to Σ and R′ is applicable to Σ′. Then, by Lemma 5.1, R(Σ) and R′(Σ′) are both normal. Certainly, R(Σ) and R′(Σ′) are compatible provided:

(c) R does not create any new environments in Σ or Σ′.

(d) R does not modify the store at a location in L_{env}(Σ).

There is just one abc rule (besides Make Environment) which violates (c) or (d): Set Local. Set Local modifies the value of the store at a location l = env-reference(u, n_{0}, n_{1}). Since Σ and Σ′ are compatible, and hence satisfy clause 3 of the definition of compatible, R(Σ) and R′(Σ′) also satisfy clause 3. Therefore, R(Σ) and R′(Σ′) are compatible.

Case 2: R is Make Environment and R′ is Alternate Make Environment. (1): Since the domain conditions of R and R′ are identical and do not

depend on anything but the form of b, clearly, R is applicable to Σ iff R is applicable to Σ′.

(2): Assume R is applicable to Σ and R′ is applicable to Σ′. Then, by Lemma 5.1, R(Σ) and R′(Σ′) are both normal. Let R(Σ) and R′(Σ′) have the form ⟨t, b, v, a, u, k, s^{⌢}a⟩ and ⟨t, b, v, a, u′, k, s^{′⌢}(rev a)⟩, respectively. By the definition of add-layer′, u′ = û. Since Σ and Σ′ are compatible, there is a permutation p of s such that s′ = p̂(s), and hence there is obviously an extension p′ of p that permutes s^{⌢}a such that s^{′⌢}(rev a) = p̂′(s^{⌢}a). The new locations in stores s^{⌢}a and s^{′⌢}(rev a) are members of L_{env}(R(Σ)). Since the values in the respective stores at these new locations are given in reverse order from one another, clause 3 of the definition of compatible holds. Clauses 2, 4, and 5 of the definition of compatible also hold since the new stores are extensions of the old stores and all of the new locations are members of L_{env}(R(Σ)). Therefore, R(Σ) and R′(Σ′) are compatible. □

Proof of Lemma 5.4 Let t be a tbc template and Σ be an initial state for t, and assume O[[Σ]] is defined. Since O[[Σ]] is defined, there is a finite sequence Σ_{0}, …, Σ_{n} of abc states and a finite sequence R_{1}, …, R_{n} of abc rules such that:

(1) Σ = Σ_{0} and 0 ≤ n.

(2) R_{i+1}(Σ_{i}) = Σ_{i+1} for all i with 0 ≤ i ≤ n − 1.

(3) Σ_{n} has the form ⟨t_{0}, ⟨⟩, v, a, u, k, s⟩ with D_{v}[[v]]|R in A = O[[Σ]].

Σ is compatible with itself since it is an initial state and contains no environments. Thus, by Lemma 7.1, there is also a finite sequence Σ′_{0}, …, Σ′_{n} of abc states and a finite sequence R′_{1}, …, R′_{n} of special rules such that:

(1) Σ = Σ′_{0}.

(2) R′_{i+1}(Σ′_{i}) = Σ′_{i+1} for all i with 0 ≤ i ≤ n − 1.

(3) Σ_{i} and Σ′_{i} are compatible for all i with 0 ≤ i ≤ n.

Since Σ_{n} and Σ′_{n} are compatible, Σ′_{n} = ⟨t_{0}, ⟨⟩, v, â, û, k̂, p̂(s)⟩ for some permutation p of s. Therefore, O′[[Σ]] = D_{v}[[v]]|R in A = O[[Σ]]. □

References

[1] J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The vlisp byte-code compiler. M 92B092, The MITRE Corporation, 1992.

[2] J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The vlisp flattener. M 92B094, The MITRE Corporation, 1992.