The Dynamic Geometry of Interaction Machine: A Call-by-need Graph Rewriter

TL;DR

This paper introduces the Dynamic GoI Machine (DGoIM), a graph rewriting abstract machine that efficiently implements call-by-need evaluation for the lambda calculus by balancing token passing and graph rewriting.

Contribution

It presents a novel token-passing abstract machine that rewrites graphs to implement call-by-need evaluation with certified time efficiency.

Findings

DGoIM can implement call-by-need evaluation.

The machine balances space and time costs effectively.

DGoIM is classified as efficient per Accattoli's taxonomy.

Abstract

Girard's Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been also successfully applied to programming language semantics. One way is to use abstract machines that pass a token on a fixed graph along a path indicated by the GoI. These token-passing abstract machines are space efficient, because they handle duplicated computation by repeating the same moves of a token on the fixed graph. Although they can be adapted to obtain sound models with regard to the equational theories of various evaluation strategies for the lambda calculus, it can be at the expense of significant time costs. In this paper we show a token-passing abstract machine that can implement evaluation strategies for the lambda calculus, with certified time efficiency. Our abstract machine, called the Dynamic GoI Machine (DGoIM), rewrites the graph to avoid replicating computation, using the token to find the redexes. The flexibility of interleaving token transitions and graph rewriting allows the DGoIM to balance the trade-off of space and time costs. This paper shows that the DGoIM can implement call-by-need evaluation for the lambda calculus by using a strategy of interleaving token passing with as much graph rewriting as possible. Our quantitative analysis confirms that the DGoIM with this strategy of interleaving the two kinds of possible operations on graphs can be classified as "efficient" following Accattoli's taxonomy of abstract machines.

Equations

$$(h,m)$$

$$\mathsf{Ax}$$

$$(h,m)$$

$$\$$

$

$$(h,\mathsf{l}:m)$$

$$\$$

$

$$(h,m)$$

$$\text{oc}$$

$$(h,m)$$

$${\mathsf{C}}_n$$

$${\mathsf{Cut}}_{\alpha }:{\mathsf{Ax}}_{\beta }:h$$

$$\mathsf{Cut}$$

$${\text{parr}}_{\alpha }:{\mathsf{Cut}}_{\beta }:{\otimes }_{\gamma }:h$$

$$\text{parr}$$

$${\text{parr}}_{\alpha }:{\mathsf{Cut}}_{\beta }:{\otimes }_{\gamma }:h$$

$$\text{parr}$$

$${\text{oc}}_{\alpha }:{\mathsf{Cut}}_{\beta }:{\mathsf{D}}_{\gamma }:h$$

$$H$$

$${\text{oc}}_{\alpha }:{\mathsf{Cut}}_{\beta }:{\mathsf{Ax}}_{\gamma }:h$$

$$\text{oc}$$

$${\text{oc}}_{\alpha }:{\mathsf{Cut}}_{\beta }:{\mathsf{C}}_{\gamma }^{n+1}:{♯}_{\delta }:h$$

$$H$$

$${\text{oc}}_{\alpha }:{\mathsf{Cut}}_{\beta }:{\mathsf{C}}_{\gamma }^1:{♯}_{\delta }:h$$

$$H$$

$$((G,{\ell }_G),(e_0,\uparrow ),\square ,\square ){⇢}^{\ast }((G,{\ell }_G),(e,d),h,m).$$

$$s{\text{rightarrowtriangle}}_{\mathsf{x}}{s}^{\prime }\stackrel{\text{def.}}{⟺}\{\begin{array}{ll}s{⇝}_{\mathsf{x}}{s}^{\prime }& \text{(if ⇝x possible)}\\ s{⇢}_{\mathsf{x}}{s}^{\prime }& \text{(if only ⇢[x possible)}.\end{array}$$

$$(\overline{t}\overline{u},E{)}_{term}$$

$$(x,E_1⟨E_2[x\leftarrow \overline{t}]⟩{)}_{term}$$

$$(\overline{v},E{)}_{term}$$

$$(\lambda x.\overline{t},E⟨A\overline{u}⟩{)}_{ctxt}$$

$$(\overline{v},E_1⟨E_2⟨x⟩[x\leftarrow A]⟩{)}_{ctxt}$$

$$\mathrm{FV}(x)$$

$$\mathrm{FV}(\lambda x.t)$$

$$\mathrm{FV}(tu)$$

$$\mathrm{FV}(t[x\leftarrow u])$$

$${\mathrm{FV}}_M(⟨\cdot ⟩)$$

$${\mathrm{FV}}_M(Et)$$

$${\mathrm{FV}}_M(E[x\leftarrow t])$$

$${\mathrm{FV}}_M(E^{\prime }⟨x⟩[x\leftarrow E])$$

$$\mathrm{FV}(E⟨t⟩)$$

$${\mathrm{FV}}_M(E⟨E^{\prime }⟩)$$

$$((\lambda x.x)(\lambda z.z),⟨\cdot ⟩{)}_{term}$$

$$((\lambda x.\lambda y.y)(\lambda z.z),⟨\cdot ⟩{)}_{term}$$

$$x^{†}$$

$$(\lambda x.t{)}^{†}$$

$$(tu{)}^{†}$$

$$(t[x\leftarrow u]{)}^{†}$$

$$x^{†}$$

Full text

1 Introduction

1.1 Token-passing Abstract Machines for $\lambda$-calculus

Girard’s Geometry of Interaction (GoI) [16] is a semantic framework for linear logic proofs [15]. One way of applying it to programming language semantics is via “token-passing” abstract machines. A term in the $\lambda$-calculus is evaluated by representing it as a graph, then passing a token along a path indicated by the GoI. Token-passing GoI decomposes higher-order computation into local token actions, or low-level interactions of simple components. It can give strikingly innovative implementation techniques for functional programs, such as Mackie’s Geometry of Implementation compiler [20], Ghica’s Geometry of Synthesis (GoS) high-level synthesis tool [12], and Schöpp’s resource-aware program transformation to a low-level language [25]. The interaction-based approach is also convenient for the complexity analysis of programs, e.g. Dal Lago and Schöpp’s IntML type system of logarithmic-space evaluation [7], and Dal Lago et al.’s linear dependent type system of polynomial-time evaluation [5, 6].

Fixed-space execution is essential for GoS, since in the case of digital circuits the memory footprint of the program must be known at compile-time, and fixed. Using a restricted version of the call-by-name language Idealised Algol [13] not only the graph, but also the token itself can be given a fixed size. Surprisingly, this technique also allows the compilation of recursive programs [14]. The GoS compiler shows both the usefulness of the GoI as a guideline for unconventional compilation and the natural affinity between its space-efficient abstract machine and call-by-name evaluation. The practical considerations match the prior theoretical understanding of this connection [9].

In contrast, re-evaluating a term by repeating its token actions poses a challenge for call-by-value evaluation (e.g. [11, 24, 18, 3]) because duplicated computation must not lead to repeated evaluation. Moreover, in call-by-value repeating token actions raises the additional technical challenge of avoiding repeating any associated computational effects (e.g. [23, 22, 4]). A partial solution to this conundrum is to focus on the soundness of the equational theory, while deliberately ignoring the time costs [22]. However, Fernández and Mackie suggest that in a call-by-value scenario, the time efficiency of a token-passing abstract machine could also be improved, by allowing a token to jump along a path, even though a time cost analysis is not given [11].

For us, solving the the problem of creating a GoI-style abstract machine which computes efficiently with evaluation strategies other than call-by-name is a first step in a longer-range research programme. The compilation techniques derived from the GoI can be extremely useful in the case of unconventional computational platforms. But if GoI-style techniques are to be used in a practical setting they need to extend beyond call-by-name, not just correctly but also efficiently.

1.2 Interleaving Token Passing with Graph Rewriting

A token jumping, rather than following a path, can be seen as a simple form of short-circuiting that path, which is a simple form of graph-rewriting. This idea first occurs in Mackie’s work as a compiler optimisation technique [20] and is analysed in more depth theoretically by Danos and Regnier in the so-called Interaction Abstract Machine [9]. More general graph-rewriting-based semantics have been used in a system called virtual reduction [8], where rewriting occurs along paths indicated by GoI, but without any token-actions. The most operational presentation of the combination of token-passing and jumping was given by Fernández and Mackie [11]. The interleaving of token actions and rewriting is also found in Sinot’s interaction nets [26, 27]. We can reasonably think of the DGoIM as their abstract-machine realisation.

We build on these prior insights by adding more general, yet still efficient, graph-rewriting facilities to the setting of a GoI token-passing abstract machine. We call an abstract machine that interleaves token passing with graph rewriting the Dynamic GoI Machine (DGoIM), and we define it as a state transition system with transitions for token passing as well as transitions for graph rewriting. What connects these two kinds of transitions is the token trajectory through the graph, its path. By examining it, the DGoIM can detect redexes and trigger rewriting actions.

Through graph rewriting, the DGoIM reduces sub-graphs visited by the token, avoiding repeated token actions and improving time efficiency. On the other hand, graph rewriting can expand a graph by e.g. copying sub-graphs, so space costs can grow. To control this trade-off of space and time cost, the DGoIM has the flexibility of interleaving token passing with graph rewriting. Once the DGoIM detects that it has traversed a redex, it may rewrite it, but it may also just propagate the token without rewriting the redex.

As a first step in our exploration of the flexibility of this machine, we consider the two extremal cases of interleaving. The first extremal case is “passes-only,” in which the DGoIM never triggers graph rewriting, yielding an ordinary token-passing abstract machine. As a typical example, the $\lambda$-term $(\lambda{x}.t)\,u$ is evaluated like this:

\lambda{x}.t$$u

       

A token enters the graph on the left at the bottom open edge.

A token visits and goes through the left sub-graph $\lambda x.t$.

Whenever a token detects an occurrence of the variable $x$ in $t$, it traverses the right sub-graph $u$, then returns carrying the resulting value.

A token finally exits the graph at the bottom open edge.

Step 3 is repeated whenever term $u$ needs to be re-evaluated. This strategy of interleaving corresponds to call-by-name reduction.

The other extreme is “rewrites-first,” in which the DGoIM interleaves token passing with as much, and as early, graph rewriting as possible, guided by the token. This corresponds to both call-by-value and call-by-need reductions, the difference between the two being the trajectory of the token. In the case of call-by-value, the token will enter the graph from the bottom, traverse the left-hand-side sub-graph, which happens to be already a value, then visit sub-graph $u$ even before $x$ is used in a call. While traversing $u$, it will cause rewrites such that when the token exits, it leaves behind the graph of a machine corresponding to a value $v$ such that $u$ reduces to $v$. The difference with call-by-need is that the token will visit $u$ only when $x$ is encountered in $\lambda x.t$. In both cases, if repeated evaluation is required then the sub-graph corresponding now to $v$ is copied, so that one copy can be further rewritten, if needed, while the original is kept for later reference.

1.3 Contributions

This work presents a DGoIM model for call-by-need, which can be seen as a case study of the flexibility achieved through controlled interleaving of rewriting and token-passing. This is achieved through a rewriting strategy which turns out to be as natural as the passes-only strategy is for implementing call-by-name. The DGoIM avoids re-evaluation of a sub-term by rewriting any sub-graph visited by a token so that the updated sub-graph represents the evaluation result, but, unlike call-by-value, it starts by evaluating the sub-graph corresponding to the function $\lambda x.t$ first. We chose call-by-need mainly because of the technical challenges it poses. Adapting the technique to call-by-value is a straightforward exercise, and we discuss other alternative in the Conclusion.

We analyse the time cost of the DGoIM with the rewrites-first interleaving, using Accattoli et al.’s general methodology for quantitative analysis [2, 1]. Their method cannot be used “off the shelf,” because the DGoIM does not satisfy one of the assumptions used in [1, Sec. 3]. Our machine uses a more refined transition system, in which several steps correspond to a single one in loc. cit.. We overcome this technical difficulty by building a weak simulation of Danvy and Zerny’s storeless abstract machine [10] to which the recipe does apply. The result of the quantitative analysis confirms that the DGoIM with the rewrites-first interleaving can be classified as “efficient,” following Accattoli’s taxonomy of abstract machines introduced in [1].

As we intend to use the DGoIM as a starting point for semantics-directed compilation, this result is an important confirmation that no hidden inefficiencies lurk within the fabric of the rather complex machinery of the DGoIM.

2 The Dynamic GoI Machine

2.1 Well-boxed Graphs

The graphs used to construct the DGoIM are essentially MELL proof structures [15] of the multiplicative and exponential fragment of linear logic. They are directed, and built over the fixed set of nodes called “generators” shown in Fig. 2.

A $\mathsf{C}_{n}$-node is annotated by a natural number $n$ that indicates its in-degree, i.e. the number of incoming edges. It generalises a contraction node, whose in-degree is $2$, and a weakening node, whose in-degree is [math], of MELL proof structures. In Fig. 2, a bunch of $n$ edges is depicted by a single arrow with a strike-out.

Graphs must satisfy the well-formedness condition below. Note that, unlike the usual approach [15], we need not assign MELL formulas to edges, nor require a graph to be a valid proof net.

Definition 2.1** (well-boxed).**

A directed graph $G$ built over the generators in Fig. 2 is well-boxed if:

• •

it has no incoming edges

• •

each $\oc$-node $v$ in $G$ comes with a sub-graph $H$ of $G$ and an arbitrary number of $\wn$-nodes $\vec{u}$ such that:

• –

the sub-graph $H$ (called “$\oc$-box”) is well-boxed inductively and has at least one outgoing edges

• –

the $\oc$-node $v$ (called “principal door of $H$”) is the target of one outgoing edge of $H$

• –

the $\wn$-nodes $\vec{u}$ (called “auxiliary doors of $H$”) are the targets of all the other outgoing edges of $H$

• •

each $\wn$-node is an auxiliary door of exactly one $\oc$-box

• •

any two distinct $\oc$-boxes with distinct principal doors are either disjoint or nested

Note that a $\oc$-box might have no auxiliary doors. We use a dashed box to indicate a $\oc$-box together with its principal door and its auxiliary doors, as in Fig. 2. The auxiliary doors are depicted by a single $\wn$-node with a thick frame and with single incoming and outgoing arrows with strike-outs. Directions of edges are omitted in the rest of the paper, if not ambiguous, to reduce visual clutter.

2.2 Pass Transitions and Rewrite Transitions

The DGoIM is formalised as a labelled transition system with two kinds of transitions, namely pass transitions $\dashrightarrow$ and rewrite transitions $\rightsquigarrow$. Labels of transitions are $\mathsf{b},\mathsf{s},\mathsf{o}$ that stand for “beta,” “substitution,” and “overheads” respectively.

Let $\mathcal{L}$ be a fixed countable (infinite) set of names. The state of the transition system $s=(\mathbb{G},p,h,m)$ consists of the following elements:

• •

a named well-boxed graph $\mathbb{G}=(G,\ell_{G})$, that is a well-boxed graph $G$ with a naming $l_{G}$ that assigns a unique name $\alpha\in\mathcal{L}$ to each node of $G$

• •

a pair $p=(e,d)$ called position, of an edge $e$ of $G$ and a direction $d\in\{\uparrow,\downarrow\}$

• •

a history stack $h$ defined by the grammar $h::=\square\mid\mathsf{Ax}_{\alpha}:h\mid\mathsf{Cut}_{\alpha}:h\mid\otimes_{\alpha}:h\mid\parr_{\alpha}:h\mid\oc_{\alpha}:h\mid\mathsf{D}_{\alpha}:h\mid\mathsf{C}^{n}_{\alpha}:h$, where $\alpha\in\mathcal{L}$ and $n$ is some positive natural number.

• •

a multiplicative stack $m$ defined by the BNF grammar $m::=\square\mid\mathsf{l}:m\mid\mathsf{r}:m$.

We refer to a node by its name, i.e. we say “a node $\alpha$” instead of “a node whose name is $\alpha$.”

A pass transition $(\mathbb{G},p,h,m)\dashrightarrow_{\mathsf{o}}(\mathbb{G},p^{\prime},h^{\prime},m^{\prime})$ changes a position using a multiplicative stack, pushes to a history stack, and keeps a named graph unchanged. All pass transitions have the label $\mathsf{o}$.

Fig. 3 shows pass transitions graphically, omitting irrelevant parts of graphs. A position $p=(e,d)$ is represented by a bullet $\bullet$ (called “token”) on the edge $e$ together with the direction $d$. Recall that an edge with a strike-out represents a bunch of edges. The transition in the last line of Fig. 3 (where we assume $n>0$) moves a token from one of the incoming edges of a $\mathsf{C}_{n}$-node to the outgoing edge of the node. Node names $\alpha\in\mathcal{L}$ are indicated wherever needed.

A rewrite transition $(\mathbb{G},(e,d),h,m)\rightsquigarrow_{\mathsf{x}}(\mathbb{G}^{\prime},(e^{\prime},d),h^{\prime},m)$ consumes some elements of a history stack, rewrites a sub-graph of a named graph, and updates a position (or, more precisely, its edge). The label $\mathsf{x}$ of a rewrite transition $\rightsquigarrow_{\mathsf{x}}$ is either $\mathsf{b}$, $\mathsf{s}$ or $\mathsf{o}$. Fig. 4 shows rewrite transition in the same manner as Fig. 3. Multiplicative stacks are not present in the figure since they are irrelevant. The $\sharp$-node represents some arbitrary node (incoming edges omitted). We can see that no rewrite transition breaks the well-boxed-ness of a graph.

The rewrite transitions (1),(2),(3), and (4) are exactly taken from MELL cut elimination [15]. The rewrite transition (5) is a variant of (1). It acts on a connected pair of a $\mathsf{Cut}$-node and an $\mathsf{Ax}$-node that arises as a result of the transition (6) or (7) but cannot be rewritten by the transition (1). These transitions (6) and (7) are inspired by the MELL cut elimination process for (binary) contraction nodes; note that we assume $n>0$ in Fig. 4.

The rewrite transition (6) in Fig. 4 deserves further explanation. The sub-graph $H^{\approx}$ is a copy of the $\oc$-box $H$ where all the names are replaced with fresh ones. The thick $\mathsf{C}_{g+f^{-1}}$-node and $\mathsf{C}_{g+2f^{-1}}$-node represent families $\{\mathsf{C}_{g(j)+f^{-1}(j)}\}_{j=0}^{m},\{\mathsf{C}_{g(j)+2f^{-1}(j)}\}_{j=0}^{m},$ of $\mathsf{C}$-nodes respectively. They are connected to $\wn$-nodes $\vec{\epsilon}=\epsilon_{0},\ldots,\epsilon_{l}$ and $\vec{\mu}=\mu_{0},\ldots,\mu_{l}$ in such a way that:

• •

the natural numbers $l,m$ satisfy $l\geq m$, and come with a surjection $f\colon\{0,\ldots,l\}\twoheadrightarrow\{0,\ldots,m\}$ and a function $g\colon\{0,\ldots,m\}\to\mathbb{N}$ to the set $\mathbb{N}$ of natural numbers

• •

each $\wn$-node $\epsilon_{i}$ and each $\wn$-node $\mu_{i}$ are both connected to the $\mathsf{C}$-node $\phi_{f(i)}$

• •

each $\mathsf{C}$-node $\phi_{j}$ has $g(j)$ incoming edges whose source is none of the $\wn$-nodes $\vec{\epsilon},\vec{\mu}$.

Some rewrite transitions introduce new nodes to a graph. We require that the uniqueness of names throughout a whole graph is not violated by these transitions. Under this requirement, the introduced names $\nu,\vec{\mu}$ and the renaming $H^{\approx}$ in Fig. 4 can be arbitrary.

Definition 2.2**.**

We call a state $((G,\ell_{G}),p,h,m)$ rooted at $e_{0}$ for an open (outgoing) edge $e_{0}$ of $G$, if there exists a finite sequence $((G,\ell_{G}),(e_{0},\uparrow),\square,\square)\dashrightarrow^{*}((G,\ell_{G}),p,h,m)$ of pass transitions such that the position $p$ appears only last in the sequence.

Lem. 2.3(1) below implies that, the DGoIM can determine whether a rewrite transition is possible at a rooted state by only examining a history stack. The rooted property is preserved by transitions.

Lemma 2.3** (rooted states).**

Let $((G,\ell_{G}),(e,d),h,m)$ be a rooted state at $e_{0}$ with a (finite) sequence

[TABLE]

History stack represents an (undirected and possibly cyclic) path of the graph $G$ connecting edges $e_{0}$ and $e$. 2. 2.

*If a transition $((G,\ell_{G}),(e,d),h,m)\mathrel{(\dashrightarrow\cup\rightsquigarrow)}((G^{\prime},\ell_{G^{\prime}}),p^{\prime},h^{\prime},m^{\prime})$ is possible, the open edges of $G^{\prime}$ are bijective to those of $G$, and the state $((G^{\prime},\ell_{G^{\prime}}),p^{\prime},h^{\prime},m^{\prime})$ is rooted at the open edge corresponding to $e_{0}$. *

Proof.

(Sketch.) The proof of the first part is by induction on the length of the sequence of move transitions. For the second part, rewrite transitions $\rightsquigarrow$ modify open edges of a graph in a bijective way. The edge that a state is rooted at can be modified only by the rewrite transitions (1) and (5) involving $\mathsf{Ax}$-nodes. ∎

2.3 Cost Analysis of the DGoIM

The time cost of updating stacks is constant, as each transition changes only a fixed number of top elements of stacks. Updating a position is local and needs constant time, as it does not require searching beyond the next edge in the graph from the current edge. We can conclude all pass transitions take constant time.

We estimate the time cost of rewrite transitions by counting updated nodes. The rewrite transitions (1)–(3) involve a fixed number of nodes, and the transition (7) eliminates one $\mathsf{C}_{1}$-node. Only the transitions (4) and (6) have non-constant time cost. The number of doors deleted in the transition (4) can be arbitrary, and so is the number of nodes introduced in the transition (6).

Pass transitions and rewrite transitions are separately deterministic (up to the choice of new names). However, both a pass transition and a rewrite transition are possible at some states. We here opt for the following “rewrites-first” way to interleave pass transitions with as much rewrite transitions as possible:

[TABLE]

The DGoIM with this strategy yields a deterministic labelled transition system $\rightarrowtriangle$ up to the choice of new names in rewrite transitions. We denote it by DGoIM⇾, making the strategy explicit. Note that there can be other strategies of interleaving although we do not explore them here.

Before we conclude, several considerations about space cost analysis. Space costs are generally bound by time costs, so from our analysis there is an implicit guarantees that space usage will not explode. But if a more refined space cost analysis is desired, the following might prove to be useful.

The space required in implementing a named well-boxed graph is bounded by the number of its nodes. The number of edges is linear in the number of nodes, because each generator has a fixed out-degree and every edge of a well-boxed graph has its source.

Additionally a $\oc$-box can be represented by associating its auxiliary doors to its principal door. This adds connections between doors to a graph that are as many as $\wn$-nodes. It enables the DGoIM to identify nodes of a $\oc$-box by following edges from its principal and auxiliary doors. Nodes in a $\oc$-box that are not connected to doors can be ignored, since these nodes are never visited by a token (i.e. pointed by a position) as long as the DGoIM acts on rooted states.

Only the rewrite transition (6) can increase the number of nodes of a graph by copying a $\oc$-box with its doors. Rewrite transitions can copy $\oc$-boxes and eliminate the $\oc$-box structure, but they never create new $\oc$-boxes or change existing ones. This means that, in a sequence of transitions that starts with a graph $G$, any $\oc$-boxes copied by the rewrite transition (6) are sub-graphs of the graph $G$. Therefore the number of nodes of a graph increases linearly in the number of transitions.

Elements of history stacks and multiplicative stacks, as well as a position, are essentially pointers to nodes. Because each pass/rewrite transition adds at most one element to each stack, the lengths of stacks also grow linearly in the number of transitions.

3 Weak Simulation of the Call-by-Need SAM

3.1 Storeless Abstract Machine (SAM)

We show the DGoIM⇾ implements call-by-need evaluation by building a weak simulation of the call-by-need Storeless Abstract Machine (SAM) defined in Fig. 5. It simplifies Danvy and Zerny’s storeless machine [10, Fig. 8] and accommodates a partial mechanism of garbage collection (namely, transition (13)). We will return to a discussion of garbage collection at the end of this section.

The SAM is a labelled transition system between configurations $(\overline{t},E)$. They are classified into two groups, namely term configurations and context configurations, that are indicated by annotations $\mathit{term},\mathit{ctxt}$ respectively. Pure terms (resp. pure values) are terms (resp. values) that contain no explicit substitutions $t[x\leftarrow u]$; we sometimes omit the word “pure” and the overline in denotation as long as that raises no confusion.

Each evaluation context $E$ contains exactly one open hole $\langle\cdot\rangle$, and replacing it with a term $t$ (or an evaluation context $E^{\prime}$) yields a term $E\langle t\rangle$ (or an evaluation context $E\langle E^{\prime}\rangle$) called plugging. In particular an evaluation context $E^{\prime}\langle x\rangle[x\leftarrow E]$ replaces the open hole of $E^{\prime}$ with $x$ and keeps the open hole of $E$.

Labels of transitions are the same as those used for the DGoIM (i.e. $\mathsf{b}$, $\mathsf{s}$ and $\mathsf{o}$). The transition (11), with the label $\mathsf{b}$, corresponds to the $\beta$-reduction where evaluation and substitution of function arguments are delayed. Substitution happens in the transitions (12) and (13), with the label $\mathsf{s}$, that replaces exactly one occurrence of a variable. The other transitions with the label $\mathsf{o}$, namely $(\overline{t},E)\to_{\mathsf{o}}(\overline{t^{\prime}},E^{\prime})$, search a redex by rearranging a configuration. The two pluggings $E\langle\overline{t}\rangle$ and $E^{\prime}\langle\overline{t^{\prime}}\rangle$ indeed yield exactly the same term.

We characterise “free” variables using multisets of variables. Multisets make explicit how many times a variable is duplicated in a term (or an evaluation context). This information of duplication is later used in translating terms to graphs.

Notation** (multiset).**

A multiset $\mathbf{x}:=[x,\ldots,x]$ consists of a finite number of $x$. The multiplicity of $x$ in a multiset $M$ is denoted by $M(x)$. We write $x\in^{k}M$ if $M(x)=k$, $x\in M$ if $M(x)>0$ and $x\notin M$ if $M(x)=0$. A multiset $M$ comes with its support set $\mathrm{supp}(M)$. For two multisets $M$ and $M^{\prime}$, their sum and difference are denoted by $M+M^{\prime}$ and $M-M^{\prime}$ respectively. Removing all $x$ from a multiset $M$ yields the multiset $M\backslash x$, e.g. ${[x,x,y]\backslash x}=[y]$.

Each term $t$ and each evaluation context $E$ are respectively assigned multisets of variables $\mathrm{FV}(t),\mathrm{FV}_{M}(E)$, with $M$ a multiset of variables. The multisets $\mathrm{FV}$ are defined inductively as follows.

[TABLE]

The following equations can be proved by a straightforward induction on $E$.

Lemma 3.1** (decomposition).**

[TABLE]

A variable $x$ is bound in a term $t$ if it appears in the form of $\lambda{x}.u$ or $u[x\to u^{\prime}]$. A variable $x$ is captured in an evaluation context $E$ if it appears in the form of $E^{\prime}[x\leftarrow\overline{t}]$ (but not in the form of $E^{\prime}\langle x\rangle[x\leftarrow E^{\prime\prime}]$). The transitions (12) and (13) depend on whether or not the bound variable $x$ appears in the evaluation context $E_{2}$. If the variable $x$ appears, the value $\overline{v}$ is kept for later use and its copy $\overline{v}^{\approx}$ is substituted for $x$. If not, the value $\overline{v}$ itself is substituted for $x$.

The SAM does not assume the $\alpha$-equivalence, but explicitly deals with it in copying a value. The copy $\overline{v}^{\approx}$ in has all its bound variables replaced by distinct fresh variables (i.e. distinct variables that do not appear in a whole configuration). This implies that the SAM is deterministic up to the choice of new variables introduced in copying.

A term $t$ is closed if $\mathrm{FV}(t)=\emptyset$; and is well-named if each variable gets bound at most once in $t$, and each bound variable $x$ in $t$ satisfies $x\notin\mathrm{FV}(t)$. An initial configuration is a term configuration $(\overline{t_{0}},\langle\cdot\rangle)_{\mathit{term}}$ where $\overline{t_{0}}$ is closed and well-named. A finite sequence of transitions from an initial configuration is called an execution. A reachable configuration $(\overline{t},E)$, that is a configuration coming with an execution from some initial configuration to itself, satisfies the following invariant properties.

Lemma 3.2** (reachable configurations).**

Let $(\overline{t},E)$ be a reachable configuration from an initial configuration $(\overline{t_{0}},\langle\cdot\rangle)_{\mathit{term}}$. The term $\overline{t}$ is a sub-term of the initial term $\overline{t_{0}}$ up to $\alpha$-equivalence, and the plugging $E\langle\overline{t}\rangle$ is closed and well-named.

Proof.

(Sketch.) The proof is by induction on the length of the execution $(\overline{t_{0}},\langle\cdot\rangle)_{\mathit{term}}\to^{*}(\overline{t},E)$. Not only the term $\overline{t}$ but also the term $u^{\prime}$ in any sub-term $t^{\prime}\,u^{\prime}$ or $t^{\prime}[x\leftarrow u^{\prime}]$ of the plugging $E\langle\overline{t}\rangle$ is a sub-term of the initial term $\overline{t_{0}}$. The transition (12) renames a value in the way that preserves closedness and the well-named-ness of pluggings. In the transition (13) where an explicit substitution for a bound variable $x$ is eliminated, the induction hypothesis ensures that the variable $x$ does not occur in the plugging $E_{1}\langle A\langle E_{2}\langle\overline{v}\rangle\rangle\rangle$. ∎

We now conclude with a brief consideration on garbage collection. Transition (13) eliminates an explicit substitution and therefore implements a partial mechanism of garbage collection. The mechanism is partial because only an explicit substitution that is looked up in an execution can be eliminated, as illustrated below. The explicit substitution $[x\leftarrow\lambda{z}.z]$ is eliminated in the first example, but not in the second example because the bound variable $x$ does not occur.

[TABLE]

We incorporate this partial garbage collection to make clear the behaviour of the DGoIM⇾, in particular the use of the rewrite transitions (6) and (7).

3.2 Translation and Weak Simulation

A weak simulation is built on top of translations of terms and evaluation contexts. The translations $(\cdot)^{\dagger}$ are inductively defined in Fig. 6 and Fig. 7. What underlies them is the so-called “call-by-value” translation of intuitionistic logic to linear logic. This translates all and only values to $\oc$-boxes that can be copied by rewrite transitions.

The translation t^{\dagger}$$\mid$$\mathrm{FV}(t) of a term $t$ is a well-boxed graph, where some edges are annotated with variables to help understanding. We continue representing a bunch of edges by a single edge and a strike-out, with annotations denoted by a multiset, and a bunch of nodes by a single thick node. The translation E_{M}^{\dagger}$$\mid$$M$$\mid$$\mathrm{FV}_{M}(E) of an evaluation context $E$, given a multiset $M$ of variables, is not a well-boxed graph because it has incoming edges. Lem. 3.3 is analogous to Lem. 3.1; their proof is by straightforward induction on $E$.

Lemma 3.3** (decomposition).**

[TABLE]

The translations $(\cdot)^{\dagger}$ are lifted to a binary relation between reachable configurations of the SAM and rooted states of the DGoIM⇾.

Definition 3.4** (binary relation $\preceq$).**

A reachable configuration $c$ and a state $((G,\ell_{G}),p,h,m)$ satisfies $c\preceq((G,\ell_{G}),p,h,m)$ if and only if:

• •

(G,p)=\begin{cases}\leavevmode\hbox to63.08pt{\vbox to43.62pt{\pgfpicture\makeatletter\hbox{\hskip 45.8078pt\lower-8.73547pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}{} {}{{}}{}{}{}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-17.07095pt}{21.3387pt}\pgfsys@moveto{-17.07095pt}{21.3387pt}\pgfsys@lineto{-17.07095pt}{34.1419pt}\pgfsys@lineto{17.07095pt}{34.1419pt}\pgfsys@lineto{17.07095pt}{21.3387pt}\pgfsys@closepath\pgfsys@moveto{17.07095pt}{34.1419pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.74445pt}{23.92921pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\overline{t}^{\dagger}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-17.07095pt}{0.0pt}\pgfsys@moveto{-17.07095pt}{0.0pt}\pgfsys@lineto{-17.07095pt}{12.8032pt}\pgfsys@lineto{17.07095pt}{12.8032pt}\pgfsys@lineto{17.07095pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{17.07095pt}{12.8032pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.08473pt}{3.84828pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{E_{\mathrm{FV}(\overline{t})}^{\dagger}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{-12.80269pt}{21.33784pt}\pgfsys@lineto{-12.80269pt}{12.80269pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}

{{}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.5}{-0.86603}{0.86603}{0.5}{-14.16248pt}{16.9257pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\tiny$\mid$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-42.8078pt}{14.56958pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathrm{FV}(\overline{t})$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{12.80269pt}{21.33784pt}\pgfsys@lineto{12.80269pt}{12.80269pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{{}} {}{}{}{}{}{}{}{} }{{}}\pgfsys@moveto{12.80217pt}{17.06958pt}\pgfsys@moveto{14.93604pt}{17.06958pt}\pgfsys@curveto{14.93604pt}{18.2481pt}{13.98068pt}{19.20345pt}{12.80217pt}{19.20345pt}\pgfsys@curveto{11.62366pt}{19.20345pt}{10.6683pt}{18.2481pt}{10.6683pt}{17.06958pt}\pgfsys@curveto{10.6683pt}{15.89107pt}{11.62366pt}{14.93571pt}{12.80217pt}{14.93571pt}\pgfsys@curveto{13.98068pt}{14.93571pt}{14.93604pt}{15.89107pt}{14.93604pt}{17.06958pt}\pgfsys@closepath\pgfsys@moveto{12.80217pt}{17.06958pt}\pgfsys@fill\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.26917pt}{14.56958pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\uparrow$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}}{}{} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{12.80269pt}{0.0pt}\pgfsys@lineto{12.80269pt}{-8.53548pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&\text{(if $c=(\overline{t},E)_{\mathit{term}}$)}\ \leavevmode\hbox to67.35pt{\vbox to64.42pt{\pgfpicture\makeatletter\hbox{\hskip 45.8078pt\lower-8.73547pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}{} {}{{}}{}{}{}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-17.07095pt}{38.40965pt}\pgfsys@moveto{-17.07095pt}{38.40965pt}\pgfsys@lineto{-17.07095pt}{51.21288pt}\pgfsys@lineto{17.07095pt}{51.21288pt}\pgfsys@lineto{17.07095pt}{38.40965pt}\pgfsys@closepath\pgfsys@moveto{17.07095pt}{51.21288pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.90001pt}{41.35016pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\overline{v}^{\diamond}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{ }{}\pgfsys@moveto{-42.6774pt}{25.60643pt}\pgfsys@moveto{-42.6774pt}{25.60643pt}\pgfsys@lineto{-42.6774pt}{55.48062pt}\pgfsys@lineto{21.3387pt}{55.48062pt}\pgfsys@lineto{21.3387pt}{25.60643pt}\pgfsys@closepath\pgfsys@moveto{21.3387pt}{55.48062pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{} {}{{}}{}{}{}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-17.07095pt}{0.0pt}\pgfsys@moveto{-17.07095pt}{0.0pt}\pgfsys@lineto{-17.07095pt}{12.8032pt}\pgfsys@lineto{17.07095pt}{12.8032pt}\pgfsys@lineto{17.07095pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{17.07095pt}{12.8032pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.08473pt}{3.84828pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$E_{\mathrm{FV}(\overline{v})}^{\dagger}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}

{}{{}}{}{{{}} {}{}{}{}{}{}{}{} }{{}}\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }{}\pgfsys@moveto{-12.8032pt}{25.60643pt}\pgfsys@moveto{-8.53548pt}{25.60643pt}\pgfsys@curveto{-8.53548pt}{27.96346pt}{-10.44618pt}{29.87416pt}{-12.8032pt}{29.87416pt}\pgfsys@curveto{-15.16023pt}{29.87416pt}{-17.07094pt}{27.96346pt}{-17.07094pt}{25.60643pt}\pgfsys@curveto{-17.07094pt}{23.2494pt}{-15.16023pt}{21.3387pt}{-12.8032pt}{21.3387pt}\pgfsys@curveto{-10.44618pt}{21.3387pt}{-8.53548pt}{23.2494pt}{-8.53548pt}{25.60643pt}\pgfsys@closepath\pgfsys@moveto{-12.8032pt}{25.60643pt}\pgfsys@fillstroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.33792pt}{22.18977pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\wn$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}{}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ } {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.4074pt}{22.77266pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{{}} {}{}{}{}{}{}{}{} }\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}\pgfsys@moveto{-12.8032pt}{25.60643pt}\pgfsys@moveto{-8.53548pt}{25.60643pt}\pgfsys@curveto{-8.53548pt}{27.96346pt}{-10.44618pt}{29.87416pt}{-12.8032pt}{29.87416pt}\pgfsys@curveto{-15.16023pt}{29.87416pt}{-17.07094pt}{27.96346pt}{-17.07094pt}{25.60643pt}\pgfsys@curveto{-17.07094pt}{23.2494pt}{-15.16023pt}{21.3387pt}{-12.8032pt}{21.3387pt}\pgfsys@curveto{-10.44618pt}{21.3387pt}{-8.53548pt}{23.2494pt}{-8.53548pt}{25.60643pt}\pgfsys@closepath\pgfsys@moveto{-12.8032pt}{25.60643pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
{}{{}}{}{{{}} {}{}{}{}{}{}{}{} }{{}}\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }{}\pgfsys@moveto{12.8032pt}{25.60643pt}\pgfsys@moveto{17.07094pt}{25.60643pt}\pgfsys@curveto{17.07094pt}{27.96346pt}{15.16023pt}{29.87416pt}{12.8032pt}{29.87416pt}\pgfsys@curveto{10.44618pt}{29.87416pt}{8.53548pt}{27.96346pt}{8.53548pt}{25.60643pt}\pgfsys@curveto{8.53548pt}{23.2494pt}{10.44618pt}{21.3387pt}{12.8032pt}{21.3387pt}\pgfsys@curveto{15.16023pt}{21.3387pt}{17.07094pt}{23.2494pt}{17.07094pt}{25.60643pt}\pgfsys@closepath\pgfsys@moveto{12.8032pt}{25.60643pt}\pgfsys@fillstroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{8.2685pt}{22.18977pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\oc$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}{}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ } {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{17.19904pt}{22.77266pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{-12.80269pt}{38.40811pt}\pgfsys@lineto{-12.80269pt}{29.87297pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}

{{}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.5}{-0.86603}{0.86603}{0.5}{-14.16248pt}{33.9953pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\tiny$\mid$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-42.8078pt}{31.63918pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathrm{FV}(\overline{v})$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{12.80269pt}{38.40811pt}\pgfsys@lineto{12.80269pt}{29.87297pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{{}} {}{}{}{}{}{}{}{} }{{}}\pgfsys@moveto{12.80217pt}{34.13918pt}\pgfsys@moveto{14.93604pt}{34.13918pt}\pgfsys@curveto{14.93604pt}{35.31769pt}{13.98068pt}{36.27304pt}{12.80217pt}{36.27304pt}\pgfsys@curveto{11.62366pt}{36.27304pt}{10.6683pt}{35.31769pt}{10.6683pt}{34.13918pt}\pgfsys@curveto{10.6683pt}{32.96066pt}{11.62366pt}{32.00531pt}{12.80217pt}{32.00531pt}\pgfsys@curveto{13.98068pt}{32.00531pt}{14.93604pt}{32.96066pt}{14.93604pt}{34.13918pt}\pgfsys@closepath\pgfsys@moveto{12.80217pt}{34.13918pt}\pgfsys@fill\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.26917pt}{31.63918pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\uparrow$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{-12.80269pt}{21.33784pt}\pgfsys@lineto{-12.80269pt}{12.80269pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}

{{}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.5}{-0.86603}{0.86603}{0.5}{-14.16248pt}{16.9257pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\tiny$\mid$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-42.8078pt}{14.56958pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathrm{FV}(\overline{v})$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{12.80269pt}{21.33784pt}\pgfsys@lineto{12.80269pt}{12.80269pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}}{}{} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{12.80269pt}{0.0pt}\pgfsys@lineto{12.80269pt}{-8.53548pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&\parbox[c]{113.81102pt}{ (if \overline{v}^{\dagger}=\leavevmode\hbox to54.54pt{\vbox to53.55pt{\pgfpicture\makeatletter\hbox{\hskip 39.40671pt\lower-2.13387pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}{} {}{{}}{}{}{}{}{{}}{}{}{}{{{}{}}}{}\pgfsys@moveto{-10.66934pt}{34.1419pt}\pgfsys@moveto{-10.66934pt}{34.1419pt}\pgfsys@lineto{-10.66934pt}{46.94513pt}\pgfsys@lineto{10.66934pt}{46.94513pt}\pgfsys@lineto{10.66934pt}{34.1419pt}\pgfsys@closepath\pgfsys@moveto{10.66934pt}{46.94513pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.90001pt}{37.08241pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\overline{v}^{\diamond}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{ }{}\pgfsys@moveto{-36.27579pt}{21.3387pt}\pgfsys@moveto{-36.27579pt}{21.3387pt}\pgfsys@lineto{-36.27579pt}{51.21288pt}\pgfsys@lineto{14.93709pt}{51.21288pt}\pgfsys@lineto{14.93709pt}{21.3387pt}\pgfsys@closepath\pgfsys@moveto{14.93709pt}{51.21288pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{{}}{}{{{}} {}{}{}{}{}{}{}{} }{{}}\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }{}\pgfsys@moveto{-6.4016pt}{21.3387pt}\pgfsys@moveto{-2.13387pt}{21.3387pt}\pgfsys@curveto{-2.13387pt}{23.69572pt}{-4.04457pt}{25.60643pt}{-6.4016pt}{25.60643pt}\pgfsys@curveto{-8.75862pt}{25.60643pt}{-10.66933pt}{23.69572pt}{-10.66933pt}{21.3387pt}\pgfsys@curveto{-10.66933pt}{18.98167pt}{-8.75862pt}{17.07097pt}{-6.4016pt}{17.07097pt}\pgfsys@curveto{-4.04457pt}{17.07097pt}{-2.13387pt}{18.98167pt}{-2.13387pt}{21.3387pt}\pgfsys@closepath\pgfsys@moveto{-6.4016pt}{21.3387pt}\pgfsys@fillstroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.93631pt}{17.92204pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\wn}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}{}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ } {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.00578pt}{18.50491pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{{}} {}{}{}{}{}{}{}{} }\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}\pgfsys@moveto{-6.4016pt}{21.3387pt}\pgfsys@moveto{-2.13387pt}{21.3387pt}\pgfsys@curveto{-2.13387pt}{23.69572pt}{-4.04457pt}{25.60643pt}{-6.4016pt}{25.60643pt}\pgfsys@curveto{-8.75862pt}{25.60643pt}{-10.66933pt}{23.69572pt}{-10.66933pt}{21.3387pt}\pgfsys@curveto{-10.66933pt}{18.98167pt}{-8.75862pt}{17.07097pt}{-6.4016pt}{17.07097pt}\pgfsys@curveto{-4.04457pt}{17.07097pt}{-2.13387pt}{18.98167pt}{-2.13387pt}{21.3387pt}\pgfsys@closepath\pgfsys@moveto{-6.4016pt}{21.3387pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{{}}{}{{{}} {}{}{}{}{}{}{}{} }{{}}\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }{}\pgfsys@moveto{6.4016pt}{21.3387pt}\pgfsys@moveto{10.66933pt}{21.3387pt}\pgfsys@curveto{10.66933pt}{23.69572pt}{8.75862pt}{25.60643pt}{6.4016pt}{25.60643pt}\pgfsys@curveto{4.04457pt}{25.60643pt}{2.13387pt}{23.69572pt}{2.13387pt}{21.3387pt}\pgfsys@curveto{2.13387pt}{18.98167pt}{4.04457pt}{17.07097pt}{6.4016pt}{17.07097pt}\pgfsys@curveto{8.75862pt}{17.07097pt}{10.66933pt}{18.98167pt}{10.66933pt}{21.3387pt}\pgfsys@closepath\pgfsys@moveto{6.4016pt}{21.3387pt}\pgfsys@fillstroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.86688pt}{17.92204pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\oc$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}{}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ } {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.79742pt}{18.50491pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{-6.40134pt}{34.14053pt}\pgfsys@lineto{-6.40134pt}{25.6054pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}

{{}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.5}{-0.86603}{0.86603}{0.5}{-7.76138pt}{29.72789pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\tiny$\mid$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-36.40671pt}{27.37177pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathrm{FV}(\overline{v})$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{6.40134pt}{34.14053pt}\pgfsys@lineto{6.40134pt}{25.6054pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}}{}{} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{-6.40134pt}{17.07027pt}\pgfsys@lineto{-6.40134pt}{8.53479pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}

{{}}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.5}{-0.86603}{0.86603}{0.5}{-7.76138pt}{12.65813pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\tiny$\mid$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-36.40671pt}{10.302pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathrm{FV}(\overline{v})$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}}{}{} {}{}{}{}{{{}{}}}{}{}{{{}{}}}{}\pgfsys@moveto{6.40134pt}{17.07027pt}\pgfsys@lineto{6.40134pt}{8.53479pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$\\ and$c=(\overline{v},E)_{\mathit{ctxt}})}\end{cases}

• •

$\ell_{G}$ is an arbitrary naming

• •

$((G,\ell_{G}),p,h,m)$ is rooted at the unique open edge of $G$.

Note that the graph $G$ in the above definition has exactly one open edge, because it is equal to the translation $E\langle\overline{t}\rangle^{\dagger}$ (Lem. 3.3) and the plugging $E\langle\overline{t}\rangle$ is closed (Lem. 3.2).

The binary relation $\preceq$ gives a weak simulation, as stated below. It is weak in Milner’s sense [21], where transitions with the label $\mathsf{o}$ are regarded as internal. We can conclude from Thm. 3.5 below that the DGoIM⇾ soundly implements the call-by-need evaluation.

Theorem 3.5** (weak simulation).**

Let a configuration $c$ and a state $s$ satisfy $c\preceq s$.

If a transition $c\to_{\mathsf{b}}c^{\prime}$ of the SAM is possible, there exists a sequence $s\rightarrowtriangle_{\mathsf{o}}^{2}\rightarrowtriangle_{\mathsf{b}}\rightarrowtriangle_{\mathsf{o}}s^{\prime}$ such that $c^{\prime}\preceq s^{\prime}$. 2. 2.

If a transition $c\to_{\mathsf{s}}c^{\prime}$ of the SAM is possible, there exists a sequence $s\rightarrowtriangle_{\mathsf{s}}\rightarrowtriangle_{\mathsf{o}}s^{\prime}$ such that $c^{\prime}\preceq s^{\prime}$. 3. 3.

If a transition $c\to_{\mathsf{o}}c^{\prime}$ of the SAM is possible, there exists a sequence $s\rightarrowtriangle_{\mathsf{o}}^{N}s^{\prime}$ such that $0<N\leq 4$ and $c^{\prime}\preceq s^{\prime}$. 4. 4.

No transition $\rightarrowtriangle$ is possible at the state $s^{\prime}$ if $c^{\prime}=(\overline{v},A)_{\mathit{ctxt}}$.

Proof.

We start with two basic observations. First, only a pass transition is possible at a state $s$ that satisfies $(\overline{t},E)_{\mathit{term}}\preceq s$, and second, no transition is possible at a state $s$ that satisfies $(\overline{v},A)_{\mathit{ctxt}}\preceq s$.

Fig. 8 shows how the DGoIM⇾ simulates each transition of the SAM. Stacks, annotations of edges, and some annotations of $\mathsf{C}$-nodes are omitted. The equations in Fig. 8 apply the decomposition properties in Lem. 3.3 as well as the other decomposition properties in the following Lem. 3.6. In the application, we exploit the closedness and well-named-ness of reachable configurations (in the sense of Lem. 3.2).

∎

Lemma 3.6** (decomposition).**

Let $M_{0},M$ be multisets of variables.

*The translation $A_{M}^{\dagger}$ of a substitution context $A$ has a unique decomposition * A_{M}^{\ddagger}$$\mid$$M$$\mid$$\mathrm{FV}_{M}(A) . 2. 2.

*If no variables in $M_{0}$ are captured in an evaluation context $E$, the translation $E_{M_{0}+M}^{\dagger}$ is equal to the graph * E_{M}^{\dagger}$$\mid$$M_{0}$$\mid$$M$$\mid$$\mathrm{FV}_{M}(E) . 3. 3.

*If each variable in $M_{0}$ is captured in an evaluation context $E$ exactly once, the translation $E_{M_{0}+M}^{\dagger}$ has a unique decomposition * E_{M}^{{\dagger}{\dagger}}$$\mathsf{C}_{M_{0}+M_{1}}$$\mathsf{Cut}$$\mid$$M$$\mid$$\mathrm{FV}_{M_{0}+M}(E)$$\mid$$M_{0}$$\mid$$M_{1}$$\mid$$\mathrm{supp}(M_{0})$$\mid . The multiset $M_{1}$ satisfies $\mathrm{supp}(M_{1})\subseteq\mathrm{supp}(M_{0})$, and the thick $\mathsf{C}_{M_{0}+M_{1}}$-node represents a family $\{\mathsf{C}_{M_{0}(x)+M_{1}(x)}\}_{x\in\mathrm{supp}(M_{0})}$ of $\mathsf{C}$-nodes.

Proof.

The proofs for 1. and 2. are by straightforward inductions on $A$ and $E$ respectively. The proof for 3. is by induction on the dimension of $M_{0}$, i.e. the size of the support set $\mathrm{supp}(M_{0})$. The base case where $M_{0}=\emptyset$ is obvious. In the inductive case, let $x$ satisfy $x\in M_{0}$. Since $x$ is captured exactly once in $E$ by assumption, the evaluation context $E$ can be decomposed as $E=E_{1}\langle E_{2}[x\leftarrow t]\rangle$ such that $x$ is not captured in $E_{1}$ or $E_{2}$. The evaluation context $E_{2}$ satisfies $x\in^{k}\mathrm{FV}_{M_{0}+M}(E_{2})$ for some positive multiplicity $k$. Moreover the multiset $M_{0}$ can be decomposed as $M_{0}=M_{1}+\mathbf{x}+M_{2}$ such that all the variables in $M_{1}$ (resp. $M_{2}$) are only captured in $E_{1}$ (resp. $E_{2}$). The translation $E_{M_{0}+M}^{\dagger}$ can be decomposed as in Fig. 9.

Finally, we let $E_{M}^{{\dagger}{\dagger}}$ consist of $(E_{2})_{M}^{{\dagger}{\dagger}},t^{\dagger},(E_{1})^{{\dagger}{\dagger}}$. ∎

4 Time Cost Analysis of Rewrites-First Interleaving

4.1 Recipe for Time Cost Analysis

Our time cost analysis of the DGoIM⇾ follows Accattoli’s recipe, described in [2, 1], of analysing complexity of abstract machines. This section recalls the recipe and explains how it applies to the DGoIM⇾.

The time cost analysis focuses on how efficiently an abstract machine implements an evaluation strategy. In other words, we are not interested in minimising the number of $\beta$-reduction steps simulated by an abstract machine. Our interest is in making the number of transitions of an abstract machine “reasonable,” compared to the number of necessary $\beta$-reduction steps determined by a given evaluation strategy.

Accattoli’s recipe assumes that an abstract machine has three groups of transitions: 1) “$\beta$-transitions” that correspond to $\beta$-reduction in which substitution is delayed, 2) transitions perform substitution, and 3) other “overhead” transitions. We incorporate this classification using the labels $\mathsf{b},\mathsf{s},\mathsf{o}$ of transitions.

Another assumption of the recipe is that, each step of $\beta$-reduction is simulated by a single transition of an abstract machine, and so is substitution of each occurrence of a variable. This is satisfied by many known abstract machines including the SAM, however not by the DGoIM⇾. The DGoIM⇾ has “finer” transitions and can take several transitions to simulate a single step of reduction (hence a single transition of the SAM, as we can observe in Thm. 3.5). In spite of this mismatch we can still follow the recipe, thanks to the weak simulation $\preceq$. It discloses what transitions of the DGoIM exactly correspond to $\beta$-reduction and substitution, and gives a concrete number of overhead transitions that the DGoIM⇾ needs to simulate $\beta$-reduction and substitution. The recipe for the time cost analysis is:

Examine the number of transitions, by means of the size of input and the number of $\beta$-transitions. 2. 2.

Estimate time cost of single transitions. 3. 3.

Derive a bound of the overall execution time cost. 4. 4.

Classify an abstract machine according to its execution time cost.

The last step is accompanied by the following taxonomy of abstract machines introduced in [1].

Definition 4.1** (classes of abstract machines [1, Def. 7.1]).**

An abstract machine is efficient if its execution time cost is linear in both the input size and the number of $\beta$-transitions. 2. 2.

An abstract machine is reasonable if its execution time cost is polynomial in the input size and the number of $\beta$-transitions. 3. 3.

An abstract machine is unreasonable if it is not reasonable.

The input size in our case is given by the size $|t|$ of a term $t$, inductively defined by:

[TABLE]

Given a sequence $r$ of transitions (of either the SAM or the DGoIM⇾), we denote the number of transitions with a label $\mathsf{x}$ in $r$ by $|r|_{\mathsf{x}}$. Since we use the fixed set $\{\mathsf{b},\mathsf{s},\mathsf{o}\}$ of labels, the length $|r|$ of the sequence $r$ is equal to the sum $|r|_{\mathsf{b}}+|r|_{\mathsf{s}}+|r|_{\mathsf{o}}$.

4.2 Number of Transitions

We first estimate the number of transitions of the SAM, and then derive estimation for the DGoIM⇾.

Lemma 4.2** (quantitative bounds for SAM).**

Each execution $e$ from an initial configuration $(\overline{t_{0}},E)_{\mathit{term}}$, comes with the following inequalities:

[TABLE]

Proof.

The proof is analogous to the discussion in [2, Sec. 11]. Let $|e|^{(\ref{SAM:O1})}$, $|e|^{(\ref{SAM:O2})}$ and $|e|^{(\ref{SAM:O3})}$ be the numbers of transitions (8), (9) and (10) in $e$, respectively. The number $|e|_{\mathsf{o}}$ is equal to the sum of these three numbers.

The transition (11) introduces one explicit substitution, and the other transitions never increase the number of explicit substitution. In particular the transition (12) copies a pure value, that means no explicit substitutions are copied. Therefore we can bound the number of transitions that concern explicit substitutions, and obtain $|e|^{(\ref{SAM:O2})}\leq|e|_{\mathsf{b}}$ and $|e|_{\mathsf{s}}\leq|e|_{\mathsf{b}}$.

Each occurrence of the transition (10) in an execution is either the last transition of the execution or followed by the transitions (11), (12) and (13). This yields the inequality $|e|^{(\ref{SAM:O3})}\leq|e|_{\mathsf{b}}+|e|_{\mathsf{s}}+1$ and hence $|e|^{(\ref{SAM:O3})}\leq 2\cdot|e|_{\mathsf{b}}+1$.

The transition (8) reduces the size of a pure term that is the first component of a configuration. The pure term is always a sub-term of the initial term $\overline{t_{0}}$ (Lem. 3.2). This means each maximal subsequence of an execution that solely consists of the transition (8) has at most the length $|\overline{t_{0}}|$. Such a maximal subsequence either occurs at the end of an execution or is followed by transitions other than the transition (8). Therefore the number of these maximal sub-sequences is no more than $|e|_{\mathsf{b}}+|e|_{\mathsf{s}}+|e|^{(\ref{SAM:O2})}+|e|^{(\ref{SAM:O3})}+1$ that can be bounded by $5\cdot|e|_{\mathsf{b}}+2$. A bound of the number $|e|^{(\ref{SAM:O1})}$ can be given by multiplying these two bounds, namely we obtain $|e|^{(\ref{SAM:O1})}\leq|\overline{t_{0}}|\cdot(5\cdot|e|_{\mathsf{b}}+2)$. ∎

Combining these bounds for the SAM with the weak simulation $\preceq$, we can estimate the number of transitions of the DGoIM⇾ as below.

Proposition 4.3** (quantitative bounds for DGoIM⇾).**

Let $r\colon s_{0}\rightarrowtriangle^{*}s$ be a sequence of transitions of the DGoIM⇾. If there exists an execution $(\overline{t_{0}},\langle\cdot\rangle)_{\mathit{term}}\to^{*}(\overline{t},E)$ of the SAM such that $s_{0}\preceq(\overline{t_{0}},\langle\cdot\rangle)_{\mathit{term}}$ and $s\preceq(\overline{t},E)$, the sequence $r$ comes with the following inequalities:

[TABLE]

Proof.

This is a direct consequence of Lem. 4.2 and Thm. 3.5. ∎

4.3 Execution Time Cost

We already discussed time cost of single transitions of the DGoIM in Sec. 2.3. It is worth noting that the discussion in Sec. 2.3 is independent of any particular choice of a rewriting and token-passing interleaving strategy.

Thm. 4.4 below gives a bound of execution time cost of the DGoIM⇾. We can conclude that, according to Accattoli’s taxonomy (see Def. 4.1), the DGoIM⇾ is “efficient” as an abstract machine for the call-by-need evaluation.

Theorem 4.4** (time cost).**

Let $C,D$ be fixed natural numbers, and $r\colon s_{0}\rightarrowtriangle^{*}s$ be a sequence of transitions of the DGoIM⇾. If there exists an execution $(\overline{t_{0}},\langle\cdot\rangle)_{\mathit{term}}\to^{*}(\overline{t},E)$ of the SAM such that $s_{0}\preceq(\overline{t_{0}},\langle\cdot\rangle)_{\mathit{term}}$ and $s\preceq(\overline{t},E)$, the total time cost $T(r)$ of the sequence $r$ satisfies:

[TABLE]

Proof.

We estimated in Sec. 2.3 that time cost of single transitions, except for the rewrite transitions (4) and (6), is constant. Time cost of these rewrite transitions (4) and (6) depends on the number of doors and/or nodes of a $\oc$-box.

Since the sequence $r$ of transitions simulates an execution of the SAM, every $\oc$-box concerned in $r$ arises as the translation of a value $\overline{v}$. By definition of the translation $(\cdot)^{\dagger}$ (Fig. 6), the graph $\overline{v}^{\dagger}$ is a $\oc$-box, with as many auxiliary doors as occurrences of free variables in $\overline{v}$. The number of auxiliary doors is no more than the number of nodes in the $\oc$-box, due to the well-boxed-ness condition, that is linear in the size $|\overline{v}|$ of the value.

Moreover the value $\overline{v}$ appears as the first component of a context configuration, and therefore it is a sub-term of the initial term $\overline{t_{0}}$ (Lem. 3.2). As a result, time cost of each occurrence of the rewrite transitions (4) and (6) in the sequence $r$ is linear in the size $\overline{t_{0}}$.

The bound of the total time cost $T(r)$ of the sequence $r$ is given by combining these estimations for single transitions with the results of Prop. 4.3. ∎

Corollary 4.5**.**

The DGoIM⇾ is an efficient abstract machine, in the sense of Def. 4.1.

5 Conclusions

We introduced the DGoIM, which can interleave token passing with graph rewriting informed by the trajectory of the token. We focused on the rewrites-first interleaving and proved that it enables the DGoIM to implement the call-by-need evaluation strategy. The quantitative analysis of time cost certified that the DGoIM⇾ gives an “efficient” implementation in the sense of Accattoli’s classification. The proof of Thm. 4.4 pointed out that eliminating and copying $\oc$-boxes are two main sources of time cost. Our results are built on top of a weak simulation of the SAM, that relates several transitions of the DGoIM to each computational task such as $\beta$-reduction and substitution.

The main feature of the DGoIM is the flexible combination of interaction and rewriting. We here briefly discuss how the flexibility can enable the DGoIM to implement evaluation strategies other than the call-by-need.

As mentioned in Sec. 1.2, the passes-only interleaving yields an ordinary token-passing abstract machine that is known to implement the call-by-name evaluation. Because no rewrites are triggered, as oppose to the rewrites-first interleaving, a token not only can pass a principal door but also can go inside a $\oc$-box and pass an auxiliary door. These behaviours are in fact not possible with the DGoIM presented in this paper; the transitions and data carried by a token are tailored to the rewrites-first interleaving. To recover an ordinary token-passing machine, we therefore need to add pass transitions that involve auxiliary doors and data structures (so-called “exponential signatures”) that deal with $\oc$-boxes, for example.

The only difference between the call-by-need and the call-by-value evaluations lies in when function arguments are evaluated. In the DGoIM, this corresponds to changing a trajectory of a token so that it visits function arguments immediately after it detects function application. Therefore, to implement the call-by-value evaluation, the DGoIM can still use the rewrites-first interleaving, but it should use a modified set of pass transitions. Further refinements, not only of the evaluation strategies but also of the graph representation could yield even more efficient implementation, such as full lazy evaluation, as hinted in [26].

Our final remarks concern programming features that have been modelled using token-passing abstract machines. Ground-type constants are handled by attaching memories to either nodes of a graph or a token, in e.g. [20, 18, 3] — this can be seen as a simple form of graph rewriting. Algebraic effects are also accommodated using memories attached to nodes of a graph in token machines [18], but their treatment would be much simplified in the DGoIM as effects are evaluated out of the term via rewriting.

Acknowledgements.

We are grateful to Ugo Dal Lago and anonymous reviewers for encouraging and insightful comments on earlier versions of this work.