Local Reasoning for
Robust Observational Equivalence
Working draft

Dan R. Ghica
University of Birmingham, UK

Koko Muroya
RIMS, Kyoto University
University of Birmingham, UK

Todd Waugh Ambridge
University of Birmingham, UK

We propose a new core calculus for programming languages with effects,
interpreted using a hypergraph-rewriting abstract machine inspired by the Geometry of Interaction. The intrinsic calculus syntax and semantics only deal
with the basic structural aspects of programming languages: variable binding, name binding, and thunking. Everything else, including features which
are commonly thought of as intrinsic, such as arithmetic or function abstraction and application, must be provided as extrinsic operations, with associatedrewrite rules. The graph representation yields natural concepts of locality androbustness for equational properties and reduction rules, which enable a novel
flexible and powerful reasoning methodology about (type-free) languages witheffects. We illustrate and motivate the technique with challenging examples
from the literature.

1

Local Reasoning for
Robust Observational Equivalence
Working draft

Dan R. Ghica
University of Birmingham, UK

Koko Muroya
RIMS, Kyoto University
University of Birmingham, UK

Todd Waugh Ambridge
University of Birmingham, UK

1. Introduction
1.1. Context and motivation
Program equivalence is an old central question in the study of programming languages.
Establishing whether two program fragments are equivalent has immediate consequences
regarding compiler optimisation and correctness, program verification and validation, andother key applications. The standard formal definition of the concept is that of observational equivalence [Morris Jr, 1969]. Two executable programs are observationally equivalent if they have the same input-output behaviour. On terms (program fragments) observational equivalence is the smallest congruence induced by using executable programs as
contexts, a definition which makes direct reasoning difficult.
The mathematical challenge of observational equivalence is two-fold. On the one hand,quantifying over all contexts is unwieldy, which led to the development of indirect methods.
As an extremal case, denotational semantics provides a model-theoretic route to proving
program equivalence [Scott and Strachey, 1971], while the interplay of syntactic (operational) and denotational techniques led to the development of hybrid methods such as
Kripke logical relations [Statman, 1985] or trace semantics [Jeffrey and Rathke, 2005]. On
the other hand, program equivalences are notoriously fragile. Adding new semantic features to a language can break equivalences and, more significantly, can invalidate reasoning
techniques wholesale. Increasing the expressiveness of a language goes hand in hand withincreasing the discriminating power of contexts, and new techniques based on bisimulation
have been devised to meet the challenge of increasingly realistic languages [Koutavas andWand, 2006].
A methodological point that became increasingly clear is that the richness of features ofmodern programming languages demands a systematic study, ideally a classification, fromthe point of view of the consequences such features have on the equational properties ofa language. The development of game semantics made it possible to give combinatorial,
syntax-independent, orthogonal characterisations for entire classes of features such as stateand control, e.g. the so-called Abramsky [1997] “cube”, or to replace the syntactic notion ofcontext by an abstracted adversary [Ghica and Tzevelekos, 2012]. A classification [Dreyer2

et al., 2012] and characterisation [Dreyer et al., 2010] of language features and their impact
on reasoning has also been undertaken using logical relations.

1.2. Overview and contribution
In this paper we present a new approach to defining effects and proving observational
equivalence based on a novel operational machinery inspired by the Geometry of Interaction (GoI) semantics of languages with effects [Hoshino et al., 2014, Muroya et al., 2016].
In contrast with the usual definition of the semantic model as a token-passing abstract
machine, we introduce a token-guided rewriting semantics of the underlying net [Muroya
and Ghica, 2017]. Unlike the original GoI machine, the graph-rewriting abstract machine
can be shown to be efficient (in the sense of Accattoli et al. [2014]) for common reduction
strategies (by-value, by-need). In addition to the theoretical interest, the graph-rewriting
abstract machine was also used to model exotic effects, inspired by machine learning applications, in which imperative computation can be transformed into pure computation by
abstracting the state [Muroya et al., 2018].
We revise and generalise the formulation of the graph-rewriting machine from graphs
to so-called hypernets, which are hierarchical hypergraphs, in the sense that entire hypergraphs can be used as edge labels. The hypernet-rewriting abstract machine is used
to interpret Spartan, a core calculus of three basic constructs: name binding, variablebinding, and thunking. Everything else, including function-abstraction and function application, must be provided as an extrinsic operation, which comes with its own associatedrewrite rules. The flow of control through the program is represented by a distinguishededge called a token (or a focus), which traverses the hypernet triggering reductions.
The main conceptual contribution of the paper arises from the hypernet formulation of
the language semantics: the underlying hypergraph for a program provides a natural notionof locality, i.e. those nodes and edges which belong to a neighbourhood around a pointof interest such as the token or a redex we want to reason about. Locality in turn gives
rise to a notion of robustness of sub-graphs, which states that rewrites occurring elsewhere
cannot interfere with it. From a reasoning perspective, locality and robustness are usefulconcepts, since they can be established via elementary case analysis comparing reduction
rules pairwise. The key technical result is a characterisation theorem (Thm. 6.14) which
establishes, informally speaking, that robustness implies observational equivalence, a very
handy conceptual tool1 .
We believe this is an important result because, for the first time, it goes beyond an enumerative approach to effects, to a syntax-independent characterisation of effects. There isno need to separate effects, for example, into state and control in order to reason about
languages with effects. In fact there is no need to separate computations into pure andeffectful. Only locality properties are important, in the sense that the formulation of aproperty involves a hypergraph neighbourhood rather than the whole graph, and thatrewrite rules associated with various operations do not interfere with the property we aim
to check. A large number of equivalences and effects encountered in programming languages will be seen to satisfy these conditions – but not all. Perhaps the simplest example
of a reasonable non-local and non-robust effect is the function stat : unit → stat foundin the OCaml Gc module, providing memory usage information amounting to measuring
the size of the term under execution. In the presence of stat, which can be defined as an
1

Our concept of locality is not to be confused with memory locality, which concerns memory accessduring program execution. Our locality, together with robustness, captures impact that operations in a
program make on other parts of the program during execution. Ours could be seen as a generalisationof memory locality, because memory access could be modelled as extrinsic features of Spartan.

3

operation in our framework, almost all basic equivalences fail, for example the beta law(since the term grows smaller).
The hypernet semantics is a genuine abstract machine in the sense that it provides
syntax-independent execution with a well-defined and reasonably realistic cost model (timeand space). The effects are not merely encoded into a base metalanguage, but can be
expressed directly as arbitrary actions on the machine state. If the aim is a languagethat enjoys a nice equational theory, then these equivalences should be robust relative todesirable equivalences. But arbitrary, possibly ill-behaved exotic effects are also definable
if so desired.
Finally, another conceptual novelty introduced here is a refinement of the notion ofcontextual equivalence. The standard definition involves a quantification over all contexts,
but in a language as flexible as Spartan contexts can be wild. Therefore it makes sense
to restrict contexts so that they only have certain shapes, which correspond to the way
contexts are formed in well-behaved languages. Moreover, equivalence is indexed by apreorder on natural numbers which allows the comparison of the number of evaluation
steps. This means that if two terms are equivalent with respect to the greater-than-orequal order then in-context substitution is guaranteed to reduce the number of evaluation
steps. This can be used as a basis for qualitative and quantitative reasoning, as neededfor example in compiler optimisation.
The structure of the paper is as follows. In Sec. 2 we present a simple calculus (Spartan)which intermediates syntactically between languages with effects and the focussed hypernet
representation. Hypernet rewriting is overviewed in Sec. 3 with enough technical detail tounderstand the examples in Sec. 4. The technical details of focussed hypernet rewriting
are given in Sec. 5, with the characterisation theorem and its proof presented in Sec. 6-7.
Sec. 8 gives an application of the main characterisation theorem to proving observational
equivalence. We conclude with a mention of related and future work.
An interpreter and visualiser of Spartan execution can be accessed online.2

2. The Spartan calculus
The syntactic elements of Spartan are a set of variables V, (ranged over by x, y), a setof atoms A, (ranged over by a), and a set of operations O (ranged over by φ). The set ofoperations is partitioned into O = OX ] O ; the partitions are called passive and active
operations. We will usually denote a sequence of variables x0 , . . . , xk by ~x, a sequence ofatoms a0 , . . . , ak by ~a, etc. These sequences may be empty, case in which we write −. We
denote the length of a sequence by |~x| and, if convenient we may treat the sequences as
sets by writing ~x ∩ ~y , y ∈ ~x, etc.
Definition 2.1 (Spartan terms). The terms of Spartan, typically ranged over by s, t, u,
are generated by the grammar:
t ::= x | a | new a ( t in t | bind x → t in t | ~y .t | φ(~t; ~t).
The term formers are variables, names, name binding, variable binding, thunking andoperations. Note that the sequences above may be empty. In particular, thunking may be
applied without binding any particular variable (−.t). In the formation of an operation
term φ(~s; ~t) arguments ~s are used eagerly and the arguments ~t lazily (we also say they aredeferred ). The eager arguments are evaluated in the given order, whereas the evaluation2

https://tnttodda.github.io/Spartan-Visualiser/4

of lazy arguments is deferred. The distinction between name-binding and variable-binding
will be seen to play a crucial role in the management of sharing vs. copying duringexecution.
The calculus provides only the most basic infrastructure. All interesting computational
content must be provided as particular operations. The following is a non-exhaustive listof such operations which may be added to the Spartan framework.
Some passive operations (constructors) that can be added to Spartan are numerical
def

def

def

constants (n = n(−; −)), pairing (ht, ui = P(t, u; −)), empty tuple (hi = hi(−; −)),
def

injections (inji (t) = inji (t; −), i ∈ {1, 2}), etc.

def

Some examples of active Spartan operations are successor (succ(t) = succ(t; −)), addef

def

def

dition (t+u = +(t, u; −)), conjunction (t & u = &(t, u; −)), conditionals (if t then u1 else u2 =def

if(t; u1 , u2 )), recursion (µx.t = µ(−; x.t)) etc.
Datatype destructors can also be added as active operations, for example projections
def

def

(πi (t) = πi (t; −), i ∈ {1, 2}), pattern matching (match t with x1 7→ u1 , x2 7→ u2 =match(t; x1 .u1 , x2 .u2 )), etc.
Operations with multiple arguments can come in different flavours depending on orderof evaluations and eagerness. For example disjunction can be left-to-right &(t, u; −), rightto-left &(u, t; −) or short-cut &(t; u). Pairs can be also evaluated left-to-right (as above),but also, right-to-left, or lazily.
Most strikingly, abstraction and application themselves can be presented as operations.
def

Abstraction is simply a thunking of the function body: λx.t = λ(−; x.t), whereas applicadef

tion can be defined by-name or by-value, left-to-right or right-to-left: t u = @(t; u)(call-by-name),
−
−
def →
def ←
t u = @ (t, u; −)(left-to-right call-by-value), or t u = @ (u, t; −)(right-to-left call-by-value).
Algebraic operations are operations of certain arity and equational properties, designed
to characterise a class of computational effects [Plotkin and Power, 2003]. All examples ofalgebraic operations from loc. cit. can be presented as (active) Spartan operations. Nondeterministic choice t(−; u1 , u2 ) selects one of its deferred argument non-deterministically;equipping it with a probability p ∈ [0, 1] yields a probabilistic choice tp (−; u1 , u2 ). Interactive input read(−; x.u) assigns an input value to bound variable x, whereas interactive
output write(t; u) produces the result of evaluating (eager) argument t as an output value.
Both operations continue with the deferred argument u. State lookup and update takeform lookup(t0 ; x.u) and, respectively, update(t0 , t; u). The difference from interactive
I/O is that the first eager argument t0 is evaluated to yield an atom, which serves as a location in a store. In their generic form, state operations deref(t0 ; −) and assign(t0 , t; −)return a stored value and the empty pair, respectively, instead of continuing with a deferred argument. Finally, creation of a local state, in the generic form, is modelled byref(t; −) that stores evaluation result of t to a fresh location (atom) and returns it.
Effect handlers are studied as a generalisation of exception handlers to algebraic effects
in Plotkin and Pretnar [2013]. In our setting, a handler that targets operations φ1 , . . . , φmcan be constructed by a passive operation handlerφ1 ,...,φm tagged with the targets. It
is natural to assume that targeted operations are never passive (e.g. lambda-abstraction,
pairing operation, injection, and handlers themselves). These handler constructors area (rare) example in which a deferred argument may bind more than one variables. A
handler can be then used with the handling operation with handle(t, u; −) to evaluate uwith handler t.
Control operators are similarly dealt with. The undelimited control operator call/cc

5

~x | ~a ` xi : ?

1≤i≤k~x | ~a ` aj : ?

1≤j≤h~x | ~a ` u : ? ~x | a, ~a ` t : ?
a∈/ ~a~x | ~a ` new a ( u in t : ?
φ ` (m; ~n) ∈ N × Np

~x | ~a ` u : ? ~x, x | ~a ` t : ?
x∈/ ~x~x | ~a ` bind x → u in t : ?

~y , ~x | ~a ` t : ?
n ≥ 0, ~x ∩ ~y = ∅~x | ~a ` ~y .t : T n (?){~x | ~a ` ti : ?}mi=1~x | ~a ` φ(~t; ~s) : ?

{~x | ~a ` sj : T nj (?)}pj=1

Figure 1: The Spartan type system
can be defined as:
defcallcc(t) = callcc(−; t),defabort(t) = abort(−; t)The delimited control operator shift/reset of Danvy and Filinski [1990] can be defined
as:
def
def
shift(t) = shift(−; t), reset(t) = reset(t; −).

2.1. The Spartan type system
The type system is primarily used to distinguish thunks from eager terms and to ensureterms are well formed. However, this type system does not enforce any notion of runtime
safety.
Eager terms have type ? and thunks have type T m (?) for some m ∈ N, representing thenumber of bound variables that accompany the thunk. Note that T 0 (?) is a valid type
and that T 0 (?) 6= ?. Types are typically ranged over by τ . A sequence τ1 , . . . , τn of types
is denoted by an expression ⊗ni=1 τi . This is empty if n = 0, and equal to a single typeif n = 1, i.e. ⊗1i=1 τ = τ . The empty sequence is written as . We use syntactic sugar00τ ⊗n ≡ ⊗ni=1 τ , and τ ⊗n ⊗ τ ⊗n = τ ⊗(n+n ) .
Each operation φ ∈ O has an arity, given in the form of φ ` (me ; ~n) ∈ N×Nmd , indicating
it takes me eager arguments and md thunks.
For a type τ and a term t, judgements are written as ~x | ~a ` t : τ , where all variables in ~x
and all atoms in ~a are distinct. The rules are given in Fig. 1, where |~x| = k, |~y | = n, |~a| = h.
If − | − ` t : ? is derivable, term t is called a program.

3. Overview of focussed graph rewriting
3.1. Monoidal hypergraphs and hypernets
Given a set X we write by X ∗ the set of elements of the free monoid over X. Given afunction f : X → Y we write f ∗ : X ∗ → Y ∗ for the pointwise application (map) of f to
the elements of X ∗ .
Definition 3.1. A monoidal hypergraph is a pair (V, E) of finite sets, vertices and (hyper)edges along with a pair of functions S : E → V ∗ , T : E → V ∗ defining the source list
and target list, respectively, of an edge.

6

Definition 3.2. A labelled monoidal hypergraph consists of a monoidal hypergraph, a setof vertex labels L, a set of edge labels M , and labelling functions fL : V → L, fM : E → M
such that:• For any edge e ∈ E, its source list S(e) consists of distinct vertices, and its target
list T (e) also consists of distinct vertices.
• For any vertex v ∈ V there exists at most one edge e ∈ E such that v ∈ S(e) and at
most one edge e0 ∈ E such that v ∈ T (e0 ).
• For any edges e1 , e2 ∈ E if fM (e1 ) = fM (e2 ) then fL∗ S(e1 ) = fL∗ S(e2 ) , andfL∗ T (e1 ) = fL∗ T (e2 ) .

In words, the label of an edge is always consistent with the number and labelling of its
endpoints. This makes it possible to use the vertex labels as types for edge labels. Givenm ∈ M we can write m : x ⇒ x0 for x, x0 ∈ L∗ such that x = fL∗ S(e) and x0 = fL∗ T (e)for any e ∈ E such that fM (e) = m.
If a vertex belongs to the target (resp. source) list of no edge we call it an input (resp.
output).

Definition 3.3. A labelled monoidal hypergraph is interfaced if inputs and outputs arerespectively ordered, and no vertex is both an input and an output.
We can type a hypergraph G : fL∗ (I) ⇒ fL∗ (O) where I, O are the lists of inputs andoutputs, respectively. In the sequel, when we say hypergraphs we always mean interfaced
labelled monoidal hypergraphs.
Definition 3.4 (Interface permutation). The permutation of the interface of a hypergraphyields another hypergraph. Let G be a hypergraph with an input list i1 , . . . , in and an
output list o1 , . . . , om . Given two bijections ρ and ρ0 on sets {1, . . . , n} and {1, . . . , m},0respectively, we write Πρρ (G) to denote the hypergraph that is defined by the same dataas G except for the input list iρ(1) , . . . , iρ(n) and the output list oρ0 (1) , . . . , oρ0 (m) .
Definition 3.5 (Hypernets). Given a set of vertex labels L and edge labels M we write
H(L, M ) for the set of hypergraphs with these labels; we also call these level-0 hypernets
H0 (L, M ). We call level-(k+1) hypernets the set of hypergraphs[
Hk+1 (L, M ) = H L, M ∪Hi (L, M ) .
i≤k

We call (labelled monoidal) hypernets the set Hω (L, M ) =Si∈N Hi (L, M ).

Informally, hypernets are nested hypergraphs, up to some finite depth, using the same
sets of labels. An edge labelled with a hypergraph is called “box” edge, and a hypergraphlabelling a box edge is called “content”. Edges of a hypernet G are said to be “shallow”.
Edges of nesting hypernets of G, i.e. edges of hypernets that recursively appear as edge
labels, are said to be “deep” edges of G. Shallow edges and deep edges of a hypernet are
altogether referred to as edges “at any depth”.

7

3.2. Graphical conventions
A monoidal hypergraph with vertices V = {v1 , v2 , v3 , v4 , v5 } and edges E = {e1 , e2 } suchthat
S(e0 ) = {v0 , v1 }T (e0 ) = S(e1 ) = {v2 , v3 , v4 }T (e1 ) = {v5 }fL = {v0 7→ m, v1 7→ m0 , v2 7→ l, v3 7→ l0 , v4 7→ l00 , vk 7→ k}

fM = {e0 7→ X, e1 7→ Y }is normally represented as

k

Y

l

l

l"

X

m

m

.

However, this style of representing hypergraphs is awkward for understanding their structure. We will often graphically represent hypergraphs as graphs, with both vertices andedges drawn as nodes marked by their label and connecting input vertices with edges, andedges with output vertices using arrows. To distinguish them, the edge labels are circled.
Since the node labels are often determined in our typed graphs by the edges we can omit
them to avoid clutter, showing only the edges and the way they link. The graph above
would be drawn like this:

l

k

k

Y

Y

l

l"

X

m

X

m

m

Graph showing the nodesmGraph hiding some nodes .

Sometimes we will draw a hypergraph so that to identify sub-graphs of interest. In
this case we may draw interface nodes twice and connect them with arrowless lines whichindicate identity, i.e. the nodes at either ends are two graphical representations of thesame node. If it is obvious from context we may just draw the identity lines between the
sub-graphs, or just one line if the entire input interface of a sub-graph is identified with8

the entire output interface of another sub-graph. For example, below we consider GX , GY
as the sub-graphs consisting just of edge X and Y , respectively:
k

GY
l

l

l"

l

l

l"

GX
m

GY

GY

GX

GX

m

The final conventions are that a bunch of parallel arrows can be drawn as a single arrow
with a dash across, and that a hypergraph-labelled edge is indicated with a dotted box,
and decorated with its type.

3.3. From terms to hypernets
We represent terms in Spartan as hypernets with vertex labels either τ or , ranged overby `. The same notational conventions apply, extended with the extra symbol . Theedge labels have unique types, and they are: the operations φ (with the edge-label-typeinherited from the Spartan type system), an instance label I : ? ⇒ , an atom label◦ :  ⇒ ?, a family of contraction labels {⊗`W :  ⇒ `, ⊗`C : `⊗2 ⇒ ` | ` ∈ {?, }}, a family of
token labels ?, X, : ? ⇒ ?. When a hypergraph is used as an edge label it must always
have type G : ? ⇒ ?⊗n ⊗ ⊗h ; the box edge is assigned type T n−k (?) ⇒ ?⊗k ⊗ ⊗h forsome k ≤ n.
The hypernet is said to be focussed if there exist only one token-labelled edge and it isshallow, plus some other basic well-formedness conditions discussed later.
`: `⊗km ⇒ `⊗k with ` ∈ {, ?}It will be helpful to define a family of subgraphs Dk,mwhich we call distributors (Def. 5.6). Intuitively, they are the k-interleaving of bunches of
?

?

⌦

⌦

∗ =⌦ ⌦ ⌦ ⌦m-contraction edges, For instance, D2,3??

 =and D3,0

⌦

⌦

??

??

⇧ ⇧ ⇧

⌦⌦⌦

.

The translation function (−)† from Spartan terms to hypernets is given in Fig 2, where⊗ki ⊗ ⊗hi ) placed sidem
i=1 Gi is a hypernet formed of a family of hypernets (Gi : ? ⇒ ?
by side. We can easily see that the hypernet of a Spartan program always has type(− | − ` t : ?)† : ? ⇒ , i.e. one input and no outputs. The hypernet of a program is
focussed by adding a ? token in the input position.

3.4. Focussed rewriting
In this section we define an abstract machine for rewriting hypernets of Spartan terms,
thus giving a notion of evaluation for the calculus. The machine is based on the Dynamic
Geometry of Interaction Machine of Muroya and Ghica [2017], which it generalises for themodelling of effects. In this section we give a brief introduction to the machine, with thefull technical details presented later, in Sec. 5.

9<latexit sha1_base64="Jh2nZzjufDgZup8qpLmTcuu8HLc=">AAAB+nicbVBNS8NAEN3Ur1q/Uj16WSyCp5KIoMeCF48V7Ac0sWy2m3bpZjfsTpQS+1O8eFDEq7/Em//GbZuDtj4YeLw3w8y8KBXcgOd9O6W19Y3NrfJ2ZWd3b//ArR62jco0ZS2qhNLdiBgmuGQt4CBYN9WMJJFgnWh8PfM7D0wbruQdTFIWJmQoecwpASv13WpggOj7PFDAE2bweNp3a17dmwOvEr8gNVSg2Xe/goGiWcIkUEGM6fleCmFONHAq2LQSZIalhI7JkPUslcTuCfP56VN8apUBjpW2JQHP1d8TOUmMmSSR7UwIjMyyNxP/83oZxFdhzmWaAZN0sSjOBAaFZzngAdeMgphYQqjm9lZMR0QTCjatig3BX355lbTP675X928vag1cxFFGx+gEnSEfXaIGukFN1EIUPaJn9IrenCfnxXl3PhatJaeYOUJ/4Hz+AJeWlBc=</latexit>?⌦k<latexit sha1_base64="Sl3Iz1RFB6udTwUrnAKCXS0z8J0=">AAAB/XicbVDLSsNAFL2pr1pf8bFzM1gEVyURQZcFNy4r2Ae0sUwmk3boZCbMTIQair/ixoUibv0Pd/6N0zYLbT1w4XDOvdx7T5hypo3nfTulldW19Y3yZmVre2d3z90/aGmZKUKbRHKpOiHWlDNBm4YZTjupojgJOW2Ho+up336gSjMp7sw4pUGCB4LFjGBjpb571IsYTqSI7vOeNCyhGg0nfbfq1bwZ0DLxC1KFAo2++9WLJMkSKgzhWOuu76UmyLEyjHA6qfQyTVNMRnhAu5YKbPcE+ez6CTq1SoRiqWwJg2bq74kcJ1qPk9B2JtgM9aI3Ff/zupmJr4KciTQzVJD5ojjjyEg0jQJFTFFi+NgSTBSztyIyxAoTYwOr2BD8xZeXSeu85ns1//aiWkdFHGU4hhM4Ax8uoQ430IAmEHiEZ3iFN+fJeXHenY95a8kpZg7hD5zPH86ilVQ=</latexit>

⇧⌦h

?
Dk,m
e +md

⇧
Dh,m
e +md

?⌦kme ?⌦kmd⇧⌦hme ⇧⌦hmd?⌦kme⇧⌦hme ?⌦kmd
⇧⌦hmd
†
†
md
e
ni
⇥m
(~
x
|
~
a
`
t
:
?)
⇥
~
x
|
~
a
`
s
:
T
(?)
i
i
i=1
i=1
m
⌦me
d
O
?
T ni (?)<latexit sha1_base64="0m85L7A0QOr3/Pd534B/envctc0=">AAACAXicbVDLSsNAFJ3UV62vqBvBzWARXJVEBF0W3LisYB/QxDCZTNqh8wgzE6GEuvFX3LhQxK1/4c6/cdpmoa0HLhzOuZd774kzRrXxvG+nsrK6tr5R3axtbe/s7rn7Bx0tc4VJG0smVS9GmjAqSNtQw0gvUwTxmJFuPLqe+t0HojSV4s6MMxJyNBA0pRgZK0XuUZBQxKVI7otAGsqJhkPIIzKJ3LrX8GaAy8QvSR2UaEXuV5BInHMiDGZI677vZSYskDIUMzKpBbkmGcIjNCB9SwWyu8Ji9sEEnlolgalUtoSBM/X3RIG41mMe206OzFAvelPxP6+fm/QqLKjIckMEni9KcwaNhNM4YEIVwYaNLUFYUXsrxEOkEDY2tJoNwV98eZl0zhu+1/BvL+pNWMZRBcfgBJwBH1yCJrgBLdAGGDyCZ/AK3pwn58V5dz7mrRWnnDkEf+B8/gCDRZbN</latexit>

i=1

?
†
~x | ~a ` (~t; ~s)?⌦(i 1)?

Di? 1,0?⌦(k i)
Dk? i,0

?⌦k
?
Dk,2

⇧⌦h
⇧
Dh,2

?⌦k
?
Dk,2

⇧⌦h
⇧
Dh,2

?⌦k ?⌦k⇧⌦h ⇧⌦h?⌦k ?⌦k⇧⌦h ⇧⌦h

⇧⌦h
⇧
Dh,0

?
(~x | ~a ` xi : ?)†?⌦k⇧⌦h(~x | ~a ` u : ?)†?

⇧⌦k⌦(j 1)⇧
Dj⇧ 1,0?
?
Dk,0⇧⌦(h j)Dh⇧ j,0I?
(~x | ~a ` aj : ?)†

?

⌦n

?⌦k
?⌦k

~y , ~x | ~a ` t : ?
?
T n (?)
†

⇧⌦h
⇧⌦h
†

?⌦k
⇧⌦h
(~x | ~a ` u : ?)†
?

?⌦k ?
⇧⌦h
?⌦k
⇧
⇧⌦h
(~x, x | ~a ` t : ?)†(~x | a, ~a ` t : ?)†?
?
(~x | ~a ` bind x ! u in t : ?)† (~x | ~a ` new a ( u in t : ?)†
?⌦(

Pm

?⌦(

1

i=1

Pm

ki ) ⌦km ⌦(

1

i=1

?

⇧

Pm

Pm

i=1

1

hi )
<latexit sha1_base64="iTIPAyFESbZbAw9xmE48aUelo9I=">AAAB/3icbVDLSsNAFJ3UV62vqODGzWARXJVEBF0W3LisYB/QxDCZTNqh8wgzE6HELvwVNy4UcetvuPNvnLZZaOuBC4dz7uXee+KMUW0879uprKyurW9UN2tb2zu7e+7+QUfLXGHSxpJJ1YuRJowK0jbUMNLLFEE8ZqQbj66nfveBKE2luDPjjIQcDQRNKUbGSpF7FCQUcSmS+yKQhnKi4TDik8itew1vBrhM/JLUQYlW5H4FicQ5J8JghrTu+15mwgIpQzEjk1qQa5IhPEID0rdUILspLGb3T+CpVRKYSmVLGDhTf08UiGs95rHt5MgM9aI3Ff/z+rlJr8KCiiw3ROD5ojRn0Eg4DQMmVBFs2NgShBW1t0I8RAphYyOr2RD8xZeXSee84XsN//ai3oRlHFVwDE7AGfDBJWiCG9ACbYDBI3gGr+DNeXJenHfnY95accqZQ/AHzucPXnuWNA==</latexit>

⇧⌦hm

1

ki ) ⌦( i=1 hi )⇧?⌦km ⇧⌦hm⇥m
Gm
i=1 Gi1⌧m⌦m
i=1 ⌧i⇥m
i=1 Gi , m > 0~x | ~a ` ~y .t : T n (?) , where |~y | = n

Figure 2: Hypernet semantics of Spartan

10⇥0i=1 Gi

?

?

?

?

⇧

⇧

⌦

⌦

⌦

⌦

I

I

?

?

?

?

•

?
?

?

?

•
? !
7

7!
?

?

(1a)
N

ni

?

?

⌦k

?

?

?

?
?

?

?

(1b)
iT

(?)

?

?

•

7!

?⌦k

X
?

X

?

N

iT

ni

•

ni

?

?⌦k

•

7!

?
X

iT

ni

(?)

N

iT

ni

(?)

N

?

?

?

•

7!

?

?

?

(4)

Figure 3: Interaction rules
In a conventional reduction semantics a subtle and often complex aspect of the reduction
bureaucracy is the identification and isolation of a subterm which is a redex from thecontext [Felleisen and Hieb, 1992]. Similarly, in an abstract machine much of the work
consists of moving information (representing the context) on and off the stack in order toreach redexes [Wright and Felleisen, 1994]. In both cases the formal machinery identifies
an implicit focus of action which either moves around the term or is acted upon via asubstitution. In the case of focussed graph rewriting the focus is represented by the tokenedge. The redex search is defined by the local interaction between the token and theneighbouring edges, which can cause the token to navigate the graph. The same local
interactions can determine a rewrite action.
The state of the token edge determines the possible actions. If the token is ? then theapplicable rules (interaction rules) are search rules, which do not change the underlying
graph; the ? token always travels in the direction of the edges and it is searching for aredex. In comparison to a conventional reduction semantics this is a narrowing of the termin-context. If the token is X then the applicable rules are also search (interaction) rules
but the token travels in the opposite direction of the edges. In comparison to a reduction
semantics this is a widening of the term-in-context normally following the detection of avalue. Finally, if the token is then a rewrite is about to be performed at the very next
step. There are two kinds of rewrites, intrinsic to the Spartan calculus and extrinsic,
defined by the operations. The intrinsic rewrites are only copying of subgraphs which are
triggered when a token interacts with contraction ⊗.
Interaction rules are in Fig. 3. These rules capture the intuition behind redex search
discussed earlier:
Rule 1. When encountering a contraction (⊗) the search token (?) becomes a rewrite
token ( ) as a copying action will follow. This rule has two sub-rules depending on whether
the focus is on the left or right branch.
Rule 2. When encountering an instance edge (I) the search token (?) changes to a value
token (X) as atoms block both evaluation and copying.
Rule 3. When encountering an operation (ψ) with at least one eager argument the searchtoken (?) will inspect the first argument.

11

t

?
t 2 { , X}
(5b)
N ni
⌦k0
?
i T (?)
?

?

(?)

t

7!

(3)

ni

?

?

?⌦k

iT

t

?

•

7!

?

N

t

?
t 2 { , X}
(5a)
N ni
⌦k0
? ?
i T (?)

?
?

??

?

?

?

?

(?)

(?) ?⌦k

t

(2)
⌦k

iT

t

?

?

N

?

Rule 4. After resolving eager argument k + 1 of an operation (ψ) the value token (X)changes to a search token (?) which proceeds to inspect the next eager argument, if itexists.
Rule 5a. After all eager arguments of an operation ψt (t ∈ {X, }), the token will change
to a t-token depending on the kind of operation ψt is, value or rewrite. (Rule 5b. is adegenerate version for operations with no eager arguments).
Contraction rules are given in Fig. 7 (Sec. 5). The extrinsic rules for various operations
are discussed in the following section, while also reasoning about contextual equivalence.

4. Observational equivalence
The hypernet model supports a new style of reasoning centered around a graph-theoretic
intuition of locality, as the incidence relation immediately identifies the relevant directinteractions arising in a term. A secondary, but equally important concept, is that ofrobustness, capturing the fact that a rewrite rule does not interfere with a particularsubgraph of interest which we call a template. The key Theorem (Thm. 6.14 in Sec. 6)
says, informally speaking, that robust templates are observational equivalences. As aproperty, robustness can be established by case analysis, comparing a template with all
operations that may occur in the context, thus providing a relatively simple route toproving observational equivalence. Since robustness is only a sufficient criterion we test
it with various challenging equivalences from the literature, involving in first instance(arbitrary untyped) state.
In the rest of the section we will formulate some such desirable equivalences. They
hold in general in well-behaved languages, but the Spartan framework is broad enoughto allow the definition of operations that would break these and most equivalences. This
is why we would refer to them for now as desiderata. We will then show that they holdwith respect to a specific operation set Oex described in Sec. 8.1. In Sec. 8 we give moredetails for one of the equivalences.
Recall that our framework is parametrised by the operation set O. Our notion of equivalence is additionally parametrised by a set BO (“behaviour”) of extrinsic rewrites associatedwith the operations O. Given two derivable judgements ~x | ~a ` t1 : ? and ~x | ~a ` t2 : ?,we write BO |= (~x | ~a ` t1 †all t2 : ?) (resp. BO |= (~x | ~a ` t1 '†all t2 : ?)) if the hypernetof t1 is a refinement (resp. equivalence) of t2 in any context, with the operation set being
O and extrinsic rewrites being BO . In particular, we write BO |= (~x | ~a ` t1 †bf t2 : ?)(resp. BO |= (~x | ~a ` t1 '†bf t2 : ?)), if the refinement (resp. equivalence) holds only in thecontexts that do not bind a hole to a variable nor an atom. These concepts are formallydefined in Sec. 8.3.
In the sequel, we simply write t1 †all t2 etc., omitting the type ? and the sequences ~xand ~a, and making the parameter BO implicit.

4.1. Structural laws
Before considering equivalences involving specific operations, it is useful to examine structural equivalences, which involve Spartan alone. Let fv (t) and fa(t) be the sets of freevariables and free atoms of a term, respectively, defined as usual.
Desiderata 4.1 (Coherences).
bind x → t in bind y → u in s '†all bind y → u in bind x → t in s,
12(1)?⌦k ⇧⌦h? ?⌦k ⇧⌦h
G

~`
GS

~`
GS

T 1 (?)

λ? ?⌦k ⇧⌦h
G

7!

@

?
?

?

Figure 4: Beta rewrite rule (G, GS are hypernets)(whenever x 6∈ fv (u), y 6∈ fv (t))

new a ( t in new b ( u in s '†all new b ( u in new a ( t in s,(2)bind x → (bind y → u in t) in s '†all bind y → u in bind x → t in s

(3)

new a ( (new b ( u in t) in s '†all new b ( u in new a ( t in s

(4)(whenever a 6∈ fa(u), b 6∈ fa(t))(whenever y 6∈ fv (s))(whenever b 6∈ fa(s))

The second batch of laws concern terms u with no variable binders (‘new’) except inside
thunks. Such terms are referentially transparent, in the sense that they can be safely
replicated or substituted in other terms:
Desiderata 4.2 (Referential transparency).
bind x → u in bind y → x in bind z → x in t '†all bind y → u in bind z → u in t,(5)(whenever x 6∈ fv (t))

bind x → u in t '†all t[u/x](6)

To be clear, the referential transparency laws hold in contexts with most “reasonable”
operations, including all mentioned in the section below. However, even though referential
transparency laws are very robust, one can think of operations which may violate themsuch as Gc.stat mentioned earlier.

4.2. OperationsFirst we consider lambda-abstraction (a passive operation) and function application (active), in particular left-to-right call-by-value. The rewrite rule when the token reaches
the application hyperedge is given in Fig. 4. The usual observational equivalences (laws)
induced by beta rewrite are:Desiderata 4.3 (Beta laws). If v is a value then→

(λx.t) @ v '†bf bind x → v in t

(Micro beta)

Moreover, if v is referentially transparent then→

(λx.t) @ v '†bf t[v/x]13(Beta)

~`
GS
?

~`
GS
?
⇧⇧
D1,1
⇧

ref

7! I

?

?

?
?

?

Figure 5: Reference creation (GS is a hypernet)
The beta law is also robust relative to the operations described in the sequel, butreasonable operations that violate it do exist. For example, we mentioned the Gc.stat()function of OCaml which returns the size of the term violates this law.
We further add to the language state (assignment and dereferencing). Since Spartan
is (essentially) untyped by default we consider state which can store any terms (or rather
values), including lambda-abstractions. The rewrite rule for reference creation (active
operation ref) is given in Fig. 5, while assignment and dereferencing are given in Fig. 6.
In the same figure we give the two rules for equality testing on references. Also note that in
the absence of type restrictions it is straightforward to tie recursive knots in the store. For
example let x = ref () in x := x stores a self-reference into x, so that any dereferencing!x, !!x, !!!x, etc., will always produce the same result. For convenience we use the following
syntactic sugar:def→t u = t@udef

νx.t = (λx.t) (ref ())
def

let x = u in t = (λx.t) u
def

u; t = (λ .t) u
Because we are focusing on the call-by-value function application, the let-binding as asugar has different behaviour from the intrinsic variable-binding.
Some desirable equivalences which hold in contexts containing stateful operations are:Desiderata 4.4 (Stateful laws).
νz.λx.x = z †bf λx.false†bfνx.f '(Freshness)f(Locality)

let x = ref 0 in (f (λ .x :=!x + 1)) (λ .!x)'†bf let x = ref 0 in (f (λ .x :=!x − 1)) (λ .−!x)†bf

let x = ref 1 in λf.((f ()); !x) 'λf.((f ()); 1)(Parametricity 1)(Parametricity 2)

The first two equivalences originate in the ν-calculus of Pitts and Stark [1993], a (CBV)
lambda-calculus extended with construct νx.t which creates a new name and binds it tox in t, plus equality testing on names. “Names” are virtually identical to unit references,
therefore for economy of presentation we will consider them as such. The proof techniques
14

?

?

⇧
C

?

?

⇧
⇧
C0
C
⇧ ⇧⌦k2 ⇧⌦k1 ⇧⇧⌦k1 ⇧⇧
C0⇧ ⇧⌦k2?

?

⇧
C⇧⌦k1 ⇧⇧
C⇧⌦k1 ⇧

⇧

⇧

I

I

I

I

I

I

I

I

?

?

?

?

?

?

?

?

⌦

? ⌦

7!

=

?

ff

=

⌦ ? ⌦

?

7!

tt

?
⌦k1

⇧

⌦k2

⇧

?
?

⌦k1

⇧
~`

⌦k2

⇧

?
?

⌦

⌦k1

~`

⇧
⇧
C
C
⇧⌦k1 ⇧ ⇧⌦k2⇧⌦k1 ⇧ ⇧⌦k2
⌦k2 ~
I
I
⇧
`
⇧⌦k2 ~`
GS
GS
7!
?
?
?
?
:=

()

?

⌦ ?

⇧

⇧

?
?

?
?
?
D1,2
?
?

⇧
C

⇧⌦k1 ⇧
I

?

⇧
C
⌦k1

7! ⇧

?

⇧⌦k1

⇧
I

!

?

?

⌦

?
⇧⌦k1

?

⌦k1

?
⇧⌦k1

?

?

⇧⌦k1

?

Figure 6: Equality, assignment, and dereferencing rewrite rules (C and C 0 are contraction
trees, and GS is a hypernet)
in loc. cit. rely on logical relations, which make essential use of the typing structure of thelanguage. In contrast, we can show that these equivalences hold even in untyped state,with the caveat that one becomes a refinement, rather than an equivalence, since equality
checking can get stuck if not applied to names.
The other equivalences originate in the Idealised Algol literature [O’Hearn and Tennent,
2013], a call-by-name language with ground-type local variables. The proofs again use logical relations, but formulated in a denotational semantics of functor categories. Escalating
the proofs to call-by-value and higher-order state requires more complex techniques suchas step-indexed logical relations [Ahmed et al., 2009]. Our approach will be seen to berather different, involving a case analysis of the operations involved as they interact in all
possible pairwise combinations, in a type-free setting.

5. Focussed graph rewriting (technical details)
In this section we give a definition of the abstract machine introduced informally in Sec. 3.4.
We call it a universal abstract machine because it can be seen as a universal algebra (theoperations) combined with a mechanism for sharing or copying resources and scheduling
evaluation. The machine, and hence the definitions below, are all globally parametrisedby the operation set O and its behaviour BO .

5.1. Auxiliary definitions
We use the terms incoming and outgoing to characterise the incidence relation between
neighbouring edges. Conventionally incidence is defined relative to nodes, but we find it
15

helpful to extend this notion to edges.
Definition 5.1 (Incoming and outgoing edges). An incoming edge of an edge e has atarget that is a source of the edge e. An outgoing edge of the edge e has a source that isa target of the edge e.
Definition 5.2 (Path). A path in a hypergraph is given by a non-empty sequence of edges,
where an edge e is followed by an edge e0 if the edge e is an incoming edge of the edge e0 .
Note that, in general, the first edge (resp. the last edge) of a path may have no source(resp. target). A path is said to be from a vertex v, if v is a source of the first edge of thepath. Similarly, a path is said to be to a vertex v 0 , if v 0 is a target of the last edge of thepath. A hypergraph G is itself said to be a path, if all edges of G comprise a path froman input (if any) and an output (if any) and every vertice is an endpoint of an edge.
Definition 5.3 (Reachability). A vertex v 0 is reachable from a vertex v if v = v 0 holds,
or there exists a path from the vertex v to the vertex v 0 .
To represent Spartan terms, we fix the vertex label set L and the edge label set MO as
described in Sec. 3.3, using the given operation set O.
L := {?, } ∪ {T n (?) | n ∈ N}

MO := {I : ? ⇒ , ? : ? ⇒ ?, X : ? ⇒ ?,: ? ⇒ ?}nid⊗ ⊗m
∪ {φ : ? ⇒ ?
i=1 T (?) | (φ ` (me ; n1 , . . . , nmd )) ∈ O}
∪ {◦ :  ⇒ ?, ⊗`W :  ⇒ `, ⊗`C : `⊗2 ⇒ ` | ` ∈ {?, }}⊗meDefinition 5.4 (Operation path). A path whose edges are all labelled with operations iscalled operation path.
Definition 5.5 (Contraction tree). For each ` ∈ {?, }, a contraction tree is a hypernet(C : `⊗k ⇒ `) ∈ H({`}, {⊗`W , ⊗`C }), such that the unique output is reachable from eachvertex.
It can be observed that, for any contraction tree, an input (if any) is not an output but
a source of a contraction edge.
`: `⊗km ⇒ `⊗k }k∈N , with ` ∈Definition 5.6 (Distributor). We define a family {Dk,m{?, }, of hypernets which we call distributors, inductively as follows:
`
D0,m
=∅
`
D1,0
=

`
D1,1
=

`

⌦

`

⌦
`

⌦

`
`

`
D1,m+1⌦m```
D1,m+2 =``Dk+1,m
= Πid
ρ

⌦

`

 ⌦k

16

`
`
`
`
Dk,m
D1,m
`⌦km `⌦m,where ∅ denotes the empty hypernet, id is the identity map, and ρ is a bijection suchthat, for each j ∈ {1, . . . , k} and i ∈ {1, . . . , m}, ρ(j + (k + 1)(i − 1)) = j + k(i − 1) andρ((k + 1)i) = km + i.
`
When k = 1, a distributor D1,m
is a contraction tree that includes one weakening edge.
It is indeed a normal form with respect to the laws on contraction trees that we introduce
?

?

⌦

⌦

∗ =⌦ ⌦ ⌦ ⌦later. For instance, D2,3??

 =and D3,0

⌦

⌦

??

??

⇧ ⇧ ⇧

⌦⌦⌦

.

Definition 5.7 (Box/stable hypernets). If a hypernet is a path of only one box edge, it iscalled box hypernet. A stable hypernet is a hypernet (G : ? ⇒ ⊗m
i=1 `i ) ∈ H(L, {I} ∪ OX ),mnmsuch that ⊗i=1 `i ∈ ({} ∪ {T (?) | n ∈ N}) and each vertex is reachable from the uniqueinput.
Definition 5.8 (Copyable hypernets). A hypernet H : ? ⇒ ?⊗k ⊗ ⊗h is called copyable0

if it is?⌦m ?⌦k0 ⇧⌦h⇧⇥m
i=1 Bi~`I or, where φ ∈ O, and each Bi is a box hypernet.
?

?

Definition 5.9 (One-way hypernets). A hypernet H is one-way if, for any pair (vi , vo ) of
an input and an output of H such that vi and vo both have type ?, any path from vi to
vo is not an operation path.
Remark 5.10 (Distributors). The reader familiar with diagrammatic languages based on
monoidal categories equipped with “sharing” (co)monoid operators, such as the ZX-calculusof Coecke and Duncan [2011], the distributor nets may seem an awkward alternative toquotienting the nets by the equational properties of the (co)monoid operator. Indeed aformulation of Spartan semantics in which distributor nets are collapsed into n-ary contractions would be quite accessible. However, the structural laws of Spartan including
equational properties of contraction, mentioned in Sec. 4.1, can be invalidated by certain
ill-behaved but definable operations. Forcing these properties into the framework does notseem to be practically possible, as it leads to intractable interactions between such complex
n-ary contractions and operations in the context as required by the key notion of robustness
which will be introduced in Sec. 6.3.

5.2. Focussed hypernets
Definition 5.11. A token edge in a hypergraph is said to be exposed if its source is an
input and its target is an output, and self-acyclic if its source and its target are different
vertices.
Definition 5.12 (Focussed hypernets). Focussed hypernets (typically ranged over by
Ġ, Ḣ, Ṅ ) are those that contain only one token edge and the edge is shallow, self-acyclic
and not exposed.
Focus-free hypernets are given by Hω (L, MO \{?, X, }), i.e. hypernets without tokenedges. A focussed hypernet Ġ can be turned into an underlying focus-free hypernet |Ġ|
with the same type, by removing its unique token edge and identifying the source and thetarget of the edge. When a focussed hypernet Ġ has a t-token, then changing the token
17label t to another one t0 yields a focussed hypernet denoted by hĠit0 /t . The source (resp.
target) of a token is called “token source” (resp. “token target”) in short.
Given a focus-free hypernet G, a focussed hypernet t;i G with the same type can beyielded by connecting a t-token to the i-th input of G if the input has type ?. Similarly, afocussed hypernet G;i t with the same type can be yielded by connecting a t-token to thei-th output of G if the output has type ?. If it is not ambiguous, we omit the index i in
the notation ;i .

5.3. Contexts
The set of holed hypernets (typically ranged over by C) is given by Hω (L, MO ∪ M), where
the edge label set MO is extended by a set M of hole labels. Hole labels are typed, andtypically ranged over by χ : ~` ⇒ `~0 .
Definition 5.13 (Contexts). A holed hypernet C is said to be context if each hole label
appears at most once (at any depth) in C.
Definition 5.14. A simple context is a context that contains a single hole, which isshallow.
When χ
~ gives a list of all and only hole labels that appear in a context C, the context
can be also written as C[~χ]; a hypernet in Hω (L, MO ) can be seen as a “context withouta hole”, C[ ].
Let C[χ~1 , χ, χ~2 ] and C 0 [χ~3 ] be contexts, such that the hole χ and the latter context C 0 havethe same type and χ~1 ∩ χ~2 ∩ χ~3 = ∅. A new context C[χ~1 , C 0 , χ~2 ] ∈ Hω (L, MO ∪ χ~1 ∪ χ~3 ∪ χ~2 )can be obtained by plugging C 0 into C: namely, by replacing the (possibly deep) hole edgeof C that has label χ with the context C 0 , and by identifying each input (resp. output)of C 0 with its corresponding source (resp. target) of the hole edge (Def. A.5). Each edgeof the new context C[χ~1 , C 0 , χ~3 ] is inherited from either C or C 0 , keeping the type; this
implies that the new context is indeed a context with hole labels χ~1 , χ~3 , χ~2 . Inputs andoutputs of the new context coincide with those of the original context C, and hence thesetwo contexts have the same type. The plugging is associative in two senses: plugging twocontexts into two holes of a context yields the same result regardless of the order, i.e.
C[χ~1 , C 0 , χ~2 , C 00 , χ~3 ] is well-defined; and nested plugging yields the same result regardless ofthe order, i.e. C[χ~1 , C 0 [χ~3 , C 00 , χ~4 ], χ~2 ] = (C[χ~1 , C 0 , χ~2 ])[χ~1 , χ~3 , C 00 , χ~4 , χ~2 ].
The notions of focussed and focus-free hypernets can be naturally extended to contexts.
˙ χ], the token is said to be entering if it is an incoming edge of a
In a focussed context C[~
hole, and exiting if it is an outgoing edge of a hole. The token may be both entering andexiting.

5.4. States and transitions
Given the two parameters O and BO , the universal abstract machine U(O, BO ) is defined
as a state transition system. It is namely given by data (SO , T ] BO ) as follows, each ofwhich we will describe in the sequel.
• SO ⊆ Hω (L, MO ) is a set of states,• T ⊆ SO × SO is a set of intrinsic transitions, and• BO ⊆ SO × SO is a set of extrinsic transitions.
18

?⌦k
H
?

⇧⌦h

?
C
0
? ?⌦k

?⌦k
?
Dk,2

⇧⌦h
⇧
Dh,2

?⌦k ?⌦k⇧⌦h ⇧⌦h

?⌦k
H
?
7!

?

⇧⌦h ?⌦k

H
?

⇧⌦h

?
C
0
? ?⌦k

⌦
?

?⌦k

0

? ?⌦k

0

Figure 7: Contraction rules, with C a contraction tree, and H a copyable hypernet
A focussed hypernet of type ? ⇒  in Hω (L, MO ) is said to be a state. A state Ġ iscalled initial if Ġ =?; |Ġ|, and final if Ġ = X; |Ġ|. A state is said to be stuck if it is not
final and cannot be followed by any transition. An execution on a focus-free hypernet
G : ? ⇒  is a sequence of transitions starting from an initial state ?; G. The following
will be apparent once transitions are defined: initial states are indeed initial in the sensethat no search transition results in an initial state; and final states are indeed final in thesense that no transition is possible from a final state.
The interaction rules in Fig. 3 specify the first class of intrinsic transitions, search transitions, and the contraction rules in Fig. 7 specify the second class of intrinsic transitions,copy transitions. These intrinsic transitions are defined as follows: for each interaction⊗•
rule Ġ 7→ Ġ0 (or resp. contraction rule Ġ 7→ Ġ0 ), if there exists a focus-free simple context
C[χ] : ? ⇒  such that C[Ġ] and C[Ġ0 ] are states, C[Ġ] → C[Ġ0 ] is a search transition (orresp. copy transition).
Search transitions are deterministic, because at most one interaction rule can be applied
at any state. Although two different contraction rules may be possible at a state, copytransitions are still deterministic. Namely, if two different contraction rules Ġ 7→ Ġ0 andḢ 7→ Ḣ 0 can be applied to the same state, i.e. there exist focus-free simple contexts CG and
CH such that CG [Ġ] = CH [Ḣ], then these two rules yield the same transition, by satisfying
CG [Ġ0 ] = CH [Ḣ 0 ]. Informally, in Fig. 7, H is determined uniquely and the choice of C does
not affect the result.
Intrinsic transitions are therefore all deterministic, and moreover, search transitions
are reversible because the inverse of the interaction rules is again deterministic. When asequence Ġ →∗ Ġ0 of transitions consists of search transitions only, it is annotated by the• ∗symbol • as Ġ →Ġ0 .
An execution on any stable net, or on representation of any value, terminates successfully
at a final state with only search transitions (by Lem. A.16, Lem. A.18 and Lem. A.20(1)).
The behaviour BO , which is a parameter of the machine, specifies a set of extrinsic transitions. Extrinsic transitions are also dubbed “compute” transitions, and each of themmust target an active operation. Namely, a transition Ġ → Ġ0 is a compute transition if:
the first state Ġ has a rewrite token ( ) that is an incoming edge of an active operation
edge; and the second state Ġ0 has a search token (?). Copy transitions or compute transitions are possible if and only if a state has a rewrite token ( ), and they always change thetoken to a search token (?). We refer to copy transitions and compute transitions altogher
as “rewrite” transitions.
Compute transitions may be specified locally, by rewrite rules, in the same manner as the19intrinsic transitions. We leave it entirely open what the actual rewrite associated to some
operation is, by having the behaviour BO as parameter as well as the operation set O. Thisis part of the semantic flexibility of our framework. We do not specify a meta-language
for encoding effects as particular transitions. Any algorithmic state transformation is
acceptable.
Remark 5.15. This abstract machine is “universal” in a sense of the word similar to theway it is used in “universal algebra” rather than in “universal Turing machine”. It is a
general abstract framework in which a very wide range of concrete abstract machines canbe instantiated by providing operations and their rewrite rules.

6. A characterisation theorem
Given the universal abstract machine U(O, BO ) with parameters O and BO , we can now
define the notions of contextual refinement and equivalence, and formalise a proof method
for them. All the technical development in this section is with respect to the machine
U(O, BO ), and hence globally parametrised by O and BO .
Firstly in Sec. 6.1, we state the condition of the machine, to which the proof method
applies. Sec. 6.2 proposes our generalised notions of contextual refinement and equivalence. Sec. 6.3 formalises the proof method as a characterisation theorem (Thm. 6.14),
introducing the key concept of robustness. Finally, in Sec. 6.4, we list some useful lemmas
that can be used in robustness check.

6.1. Determinism and refocusing
We here focus on the situation where the universal abstract machine is both deterministic
as a state transition system, and refocusing in the following sense.
Definition 6.1 (Rooted states and refocusing machine).
∗•• A state Ġ is rooted if ?; |Ġ| →Ġ.

• The universal abstract machine U(O, BO ) is refocusing if every transition preserves
the rooted property.
Because intrinsic transitions are all deterministic, the machine becomes deterministic if
the behaviour BO specifies deterministic compute transitions.
Any initial state is trivially rooted, and search transitions preserve the rooted property. The stationary property below gives a sufficient condition for a rewrite transition topreserve the rooted property (Lem. A.13).
Definition 6.2 (Stationary rewrite transitions). A rewrite transition Ġ → Ġ0 is stationary
if there exist a focus-free simple context C, focus-free hypernets H and H 0 , and a numberi ∈ N, such that H is one-way, Ġ = C[ ;i H] and Ġ0 = C[?;i H 0 ], and the following holds.
For any j ∈ N\{i}, such that C[?;j H] is a state, there exists a state Ṅ with a rewrite•
token, such that C[?;j H] →Ṅ .
Copy transitions are stationary, and hence they preserve the rooted property, because
each input of the contraction tree C in Fig. 7 is a source of a contraction edge. Therefore,
the machine becomes refocusing if the behaviour BO specifies compute transitions that
preserve the rooted property.

20Remark 6.3 (Refocusing). When a rewrite transition results in a rooted state Ṅ 0 , starting
the search process (i.e. search transitions) from the state Ṅ 0 can be seen as resuming• ∗Ṅ 0 , from an initial state, on the underlying hypernet |Ṅ 0 |.
the search process ?; |Ṅ 0 | →Resuming redex search after a rewrite, rather than starting from scratch, is an important
aspect of abstract machines. In the case of the lambda-calculus, enabling the resumption
is identified as one of the key steps (called “refocusing”) to synthesise abstract machinesfrom reduction semantics by Danvy et al. [2012]. In our setting, it is preservation of therooted property that justifies the resumption.
The stationary property, as a sufficient condition of preservation of the rooted property,
characterises many operations with local behaviour. Compute transitions of operations thatinvolve non-local change of a token position, like label jumping, could preserve the rooted
property without being stationary.

6.2. Contextual refinement and equivalence
We propose notions of contextual refinement and equivalence that check for successful
termination of execution, taking the number of transitions into account. These notions
are with respect to the universal abstract machine U(O, BO ), and parametrised by thefollowing: a set C ⊆ Hω (L, MO ∪ M) of focus-free contexts that is closed under plugging(i.e. for any contexts C[χ~1 , χ, χ~2 ], C 0 ∈ C such that C[χ~1 , C 0 , χ~2 ] is defined, C[χ~1 , C 0 , χ~2 ] ∈ C);
and a preorder Q on natural numbers.
Definition 6.4 (State refinement and equivalence). Let Q be a preorder on N, and Ġ1
and Ġ2 be two states.
˙ Q Ġ2 ), if for any number• Ġ1 is said to refine Ġ2 up to Q, written as BO |= (Ġ1 
k1 ∈ N and any final state Ṅ1 such that Ġ1 →k1 Ṅ1 , there exist a number k2 ∈ N
and a final state Ṅ2 such that k1 Q k2 and Ġ2 →k2 Ṅ2 .
˙ Q Ġ2 ), if• Ġ1 and Ġ2 are said to be equivalent up to Q, written as BO |= (Ġ1 '˙ Q Ġ2 ) and BO |= (Ġ2 ˙ Q Ġ1 ).
BO |= (Ġ1 
Definition 6.5 (Contextual refinement and equivalence). Let C be a set of contexts thatis closed under plugging, Q be a preorder on N, and H1 and H2 be focus-free hypernetsof the same type.
• H1 is said to contextually refine H2 in C up to Q, written as BO |= (H1 C
Q H2 ),
if any focus-free context C[χ] ∈ C, such that ?; C[H1 ] and ?; C[H2 ] are states, yields
˙ Q ?; C[H2 ]).
refinement BO |= (?; C[H1 ] • H1 and H2 are said to be contextually equivalent in C up to Q, written as BO |=CC(H1 'CQ H2 ), if BO |= (H1 Q H2 ) and BO |= (H2 Q H1 ).
˙ Q Ġ2 etc., making the parameter BO implicit.
In the sequel, we simply write Ġ1 C
˙ Q and  are indeed preorders, and accordingly, equivalences
Because Q is a preorder, QC˙ Q and 'Q are indeed equivalences (Lem A.22). Examples of preorder Q include: the'universal relation N × N, the “greater-than-or-equal” order ≥N , and the equality =N .
When the relation Q is the universal relation N × N, the notions concern successful
termination, and the number of transitions is irrelevant. If all compute transitions areCdeterministic, contextual equivalences 'C≥N and '=N coincide for any C (as a consequenceof Lem. A.23).

21

C
Because C is closed under plugging, the contextual notions C
Q and 'Q indeed become
congruences. Namely, for any H1 C H2 and C ∈ C such that C[H1 ] and C[H2 ] are defined,
C[H1 ] C C[H2 ], where  ∈ {Q , 'Q }.
As the parameter C, we will particularly use the set CO ⊆ Hω (L, MO ∪ M) of any
focus-free contexts, and its subset CO-bf of binding-free contexts.

Definition 6.6 (Binding-free contexts). A focus-free context C is said to be binding-free
if there exists no path, at any depth, from a source of a contraction, atom, box or holeedge, to a source of a hole edge.
The set CO is closed under plugging, and so is the set CO-bf (Lem. A.21). Restriction
to binding-free contexts are necessary to focus on call-by-value languages, because only
values are bound in these languages. The restriction reflects syntactical restriction oncontexts as C ::= [ ] | φ(~t, C, ~t0 ; ~s) | ~y .C | bind x → t in C | new a ( t in C, where thehole ‘[ ]’ does not appear in the bound positions.

6.3. Templates and robustness
Reasoning with graphs is based on the concept of template. Informally speaking, templates
are families of graphs which will be used in (in)equational reasoning. The rewrite rules ofthe operations are natural candidates for templates. For example the families of graphsinterpreting Spartan terms for m+n and p (where p = m+n) could be used as templates.
But any families of graphs, subject to the conditions below, can be used as templates.
Throughout this section, let C be a set of contexts, and Q, Q0 and Q00 be binary relations
on N.
Definition 6.7 (Pre-template). A pre-template is a union C := ∪I∈I CI of a family ofbinary relations on focus-free hypernets Hω (L, MO \{?, X, }) indexed by a set I of types,
such that for any G1 CI G2 where I ∈ I, G1 and G2 are focus-free hypernets with type
G1 : I and G2 : I.
Obviously, if C is a pre-template, its converse C−1 is also a pre-template.
Definition 6.8 ((Quasi-)specimens). Let C be a pre-template, and R and R0 be binary
relations on states.
˙ χ]; H~ 1 ; H~ 2 ) is a C-specimen of C if the following hold:
1. A triple (C[~˙ χ]| ∈ C, and |~(A) |C[~
χ| = |H~ 1 | = |H~ 2 |.

χ|}.
(B) Hi1 C Hi2 for each i ∈ {1, . . . , |~˙ H~ p ] is a state for each p ∈ {1, 2}.
(C) C[

2. A pair (Ṅ1 , Ṅ2 ) of states is a quasi-C-specimen of C up to (R, R0 ), if there exists a
˙ H~ 1 ; H~ 2 ) of C such that the following hold:C-specimen (C;˙ Ṅ1 and Ṅ2 all have the same label.
(A) The tokens of C,

˙ H~ 1 ] and C[
˙ H~ 2 ] are also rooted, Ṅ1 R C[
˙ H~ 1 ],(B) If Ṅ1 and Ṅ2 are rooted, then C[0~˙ H 2 ] R Ṅ2 .
and C[

We can refer to the token label of a C-specimen and a quasi-C-specimen. Any C˙ H~ 1 ; H~ 2 ) gives a quasi-C-specimen (C[˙ H~ 1 ], C[H˙ 2 ]) up to (=, =). We say a
specimen (C;~~˙ χ]; H 1 ; H 2 ) is single if |~C-specimen (C[~χ| = 1, i.e. the context C˙ has exactly one hole edge
(at any depth).
22

Definition 6.9 (Input-safety). A pre-template C is (C, Q, Q0 )-input-safe if, for any C˙ H~ 1 ; H~ 2 ) of C such that C˙ has an entering search token, one of the following
specimen (C;holds.
˙ H~ p ] →∗ Ṅp for each p ∈ {1, 2}.
(I) There exist two stuck states Ṅ1 and Ṅ2 such that C[(II) There exist a C-specimen (Ċ 0 ; H~01 ; H~02 ) of C and two numbers k1 , k2 ∈ N, such that˙ H~ 1 ] →1+k1 Ċ 0 [H~01 ],the token of Ċ 0 is not a rewrite token and not entering, (1 + k1 ) Q k2 , C[
˙ H~ 2 ] →k2 Ċ 0 [H~02 ].
and C[

˙ Q0 , '˙ Q0 ), whose token is not a(III) There exist a quasi-C-specimen (Ṅ1 , Ṅ2 ) of C up to ('˙ H~ 1 ] →1+k1 Ṅ1 ,rewrite token, and two numbers k1 , k2 ∈ N, such that (1 + k1 ) Q (1 + k2 ), C[
˙ H~ 2 ] →1+k2 Ṅ2 .
and C[
Definition 6.10 (Output-closure). A pre-template C is output-closed if, for any hypernets
H1 C H2 , either H1 or H2 is one-way.

Definition 6.11 (Templates). A pre-template C is a (C, Q, Q0 )-template, if it is (C, Q, Q0 )input-safe and also output-closed.
Definition 6.12 (Robustness). A pre-template C is (C, Q, Q0 , Q00 )-robust relative to a
˙ H~ 1 ; H~ 2 ) of C, such that C[
˙ H~ 1 ] = Ṅrewrite transition Ṅ → Ṅ 0 if, for any C-specimen (C;and the token of C˙ is a rewrite token and not entering, one of the following holds.
˙ H~ 1 ] or C[
˙ H~ 2 ] is not rooted.
(I) C[(II) There exists a stuck state N˙ 00 such that Ṅ 0 →∗ N˙ 00 .

˙ Q0 , ˙ Q00 ), whose token is not(III) There exist a quasi-C-specimen (N˙100 , N˙200 ) of C up to (a rewrite token, and two numbers k1 , k2 ∈ N, such that (1 + k1 ) Q k2 , Ṅ 0 →k1 N˙100 , and˙ H~ 2 ] →k2 N˙ 00 .
C[
2Finally, the characterisation theorem (Thm. 6.14 below) enables us to prove contextual˙
˙refinement C
Q using state refinements Q0 and Q00 , under the assumption that the triple
000(Q, Q , Q ) is “reasonable” in the following sense.
Definition 6.13 (Reasonable triples). A triple (Q, Q0 , Q00 ) of preorders on N is reasonable
if the following hold:(A) Q is closed under addition, i.e. any k1 Q k2 and k10 Q k20 satisfy (k1 + k10 ) Q (k2 + k20 ).
(B) Q0 ⊆ ≥N , and Q0 ⊆ Q00 .
(C) Q0 ◦ Q ◦ Q00 ⊆ Q, where ◦ denotes composition of binary relations.

Examples of a reasonable triple (Q, Q0 , Q00 ) include: (N × N, ≥N , N × N), (N × N, ≥N , ≥N ),(N × N, =N , =N ), (≥N , ≥N , ≥N ), (≥N , =N , ≥N ), (≤N , =N , ≤N ), (≥N , =N , =N ), (≤N , =N , =N ),(=N , =N , =N ).
Theorem 6.14. If an universal abstract machine U(O, BO ) is deterministic and refocusing, it satisfies the following property. For any set C ⊆ Hω (L, MO ∪ M) of contexts thatis closed under plugging, any reasonable triple (Q, Q0 , Q00 ), and any pre-template C on
focus-free hypernets Hω (L, MO \{?, X, }):1. If C is a (C, Q, Q0 )-template and (C, Q, Q0 , Q00 )-robust relative to all rewrite transitions, then C implies contextual refinement in C up to Q, i.e. any G1 C G2 implies
G1 C
Q G2 .
23

2. If C is a (C, Q−1 , Q0 )-template and the converse C−1 is (C, Q, Q0 , Q00 )-robust relative
to all rewrite transitions, then C−1 implies contextual refinement in C up to Q, i.e.
any G1 C G2 implies G2 C
Q G1 .
Proof. This is a consequence of Prop. 7.6, Prop. 7.2 and Prop. 7.4 in Sec. 7.
Remark 6.15 (Monotonicity). Contextual/state refinement and equivalence are monotonic with respect to Q, in the sense that Q1 ⊆ Q2 implies Q1 ⊆ Q2 for each  ∈˙ ',˙ C , 'C }. Contextual refinement and equivalence are anti-monotonic with respect to{,C, in the sense that C1 ⊆ C2 implies C2 ⊆ C1 for each  ∈ {Q , 'Q }. This means, inCCparticular, 'QO ⊆ 'QO-bf .
Given that C1 ⊆ C2 , Q1 ⊆ Q2 , Q01 ⊆ Q02 , Q01 ⊆ Q02 , R1 ⊆ R2 and R10 ⊆ R20 , the following
holds. Any C1 -specimen is a C2 -specimen, and any quasi-C1 -specimen up to (R1 , R10 ) is aquasi-C2 -specimen up to (R2 , R20 ). Any (C, Q1 , Q01 )-template is a (C, Q2 , Q02 )-template. If
C is (C, Q1 , Q01 , Q001 )-robust relative to a rewrite transition, then it is also (C, Q2 , Q02 , Q002 )robust relative to the same transition. Note that the notions of template and robustness
are not monotonic nor anti-monotonic with respect to C.
To prove that a pre-template C induces contextual equivalence, one can use Thm. 6.14(1)twice with respect to C and C−1 . One can alternatively use Thm. 6.14(1) and Thm. 6.14(2),both with respect to C. This alternative approach is often more economical. The reason
is that the approach involves proving input-safety of C with respect to two parameters
1(C, Q, Q0 ) and (C, Q , Q0 ), which typically boils down to a proof for one parameter, thanks
to the monotonicity.

6.4. Sufficient conditions for robustness
A proof of robustness becomes trivial for a specimen with a rewrite token that gives a
non-rooted state. Thanks to the lemma below, we can show that a state is not rooted, by
checking paths from the token target.
Definition 6.16 (Accessible paths).
• A path of a hypernet is said to be accessible if it consists of edges whose all sources
have type ?.
• An accessible path is called stable if the labels of its edges are included in {I} ∪ OX .
• An accessible path is called active if it starts with one active operation edge andpossibly followed by a stable path.
Note that box edges and atom edges never appear in an accessible path.
Lemma 6.17. If a state has a rewrite token that is not an incoming edge of a contraction
edge, then the state satisfies the following property: If there exists an accessible, but not
active, path from the token target, then the state is not rooted.
Proof. This is a contraposition of a consequence of Lem. A.10 and Lem. A.20(2).
Checking the condition (III) of robustness (see Def. 6.12) involves finding a quasi-C˙ Q0 , 
˙ Q00 ), namely checking the condition (B) of Def. 6.8(2). The
specimen of C up to (˙following lemma enables us to use contextual refinement C
Q0 to yield state refinement Q0 ,via single C-specimens of a certain pre-template C.

24

Definition 6.18. A pre-template C is a trigger if it satisfies the following:˙(A) For any single C-specimen (C[χ];H 1 ; H 2 ) of C, such that C˙ has an entering search
˙ p ] → hC[H˙ p ]i /? for each p ∈ {1, 2}.
token, C[H(B) For any hypernets H 1 C H 2 , both H1 and H2 are one-way.

Lemma 6.19. Let C be a set of contexts, and Q0 be a binary relation on N such that, forany k0 , k1 , k2 ∈ N, (k0 + k1 ) Q0 (k0 + k2 ) implies k1 Q0 k2 . Let C be a pre-template that is a12
˙
trigger and implies contextual refinement C
Q0 . For any single C-specimen (C[χ]; H ; H )˙ 1 ] and C[H˙ 2 ] isof C, if compute transitions are all deterministic, and one of states C[H˙ 1] 
˙ 2 ].
˙ Q0 C[Hrooted, then the other state is also rooted, and moreover, C[HProof. This is a corollary of Lem. A.24.
Remark 6.20. The notion of contextual refinement concerns initial states, and therefore,
only enables us to safely replace a part of a hypernet before execution. Because any initialstate is rooted, if all transitions preserve the rooted property, we can safely assume thatany state that arises in an execution is rooted. If all transitions are also deterministic,
Lem. 6.19 enables us to use some contextual refinement and safely replace a part of a
hypernet during execution. This can validate run-time garbage collection, for example.

7. Proof of the characterisation theorem
This section details the proof of Thm. 6.14, with respect to the machine U(O, BO ) parametrised
by O and BO .
At the core of the proof is step-wise reasoning, or transition-wise reasoning, using a lax
variation of simulation. Providing a simulation boils down to case analysis on transitions,
namely on possible interactions between the token and parts of states contributed by a pretemplate. While output-closure helps us disprove some cases, input-safety and robustness
give the cases that are specific to a pre-template and an operation set.
We also employ the so-called up-to technique in the use of quasi-specimens. Our variation of simulation is up to state refinements, with a quantitative restriction implemented
by the notion of reasonable triple. This restriction is essential to make this particular
up-to technique work, in combination with our lax variation of simulation. A similar formof up-to technique is studied categorically by Bonchi et al. [2017], but for the ordinary
notion of (weak) simulation, without this quantitative restriction.
The lax variation of simulation we use is namely (Q, Q0 , Q00 )-simulation, parametrised
˙ Q,
by a triple (Q, Q0 , Q00 ). This provides a sound approach to prove state refinement 000
˙ Q0 and ˙ Q00 , given that all transitions are deterministic and (Q, Q , Q ) forms ausing reasonable triple.
Definition 7.1 ((Q, Q0 , Q00 )-(bi)simulations). Let R be a binary relation on states, and(Q, Q0 , Q00 ) be a triple of preorders on N. The binary relation R is a (Q, Q0 , Q00 )-simulationif, for any two related states Ġ1 R Ġ2 , the following (A) and (B) hold:(A) If Ġ1 is final, Ġ2 is also final.
(B) If there exists a state Ġ01 such that Ġ1 → Ġ01 , one of the following (I) and (II) holds:(I) There exists a stuck state Ġ001 such that Ġ01 →∗ Ġ001 .

˙ Q0 ◦ R ◦ ˙ Q00 )(II) There exist two states Ḣ1 and Ḣ2 , and numbers k1 , k2 ∈ N, such that Ḣ1 (Ḣ2 , (1 + k1 ) Q k2 , Ġ01 →k1 Ḣ1 , and Ġ2 →k2 Ḣ2 .
25

Proposition 7.2. When the universal abstract machine U(O, BO ) is deterministic, itsatisfies the following.
For any binary relation R on states, and any reasonable triple (Q, Q0 , Q00 ), if R is a
(Q, Q0 , Q00 )-simulation, then R implies refinement up to Q, i.e. any Ġ1 R Ġ2 implies
˙ Q Ġ2 .
Ġ1 
Proof. Our goal is to show the following: for any states Ġ1 R Ġ2 , any number k1 ∈ N andany final state Ṅ1 , such that Ġ1 →k1 Ṅ1 , there exist a number k2 ∈ N and a final stateṄ2 such that k1 Q k2 and Ġ2 →k2 Ṅ2 . The proof is by induction on k1 ∈ N.
In the base case, when k1 = 0, the state Ġ1 is itself final because Ġ1 = Ṅ1 . Because R is
a (Q, Q0 , Q00 )-simulation, Ġ2 is also a final state, which means we can take 0 as k2 and Ġ2
itself as Ṅ2 . Because (Q, Q0 , Q00 ) is a reasonable triple, Q is a preorder and 0 Q 0 holds.
In the inductive case, when k1 > 0, we assume the induction hypothesis on any h ∈ Nsuch that h < k1 . Now that k1 > 0, there exists a state Ġ01 such that Ġ1 → Ġ01 →k−1 Ṅ1 .
Because all intrinsic transitions are deterministic, the assumption that compute transitions
are all deterministic implies that states and transitions comprise a deterministic abstract
rewriting system, in which final states and stuck states are normal forms. By Lem. A.6,
we can conclude that there exists no stuck state Ġ001 such that Ġ01 →∗ Ġ001 .
Therefore, by R being a (Q, Q0 , Q00 )-simulation, there exist two states Ḣ1 and Ḣ2 , and˙ Q0 ◦ R ◦ ˙ Q00 ) Ḣ2 , (1 + l1 ) Q l2 , Ġ01 →l1 Ḣ1 , andnumbers l1 , l2 ∈ N, such that Ḣ1 (Ġ2 →l2 Ḣ2 . By the determinism, 1 + l1 ≤ k1 must hold; if Ḣ1 is a final state, Ġ01 →l1 Ḣ1must coincide with Ġ01 →k−1 Ṅ1 ; otherwise, Ġ01 →l1 Ḣ1 must be a suffix of Ġ01 →k−1 Ṅ1 .
There exist two states Ḣ3 and Ḣ4 , and we have the following situation, where the relations
˙ Q0 and ˙ Q00 are represented by vertical dotted lines from top to bottom.
R, 
G˙1

k1 −1−l1

l1

/ Ḣ1

/ G˙0

1

/

N˙1

˙ 0

Q
R

Ḣ3
R
Ḣ4
˙


(1+l1 ) Q l2

l2

/ Ḣ2

G˙2

Q00

We expand the above diagram as below (indicated by magenta), in three steps.
G˙1

/ G˙0

1

l1

/ Ḣ1

k1 −1−l1/

N˙1

˙ 0 (k1 −1−l1 ) Q0 m3

Q
Ḣ3
R

(1+l1 ) Q l2m3/

m3 Q m 4

R
Ḣ4

m4

/

˙ 00

Q
G˙2

l2

/ Ḣ2

26

N˙3

N˙4

m4 Q00 m2
m2

/

N˙2

Firstly, by definition of state refinement, there exist a number m3 ∈ N and a final stateṄ3 such that (k1 − 1 − l1 ) Q0 m3 and Ḣ3 →m3 Ṅ3 . Because (Q, Q0 , Q00 ) is a reasonable
triple, Q0 ⊆≥N , and hence k1 > k1 − 1 − l1 ≥ m3 . Therefore, secondly, by induction
hypothesis on m3 , there exist a number m4 ∈ N and a final state Ṅ4 such that m3 Q m4
and Ḣ4 →m4 Ṅ4 . Thirdly, by definition of state refinement, there exist a number m2 ∈ N
and a final state Ṅ2 such that m4 Q00 m2 and Ḣ2 →m2 Ṅ2 .
Now we have (k1 − 1 − l1 ) Q0 m3 , m3 Q m4 and m4 Q00 m2 , which means (k1 − 1 −l1 ) (Q0 ◦ Q ◦ Q00 ) m2 . Because (Q, Q0 , Q00 ) is a reasonable triple, this implies (k1 − 1 − l1 ) Q
m2 , and moreover, k1 Q (l2 + m2 ). We can take l2 + m2 as k2 .
The token in a focussed context C˙ is said to be remote, if it is a search token, a value
token, or not entering. The procedure of contextual lifting reduces a proof of contextualrefinement down to that of state refinement.
Definition 7.3 (Contextual lifting). Let C ⊆ Hω (L, MO ∪ M) be a set of contexts. Givena pre-template C on focus-free hypernets Hω (L, MO \{?, X, }), its C-contextual lifting
CC is a binary relation on states defined by: Ġ1 CC Ġ2 if there exists a C-specimen
˙ H~ 1 ; H~ 2 ) of C, such that the token of C˙ is remote, Ġp = C[˙ H~ p ], and C[
˙ H~ p ] is rooted, for(C;each p ∈ {1, 2}.
The contextual lifting CC is by definition a binary relation on rooted states.
Proposition 7.4. For any set C ⊆ Hω (L, MO ∪ M) of contexts that is closed under plugging, any preorder Q on N, and any pre-template C on focus-free hypernets Hω (L, MO \{?, X, }),˙ Q (resp. equivalence '˙ Q ), then C implies
if the C-contextual lifting CC implies refinement CCcontextual refinement Q (resp. contextual equivalence 'Q ).
Proof of refinement case. Our goal is to show that, for any H1 C H2 and any focus-free˙Qcontext C[χ] ∈ C such that ?; C[H1 ] and ?; C[H2 ] are states, we have refinement ?; C[H1 ] ?; C[H2 ].
Because ?; C[Hp ] =?; (C[Hp ]) = (?; C)[Hp ] for p ∈ {1, 2}, and |?; C| = C ∈ C, the triple((?; C); H1 ; H2 ) is a C-specimen of C with a search token. Moreover the states ?; C[H1 ]and ?; C[H2 ] are trivially rooted. Therefore, ?; C[H1 ] CC ?; C[H2 ], and by the assumption,
˙ Q ?; C[H2 ].
?; C[H1 ] Proof of equivalence case. It suffices to show that, for any H1 C H2 and any focus-free˙Qcontext C[χ] ∈ C such that ?; C[H1 ] and ?; C[H2 ] are states, we have refinements ?; C[H1 ] ˙ Q ?; C[H1 ], i.e. equivalence ?; C[H1 ] '˙ Q ?; C[H2 ].
?; C[H2 ] and ?; C[H2 ] Because ?; C[Hp ] =?; (C[Hp ]) = (?; C)[Hp ] for p ∈ {1, 2}, and |?; C| = C ∈ C, the triple((?; C); H1 ; H2 ) is a C-specimen of C with a search token. Moreover the states ?; C[H1 ]and ?; C[H2 ] are trivially rooted. Therefore, ?; C[H1 ] CC ?; C[H2 ], and by the assumption,
˙ Q ?; C[H2 ].
?; C[H1 ] 'Lemma 7.5. For any set C ⊆ Hω (L, MO ∪ M) of contexts that is closed under plugging,any pre-template C on focus-free hypernets Hω (L, MO \{?, X, }), and any C-specimen˙ χ]; H~ 1 ; H~ 2 ) of C, the following holds.
(C[~˙ H~ 1 ] is final (resp. initial) if and only if the state C[
˙ H~ 2 ] is final (resp.
1. The state C[
initial).
˙ H~ 1 ] and C[
˙ H~ 2 ] are both rooted states, then the token of
2. If C is output-closed, and C[
C˙ is not exiting.
27

˙ H~ 1 ] and C[
˙ H~ 2 ] are both rooted states, the token of C˙ is a
3. If C is output-closed, C[
˙ H~ 1 ] orvalue token or a non-entering search token, and a transition is possible from C[
˙ H~ 2 ], then there exists a focussed context Ċ 0 with a remote token such that |Ċ 0 | = |C|
˙
C[
p
0
p
˙ H~ ] → Ċ [H~ ] for each p ∈ {1, 2}.
and C[
˙ H~ p ] is
Proof of point (1). Let (p, q) be an arbitrary element of a set {(1, 2), (2, 1)}. If C[p˙~˙
final (resp. initial), the token source is an input in C[H ]. Because input lists of C[H~ p ], C˙
˙ H~ q ] all coincide, the token source must be an input in C,
˙ and in C[
˙ H~ q ] too. This
and C[q˙~means C[H ] is also a final (resp. initial) state.
Proof of point (2). This is a consequence of the contraposition of Lem. A.12(3).
˙ H~ 1 ] or C[
˙ H~ 2 ] is necessarily a search
Proof of the point (3). The transition possible from C[
˙ we can confirm that the search transitiontransition. By case analysis on the token of C,
˙applies an interaction rule to the token and an edge from C.
• When the token of C˙ is a value token, the transition can only change the token andits incoming operation edge. Because C is output-closed, by the point (2), the tokenof C˙ is not exiting. This implies that the incoming operation edge of the token is˙ H~ 1 ] and C[
˙ H~ 2 ].
from C˙ in both states C[• When the token of C˙ is a non-entering search token, the transition can only change
˙ the outgoing
the token and its outgoing edge. Because the token is not entering in C,
~
~
1
2
˙
˙
˙
edge is from C in both states C[H ] and C[H ].
Therefore, there exist a focus-free simple context C0 [χ, χ~ ] and an interaction rule Ṅ0 7→ Ṅ00 ,such that C˙ = C0 [Ṅ0 , χ~ ], and C0 [Ṅ00 , χ~ ] is a focussed context.
˙ = |C0 [Ṅ0 , χ
Examining interaction rules confirms |Ṅ0 | = |Ṅ00 |, and hence |C|~ ]| = |C0 [Ṅ00 , χ~ ]|.
By definition of search transitions, we have:˙ H~ p ] = C0 [Ṅ0 , H~ p ] → C0 [Ṅ 0 , H~ p ]C[0for each p ∈ {1, 2}.
The rest of the proof is to check that C0 [Ṅ00 , χ~ ] has a remote token, namely that, if its
token is a rewrite token, the token is not entering. This is done by inspecting interaction
rules.
• When the interaction rule Ṅ0 7→ Ṅ00 changes a value token to a rewrite token, thismust be the interaction rule (5a), which means Ṅ00 consists of the rewrite token andits outgoing operation edge. The operation edge remains to be a (unique) outgoingedge of the token in C0 [Ṅ00 , χ~ ], and hence the token is not entering in C0 [Ṅ00 , χ~ ].
• When the interaction rule Ṅ0 7→ Ṅ00 changes a search token to a rewrite token,
this must be the interaction rule (1a), (1b) or (5b), which means Ṅ00 = hṄ0 i /? .
˙ the token is also not entering in
Because the token is not entering in C0 [Ṅ0 , χ~ ] = C,0C0 [Ṅ0 , χ~ ] = hC0 [Ṅ0 , χ~ ]i /? .
Proposition 7.6. When the universal abstract machine U(O, BO ) is deterministic andrefocusing, it satisfies the following, for any set C ⊆ Hω (L, MO ∪ M) of contexts thatis closed under plugging, any reasonable triple (Q, Q0 , Q00 ), and any pre-template C on
focus-free hypernets Hω (L, MO \{?, X, }).
28

1. If C is a (C, Q, Q0 )-template and (C, Q, Q0 , Q00 )-robust relative to all rewrite transitions, then the C-contextual lifting CC is a (Q, Q0 , Q00 )-simulation.
2. If C is a (C, Q−1 , Q0 )-template and the converse C−1 is (C, Q, Q0 , Q00 )-robust relative
to all rewrite transitions, then the C-contextual lifting C−1(Q, Q0 , Q00 )-simulation.

Cof the converse is a˙ H~ 1 ; H~ 2 ) be an arbitrary C-specimen of C, such that the token of C˙
Proof prelude. Let (C;˙ H~ p ] is a rooted state for each p ∈ {1, 2}. By definition of contextual
is remote, and Ġp := C[C

lifting, Ġ1 CC Ġ2 , and equivalently, Ġ2 (CC )−1 Ġ1 . Note that C−1 = (CC )−1 .
˙ This implies
Because C is output-closed, by Lem. 7.5(2), the token is not exiting in C.
˙
that, if the token has an incoming edge in Ġ1 or Ġ2 , the incoming edge must be from C.
Because the machine is deterministic and refocusing, rooted states and transitions comprise a deterministic abstract rewriting system, in which final states and stuck states arenormal forms. By Lem. A.6, from any state, a sequence of transitions that result in a final
state or a stuck state is unique, if any.
Because (Q, Q0 , Q00 ) is a reasonable triple, Q0 and Q00 are reflexive. By Lem. A.22, this˙ Q0 and ˙ Q00 are reflexive, and hence CC ⊆ 
˙ Q0 ◦ CC ◦ 
˙ Q00 , and (CC )−1 ⊆implies that ˙ Q0 ◦ (CC )−1 ◦ 
˙ Q00 .

Proof of the point (1). Our goal is to check conditions (A) and (B) of Def. 7.1 for thestates Ġ1 CC Ġ2 .
If Ġ1 is final, by Lem. 7.5(1), Ġ2 is also final. The condition (A) of Def. 7.1 is fulfilled.
If there exists a state Ġ01 such that Ġ1 → Ġ01 , we show that one of the conditions (I)˙and (II) of Def. 7.1 is fulfilled, by case analysis of the token in C.
• When the token is a value token, or a search token that is not entering, by Lem. 7.5(3),˙ andthere exists a focussed context Ċ 0 with a remote token, such that |Ċ 0 | = |C|
p
0
p
˙
~
~
Ġp = C[H ] → Ċ [H ] for each p ∈ {1, 2}. We have the following situation, namely
the black part of the diagram below. Showing the magenta part confirms that thecondition (II) of Def. 7.1 is fulfilled.
˙ H~1 ]
G˙1 =C[
1Q1
CC
~
2
˙
˙
G2 =C[H ]/ C˙0 [H~1 ] = G˙0

1CC/ C˙0 [H~2 ]By the determinism, Ċ 0 [H~ 1 ] = Ġ01 . Because (Q, Q0 , Q00 ) is a reasonable triple, Q is˙ ∈ C, so (Ċ 0 ; H~ 1 ; H~ 2 ) is aa preorder and 1 Q 1. The context Ċ 0 satisfies |Ċ 0 | = |C|C-specimen of C. The context Ċ 0 has a remote token, and the states Ċ 0 [H~ 1 ] andĊ 0 [H~ 2 ] are both rooted. Therefore, we have Ċ 0 [H~ 1 ] CC Ċ 0 [H~ 2 ].
˙ because C is (C, Q, Q0 )-input• When the token is a search token that is entering in C,
safe, we have one of the following three situations corresponding to (I), (II) and (III)of Def. 6.9.
– There exist two stuck states Ṅ1 and Ṅ2 such that Ġp →∗ Ṅp for each p ∈ {1, 2}.
By the determinism of transitions, we have Ġ1 → Ġ01 →∗ Ṅ1 , which means thecondition (I) of Def. 7.1 is satisfied.
– There exist a C-specimen (Ċ 0 ; H~01 ; H~02 ) of C and two numbers k1 , k2 ∈ N, suchthat the token of Ċ 0 is not a rewrite token and not entering, (1 + k1 ) Q k2 ,29

˙ H~ 1 ] →1+k1 Ċ 0 [H~01 ], and C[
˙ H~ 2 ] →k2 Ċ 0 [H~02 ]. By the determinism of transitions,C[
we have the following situation, namely the black part of the diagram below.
Showing the magenta part confirms that the condition (II) of Def. 7.1 is fulfilled.
˙ H~1 ]
G˙1 =C[/ G˙0

k1/ C˙0 [H~01 ]CC˙
˙ H~2 ]
G2 =C[(1+k1 ) Q k2

CCk2
/ C˙0 [H~02 ]1

The context Ċ 0 has a remote token, and states Ċ 0 [H~01 ] and Ċ 0 [H~02 ] are rooted.
Therefore, Ċ 0 [H~01 ] CC Ċ 0 [H~02 ].

˙ Q0 , '˙ Q0 ), whose token is– There exist a quasi-C-specimen (Ṅ1 , Ṅ2 ) of C up to ('not a rewrite token, and two numbers k1 , k2 ∈ N, such that (1 + k1 ) Q (1 + k2 ),˙ H~ 1 ] →1+k1 Ṅ1 , and C[
˙ H~ 2 ] →1+k2 Ṅ2 . By the determinism of transitions,C[
we have the following situation, namely the black part of the diagram below.
Showing the magenta part confirms that the condition (II) of Def. 7.1 is fulfilled.
˙ H~1 ]
G˙1 =C[/ G˙0CC
˙ H~2 ]
˙
G2 =C[(1+k1 ) Q (1+k2 )

1

k1
/ N˙1
˙ 0 ◦CC ◦
˙ 00

Q
Q
1+k2
/ N˙2

˙ Q0 , '˙ Q0 ), and states Ṅ1
Because (Ṅ1 , Ṅ2 ) is a quasi-C-specimen of C up to ('~~and Ṅ2 are rooted, there exists a C-specimen (Ċ 0 ; H 01 ; H 02 ) of C with a non˙ Q0 Ċ 0 [H~01 ],rewrite token, such that Ċ 0 [H~01 ] and Ċ 0 [H~02 ] are also rooted, Ṅ1 '˙ Q0 Ṅ2 . Because (Q, Q0 , Q00 ) is a reasonable triple, Q0 ⊆ Q00 , andand Ċ 0 [H~02 ] '˙ Q0 ⊆ '˙ Q00 . Therefore, we have:hence '
˙ Q00 Ṅ2 .
˙ Q0 Ċ 0 [H~01 ] CC Ċ 0 [H~02 ] Ṅ1 • When the token is a rewrite token, Ġ1 → Ġ01 is a rewrite transition, and by definition
˙ Because C is (C, Q, Q0 , Q00 )of contextual lifting, the token is not entering in C.
robust relative to all rewrite transitions, and Ġ1 and Ġ2 are rooted, we have one of
the following two situations corresponding to (II) and (III) of Def. 6.12.
– There exists a stuck state Ṅ such that Ġ01 →∗ Ṅ . The condition (I) of Def. 7.1
is satisfied.
˙ Q0 , ˙ Q00 ), whose token– There exist a quasi-C-specimen (Ṅ1 , Ṅ2 ) of C up to (is not a rewrite token, and two numbers k1 , k2 ∈ N, such that (1 + k1 ) Q k2 ,Ġ01 →k1 Ṅ1 , and Ġ2 →k2 Ṅ2 . We have the following situation, namely theblack part of the diagram below. Showing the magenta part confirms that thecondition (II) of Def. 7.1 is fulfilled.
/ G˙0

˙ H~1 ]
G˙1 =C[1(1+k1 ) Q k2
CC
~
2
˙
˙
G2 =C[H ]k1/ N˙1
˙ 0 ◦CC ◦
˙ 00

Q
Q
k2
/ N˙2

˙ Q0 , ˙ Q00 ), and states Ṅ1
Because (Ṅ1 , Ṅ2 ) is a quasi-C-specimen of C up to (and Ṅ2 are rooted, there exists a C-specimen (Ċ 0 ; H~01 ; H~02 ) of C with a non˙ Q0 Ċ 0 [H~01 ],rewrite token, such that Ċ 0 [H~01 ] and Ċ 0 [H~02 ] are also rooted, Ṅ1 
˙ Q00 Ṅ2 . This means Ċ 0 [H~01 ] CC Ċ 0 [H~02 ], and hence:and Ċ 0 [H~02 ] ˙ Q0 Ċ 0 [H~01 ] CC Ċ 0 [H~02 ] ˙ Q00 Ṅ2 .
Ṅ1 
30

Proof of the point (2). It suffices to check the “reverse” of conditions (A) and (B) of
Def. 7.1 for the states Ġ2 (CC )−1 Ġ1 , namely the following conditions (A’) and (B’).
(A’) If Ġ2 is final, Ġ1 is also final.
(B’) If there exists a state Ġ02 such that Ġ2 → Ġ02 , one of the following (I’) and (II’)
holds.
(I’) There exists a stuck state Ġ002 such that Ġ02 →∗ Ġ002 .
˙ Q0 ◦ (CC )−1 ◦ 
˙ Q0 )(II’) There exist two states Ṅ2 and Ṅ1 , and numbers k2 , k1 ∈ N, such that Ṅ2 (kk
0Ṅ1 , (1 + k2 ) Q k1 , Ġ2 → 2 Ṅ2 , and Ġ1 → 1 Ṅ1 .
The proof is mostly symmetric to the point (1). Note that there is a one-to-one
correspondence between C-specimens of C and C-specimens of C−1 ; any C-specimen(C˙0 ; H~01 ; H~02 ) of C gives a C-specimen (C˙0 ; H~02 ; H~01 ) of C−1 . Because C is output-closed,
its converse C−1 is also output-closed.
If Ġ2 is final, by Lem. 7.5(1), Ġ1 is also final. The condition (A’) is fulfilled.
If there exists a state Ġ02 such that Ġ2 → Ġ02 , we show that one of the conditions (I’)˙
and (II’) above is fulfilled, by case analysis of the token in C.
• When the token is a value token, or a search token that is not entering, by Lem. 7.5(3),˙ andthere exists a focussed context Ċ 0 with a remote token, such that |Ċ 0 | = |C|˙ H~ p ] → Ċ 0 [H~ p ] for each p ∈ {1, 2}. We have the following situation, namelyĠp = C[the black part of the diagram below. Showing the magenta part confirms that thecondition (II’) is fulfilled.
˙/ C˙0 [H~2 ] = G˙0

˙ ~1 ]

G2 =C[H
C −1

2

1Q1
(C )
˙ H~1 ]
G˙1 =C[(CC )−1/ C˙0 [H~1 ]By the determinism, Ċ 0 [H~ 2 ] = Ġ02 . Because (Q, Q0 , Q00 ) is a reasonable triple, Q is˙ ∈ C, so (Ċ 0 ; H~ 2 ; H~ 1 ) is aa preorder and 1 Q 1. The context Ċ 0 satisfies |Ċ 0 | = |C|C-specimen of C−1 . The context Ċ 0 has a remote token, and the states Ċ 0 [H~ 1 ] andĊ 0 [H~ 2 ] are both rooted. Therefore, we have Ċ 0 [H~ 2 ] (CC )−1 Ċ 0 [H~ 1 ].
˙ because C is (C, Q−1 , Q0 )• When the token is a search token that is entering in C,
input-safe, we have one of the following three situations corresponding to (I), (II)and (III) of Def. 6.9.
– There exist two stuck states Ṅ1 and Ṅ2 such that Ġp →∗ Ṅp for each p ∈ {1, 2}.
By the determinism of transitions, we have Ġ2 → Ġ02 →∗ Ṅ2 , which means thecondition (I’) is satisfied.
– There exist a C-specimen (Ċ 0 ; H~01 ; H~02 ) of C and two numbers k1 , k2 ∈ N, suchthat the token of Ċ 0 is not a rewrite token and not entering, (1 + k1 ) Q−1 k2 ,˙ H~ 1 ] →1+k1 Ċ 0 [H~01 ], and C[
˙ H~ 2 ] →k2 Ċ 0 [H~02 ]. We have the following situation,
C[
namely the black part of the diagram below.
k2/

˙ H~2 ]
G˙2 =C[(CC )−1
˙ H~1 ]
G˙1 =C[

k2 Q (1+k1 )
1+k1

31

/

C˙0 [H~02 ](CC )−1C˙0 [H~01 ]The magenta part holds, because the token of Ċ 0 is not a rewrite token andnot entering, and because states Ċ 0 [H~01 ] and Ċ 0 [H~02 ] are rooted. We check thecondition (II’) by case analysis on the number k2 .
∗ When k2 > 0, by the determinism of transitions, we have the following
diagram, which means the condition (II’) is fulfilled.
k2 −1

/

/ G˙0

˙ H~2 ]
G˙2 =C[

2(CC )−1(CC )−1

k2 Q (1+k1 )1+k1/

˙ H~1 ]
G˙1 =C[C˙0 [H~02 ]C˙0 [H~01 ]˙ H~ 2 ] = Ċ 0 [H~02 ], and we have the following situation,∗ When k2 = 0, Ġ2 = C[namely the black part of the diagram below.
0/

˙ H~2 ]
G˙2 =C[
C −1

(C )

C −1

0 Q (1+k1 )

(C )
1+k1

/

˙ H~1 ]
G˙1 =C[/ G˙0 =C˙00 [H~01 ]G˙2 =C˙0 [H~02 ]C˙0 [H~01 ]2(CC )−1

1Q1/ C˙00 [H~01 ]Because Ġ2 → Ġ02 , and the token of Ċ 0 is a value token, or a non-entering
search token, by Lem. 7.5(3), there exists a focussed context C˙00 with a remote token, such that |C˙00 | = |Ċ 0 | and Ċ 0 [H~0p ] → C˙00 [H~0p ] for each p ∈ {1, 2}.
By the determinism of transitions, Ġ02 = C˙00 [H~01 ]. Because (Q, Q0 , Q00 ) isa reasonable triple, Q is a preorder and 1 Q 1. The context C˙00 satisfies|C˙00 | = |Ċ 0 | ∈ C, so (C˙00 ; H~02 ; H~01 ) is a C-specimen of C−1 . The context C˙00
has a remote token, and the states C˙00 [H~01 ] and C˙00 [H~02 ] are both rooted.
Therefore, we have C˙00 [H~02 ] (CC )−1 C˙00 [H~01 ]. Finally, because (Q, Q0 , Q00 ) isa reasonable triple, Q is closed under addition, and hence 1 Q (2 + k1 ). The
condition (II’) is fulfilled.

˙ Q0 , '˙ Q0 ), whose token is– There exist a quasi-C-specimen (Ṅ1 , Ṅ2 ) of C up to ('not a rewrite token, and two numbers k1 , k2 ∈ N, such that (1+k1 ) Q−1 (1+k2 ),˙ H~ 1 ] →1+k1 Ṅ1 , and C[
˙ H~ 2 ] →1+k2 Ṅ2 . By the determinism of transitions,C[
we have the following situation, namely the black part of the diagram below.
Showing the magenta part confirms that the condition (II’) is fulfilled.
˙ H~2 ]
G˙2 =C[(CC )−1
˙ H~1 ]
G˙1 =C[/ G˙0

2(1+k2 ) Q (1+k1 )

k2
/ N˙2
˙ 0 ◦(CC )−1 ◦
˙ 00

Q
Q
1+k1
/ N˙1

˙ Q0 , '˙ Q0 ), and states Ṅ1
Because (Ṅ1 , Ṅ2 ) is a quasi-C-specimen of C up to ('
~
~
0
01
02
and Ṅ2 are rooted, there exists a C-specimen (Ċ ; H ; H ) of C with a non˙ Q0 Ċ 0 [H~01 ],rewrite token, such that Ċ 0 [H~01 ] and Ċ 0 [H~02 ] are also rooted, Ṅ1 '˙ Q0 Ṅ2 . Because (Q, Q0 , Q00 ) is a reasonable triple, Q0 ⊆ Q00 , andand Ċ 0 [H~02 ] '˙ Q0 ⊆ '˙ Q00 . Therefore, we have:hence '
˙ Q0 Ċ 0 [H~02 ] (CC )−1 Ċ 0 [H~01 ] ˙ Q00 Ṅ1 .
Ṅ2 • When the token is a rewrite token, Ġ2 → Ġ02 is a rewrite transition, and by definition
˙ Because C−1 is (C, Q, Q0 , Q00 )of contextual lifting, the token is not entering in C.
robust relative to all rewrite transitions, and Ġ1 and Ġ2 are rooted, we have one of
the following two situations corresponding to (II) and (III) of Def. 6.12.
32

m

n

?

?
+

p

?

?
7!

?

?

?

Figure 8: Arithmetic rewrite rule (selected), where m, n, p ∈ N and p = m + n– There exists a stuck state Ṅ such that Ġ02 →∗ Ṅ . The condition (I’) is satisfied.
˙ Q0 , ˙ Q00 ), whose token– There exist a quasi-C-specimen (Ṅ2 , Ṅ1 ) of C−1 up to (is not a rewrite token, and two numbers k2 , k1 ∈ N, such that (1 + k2 ) Q k1 ,Ġ02 →k2 Ṅ2 , and Ġ1 →k1 Ṅ1 . We have the following situation, namely theblack part of the diagram below. Showing the magenta part confirms that thecondition (II’) is fulfilled.
/ G˙0

˙ H~2 ]
G˙2 =C[2(1+k2 ) Q k1
(CC )−1
˙ H~1 ]
G˙1 =C[k2/ N˙2
˙ 0 ◦(CC )−1 ◦
˙ 00

Q
Q
k1
/ N˙1

˙ Q0 , ˙ Q00 ), and states
Because (Ṅ2 , Ṅ1 ) is a quasi-C-specimen of C−1 up to (Ṅ2 and Ṅ1 are rooted, there exists a C-specimen (Ċ 0 ; H~02 ; H~01 ) of C−1 with a
˙ Q0 Ċ 0 [H~02 ],non-rewrite token, such that Ċ 0 [H~02 ] and Ċ 0 [H~01 ] are also rooted, Ṅ2 C
˙ 00 Ṅ1 . This means Ċ 0 [H~02 ] C−1 Ċ 0 [H~01 ], and hence:and Ċ 0 [H~01 ] Q˙ Q0 Ċ 0 [H~02 ] (CC )−1 Ċ 0 [H~01 ] ˙ Q00 Ṅ1 .
Ṅ2 

8. Applications of the characterisation theorem
This section shows applications of Thm. 6.14, with respect to an instantiation U(Oex , BOex )of the universal abstract machine. We start by defining the specific operation set Oex andits behaviour BOex in Sec. 8.1, which are informally introduced in Sec. 4.2, and proceed
to illustrate proofs of the observational equivalences listed in Sec. 4. Necessary templates
and their robustness are discussed in Sec. 8.2. Sec. 8.3 formally defines the notion ofobservational equivalence on terms, and describes how the templates can be combined toprove the observational equivalences. Finally, Sec. 8.4 and Sec. 8.5 give further details of
the reasoning about templates and their robustness.

8.1. Properties of compute transitions
ex we use here is given by passive operations Oex =The operation set Oex = Oex
X ] O
X
→

N∪{λ, tt, ff} and active operations Oex = {@, ref, =, :=, !, +, −, −1 }. The last three active
operations ‘+’, ‘−’ and ‘−1 ’ are addition, subtraction and negation of natural numbers,
respectively, and the other active operations are as discussed in Sec. 4.2.

33

`

`

`

⊗ /⌦Assoc ⊗`⊗ /⌦Comm ⊗

`

`

⊗

⊗

`
` ?⌦k ⇧⌦h?⌦k ⇧⌦h?⌦k ⇧⌦h⌦(n+k) ⌦h⌦(n+k) ⌦h?
⇧?
⇧⊗ /⌦Idem ⊗ H
0?⌦k ⇧⌦h⇧⇢id (G) /BPerm ⇧⇢?
G
id
GC D ? D ⇧
?
?
/
k,0
h,0
` `
?
T n (?)T n (?)C` ⊗ ⊗<latexit sha1_base64="KF+NWGrc7RCmz91JrPxwQQLfzlw=">AAACBHicbVDLSsNAFJ34rPUVddnNYBHqpiQi6LLgQpcV7AOaGCaTaTt0JhNmJkIJWbjxV9y4UMStH+HOv3HSZqGtBy4czrmXe+8JE0aVdpxva2V1bX1js7JV3d7Z3du3Dw67SqQSkw4WTMh+iBRhNCYdTTUj/UQSxENGeuHkqvB7D0QqKuI7PU2Iz9EopkOKkTZSYNe8Nr3PPDkWeZB5HOmx5BmN8rxxfRrYdafpzACXiVuSOijRDuwvLxI45STWmCGlBq6TaD9DUlPMSF71UkUShCdoRAaGxogT5WezJ3J4YpQIDoU0FWs4U39PZIgrNeWh6SzOVIteIf7nDVI9vPQzGiepJjGeLxqmDGoBi0RgRCXBmk0NQVhScyvEYyQR1ia3qgnBXXx5mXTPmq7TdG/P6y1YxlEBNXAMGsAFF6AFbkAbdAAGj+AZvII368l6sd6tj3nrilXOHIE/sD5/ABklmEA=</latexit><latexit sha1_base64="T157myBTo65GMqrL00/4OcfPSYo=">AAACAnicbVDLSsNAFJ34rPUVdSVuBovoqiQi6LLgxmUF+4Amhslk0g6dyYSZiVBCcOOvuHGhiFu/wp1/46TNQlsPXDiccy/33hOmjCrtON/W0vLK6tp6baO+ubW9s2vv7XeVyCQmHSyYkP0QKcJoQjqaakb6qSSIh4z0wvF16fceiFRUJHd6khKfo2FCY4qRNlJgH3ptep97ciROiyD3ONIjyXMaFUVgN5ymMwVcJG5FGqBCO7C/vEjgjJNEY4aUGrhOqv0cSU0xI0XdyxRJER6jIRkYmiBOlJ9PXyjgiVEiGAtpKtFwqv6eyBFXasJD01neqOa9UvzPG2Q6vvJzmqSZJgmeLYozBrWAZR4wopJgzSaGICypuRXiEZIIa5Na3YTgzr+8SLrnTddpurcXjRas4qiBI3AMzoALLkEL3IA26AAMHsEzeAVv1pP1Yr1bH7PWJauaOQB/YH3+AAp8l7s=</latexit>

`

` `

?⌦k

` `
`
`

` `

` `
G
?
T n (?)

`
`

⇧⌦h
⇧⌦h

?⌦k

⊗

⊗
?⌦(n+k)`⌦k/BPullC⌦h` ` ⇧` ` ⇧⌦hG?
T n (?)?
?⌦(n+k)

⌦h

` ⇧
`

⊗

0

`

⊗
?⌦k
⌦(n+k)?⌦(n+k) ⇧⌦h?
/BPullWG?
T n (?)G?
T n (?)⇧⌦h⇧⌦h⌦(h+h0 )0Figure 9: Structural pre-templates (C :  ⇒ ? is a contraction tree, H is a copyable
hypernet, G is a hypernet, (ρ, ρ0 ) is a box-permutation pair)
The behaviour BOex , namely compute transitions for the active operations Oex , are all
defined locally via rewrite rules; for function application in Fig. 4, reference manipulationin Fig. 5 and Fig. 6, and arithmetic in Fig. 8 (showing just addition, but other operators
can be similarly added). In these rules, the hypernet GS is additionally required to bestable.
Determinism and refocusing of the particular machine U(Oex , BOex ) boils down to determinism and preservation of the rooted property of compute transitions.
→

Compute transitions of operations {@, ref, +, −, −1 } are deterministic, because at mostone rewrite rule can be applied to each state. In particular, the stable hypernet GS in the
figures is uniquely determined (by Lem. A.15(3)).
As discussed in Sec. 5, copy transitions are all deterministic, because different contraction rules applied to a single state result in the same state. Compute transitions ofname-accessing operations {=, :=, !} are deterministic for the same reason.
Compute transitions of all the operations Oex are stationary, and hence they preserve
the rooted property. The stationary property can be checked using local rewrite rules.
Namely, in each rewrite rule Ḣ 7→ Ḣ 0 of the operations, only one input of |Ḣ| has type?, and Ḣ = ; |Ḣ| and Ḣ 0 = ?; |Ḣ 0 |. Moreover, any output of |Ḣ| with type ? is a targetof an atom edge or a box edge (by definition of stable hypernets), which implies |Ḣ| isone-way.
Because any initial state is rooted, given that all transitions preserve the rooted property,
we can safely assume that any state that arises in an execution is rooted. This means thatthe additional specification on stable hypernets in local rewrite rules is in fact guaranteed
to be satisfied in any execution (by Lem. A.10, Lem. A.20 and Lem. A.18).

8.2. Example templates
Now we enumerate pre-templates that we will use to prove the equivalences listed inSec. 4. We use the following auxiliary definition to specify one of these pre-templates(namely CBPerm in Fig. 9).
Definition 8.1 (Box-permutation pair). For any n, k, h ∈ N, let ρ and ρ0 be bijections
on sets {1, . . . , n + k + h} and {1, . . . , k + h}, respectively. These bijectons form a boxpermutation pair (ρ, ρ0 ) if, for each i ∈ {1, . . . , n + k + h}, the following holds:(A) ρ(i) = i if 1 ≤ i ≤ n,34

0?⌦(k+k ) 0 ⇧ 0?⌦k ⇧⌦hH?⌦k ⇧⌦h
?
H
?
? ⇧⌦h
?⌦k
?⌦(n+k) ? ⇧⌦h?⌦(n+k) ? ⇧⌦hGG/BPullD?
?
T n (?)T n (?)

(B) ρ(i) = ρ0 (i − n) if n < i ≤ n + k + h,(C) 1 ≤ ρ0 (i − n) ≤ k if n < i ≤ n + k,(D) k < ρ0 (i − n) ≤ k + h if n + k < i ≤ n + k + h.
The pre-templates we use are classified into three: structural pre-templates, operational
pre-templates, and name-exhaustive pre-templates. While the structural laws in Sec. 4.1
can be proved using only structural pre-templates, the beta laws and stateful laws in
Sec. 4.2 require operational and name-exhaustive pre-templates as well as structural pretemplates.
Fig. 9 shows all the structural pre-templates but the one derived from contraction rules:
namely, |Ġ1 | C⊗ |Ġ2 | whenever Ġ1 7→ Ġ2 is a contraction rule. The structural pretemplates primarily concern contraction edges, weakening edges and box edges. Contextual
equivalences implied by C⊗Assoc , C⊗Comm and C⊗Idem enable the so-called idempotent
completion (aka. Karoubi envelope or Cauchy completion) on contractions and weakenings.
This means that contraction trees with the same type can be identified, so long as they
contain at least one weakening edge.
We use two operational pre-templates, which are directly derived from some local rewrite→

rules of active operations. Namely, |Ġ1 | C @ |Ġ2 | if Ġ1 7→ Ġ2 is a beta rewrite rule (Fig. 4);
and |Ġ1 | Cref |Ġ2 | if Ġ1 7→ Ġ2 is a reference-creation rewrite rule (Fig. 5). Note that we
keep the additional specification that GS in these figures are stable hypernets.
Fig. 10 shows the last class of pre-templates, namely four name-exhaustive pre-templates.
They are specific to the four stateful laws in Conj. 4.4, and they analyse possible usagesof a single name of interest.
Output-closure of all the pre-templates can be easily checked, typically by spotting thatan input or an output, of type ?, is a source or a target of a contraction, atom or box edge.
Table. 1 outlines the way we will use Thm. 6.14 on all the pre-templates. For example,⊗
C is a (COex , ≥N , =N )-template, as shown in the “template” column, and both itself
and its converse are (COex , =N , =N , =N )-robust relative to all rewrite transitions, as shownin the “robustness” columns. Thanks to the monotonicity (Remark 6.15), we can use
Thm. 6.14(1) with a reasonable triple (≥N , =N , =N ), and Thm. 6.14(2) with a reasonable
C ex
C ex
triple (≤N , =N , =N ). Consequently, H1 C⊗ H2 implies H1 ≥ON H2 and H2 ≤ON H1 ,which is shown in the “implication of H1 C H2 ” column.
Pre-templates that relate hypernets with no input of type ? are trivially a (C, Q, Q0 )template for any C, Q and Q0 . The table uses ‘, , ’ to represent this situation.
For many pre-templates, a reasonable triple can be found by selecting “bigger” parameters from those of input-safety and robustness, thanks to the monotonicity. However,pre-templates CBPullD , CNE3 and CNE4 require non-trivial use of the monotonicity. For
each of these pre-templates, an upper row shows a parameter (C, Q1 , Q01 , Q001 ) that makesit (or its converse) robust, and a lower row shows a parameter (C, Q2 , Q02 , Q002 ) to which
Thm. 6.14 can be applied.
In the table, cyan symbols indicate where a proof of input-safety or robustness relies oncontextual refinement. The “dependency” column indicates which pre-templates can beused to prove the necessary contextual refinement, given that these pre-templates imply
contextual refinement as shown elsewhere in the table. This reliance specifically happensin finding a quasi-specimen, using contextual refinements/equivalences via Lem. 6.19. In
the case of C⊗ , its input-safety and robustness are proved under the assumption that
C ex
C⊗Assoc and C⊗Comm imply contextual equivalence '=ON .
The restriction to binding-free contexts plays a crucial role only in robustness regarding
35

()
⇧
D1,1

I
C

?⌦m
?
?

??
D1,1
m

?
⇥ ⊗

m1

m

=

⇥

<latexit sha1_base64="trrDvg31bl8xLZSC6wegx4xo65A=">AAAB/HicbVBNS8NAEN34WetXtEcvi0XwVBIR9Fjw4rGC/YA2hs120y7dzYbdiRBC/StePCji1R/izX/jts1BWx8MPN6bYWZelApuwPO+nbX1jc2t7cpOdXdv/+DQPTruGJVpytpUCaV7ETFM8IS1gYNgvVQzIiPButHkZuZ3H5k2XCX3kKcskGSU8JhTAlYK3drAANEPxUABl8xgGfrT0K17DW8OvEr8ktRRiVbofg2GimaSJUAFMabveykEBdHAqWDT6iAzLCV0Qkasb2lC7KagmB8/xWdWGeJYaVsJ4Ln6e6Ig0phcRrZTEhibZW8m/uf1M4ivg4InaQYsoYtFcSYwKDxLAg+5ZhREbgmhmttbMR0TTSjYvKo2BH/55VXSuWj4XsO/u6w3cRlHBZ2gU3SOfHSFmugWtVAbUZSjZ/SK3pwn58V5dz4WrWtOOVNDf+B8/gDM+JS9</latexit>

?
?

?

⇧
D1,1
/NE2

?

NE1

/

λ

?
?⌦m

?
?⌦m

⊗

k

-k

⇧
D1,1

⇧
D1,1

I

I

C

C

?⌦m1

;

I

λ

?⌦m1
?
? ??
D1,2
m1
⇥ ⊗

?

??
D1,2

<latexit sha1_base64="trrDvg31bl8xLZSC6wegx4xo65A=">AAAB/HicbVBNS8NAEN34WetXtEcvi0XwVBIR9Fjw4rGC/YA2hs120y7dzYbdiRBC/StePCji1R/izX/jts1BWx8MPN6bYWZelApuwPO+nbX1jc2t7cpOdXdv/+DQPTruGJVpytpUCaV7ETFM8IS1gYNgvVQzIiPButHkZuZ3H5k2XCX3kKcskGSU8JhTAlYK3drAANEPxUABl8xgGfrT0K17DW8OvEr8ktRRiVbofg2GimaSJUAFMabveykEBdHAqWDT6iAzLCV0Qkasb2lC7KagmB8/xWdWGeJYaVsJ4Ln6e6Ig0phcRrZTEhibZW8m/uf1M4ivg4InaQYsoYtFcSYwKDxLAg+5ZhREbgmhmttbMR0TTSjYvKo2BH/55VXSuWj4XsO/u6w3cRlHBZ2gU3SOfHSFmugWtVAbUZSjZ/SK3pwn58V5dz4WrWtOOVNDf+B8/gDM+JS9</latexit>!

1<latexit sha1_base64="37X0g/FJ6PBf627vONoXDb4BlL8=">AAAB/HicbVBNS8NAEN3Ur1q/oj16WSyCp5IUQY8FLx4r2A9oYthsN+3S3STsToQQ6l/x4kERr/4Qb/4bt20O2vpg4PHeDDPzwlRwDY7zbVU2Nre2d6q7tb39g8Mj+/ikp5NMUdaliUjUICSaCR6zLnAQbJAqRmQoWD+c3sz9/iNTmifxPeQp8yUZxzzilICRArvuaSDqofAS4JJpLIPWLLAbTtNZAK8TtyQNVKIT2F/eKKGZZDFQQbQeuk4KfkEUcCrYrOZlmqWETsmYDQ2NidnkF4vjZ/jcKCMcJcpUDHih/p4oiNQ6l6HplAQmetWbi/95wwyia7/gcZoBi+lyUZQJDAmeJ4FHXDEKIjeEUMXNrZhOiCIUTF41E4K7+vI66bWartN07y4bbVzGUUWn6AxdIBddoTa6RR3URRTl6Bm9ojfryXqx3q2PZWvFKmfq6A+szx/OfZS+</latexit>

+

?⌦m2
?
? ?

m2

⇥⊗ !
?

:=

?

<latexit sha1_base64="trrDvg31bl8xLZSC6wegx4xo65A=">AAAB/HicbVBNS8NAEN34WetXtEcvi0XwVBIR9Fjw4rGC/YA2hs120y7dzYbdiRBC/StePCji1R/izX/jts1BWx8MPN6bYWZelApuwPO+nbX1jc2t7cpOdXdv/+DQPTruGJVpytpUCaV7ETFM8IS1gYNgvVQzIiPButHkZuZ3H5k2XCX3kKcskGSU8JhTAlYK3drAANEPxUABl8xgGfrT0K17DW8OvEr8ktRRiVbofg2GimaSJUAFMabveykEBdHAqWDT6iAzLCV0Qkasb2lC7KagmB8/xWdWGeJYaVsJ4Ln6e6Ig0phcRrZTEhibZW8m/uf1M4ivg4InaQYsoYtFcSYwKDxLAg+5ZhREbgmhmttbMR0TTSjYvKo2BH/55VXSuWj4XsO/u6w3cRlHBZ2gU3SOfHSFmugWtVAbUZSjZ/SK3pwn58V5dz4WrWtOOVNDf+B8/gDM+JS9</latexit>

⊗

ff

⇥

()

<latexit sha1_base64="37X0g/FJ6PBf627vONoXDb4BlL8=">AAAB/HicbVBNS8NAEN3Ur1q/oj16WSyCp5IUQY8FLx4r2A9oYthsN+3S3STsToQQ6l/x4kERr/4Qb/4bt20O2vpg4PHeDDPzwlRwDY7zbVU2Nre2d6q7tb39g8Mj+/ikp5NMUdaliUjUICSaCR6zLnAQbJAqRmQoWD+c3sz9/iNTmifxPeQp8yUZxzzilICRArvuaSDqofAS4JJpLIPWLLAbTtNZAK8TtyQNVKIT2F/eKKGZZDFQQbQeuk4KfkEUcCrYrOZlmqWETsmYDQ2NidnkF4vjZ/jcKCMcJcpUDHih/p4oiNQ6l6HplAQmetWbi/95wwyia7/gcZoBi+lyUZQJDAmeJ4FHXDEKIjeEUMXNrZhOiCIUTF41E4K7+vI66bWartN07y4bbVzGUUWn6AxdIBddoTa6RR3URRTl6Bm9ojfryXqx3q2PZWvFKmfq6A+szx/OfZS+</latexit>

!

?⌦m2
?
? ?

m2

⇥⊗ !

1
-

/NE3

-

:=

?

?

λ

λ

λ

λ

?

?

?

?

?⌦m1

<latexit sha1_base64="37X0g/FJ6PBf627vONoXDb4BlL8=">AAAB/HicbVBNS8NAEN3Ur1q/oj16WSyCp5IUQY8FLx4r2A9oYthsN+3S3STsToQQ6l/x4kERr/4Qb/4bt20O2vpg4PHeDDPzwlRwDY7zbVU2Nre2d6q7tb39g8Mj+/ikp5NMUdaliUjUICSaCR6zLnAQbJAqRmQoWD+c3sz9/iNTmifxPeQp8yUZxzzilICRArvuaSDqofAS4JJpLIPWLLAbTtNZAK8TtyQNVKIT2F/eKKGZZDFQQbQeuk4KfkEUcCrYrOZlmqWETsmYDQ2NidnkF4vjZ/jcKCMcJcpUDHih/p4oiNQ6l6HplAQmetWbi/95wwyia7/gcZoBi+lyUZQJDAmeJ4FHXDEKIjeEUMXNrZhOiCIUTF41E4K7+vI66bWartN07y4bbVzGUUWn6AxdIBddoTa6RR3URRTl6Bm9ojfryXqx3q2PZWvFKmfq6A+szx/OfZS+</latexit>?⌦m2<latexit sha1_base64="trrDvg31bl8xLZSC6wegx4xo65A=">AAAB/HicbVBNS8NAEN34WetXtEcvi0XwVBIR9Fjw4rGC/YA2hs120y7dzYbdiRBC/StePCji1R/izX/jts1BWx8MPN6bYWZelApuwPO+nbX1jc2t7cpOdXdv/+DQPTruGJVpytpUCaV7ETFM8IS1gYNgvVQzIiPButHkZuZ3H5k2XCX3kKcskGSU8JhTAlYK3drAANEPxUABl8xgGfrT0K17DW8OvEr8ktRRiVbofg2GimaSJUAFMabveykEBdHAqWDT6iAzLCV0Qkasb2lC7KagmB8/xWdWGeJYaVsJ4Ln6e6Ig0phcRrZTEhibZW8m/uf1M4ivg4InaQYsoYtFcSYwKDxLAg+5ZhREbgmhmttbMR0TTSjYvKo2BH/55VXSuWj4XsO/u6w3cRlHBZ2gU3SOfHSFmugWtVAbUZSjZ/SK3pwn58V5dz4WrWtOOVNDf+B8/gDM+JS9</latexit>?⌦m1<latexit sha1_base64="37X0g/FJ6PBf627vONoXDb4BlL8=">AAAB/HicbVBNS8NAEN3Ur1q/oj16WSyCp5IUQY8FLx4r2A9oYthsN+3S3STsToQQ6l/x4kERr/4Qb/4bt20O2vpg4PHeDDPzwlRwDY7zbVU2Nre2d6q7tb39g8Mj+/ikp5NMUdaliUjUICSaCR6zLnAQbJAqRmQoWD+c3sz9/iNTmifxPeQp8yUZxzzilICRArvuaSDqofAS4JJpLIPWLLAbTtNZAK8TtyQNVKIT2F/eKKGZZDFQQbQeuk4KfkEUcCrYrOZlmqWETsmYDQ2NidnkF4vjZ/jcKCMcJcpUDHih/p4oiNQ6l6HplAQmetWbi/95wwyia7/gcZoBi+lyUZQJDAmeJ4FHXDEKIjeEUMXNrZhOiCIUTF41E4K7+vI66bWartN07y4bbVzGUUWn6AxdIBddoTa6RR3URRTl6Bm9ojfryXqx3q2PZWvFKmfq6A+szx/OfZS+</latexit>

?⌦m2

1
⇧
D1,1

I
C

?⌦m1
?
?? ?
D1,1
<latexit sha1_base64="trrDvg31bl8xLZSC6wegx4xo65A=">AAAB/HicbVBNS8NAEN34WetXtEcvi0XwVBIR9Fjw4rGC/YA2hs120y7dzYbdiRBC/StePCji1R/izX/jts1BWx8MPN6bYWZelApuwPO+nbX1jc2t7cpOdXdv/+DQPTruGJVpytpUCaV7ETFM8IS1gYNgvVQzIiPButHkZuZ3H5k2XCX3kKcskGSU8JhTAlYK3drAANEPxUABl8xgGfrT0K17DW8OvEr8ktRRiVbofg2GimaSJUAFMabveykEBdHAqWDT6iAzLCV0Qkasb2lC7KagmB8/xWdWGeJYaVsJ4Ln6e6Ig0phcRrZTEhibZW8m/uf1M4ivg4InaQYsoYtFcSYwKDxLAg+5ZhREbgmhmttbMR0TTSjYvKo2BH/55VXSuWj4XsO/u6w3cRlHBZ2gU3SOfHSFmugWtVAbUZSjZ/SK3pwn58V5dz4WrWtOOVNDf+B8/gDM+JS9</latexit><latexit sha1_base64="37X0g/FJ6PBf627vONoXDb4BlL8=">AAAB/HicbVBNS8NAEN3Ur1q/oj16WSyCp5IUQY8FLx4r2A9oYthsN+3S3STsToQQ6l/x4kERr/4Qb/4bt20O2vpg4PHeDDPzwlRwDY7zbVU2Nre2d6q7tb39g8Mj+/ikp5NMUdaliUjUICSaCR6zLnAQbJAqRmQoWD+c3sz9/iNTmifxPeQp8yUZxzzilICRArvuaSDqofAS4JJpLIPWLLAbTtNZAK8TtyQNVKIT2F/eKKGZZDFQQbQeuk4KfkEUcCrYrOZlmqWETsmYDQ2NidnkF4vjZ/jcKCMcJcpUDHih/p4oiNQ6l6HplAQmetWbi/95wwyia7/gcZoBi+lyUZQJDAmeJ4FHXDEKIjeEUMXNrZhOiCIUTF41E4K7+vI66bWartN07y4bbVzGUUWn6AxdIBddoTa6RR3URRTl6Bm9ojfryXqx3q2PZWvFKmfq6A+szx/OfZS+</latexit>

? ?
m1

⇥

??
D1,1

?⌦m2
?
? ?

?
m1

m2

⊗ !

()

?

?

@
λ

@

λ

?

?

λ

<latexit sha1_base64="trrDvg31bl8xLZSC6wegx4xo65A=">AAAB/HicbVBNS8NAEN34WetXtEcvi0XwVBIR9Fjw4rGC/YA2hs120y7dzYbdiRBC/StePCji1R/izX/jts1BWx8MPN6bYWZelApuwPO+nbX1jc2t7cpOdXdv/+DQPTruGJVpytpUCaV7ETFM8IS1gYNgvVQzIiPButHkZuZ3H5k2XCX3kKcskGSU8JhTAlYK3drAANEPxUABl8xgGfrT0K17DW8OvEr8ktRRiVbofg2GimaSJUAFMabveykEBdHAqWDT6iAzLCV0Qkasb2lC7KagmB8/xWdWGeJYaVsJ4Ln6e6Ig0phcRrZTEhibZW8m/uf1M4ivg4InaQYsoYtFcSYwKDxLAg+5ZhREbgmhmttbMR0TTSjYvKo2BH/55VXSuWj4XsO/u6w3cRlHBZ2gU3SOfHSFmugWtVAbUZSjZ/SK3pwn58V5dz4WrWtOOVNDf+B8/gDM+JS9</latexit>⇥⊗ !

<latexit sha1_base64="37X0g/FJ6PBf627vONoXDb4BlL8=">AAAB/HicbVBNS8NAEN3Ur1q/oj16WSyCp5IUQY8FLx4r2A9oYthsN+3S3STsToQQ6l/x4kERr/4Qb/4bt20O2vpg4PHeDDPzwlRwDY7zbVU2Nre2d6q7tb39g8Mj+/ikp5NMUdaliUjUICSaCR6zLnAQbJAqRmQoWD+c3sz9/iNTmifxPeQp8yUZxzzilICRArvuaSDqofAS4JJpLIPWLLAbTtNZAK8TtyQNVKIT2F/eKKGZZDFQQbQeuk4KfkEUcCrYrOZlmqWETsmYDQ2NidnkF4vjZ/jcKCMcJcpUDHih/p4oiNQ6l6HplAQmetWbi/95wwyia7/gcZoBi+lyUZQJDAmeJ4FHXDEKIjeEUMXNrZhOiCIUTF41E4K7+vI66bWartN07y4bbVzGUUWn6AxdIBddoTa6RR3URRTl6Bm9ojfryXqx3q2PZWvFKmfq6A+szx/OfZS+</latexit>

/NE4

⇥

?
m2

⊗1

()

?

@
λ

?⌦m2

@

λ

?

?

λ

?
?⌦m1

<latexit sha1_base64="trrDvg31bl8xLZSC6wegx4xo65A=">AAAB/HicbVBNS8NAEN34WetXtEcvi0XwVBIR9Fjw4rGC/YA2hs120y7dzYbdiRBC/StePCji1R/izX/jts1BWx8MPN6bYWZelApuwPO+nbX1jc2t7cpOdXdv/+DQPTruGJVpytpUCaV7ETFM8IS1gYNgvVQzIiPButHkZuZ3H5k2XCX3kKcskGSU8JhTAlYK3drAANEPxUABl8xgGfrT0K17DW8OvEr8ktRRiVbofg2GimaSJUAFMabveykEBdHAqWDT6iAzLCV0Qkasb2lC7KagmB8/xWdWGeJYaVsJ4Ln6e6Ig0phcRrZTEhibZW8m/uf1M4ivg4InaQYsoYtFcSYwKDxLAg+5ZhREbgmhmttbMR0TTSjYvKo2BH/55VXSuWj4XsO/u6w3cRlHBZ2gU3SOfHSFmugWtVAbUZSjZ/SK3pwn58V5dz4WrWtOOVNDf+B8/gDM+JS9</latexit>⇥⊗ 1?

<latexit sha1_base64="37X0g/FJ6PBf627vONoXDb4BlL8=">AAAB/HicbVBNS8NAEN3Ur1q/oj16WSyCp5IUQY8FLx4r2A9oYthsN+3S3STsToQQ6l/x4kERr/4Qb/4bt20O2vpg4PHeDDPzwlRwDY7zbVU2Nre2d6q7tb39g8Mj+/ikp5NMUdaliUjUICSaCR6zLnAQbJAqRmQoWD+c3sz9/iNTmifxPeQp8yUZxzzilICRArvuaSDqofAS4JJpLIPWLLAbTtNZAK8TtyQNVKIT2F/eKKGZZDFQQbQeuk4KfkEUcCrYrOZlmqWETsmYDQ2NidnkF4vjZ/jcKCMcJcpUDHih/p4oiNQ6l6HplAQmetWbi/95wwyia7/gcZoBi+lyUZQJDAmeJ4FHXDEKIjeEUMXNrZhOiCIUTF41E4K7+vI66bWartN07y4bbVzGUUWn6AxdIBddoTa6RR3URRTl6Bm9ojfryXqx3q2PZWvFKmfq6A+szx/OfZS+</latexit>

?⌦m2

?
?⌦m1

Figure 10: Name-exhaustive pre-templates (C is a contraction tree)36template

C⊗Assoc

robustness(input-safety)of C

of C−1

dependency

implication of H1 C H2

COex , =, =COex , =, =, =COex , =, =, =—H1 '=ON

C ex

H2COex , =, =COex , =, =, =COex , =, =, =—C ex
H1 '=ON H2⊗Idem

, , COex , =, =, =COex , =, =, =—H1 '=ONC⊗

COex , ≥, =COex , =, =, =COex , =, =, =C⊗CommC

C⊗Assoc
C

⊗Comm

C ex

C ex

H1 ≥O

N

H2
H2 ,

C ex

H2 ≤O

H1

N

CGC

, , COex , =, =, =COex , =, =, =—C ex
H1 '=ON H2

CBPerm, , COex , =, =, =COex , =, =, =—H1 '=ON

C ex

H2

C

⊗Assoc

CBPullC, , COex , =, =, =COex , =, =, =C⊗CommC ex

H1 '=ON

H2

C⊗Idem
CBPullW, , COex , =, =, =COex , =, =, =C⊗IdemC⊗Assoc

CBPullD, , COex , =, =, ≤COex , =, ≥, =

C

⊗Comm

C ex

H1 '=ONC ex

H1 ≤ON

H2
H2 ,C⊗IdemCOex , ≤, =, ≤C⊗

COex , ≥, ≥, ≥C ex

H2 ≥O

N

H1

CGC
→

C@

COex , ≥, =COex -bf , =, =, =C ex -bf

COex -bf , =, =, =—COex -bf , ≥, =Cref

COex , ≥, =COex -bf , =, =, =H1 ≥ON

C ex -bf

COex -bf , =, =, =—COex -bf , ≥, =

H2 ,

C ex
H2 ≤O -bf H1N

H1 ≥O

N

H2 ,

C ex
H2 ≤O -bf H1
NC⊗Assoc
CNE1

COex , =, =COex , ≥, =, =—C⊗IdemC ex

H1 ≥O

N

H2

CGC
CNE2

, , COex , =, =, =—COex , =, =, =C

⊗Assoc

CNE3

CNE4

COex , =, =COex , =, =COex , ≤, ≥, ≤COex , ≥, ≥, ≤COex , N × N, ≥, N × N

COex , N × N, ≥, N × N

COex , ≥, ≥, =COex , ≤, =, ≤

C

⊗Idem

H2

C ex

O
H1 'N×N
H2

C⊗
CGC
C⊗Assoc
C

⊗Idem

C⊗

COex , ≥, ≥, ≥C ex

H1 '=ONCGC

C ex

H1 ≥ONC ex

H2 ≤ON

H2

H1

Table 1: Templates, with their robustness and implied contextual refinements/equivalences( denotes anything)37→

the operational pre-templates C @ and Cref . In fact, these pre-templates are input-safewith respect to both COex and COex -bf . This gap reflects duplication behaviour on atomedges, which is only encountered in a proof of robustness. A shallow atom edge is never
duplicated, whereas a deep one can be duplicated as a part of a box (which represents athunk).
Finally, the pre-template CNE1 is the only example whose converse is not robust. Thisis because the equality operation ‘=’ is only defined on names, whereas it is possible in
Spartan to give values, other than names, as arguments of the equality operation.
The key part of proving input-safety or robustness of a pre-template is to analyse how
a rewrite transition involves edges (at any depth) of a state that are contributed by the
pre-template. Given that all rewrite transitions (including copy transitions) are specified
by local rewrite rules, the analysis boils down to check possible overlaps between a local
rule and the pre-template. A typical situation is where a local rule simply preserves
or duplicates edges contributed by a pre-template, without breaking them. Lem. 8.3 inSec. 8.4 identifies two such situations: when the overlaps are all about deep edges, andwhen the pre-template relates contraction trees only.

8.3. Observational equivalences on terms
The notion of observational refinement on terms, informally introduced in Sec. 4, can now
be defined using the contextual refinement on hypernets as follows. Let (X, Y ) be a pair(all, O) or (bf, O-bf) of annotations. Given two derivable judgements ~x | ~a ` t1 : ? and~x | ~a ` t2 : ?, we write BO |= (~x | ~a ` t1 †X t2 : ?) (resp. BO |= (~x | ~a ` t1 '†X t2 : ?)) ifYYBO |= ((~x | ~a ` t1 : τ )† C
x | ~a ` t2 : τ )† ) (resp. BO |= ((~x | ~a ` t1 : τ )† 'C
x | ~a `N×N (~
N×N (~†
t2 : τ ) )).
The refinements †all and †bf enjoy different congruence results, which can be describedin terms of syntactical contexts. Let term-contexts and their binding-free restriction be
defined by the following grammar:
C ::= [ ] | new a ( t in C | bind x → t in C
| new a ( C in t | bind x → C in t
| ~y .C | φ(~t, C, ~t0 ; ~s)(term-contexts)

C̃ ::= [ ] | new a ( t in C̃ | bind x → t in C̃| ~y .C̃ | φ(~t, C̃, ~t0 ; ~s)(binding-free term-contexts)
The type system of Spartan (Fig. 1) can be extended to term-contexts, by annotating
the hole ‘[ ]’ as ‘[ ]~x|~a ’ and adding a typing rule ~x | ~a ` [ ]~x|~a : ?. We write C[ ]~x|~a when thehole of C is annotated with ~x | ~a.
Lemma 8.2. Let ~x | ~a ` t1 : ? and ~x | ~a ` t2 : ? be derivable judgements. Let C bea term-context, x~0 be a sequence of variables and a~0 be a sequence of atoms, such thatx~0 | a~0 ` C[ ]~x|~a : ?.
1. If ~x | ~a ` t1 †all t2 : ?, then x~0 | a~0 ` C[t1 ] †all C[t2 ] : ?.
2. If ~x | ~a ` t1 '†all t2 : ?, then x~0 | a~0 ` C[t1 ] '†all C[t2 ] : ?.
3. If ~x | ~a ` t1 †bf t2 : ?, and C is binding-free, then x~0 | a~0 ` C[t1 ] †bf C[t2 ] : ?.
4. If ~x | ~a ` t1 '†bf t2 : ?, and C is binding-free, then x~0 | a~0 ` C[t1 ] '†bf C[t2 ] : ?.
38

→
⊗

Weakening
Exchange
Struct. (1) (2)Struct. (3) (4)Aux. Copy
Aux. Subst.
Struct. (5)Struct. (6)

Assoc

◦
◦
◦
•
◦
◦

Comm

◦
◦
◦
•
◦
◦

⊗

Idem
◦

◦, (W)◦, (W)◦•◦, (W)◦, (W)

⊗

GC

◦
◦
◦
◦

◦
◦
◦
◦

BPerm

BPullC

◦
(Ex)
◦
•
◦
◦

◦
•
◦
◦

◦

Micro beta
Freshness
Locality
Param. 1
Param. 2⊗

BPullW◦

BPullD

•
•

ref

NEi

◦
◦
◦
◦

1
2
3
4

(W)
(W)

◦

◦

◦, (Ex)◦◦(W)◦, (W)◦◦◦(Ex)◦, (W)◦, (W)◦, (W)◦, (W)

@

•

◦

◦

•
•

◦
◦

◦
◦

◦, (W)(W)◦, (W)◦, (W)◦◦◦◦

Table 2: Dependency of contextual refinements/equivalences on templates
Proof outline. The translation (−)† of Spartan terms to hypernets (Fig. 2) can be extended to term-contexts, by translating the rule ~x | ~a ` [ ]~x|~a : ? into a path hypernetχ : ? ⇒ ?⊗|~x| ⊗ ⊗|~a| . Translating term-contexts indeed yields (graphical) contexts, andtranslating binding-free term-contexts yields (graphical) binding-free contexts (proof by
induction on (binding-free) term-contexts).
For each i ∈ {1, 2}, a judgement x~0 | a~0 ` C[ti ] : ? is derivable, and moreover,(x~0 | a~0 ` C[ti ] : ?)† = (x~0 | a~0 ` C[ ]~x|~a : ?)† [(~x | ~a ` ti : ?)† ](proof by induction on C). The congruence property of contextual refinements concludes
the proof.
Each law in Sec. 4 can be proved for the operation sets Oex
X = N ∪ {λ, tt, ff} and→Oex = {@, ref, =, :=, !, +, −, −1 },by combining the pre-templates. The assumption here is that the pre-templates imply
contextual refinement as listed in Table 1. We describe below how each law depends on
pre-templates, using Table 2. The (full) Beta law is simply the combination of the Micro
Beta law and the substitution law (6), so it is omitted in the table.
Some rows of the table (namely: Weakening, Exchange, Auxiliary Copy and Auxiliary
Substitution) represent auxiliary laws shown in Fig. 11. When a law can be proved using
the Weakening or Exchange law, it is indicated by (W) or (E), respectively, in the table.
The Auxiliary Copy law is used to prove both the Structural laws (5) and (6), while the
Auxiliary Substitution law is used to prove the Structural law (6).
The symbol ‘◦’ indicates direct dependency on pre-templates, in the sense that a law
can be proved by combining contextual refinements implied by these pre-templates. For
these pre-templates to imply contextual refinements, some other pre-templates may needto imply contextual refinements; these other pre-templates are indirectly depended by thelaw. The indirect dependency is indicated by the symbol ‘•’.
Thanks to the Weakening law, it suffices to check the minimum judgement to prove
an observational equivalence. This is the case for binding-free contexts, too, because any
context that consists of a hole with no target, and weakening edges, is binding-free. For
example, Fig. 12 illustrates a proof of the Parametricity 2 law in the empty environment(− | − `  : ?), and this proof is enough to show the law in any environment (~x | ~a `  : ?).
39

?
?⌦k1 ? ?⌦k2 ⇧⌦h(~x, z, ~y | ~a ` t : ⌧ )†⌧?⌦k1 ⊗ ?⌦k2 ⇧⌦h(~x, ~y | ~a ` t : ⌧ )†
⌧
⇧

'Call
=N

?⌦k ⇧⌦h1 ⇧ ⇧⌦h2(~x | ~a, b, ~c ` t : ⌧ )†⌧?⌦k ⇧⌦h1 ⊗ ⇧⌦h2(~x | ~a, ~c ` t : ⌧ )†
⌧

'Call
=N

(a) Weakening (z ∈/ fv (t), b ∈/ fa(t))
??
⌦k

⌦k

h

? 1 ??? 2 ⇧?⌦k1 ? ? ?⌦k2 ⇧h(~x, z, z 0 , ~y | ~a ` t : ⌧ )† 'Callx, z 0 , z, ~y | ~a ` t : ⌧ )†
=N (~
⌧
⌧
⇧⇧
?⌦k ⇧⌦h1 ⇧ ⇧ ⇧h2?⌦k ⇧⌦h1 ⇧ ⇧ ⇧h2
Call(~x | ~a, c, c0 , ~b ` t : ⌧ )† '=N (~x | ~a, c0 , c, ~b ` t : ⌧ )†⌧⌧(b) Exchange
?⌦k
?
Dk,n

?⌦k ⇧⌦h(~x | ~a ` t : ?)†
?
D1,n

?⌦n

'Call
=N⇥N

⇧⌦h
⇧
Dh,n

⇥n (~x | ~a ` t : ?)†?⌦n(c) Auxiliary Copy (t is referentiallytransparent)?⌦k1 ?⌦k ?⌦k2 ⇧⌦h ⇧⌦h1<latexit sha1_base64="yDSn3JKKKDVSIW8ZYCB1lL0jdCs=">AAACVHicbZFLSwMxFIUzU6u1vqou3QSLUBHKTBF0WXDjsoJ9QFuHTCZtw2SSIbkjlKE/UheCv8SNC9MHqG0vBA7fuZebnISp4AY879NxCzvF3b3Sfvng8Oj4pHJ61jEq05S1qRJK90JimOCStYGDYL1UM5KEgnXD+GHud1+ZNlzJZ5imbJiQseQjTglYFFTigQGiX/KBAp4wg2sS3+A48K9n5TUn3iRBw7KIk0TJ6BdPtsLAnwWVqlf3FoU3hb8SVbSqVlB5H0SKZgmTQAUxpu97KQxzooFTweyazLCU0JiMWd9KSeymYb4IZYavLInwSGl7JOAF/TuRk8SYaRLazoTAxKx7c7jN62cwuh/mXKYZMEmXi0aZwKDwPGEccc0oiKkVhGpu74rphGhCwf5D2Ybgrz95U3Qadd+r+0+31SZexVFCF+gS1ZCP7lATPaIWaiOK3tCXgxzH+XC+3YJbXLa6zmrmHP0r9/gH0rezcQ==</latexit>?⌦k ⇧⌦h(~x | ~a ` t : ?)†?

?⌦k1 ?⌦k ?⌦k2 ⇧⌦h ⇧⌦h1?⌦(n+k1 ) ?⌦k ?⌦k2 ⇧⌦h ⇧⌦h1?⌦k1 ? ?⌦k2 ⇧⌦h1?
? ?⌦k2 ⇧⌦h1 Call
G
'=N⇥N
?
T n (?)⌦(n+k1 )?⌦k ⇧⌦h(~x | ~a ` t : ?)†?
?⌦(n+k1 ) ? ?⌦k2 ⇧⌦h1G?
T n (?)(d) Auxiliary Substitution (t referentially transparent)

Figure 11: Auxiliary laws40

~ @()))~~(− | − ` (λx.λf.(λz.!x)@(f@(ref1) : ?)† =
??
D1,1
??
?
D2,2
?
D2,1

??
D1,1
?
D2,2

??
D1,1

? ?? ?
D3,1
?
D1,1

?
?
⊗ D2,0
D1,1

⊗⊗ !
?

()

λ

@
@

?
λ

'Call 1/⌦Assoc
B /⌦Comm C
BC
B /⌦Idem C
B ⌦BParam C
B /C
B ⌦BPullC C@ /A/BPullW

?

?

⊗

!

0

??
D1,1

?

??
D1,1

?

'Cbf
/ref

()

λ

?

?

⊗

!
()
@

@

@

?

?

λ

?

?
λ

@

1

?

λ

1

?
ref

λ

1

⇧
D1,1

?
ref

λ

λ

I

@

@

@

?

?

?

1

⇧
D1,1

I

??
D1,1
Cbf

⇣' ! ⌘
/@

??
D1,1

??
D1,2

?

?
?
D1,1

'Call
(/NE4 )

'Call 1/⌦Assoc
B /⌦Comm C
B ⌦Idem C@ /A/BPullW0<latexit sha1_base64="d4WmaNS9XS1QXN6iYX15izckke8=">AAAChHicbVFdixMxFM2MuruOX1UffQkWcQUpM7qiT1LYFx9XsLsLnVqS9M40bD7G5I5SwvwS/5Vv/hsz7Qjr1guBwzn3npuc8EZJj3n+O0lv3b5zcHh0N7t3/8HDR6PHT869bZ2AmbDKukvOPChpYIYSFVw2DpjmCi741WmvX3wH56U1X3DTwEKz2shKCoaRWo5+lhxqaQJzjm26ILqs9FLDt6+h1AzXnNPTLXA68KqLapmVCio8zvYH0UlmagW9HudtvxcwlE7Wa4x99kcX/ppNu94MzGowyHZdr65zy9E4n+TbovugGMCYDHW2HP0qV1a0GgwKxbyfF3mDi+iGUiiIO1oPDRNXrIZ5hIZp8IuwDbGjLyKzopV18RikW/b6RGDa+43msbN/g7+p9eT/tHmL1YdFkKZpEYzYLapaRdHS/kfoSjoQqDYRMOFkvCsVa+aYwJhfFkMobj55H5y/mRT5pPh8Mp7SIY4j8ow8J8ekIO/JlHwiZ2RGRJIkL5M8KdKD9HX6Nn23a02TYeYp+afSj38ALtPG4A==</latexit>

?

?

?

⊗

!

⊗ 1

?

()

λ

@
@

?

?

()

λ

@

?
D1,1
?
D1,2

??
?
D2,0
1

?
D1,1

?
D1,0

?

()

λ

@

@

@

?

?

λ

λ

λ

?

?

?

~ @())~= (− | − ` λf.(λz.1)@(f: ?)† .
Figure 12: A proof outline of the Parametricity 2 law, in the empty environment

41

8.4. Local reasoning
For the particular operation set Oex , the following lemma identifies two typical situations,where a local rule simply preserves or duplicates edges contributed by a pre-template,
without breaking them.
Lemma 8.3. Assume any C-specimen of an output-closed pre-template C that has theform~0 , C˙2 [χ~00 ]]; G~ 0 , G~00 ; H~ 0 , H~ 00 ),(C1 [χ
~ 0 , C˙2 [G~00 ]] and C1 [H~ 0 , C˙2 [H~ 00 ]] are states, andand any focussed hypernet Ṅ , such that C1 [G00
C˙2 [G~ ] 7→ Ṅ is a contraction rule or a local rewrite rule of an operation of Oex =→{@, ref, =, :=, !, +, −, −1 }.

1. If all holes of C˙2 are deep, then there exist a focussed context C˙20 and two sequences G~000
and H~000 of focus-free hypernets, such that C˙2 [G~00 ] 7→ C˙20 [G~000 ] = Ṅ , C˙2 [H~ 00 ] 7→ C˙20 [H~000 ],000
and G000i C Hi for each index i.

~ 0 , C˙2 [G~00 ]] and C1 [H~ 0 , C˙2 [H~ 00 ]] are
2. In the situation of (1), if additionally both states C1 [G~0 , C˙0 [χ~000 ]]|~0 , C˙2 [χ~00 ]]| is binding-free, then C˙0 can be taken so that |C1 [χrooted, and |C1 [χ2
2is also binding-free.
3. If the pre-template C is a relation on contraction trees, then there exist a focussed
context C˙20 and two sequences G~000 and H~000 of focus-free hypernets, such that C˙2 [G~00 ] 7→000
C˙20 [G~000 ] = Ṅ , C˙2 [H~ 00 ] 7→ C˙20 [H~000 ], and G000
i C Hi for each index i.
Proof of the point (1). The proof is by case analysis on the local rule C˙2 [G~00 ] 7→ Ṅ .
• When the rule is a contraction rule, the rule simply duplicates all box edges withoutchanging any deep edges. Because all holes of C˙2 are deep, there exists a focussed
context C˙20 , whose holes are all deep, such that C˙2 [G~00 ] 7→ C˙20 [G~00 , G~00 ] is a contraction
rule. Moreover, C˙2 [H~ 00 ] 7→ C˙20 [H~ 00 , H~ 00 ] is also a contraction rule.
• When the rule is a beta rewrite rule, the rule replaces a box edge with the hypernetthat labels the box. Because all holes of C˙2 are deep, there exists a focussed context
C˙20 such that C˙2 [G~00 ] 7→ C˙20 [G~00 ] is a beta rewrite rule. Moreover, C˙2 [H~ 00 ] 7→ C˙20 [H~ 00 ] isalso a beta rewrite rule.
• Otherwise, the rule does not involve any deep edge. This means the focussed context
C˙2 must have no hole, and the sequences G~00 and H~ 00 must be empty. We can take afocussed context C˙20 with no hole, such that C˙2 [ ] 7→ C˙20 [ ].
Because contraction rules and local rewrite rules are all deterministic, C˙20 [G~000 ] = Ṅ follows
from C˙2 [G~00 ] 7→ C˙20 [G~000 ].
Proof of the point (2). The proof is built on top of the proof of the point (1). In particular,
we assume that all holes of C˙20 are deep in the case of contraction rules, and C˙20 has no hole→in the case of local rules of Oex \{@}. Under this assumption, our goal is to prove that
~0 , C˙0 ]| is binding-free.
|C1 [χ
2~0 , |C˙2 |] and C 0 denote C1 [χ~0 , |C˙0 |]. Because C = |C1 [χ~0 , C˙2 ]| and C 0 =Let C denote C1 [χ
2~0 , C˙0 ]|, it suffices to prove that C 0 is binding-free, given that C is binding-free.
|C1 [χ
2
Firstly, because C is binding-free, |C˙2 | is necessarily binding-free. By inspecting the local
rule C˙2 [G~00 ] 7→ C˙20 [G~000 ], we check below that |C˙20 | is also binding-free.
42• When the rule is a contraction rule, or a beta rewrite rule, any path that makes |C˙20 |not binding-free gives a path in |C˙2 |, which leads to a contradiction.
• Otherwise, |C˙20 | is trivially binding-free because it does not have any hole edges.
Now we prove that C 0 is binding-free by contradiction; we assume that there exists apath P in C 0 , from a source of a contraction, atom, box or hole edge e, to a source of a~0 , χ]), and eχ denote the hole edge
hole edge e0 . Let χ be the last hole label of C1 (i.e. C1 [χof C1 labelled with χ. We derive a contradiction by case analysis on the path P .
• When e0 comes from C1 , and the path P consists of edges from C1 only, the path P
gives a path in C1 . Because P does not contain eχ , it also gives a path in C. This
contradicts C being binding-free.
• When e0 comes from C1 , and the path P contains an edge from C2 , by finding thelast edge from C2 in P , we can take a suffix of P that gives a path P 0 from a targetof the hole edge eχ to a source of the hole edge e0 , in C1 . Because the suffix path P 0
does not contain eχ , it gives a path in C. We inspect the local rule C˙2 [G~00 ] 7→ C˙20 [G~000 ]as follows.
– When the rule is a contraction rule, because each output of |C˙2 | is reachable froma source of a contraction edge, adding the contraction edge at the beginning of
P 0 gives a path in C from a source of the contraction edge to a source of thehole edge e0 . This contradicts C being binding-free.
→– When the rule is a rewrite rule of operations {@, ref, =, :=, !}, P 0 gives a pathin C to the hole edge e0 , from either of the following: a target of an atom orbox edge; or a source of a contraction, atom or a box edge (by typing). This
contradicts C being binding-free.
– Otherwise, i.e. when the rule is a rewrite rule of operations {+, −, −1 }, the holeedge eχ actually does not have any target. This contradicts, in the first place,the path P containing an edge from C2 .

• When both e and e0 come from |C˙20 |, and the path P gives a path in |C˙20 |, thiscontradicts |C˙20 | being binding-free.
• When both e and e0 come from |C˙20 |, and the path P does not give a single path in|C˙20 |, we inspect the local rule C˙2 [G~00 ] 7→ C˙20 [G~000 ] as follows.
– When the rule is a contraction rule, all holes of C˙20 are deep. It is impossible for
P , which is to a target of a deep hole edge, not to give a path in |C˙0 |. This is a2

contradiction.

→– When the rule is a local rewrite rule of any operations but ‘@’, C˙20 actually does
not have any hole edge. It is impossible for the hole edge e0 to be from |C˙20 |.
This is a contradiction.
– When the rule is a beta rewrite rule, the hole edge eχ actually has only one
source. If P consists of edges from |C˙20 | only, the source must be also a targetof eχ ; otherwise, P has a sub-sequence that gives a path in C1 . In either case,there exists a path P 0 from the source of eχ to the source of eχ , i.e. a cyclearound the source of eχ , in C1 . This cycle gives a cycle in C around the sourceof eχ .
43

In the case of a beta rewrite rule, outputs are all reachable from the input, which coincides with the token source, in C˙2 [χ~00 ]. Therefore, the cy~0 , C˙2 [χ~00 ]], around the token source. Because
cle P 0 also gives a cycle in C1 [χ~0 , C˙2 [χ~00 ]]; G~ 0 , G~00 ; H~ 0 , H~ 00 ) is a C-specimen of the output-closed pre-template(C1 [χ
~ 0 , C˙2 [G~00 ]] and C1 [H~ 0 , C˙2 [H~ 00 ]]C, by Lem. A.12(3), at least one of the states C1 [Gis not rooted. This is a contradiction.
• When e comes from C1 and e0 comes from |C˙20 |, we inspect the local rule C˙2 [G~00 ] 7→
C˙20 [G~000 ] as follows.
– When the rule is a contraction rule, by finding the last edge from C1 in P , we
can take a suffix of P that gives a path P 0 from an input to a source of the holeedge e0 in |C˙20 |. However, the path P 0 cannot exist because the hole edge e0 is
deep in |C˙20 |. This is a contradiction.
→– When the rule is a local rewrite rule of any operations but ‘@’, C˙20 actually does
not have any hole edge. It is impossible for the hole edge e0 to be from |C˙20 |.
This is a contradiction.
– When the rule is a beta rewrite rule, by finding the first edge from |C˙0 | in P ,2

we can take a prefix of P that gives a path P 0 from a source of the edge e to asource of the hole edge eχ , in C1 . Because P does not contain eχ , P 0 does notcontain eχ either.

In the case of a beta rewrite rule, eχ has only one source, and the input of C˙2 [χ~00 ]coincides with the token source. Therefore, P 0 gives a path from a source of e to
~0 , C˙2 [χ~00 ]], and this path is not an operation path, because
the token source in C1 [χ~0 , C˙2 [χ~00 ]]; G~ 0 , G~00 ; H~ 0 , H~ 00 ) is a C-specimen ofof its first edge e. Because (C1 [χthe output-closed pre-template C, by Lem. A.12(3), at least one of the states~ 0 , C˙2 [G~00 ]] and C1 [H~ 0 , C˙2 [H~ 00 ]] is not rooted. This is a contradiction.
C1 [GProof of the point (3). The proof is by case analysis on the local rule C˙2 [G~00 ] 7→ Ṅ .
• When the rule is a contraction rule, the rule simply duplicates all box edges without changing any deep edges, and does not change any existing shallow contraction/weakening edges. Because C relates only contraction trees, deep edges from
G~00 are duplicated and shallow ones from G~00 are preserved, by the rule. There exist
a sequence G~000 of contraction trees and a focussed context C˙20 , such that G~000 ⊆ G~00
(as sets) and C˙2 [G~00 ] 7→ C˙20 [G~00 , G~000 ] is a contraction rule. Moreover, there exists a
sequence H~000 of contraction trees that satisfies H~000 ⊆ H~ 00 (as sets) and corresponds
to G~000 . Because C relates only contraction trees, C˙2 [H~ 00 ] 7→ C˙20 [H~ 00 , H~000 ] is also acontraction rule.
• When the rule is a beta rewrite rule, the rule involves no shallow contraction trees.
Because C relates only contraction trees, all holes of C˙2 must be deep, and the proof
is reduced to the point (1).
• When the rule is a rewrite rule of name-accessing operations {=, :=, !}, the rulepreserves contraction trees at any depth. There exists a focussed context C˙20 suchthat C˙2 [G~00 ] 7→ C˙20 [G~00 ] is a local rewrite rule. Moreover, because C relates only
contraction trees, C˙2 [H~ 00 ] 7→ C˙20 [H~ 00 ] is also a local rewrite rule.
44

`
`
D1,2
`
D1,2

` ` `
`
`
D1,2

`
`
D1,2
/1

`
D1,2

⊗⊗

⇧
⇧
D1,1

`

⊗

`
`
D1,2
` `

`
`
`
`
D1,2
D1,2

` ` `
`
`
D1,2

`
`
D1,2
/2 D1,2

` ` `

`
`
D1,2
` ` /3` ` `` ` ` `
0

` `

/4
`

⊗⊗

` `

⊗

0

?⌦k
Dk?0 ,2⇧⌦hDh⇧ 0 ,2

H

H

⇧
⇧
⇧
D1,2
/6 D1,1
⇧ ⇧
⇧

⇧
⇧
D1,2
⇧ ⇧
I

I

?

?

?

⊗
0

?
D1,2

?⌦k ? ⇧⌦h?⌦k ? ⇧⌦h?⌦(n+k) ? ⇧⌦h ?⌦(n+k) ? ⇧⌦h
G
G
?
?
n
n
T (?)
T (?)

⇧

⊗

?

⊗
0

?⌦k ? ⇧⌦h?⌦k ? ⇧⌦h?⌦(n+k) ? ⇧⌦h ?⌦(n+k) ? ⇧⌦h
G
G
?
?
n
n
T (?)
T (?)

/7

⊗ D1,1?

I?⌦k ⇧⌦h
H
/5

k

k

?
?
?
D1,2
/9
? ?
⇧
⇧

⊗

⇧
⇧
D1,1
⇧
⇧
⇧
⇧
D1,2
/8 D1,1
⇧
⇧
⇧
D1,2
⇧
⇧
?

I

⊗ I
?

⊗

Figure 13: Triggers (H is a copyable hypernet, and G is a hypernet)• Otherwise, the rule involves no contraction trees, which means the focussed context
C˙2 must have no hole, and the sequences G~00 and H~ 00 must be empty. We can take afocussed context C˙20 with no hole, such that C˙2 [ ] 7→ C˙20 [ ].
Because contraction rules and local rewrite rules are all deterministic, C˙20 [G~000 ] = Ṅ follows
from C˙2 [G~00 ] 7→ C˙20 [G~000 ].

8.5. Details of input-safety and robustness proofs
In this section we give some details of proving input-safety and robustness of the pretemplates.
Fig. 13 lists triggers that we use to prove some input-safety and robustness of the pretemplates. Table 3 shows contextual refinements/equivalences implied by these triggers,
given that some pre-templates (shown in the “dependency” column) imply contextualrefinement as shown in Table 1. All the implications can be proved simply using thecongruence property and transitivity of contextual refinement. Table 3 shows which pretemplate requires each trigger in its proof of input-safety or robustness (in the “used for”
column). Note that the converse of any trigger is again a trigger.
Recall that there is a choice of contraction trees upon applying a contraction rule orsome local rewrite rule. The minimum choice is to collect only contraction edges whosetarget is reachable from the token target. The maximum choice is to take the contractiontree(s) so that no contraction or weakening edge is incoming to the unique hole edge in acontext.
8.5.1. Pre-templates on contraction trees
First we check input-safety and robustness of C⊗Assoc , C⊗Comm and C⊗Idem , which are allon contraction trees.
input-safety of C⊗Assoc and C⊗Comm can be checked as follows. Given a COex -specimen
˙ H~ 1 ; H~ 2 ) with an entering search token, because any input of a contraction tree is a(C;45

implication of H1 C H2

dependency

used for

C1

C⊗Assoc , C⊗Comm

H1 '=ON

H2

C⊗

C2

C⊗Assoc , C⊗Comm

H1 '=ON

H2

C⊗

C3

C⊗Assoc , C⊗Comm , C⊗Idem

H1 '=ON

H2

CBPullC

C4

C⊗Idem

H1 '=ON

H2

CBPullW , CNE3C5C⊗Assoc , C⊗Comm , C⊗Idem , C⊗ , CGC

C6C⊗Assoc , C⊗Idem , CGC

H1 '=ON

H2

CNE1 , CNE4

C7C⊗Idem , C⊗GC

H1 '=ON

H2

CNE1

C8

C⊗Assoc , C⊗Idem , CGC

H1 '=ON

H2

CNE3

C9

C⊗ , CGC

C ex
C ex
C ex
C ex

H1 ≤ONC ex

H2 , H2 ≥ON

C ex

C ex
C ex
C ex

H1 ≥ONC ex

H2 , H2 ≤ON

C ex

H1

H1

CBPullD

CNE3 , CNE4

Table 3: Triggers and their implied contextual refinements/equivalences
source of a contraction edge, we have:•˙ H~ 2 ] →˙ H~ 2 ]i /? .
C[
hC[

•
˙ H~ 1 ] →˙ H~ 1 ]i /? ,C[hC[

˙ H~ 1 ]i /? if and only if a rewrite
It can be observed that a rewrite transition is possible in hC[
˙ H~ 2 ]i . When a rewrite transition is possible in both states,transition is possible in hC[/?

we can use Lem. 8.3(3), by considering a maximal possible contraction rule. The resultsof the rewrite transition can be given by a new quasi-COex -specimen up to (=, =) (here =denotes equality on states). When no rewrite transition is possible, both of the states are
not final but stuck.
Robustness of the three pre-templates and their converse can also be proved using
Lem. 8.3(3), by considering a maximal possible local (contraction or rewrite) rule in eachcase.
8.5.2. Input-safety of pre-templates not on contraction trees
As mentioned in Sec. 8.2, pre-templates that relate hypernets with no input of type ? are→trivially input-safety for any parameter (C, Q, Q0 ). This leaves us pre-templates C⊗ , C @ ,Cref , CNE1 , CNE3 and CNE4 to check.
As for C⊗ , note that the pre-template C⊗ relates hypernets with at least one input.
Any COex -specimen of C⊗ with an entering search token can be turned into the form
(C[(?;j χ), χ~ ]; H 1 , H~ 1 ; H 2 , H~ 2 ) where j is a positive number. The proof is by case analysis
on the number j.
• When j = 1, we have:•C[(?;j H 1 ), H~ 1 ] →C[( ;j H 1 ), H~ 1 ]→ C[(?;j H 2 ), H~ 1 ].

46

~]
We can take (C[(?;j H 2 ), χ~ ]; H~ 1 ; H~ 2 ) as a COex -specimen, and the token in C[(?;j H 2 ), χ
is not entering.
• When j > 1, the token target must be a source of a contraction edge. There exist
a focus-free context C 0 [χ0 ], two focus-free hypernets H 01 C⊗ H 02 and a focus-free
hypernet G, such that•
C[(?;j H 1 ), H~ 1 ] →C[( ;j H 1 ), H~ 1 ]→ C[(?;j C 0 [H 01 ]), H~ 1 ],•C[(?;j H 2 ), H~ 2 ] →C[( ;j H 2 ), H~ 2 ]→ C[(?;j G), H~ 2 ],˙ =N G given by the trigger C1 via Lem. 6.19. The results of theseand C 0 [H 02 ] '˙ =N ).
sequences give a quasi-COex -specimen up to (=, '→A proof of input-safety of the operational pre-templates C @ and Cref is a simpler versionof that of C⊗ , because the operational pre-templates relate hypernets with only one input.
Let C be either COex or COex -bf . Any C-specimen of an operational pre-template withan entering search token can be turned into the form (C[(?; χ), χ~ ]; H 1 , H~ 1 ; H 2 , H~ 2 ); note⊗that the parameter j that we had for C is redundant in ?; χ. We have:•C[(?; H 1 ), H~ 1 ] →C[( ; H 1 ), H~ 1 ]→ C[(?; H 2 ), H~ 1 ].

We can take (C[(?; H 2 ), χ~ ]; H~ 1 ; H~ 2 ) as a COex -specimen, and the token in C[(?;j H 2 ), χ~ ] isnot entering. This data gives a COex -bf -specimen when C = COex -bf , which follows fromthe closedness of COex -bf with respect to plugging (Lem. A.21). Note that ?; H 1 can beseen as a context with no holes, which is trivially binding-free.
Finally, we look at the name-exhaustive pre-templates CNE1 , CNE3 and CNE4 . Any
COex -specimen of one of these pre-templates, with an entering search token, can be turned
into the form (C[(?;j χ), χ~ ]; H 1 , H~ 1 ; H 2 , H~ 2 ) where j is a positive number. The token target
is a source of an edge labelled with λ ∈ Oex
X , so we have:•C[(?;j H 1 ), H~ 1 ] →C[(X;j H 1 ), H~ 1 ],•C[(?;j H 2 ), H~ 2 ] →C[(X;j H 2 ), H~ 2 ].

The results of these sequences give a quasi-COex -specimen up to (=, =).
8.5.3. Robustness of pre-templates not on contraction trees: a principle
˙ H~ 1 ] → Ṅ 0 from the state
Robustness can be checked by inspecting rewrite transition C[
˙ H~ 1 ; H~ 2 ) of a pre-template, where the token of C˙ is not entering.
given by a specimen (C;We in particular consider the minimum local (contraction or rewrite) rule Ġ 7→ Ġ0 appliedin this transition. This means that, in the hypernet Ġ, every vertex is reachable from thetoken target.
The inspection boils down to analyse how the minimum local rule involves edges thatcome from the hypernets H~ 1 . If all the involvement is deep, i.e. only deep edges from H~ 1˙
are involved in the local rule, these deep edges must come via deep holes in the context C.
We can use Lem. 8.3(1).
47If the minimum local rule involves shallow edges that are from H~ 1 , endpoints of these˙ some holes
edges are reachable from the token target. This means that, in the context C,
are shallow and their sources are reachable from the token target. Moreover, given that˙ the context has a path from the token target to a source ofthe token is not entering in C,a hole edge.
~`⇥ i Bi

?⌦k
!

?

C
?

?⌦k

0

?

Figure 14: A shallow overlap (C is a contraction tree, Bi are box edges)
For example, in checking robustness of CBPerm with respect to copy transitions, one
situation of shallow overlaps is when Ġ is in the form in Fig. 14, and some of the box
edges Bi are from H~ 1 . Taking the minimum contraction rule means that C in the graphis a contraction tree that gives a path from the token target. This path C followed by theoperation edge φ corresponds to paths from the token target to hole sources in the context
˙C.
So, if the minimum local rule involves shallow edges that are from H~ 1 , the context C˙necessarily has a path P from the token target to a hole source. The path becomes a path˙ H~ 1 ], from the token target to a source of an edge e that is from H~ 1 . The
in the state C[edge e is necessarily shallow, and also involved in the application of the minimum local
rule, because of the connectivity of Ġ. Moreover, a source of the edge e is an input, in therelevant hypernet of H~ 1 . By inspecting minimum local rules, we can enumerate possiblelabelling of the path P and the edge e, as summarised in Table 4. Explanation on thenotation used in the table is to follow.
We use the regular-expression like notation in Table 4. For example, (⊗?C )+ · Oex represents finite sequences of edge labels, where more than one occurrences of the label ⊗?C
is followed by one operation φ ∈ Oex . This characterises paths that inhabit the overlap
shown in Fig. 14, i.e. the contraction tree C followed by the operation edge φ. Note that
this regular-expression like notation is not a proper regular expression, because it is overthe infinite alphabet MOex , the edge label set, and it accordingly admits infinite alternation(aka. union) implicitly.
To wrap up, checking robustness of each pre-template (that are not on contraction trees)boils down to using Lem. 8.3(1) and/or analysing the cases enumerated in the table above.
8.5.4. Robustness of C⊗ and its converse
Robustness check of the pre-template C⊗ with respect to copy transitions has two cases.
The first case is when one shallow overlap is caused by a path characterised by (⊗?C )+ , andthe second case is when no shallow overlaps are present and Lem. 8.3(1) can be used.
In the first case, namely, a COex -specimen with a non-entering rewrite token can beturned into the form (C[Ċ 0 [χ0 ], χ~ ]; H 1 , H~ 1 ; H 2 , H~ 2 ) where j is a positive number, and Ċ 0
is a focussed context in the form of Fig. 15. A rewrite transition is possible on bothstates given by the specimen, in which a contraction rule is applied to Ċ 0 [H 1 ] and Ċ 0 [H 2 ].
48

local rulelabels of path Plabel of edge econtraction(⊗?C )+ · Oex(⊗?C )+⊗? , I, Oex
C

→

→

@
→

ref
=
:=
!
+
−

−1

@·λ

box
box

∗
@ · (Oex
X)∗
ref · (OexX)=
= · I · (⊗C )∗∗⊗ ∗:= · (Oex
X ) · I · ( C)∗:= · (OexX)!
! · I · (⊗C )∗
+

Oex
X, I
Oex
X, I
I
⊗ , ◦C⊗ , ◦
C
Oex
X, I

I
⊗ , ◦
C
N

−

N

−1

N

Table 4: Summary of paths that witness shallow overlaps
~`
χ

?⌦k1

? ?⌦k2

C
?

?⌦k

?

Figure 15: A focussed context (C is a contraction tree)
Results of the rewrite transition give a new quasi-COex -specimen. When k1 = 0, this˙ =N ), using the trigger C2 . When k1 > 0, the quasi-specimen
quasi-specimen is up to (=, '˙ =N ), but using the trigger C1 .
is also up to (=, 'Robustness check of the pre-template C⊗ with respect to rewrite transitions always boils
down to Lem. 8.3(1). This is intuitively because no local rewrite rule of operations involves
any shallow contraction edge of type ?.
Robustness of (C⊗ )−1 can be checked in a similar manner. Namely, using Table 4,
shallow overlaps are caused by paths:(⊗?C )+ ,→∗@ · (OexX) ,∗ref · (Oex
X) ,

=,

+,

∗
:= · (Oex
X) ,

−,

!,

−1

from the token target. All paths but (⊗?C )+ gives rise to a state that is not rooted, which
can be checked using Lem. 6.17. This reduces the robustness check of (C⊗ )−1 to that ofC⊗ .
49

8.5.5. Robustness of CGC and CNE2 , and their converse
These four pre-templates both relate hypernets with no inputs. Proofs of robustnessof them and their converse always boils down to the use of Lem. 8.3(1), following thediscussion in Sec. 8.5.3. Namely, it is impossible to find the path P in the context C˙ fromthe token target to a hole source.
8.5.6. Robustness of CBPerm , CBPullC , CBPullW and CBPullD , and their converse
These eight pre-templates all concern boxes. Using Table 4, shallow overlaps are caused→by paths (⊗?C )+ · Oex and @ · λ from the token target.

→

Robustness check with respect to compute transitions of operations Oex \{@} always
boil down to Lem. 8.3(1).
→→As for compute transitions of the operation ‘@’, either one path @ · λ causes one shallow
overlap, or all overlaps are deep. The latter situation boils down to Lem. 8.3(1). In theformer situation, a beta rule involves one box that is contributed by a pre-template, andstates given by a COex -specimen are turned into a quasi-COex -specimen up to (=, =), by
one rewrite transition.
As for copy transitions, there are two possible situations.
• Paths (⊗?C )+ · Oex cause some shallow overlaps and there are some deep overlaps too.
• All overlaps are deep, which boils down to Lem. 8.3(1).
In the first situation, some of the shallow boxes duplicated by a contraction rule are contributed by a pre-template, and other duplicated boxes may have deep edges contributedby the pre-template. By tracking these shallow and deep contributions in a contraction
rule, it can be checked that one rewrite transition turns states given by a COex -specimen
into a quasi-COex -specimen. This quasi-specimen is up to the following, depending on
pre-templates:• (=, =) for CBPerm and its converse,
˙ =N ) for CBPullC , and ('˙ =N , =) for its converse, using the trigger C3 ,• (=, '
˙ =N ) for CBPullW , and ('˙ =N , =) for its converse, using the trigger C4 , and• (=, '˙ ≤ ) for CBPullD , and (˙ ≥ , =, ) for its converse, using the trigger C5 .
• (=, NN
8.5.7. Robustness of operational pre-templates and their converse
For the operational pre-templates and their converse, we use the class COex -bf of bindingfree contexts. This restriction is crucial to rule out some shallow overlaps.
→

Using Table 4, shallow overlaps with the operational pre-templates C @ and Cref arecaused by paths (⊗?C )+ from the token context. However, the restriction to binding-freecontexts makes this situation impossible, which means the robustness check always boils
down to Lem. 8.3(1) and Lem. 8.3(2).

50→In checking robustness of the converse (C @ )−1 and (Cref )−1 , shallow overlaps are causedby paths:(⊗?C )+ ,→∗@ · (OexX) ,∗ref · (Oex
X) ,

=,

+,

∗
:= · (Oex
X) ,

−,

−1

!,

from the token target. Like the case of (C⊗ )−1 , all paths but (⊗?C )+ give rise to a statethat is not rooted, which can be checked using Lem. 6.17. The paths (⊗?C )+ are impossible
because of the binding-free restriction. As a result, this robustness check also boils down
to Lem. 8.3(1) and Lem. 8.3(2).
8.5.8. Robustness of name-exhaustive pre-templates on lambda-abstractions, andtheir converse
We here look at the three name-exhaustive pre-templates CNE1 , CNE3 and CNE4 , and theirconverse. All these six pre-templates concern lambda-abstractions, and they give rather
rare examples of robustness check where we compare different numbers of transitions.
Using Table 4, shallow overlaps with these pre-templates are caused by paths:→∗@ · (OexX) ,(⊗?C )+ ,∗ref · (OexX) ,∗:= · (OexX)

from the token target.

→

As for compute transitions of operations Oex \{@}, there are two possible situations.
∗ex ∗• Shallow overlaps are caused by paths ref · (Oex
X ) or := · (OX ) .

• There is no overlap at all, which boils down to Lem. 8.3(1).
In the first situation, a stable hypernet GS of a local rewrite rule (see e.g. Fig. 5) contains
shallow edges, labelled with λ ∈ Oex
X , that are contributed by a pre-template. The overlapped shallow contributions are not modified at all by the rewrite rule, and consequently,
one rewrite transition results in a quasi-COex -specimen up to (=, =).
As for copy transitions, either one path (⊗?C )+ causes one shallow overlap, or all overlaps are deep. The latter situation boils down to Lem. 8.3(1). In the former situation,
one lambda-abstraction contributed by a pre-template gets duplicated. Namely, a COex specimen with a non-entering rewrite token can be turned into the form (C[Ċ 0 [χ0 ], χ~ ]; H 1 , H~ 1 ; H 2 , H~ 2 )where Ċ 0 is a focussed context in the form of Fig. 15. There exist a focussed context C˙00
and two hypernets G1 CNE1 G2 such that:
C[Ċ 0 [H 1 ], H~ 1 ] → C[C˙00 [G1 ], H~ 1 ],C[Ċ 0 [H 2 ], H~ 2 ] → C[C˙00 [G2 ], H~ 2 ].
Results of these rewrite transitions give a new quasi-COex -specimen up to (=, =).
→As for compute transitions of the operation ‘@’, there are two possible situations.
→• One path @ causes a shallow overlap of the edge that has label λ and gets eliminated→∗by a beta rewrite rule, and possibly some other paths @·(OexX ) cause shallow overlaps
in the stable hypernet GS (see Fig. 4).

51

→

∗
• There are possibly deep overlaps, and paths @ · (Oex
X ) may cause shallow overlaps
in the stable hypernet GS .

In the second situation, all overlaps are not modified at all by the beta rewrite rule,
except for some deep overlaps turned shallow. Consequently, one rewrite transition results
in a quasi-COex -specimen up to (=, =).
In the first situation, one lambda-abstraction contributed by the pre-template is modified, while all the other shallow overlaps (if any) are not. We can focus on the lambda→

abstraction. The beta rewrite acts on the lambda-abstraction, an edge labelled with ‘@’,and the stable hypernet GS .
In the case of CNE1 , application of the beta rule is followed by a few more transitions.
When GS is not an instance edge, we can prove that a token eventually gets stuck, failingto apply a rewrite rule of the equality operation ‘=’. When GS is simply an instance edge,a token may still get stuck for the same reason, but if there is an applicable rewrite rule˙ =N ), using
˙ =N , 'of the equality operation ‘=’, we obtain a quasi-COex -specimen up to ('6
7
GC
triggers C and C on the left, and C
on the right.
The case of CNE3 and CNE4 , and their converse, is similar. The only difference is thetriggers used to find a quasi-specimen, as summarised in Table 3.

9. Related and future work
Our Spartan UAM is motivated by a need for a flexible and expressive framework in whicha wide variety of effects can be given a cost-accurate model. As discussed, this opens thedoor to a uniform study of operations and their interactions. Defining new styles of abstract
machines is a rich and attractive vein of research. The “monoidal computer” of Pavlovic[2013] or the “evolving algebras” of Gurevich [2018] are such examples. What sets theSpartan UAM apart is the fact that it can be used, rather conveniently, for reasoning
robustly about observational equivalence.
It is well known that observational equivalence is fragile, in the sense that the validityof an equation depends not only on the operations involved in the operation itself but
also on the operations used in the context. Therefore, the addition of any new operation
to a language may invalidate some or all of its equations even if they do not concern theoperation itself. Consequently, reasoning about “real-life” languages must be constrained
to a syntactically idealised subset which cannot support exotic extrinsics (e.g. Gc.stat,discussed earlier) or, more significantly, foreign function calls, which can be seen as a very
general, programmable form of extrinsic operation. This is, in some sense, unavoidable.
An even more troubling aspect of observational equivalence is that the proof methods
themselves are fragile, in the sense that language additions may violate the very principles
on which proofs are constructed. This issue is addressed by Dreyer et al. [2012] by carefully
distinguishing between various kinds of operations (state vs. control). Using Kripke
relations, Dreyer et al. [2010] goes beyond an enumerative classification of effects to using
characterisations of effects in the aid of reasoning; the notion of island introduced in loc.
cit. has similar intuitions to our robustness property. More radical approaches are down toreplacing the concept of a syntactic context with an “epistemic” context, akin to a DolevYao-style attacker by Ghica and Tzevelekos [2012], or by characterising combinatoriallythe interaction between a term and its context as is the case with the game semantics
of Abramsky et al. [2013], Hyland and Ong [2000] or the trace semantics of Jeffrey and
Rathke [2005]. Our paper is a new approach to this problem which, by using a uniform

52

graph representation of the the program and its configuration can take the useful notionof locality beyond state, the overall program.
We argue that our approach is both flexible and elementary. A specific version of thisformalism has been used to prove, for example, the soundness of exotic operations involvedin (a functional version of) Google’s TensorFlow machine learning library by Muroya et al.
[2018]. Even though the proofs can seem complicated, this is in part due to the graphbased formalism being new, and in part due to the fact that proofs of equivalences arelengthy case-based analyses. But herein lies the simplicity and the robustness of theapproach, avoiding the discovery of clever-but-fragile language invariants which can beused to streamline proofs. Our tedious-but-elementary proofs on the other hand seem
highly suitable for automation – this is for future work.
The original motivation of the DGoI machine given by Muroya and Ghica [2017] was toproduce an abstract machine that expresses the computational intuitions of the GoI while
correctly modelling the cost of evaluation, particularly for call-by-value and call-by-need.
Although the Universal Abstract Machine framework does not aim at efficiency, one canthink of a cost model of the machine in a similar way as the DGoI machine. Moreover,the indexing of observational equivalence with a preorder representing the number of steps
gives a direct avenue for modelling and comparing computation costs. For example, thebeta law (Tbl. 1) is indexed by the normal order on N, which indicates that one side
always requires fewer steps than the other in the evaluation process. The only details tobe resolved are associating costs (time and space) with steps, in particular different costs
for different operations.
Another strand of research related to ours is work on defining programming languages
with effects. We are not so much interested in “simulated effects”, which are essentiallythe encoding of effectful behaviour into pure languages, and which can be achieved via
monads [Wadler, 1998], but we are interested in genuine “native” effects which happen
outside of the language. Semantically this has been introduced by Plotkin and Power[2008] and more recently developed by Møgelberg and Staton [2011]. Spartan in somesense takes the idea to the extreme by situating all operations (pure or effectful) outside of
the program, in “the world”, and keeping as intrinsic to the language only the structural
aspects of copying vs. sharing, and scheduling of computation via thunking.
Nested (hyper)graphs are inspired by the exponential boxes of proof nets, a graphical representation of linear logic proofs [Girard, 1987] and have an informal connection to Milner[2001]’s bigraphs. Exponential boxes can be formalised by parametrising an agent (whichcorresponds to an edge in our setting) by a net, as indicated by Lafont [1995]. In the framework of interaction nets [Lafont, 1990] that subsume proof nets, agents can be coordinatedto represent a boundary of a box, as suggested by Mackie [1998]. An alternative representation of boxes that use extra links between agents is proposed by Accattoli and Guerrini[2009]. Our graphical formulation of boxes shares the idea with the first parametrising
approach, but we have flexibility regarding types of a box edge itself and its content (i.e.
the hypernet that labels it). We use box edges to represent thunks, and a box edge canhave less targets than outputs of its contents, reflecting the number of bound variables athunk has. This generalised box structure is also studied by Drewes et al. [2002] as hierarchical graphs, in the context of double-pushout graph transformation [Rozenberg, 1997],
an well-established algebraic approach to graph rewriting. Investigating local reasoning inthis context is an important future direction.
Interaction nets are another established framework of graph rewriting, in which various
evaluations of pure lambda-calculus can be implemented [Sinot, 2005, 2006]. The ideaof having the token to represent an evaluation strategy can be found in loc. cit., which53

suggests that our focussed rewriting on hypernets could be implemented using interaction
nets. However, the local reasoning we are aiming at with focussed rewriting does not seemeasy in the setting of interaction nets, because of technical subtleties observed in loc. cit.;
namely, a status of evaluation is remembered by not only the token but also some otheragents around an interaction net.
Hypernets could also perhaps be formalised as string diagrams, with boxes modelled as“functorial boxes” by Melliès [2006]. In fact, the representation of simple local state doneby Mellies [2014] using string diagrams bears many informal connections to Spartan.
However, this would mean accommodating some equations on hypernets built in. With
Spartan terms to represent, it is not clear what should be, or can be, such a builtin equation. Our aim is rather to provide a framework in which we can reason about,and figure out, the equations. This is also why the use of Frobenius structures to model
variables as in Bonchi et al. [2016] is not automatic in the case of focussed graph rewriting.
Another future work is the introduction of a more meaningful type system. The typesystem of Spartan is very weak, and we consider it a strength of the approach thatequivalences can be proved without the aid of a powerful type infrastructure. On theother hand, in order to avoid stuck configurations and ensure safety of evaluation types
are required. The usage of more expressive types is perfectly compatible with Spartan,and is something we intend to explore. In particular we would like to study notions oftyping which are germane to Spartan, capturing its concepts of locality and robustness.
Beyond types, if we look at logics there are some appealing similarities between Spartan and separation logic [Reynolds, 2002]. The division of nodes into copying nodes via
variables and sharing nodes via atoms is not accidental, and their different contraction
properties match those from bunched implications [O’Hearn and Pym, 1999]. On a deeper
level, the concepts of locality and in particular robustness developed here are related to
the “frame” rule of separation logic.
Finally, our formulation of equivalence has some self-imposed limitations needed to limit
the complexity of the technical presentation. We are hereby concerned with sequential anddeterministic computation. Future work will show how these restrictions can be relaxed.
Parallelism and concurrency can be naturally simulated using multi-token reductions, as
inspired by the multi-token GOI machine of Lago et al. [2017], whereas nondeterminism (orprobabilistic evaluation) requires no changes to the machinery but rather a new definitionof observational equivalence. This is work we are aiming to undertake in the future.

References
S. Abramsky. Game semantics for programming languages. In 22nd International Symposium on Mathematical Foundations of Computer Science, MFCS 1997, August 25-29
1997, Bratislava, Slovakia, pages 3–4, 1997. doi:10.1007/BFb0029944.
S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF.
abs/1311.6125, 2013. URL http://arxiv.org/abs/1311.6125.

CoRR,

B. Accattoli and S. Guerrini. Jumping boxes. In CSL 2009, volume 5771 of Lect. Notes
Comp. Sci., pages 55–70. Springer, 2009. doi:10.1007/978-3-642-04027-6 7.
B. Accattoli, P. Barenbaum, and D. Mazza. Distilling abstract machines. In 19th ACM
SIGPLAN International Conference on Functional Programming, ICFP 2014, September 1-3 2014, Gothenburg, Sweden, pages 363–376, 2014. doi:10.1145/2628136.2628154.

54

A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence.
In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, January 21-23 2009, Savannah, GA, USA, pages 340–353, 2009.
doi:10.1145/1480881.1480925.
F. Bonchi, F. Gadducci, A. Kissinger, P. Soboci’nski, and F. Zanasi. Rewriting modulo
symmetric monoidal structure. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016,
pages 710–719, 2016. doi:10.1145/2933575.2935316.
F. Bonchi, D. Petrisan, D. Pous, and J. Rot. A general account of coinduction up-to. Acta
Inf., 54(2):127–190, 2017. doi:10.1007/s00236-016-0271-4.
B. Coecke and R. Duncan. Interacting quantum observables: categorical algebra anddiagrammatics. New Journal of Physics, 13(4):043016, 2011. doi:10.1088/13672630/13/4/043016.
O. Danvy and A. Filinski. Abstracting control. In ACM Conference on LISP and Functional Programming, LFP 1990, June 27-29 1990, Nice, France, pages 151–160, 1990.
doi:10.1145/91556.91622.
O. Danvy, K. Millikin, J. Munk, and I. Zerny. On inter-deriving small-step and big-stepsemantics: A case study for storeless call-by-need evaluation. Theor. Comput. Sci., 435:
21–42, 2012. doi:10.1016/j.tcs.2012.02.023.
F. Drewes, B. Hoffmann, and D. Plump. Hierarchical graph transformation. J. Comput.
Syst. Sci., 64(2):249–283, 2002. doi:10.1006/jcss.2001.1790.
D. Dreyer, G. Neis, A. Rossberg, and L. Birkedal. A relational modal logic for higher-orderstateful adts. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL ’10, pages 185–198, New York, NY,
USA, 2010. ACM. ISBN 978-1-60558-479-9. doi:10.1145/1706299.1706323.
D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program., 22(4-5):477–528, 2012.
doi:10.1017/S095679681200024X.
M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control
and state. Theor. Comput. Sci., 103(2):235–271, 1992. doi:10.1016/0304-3975(92)900147.
D. R. Ghica and N. Tzevelekos. A system-level game semantics. Electr. Notes Theor.
Comput. Sci., 286:191–211, 2012. doi:10.1016/j.entcs.2012.08.013.
J. Girard. Linear logic.
3975(87)90045-4.

Theor. Comput. Sci., 50:1–102, 1987.

doi:10.1016/0304-

Y. Gurevich. Evolving algebras 1993: Lipari guide. arXiv preprint arXiv:1808.06255,
2018. URL https://arxiv.org/abs/1808.06255.
N. Hoshino, K. Muroya, and I. Hasuo. Memoryful geometry of interaction: from coalgebraic components to algebraic effects. In Joint Meeting of the 23rd EACSL Annual
Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, July 14-18 2014, Vienna,
Austria, pages 52:1–52:10, 2014. doi:10.1145/2603088.2603124.
55

J. M. E. Hyland and C. L. Ong. On full abstraction for PCF: I, II, and III. Inf. Comput.,
163(2):285–408, 2000. doi:10.1006/inco.2000.2917.
A. Jeffrey and J. Rathke. Java jr: Fully abstract trace semantics for a core java language.
In 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint
European Conferences on Theory and Practice of Software, ETAPS 2005, April 4-8
2005, Edinburgh, UK, pages 423–438, 2005. doi:10.1007/978-3-540-31987-0 29.
V. Koutavas and M. Wand. Small bisimulations for reasoning about higher-order imperative programs. In 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, January 11-13 2006, Charleston, SC, USA, pages
141–152, 2006. doi:10.1145/1111037.1111050.
Y. Lafont. Interaction nets. In 17th Annual ACM Symposium on Principles of Programming Languages, POPL 1990, January 1990, San Francisco, California, USA, pages
95–108, 1990. doi:10.1145/96709.96718.
Y. Lafont.
From proof nets to interaction nets, page 225248.
LondonMathematical Society Lecture Note Series. Cambridge University Press, 1995.
doi:10.1017/CBO9780511629150.012.
U. D. Lago, R. Tanaka, and A. Yoshimizu. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. In 32nd Annual ACM/IEEE Symposiumon Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages
1–12, 2017. doi:10.1109/LICS.2017.8005112.
I. Mackie. Linear logic With boxes. In 13th IEEE Symposium on Logic in Computer Science, June 21-24 1998, Indianapolis, IN, USA, pages 309–320, 1998.
doi:10.1109/LICS.1998.705667.
P. Melliès. Functorial boxes in string diagrams. In 20th International Workshop on Computer Science Logic, CSL 2006, 15th Annual Conference of the EACSL, September 25-29
2006, Szeged, Hungary, pages 1–30, 2006. doi:10.1007/11874683 1.
P.-A. Mellies. Local states in string diagrams. In Rewriting and Typed Lambda Calculi,
pages 334–348. Springer, 2014. doi:10.1007/978-3-319-08918-8 23.
R. Milner. Bigraphical reactive systems. In International Conference on Concurrency
Theory, pages 16–35. Springer, 2001. doi:10.1007/3-540-44685-0 2.
R. E. Møgelberg and S. Staton. Linearly-used state in models of call-by-value. In 4thInternational Conference on Algebra and Coalgebra in Computer Science, CALCO 2011,
August 30 - September 2 2011, Winchester, UK, pages 298–313, 2011. doi:10.1007/9783-642-22944-2 21.
J. H. Morris Jr. Lambda-calculus models of programming languages. PhD thesis, Massachusetts Institute of Technology, 1969. URL https://dspace.mit.edu/handle/
1721.1/64850.
K. Muroya and D. R. Ghica. The dynamic geometry of interaction machine: A callby-need graph rewriter. In 26th EACSL Annual Conference on Computer Science
Logic, CSL 2017, August 20-24 2017, Stockholm, Sweden, pages 32:1–32:15, 2017.
doi:10.4230/LIPIcs.CSL.2017.32.

56

K. Muroya, N. Hoshino, and I. Hasuo. Memoryful geometry of interaction II: recursion andadequacy. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January
20-22 2016, pages 748–760, 2016. doi:10.1145/2837614.2837672.
K. Muroya, S. W. T. Cheung, and D. R. Ghica. The geometry of computation-graphabstraction. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2018, Oxford, UK, July 09-12 2018, pages 749–758, 2018.
doi:10.1145/3209108.3209127.
P. O’Hearn and R. Tennent. ALGOL-like Languages. Springer Science & Business Media,
2013. URL 10.1007/978-1-4612-4118-8.
P. W. O’Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic
Logic, 5(2):215–244, 1999. doi:10.2307/421090.
D. Pavlovic. Monoidal computer I: Basic computability by string diagrams. Information
and Computation, 226:94–116, 2013. doi:10.1016/j.ic.2013.03.007.
A. M. Pitts and I. D. B. Stark. Observable properties of higher order functions thatdynamically create local names, or what’s new? In 18th International Symposiumon Mathematical Foundations of Computer Science 1993, MFCS 1993, August 30 September 3 1993, Gdansk, Poland, pages 122–141, 1993. doi:10.1007/3-540-57182-5 8.
G. D. Plotkin and J. Power. Algebraic operations and generic effects. Applied Categorical
Structures, 11(1):69–94, 2003. doi:10.1023/A:1023064908962.
G. D. Plotkin and J. Power. Tensors of comodels and models for operational semantics.
Electr. Notes Theor. Comput. Sci., 218:295–311, 2008. doi:10.1016/j.entcs.2008.10.018.
G. D. Plotkin and M. Pretnar. Handling algebraic effects. Logical Methods in Computer
Science, 9(4), 2013. doi:10.2168/LMCS-9(4:23)2013.
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings
17th Annual IEEE Symposium on Logic in Computer Science, pages 55–74. IEEE, 2002.
doi:10.1109/LICS.2002.1029817.
G. Rozenberg, editor. Handbook of graph grammars and computing by graph transformations, volume 1: foundations. World Scientific, 1997. ISBN 9810228848.
D. S. Scott and C. Strachey. Toward a mathematical semantics for computer languages,
volume 1. Oxford University Computing Laboratory, Programming Research Group,
1971. URL https://www.cs.ox.ac.uk/files/3228/PRG06.pdf.
F. Sinot. Call-by-name and call-by-value as token-passing interaction nets. In 7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005, April 21-23
2005, Nara, Japan, pages 386–400, 2005. doi:10.1007/11417170 28.
F. Sinot. Call-by-need in token-passing nets. Mathematical Structures in Computer Science, 16(4):639–666, 2006. doi:10.1017/S0960129506005408.
R. Statman. Logical relations and the typed lambda-calculus. Information and Control,65(2/3):85–97, 1985. doi:10.1016/S0019-9958(85)80001-2.

57

P. Wadler. The marriage of effects and monads. In ACM SIGPLAN Notices, volume 34:1,
pages 63–74. ACM, 1998. doi:10.1145/289423.289429.
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput.,
115(1):38–94, 1994. doi:10.1006/inco.1994.1093.

58

A. Technical appendix
A.1. Equivalent definitions of hypernets
Informally, hypernets are nested hypergraphs, and one hypernet can contain nested hypergraphs up to different depths. This intuition
is reflected by Def. 3.5 of hypernets, inSparticular the big union in Hk+1 (L, M ) = H L, M ∪ i≤k Hi (L, M ) . In fact, the definition can be replaced by a simpler, but possibly less intuitive, definition below that does
not explicitly deal with the different depths of nesting.
Definition A.1. Given sets L and M , a set Hk0 (L, M ) is defined by induction on k ∈ N:
H00 (L, M ) := H(L, M )


0
Hk+1
(L, M ) := H L, M ∪ Hk0 (L, M )and hence a set Hω0 (L, M ) :=S

0i∈N Hi (L, M ).

Lemma A.2. Given arbitrary sets L and M , any two numbers k, k 0 ∈ N satisfy Hk0 (L, M ) ⊆0
Hk+k0 (L, M ).
Proof. If k 0 = 0, the inclusion trivially holds. If not, i.e. k 0 > 0, it can be proved byinduction on k ∈ N. The key reasoning principle we use is that M ⊆ M 0 implies H(L, M ) ⊆H(L, M 0 ).
In the base case, when k = 0 (and k 0 > 0), we have
H00 (L, M ) = H(L, M )⊆ H L, M ∪ Hk0 0 −1 (L, M ) = Hk0 0 (L, M ).

In the inductive case, when k > 0 (and k 0 > 0), we have0(L, M )
Hk0 (L, M ) = H L, M ∪ Hk−100
⊆ H L, M ∪ Hk−1+k= Hk+k0 (L, M )0 (L, M )where the inclusion is by induction hypothesis on k − 1.

Proposition A.3. Any sets L and M satisfy Hk (L, M ) = Hk0 (L, M ) for any k ∈ N, andhence Hω (L, M ) = Hω0 (L, M ).
Proof. We first prove Hk (L, M ) ⊆ Hk0 (L, M ) by induction on k ∈ N. The base case, whenk = 0, is trivial. In the inductive case, when k > 0, we have[
Hk (L, M ) = H L, M ∪Hi (L, M )⊆ H L, M ∪

i≤k−1

[

i≤k−1


Hi0 (L, M )0= H L, M ∪ Hk−1
(L, M )

= Hk0 (L, M ).

59

(by I.H.)(by Lem. A.2)

The other direction, i.e. Hk0 (L, M ) ⊆ Hk (L, M ), can be also proved by induction onk ∈ N. The base case, when k = 0, is again trivial. In the inductive case, we have0
Hk0 (L, M ) = H L, M ∪ Hk−1
(L, M )


⊆ H L, M ∪ Hk−1 (L, M )(by I.H.)[⊆ H L, M ∪Hi (L, M )i≤k−1= Hk (L, M ).

Given a hypernet G, by Lem. A.2 and Prop. A.3, there exists a minimum number ksuch that G ∈ Hk0 (L, M ), which we call the “minimum level” of G.
Lemma A.4. Any hypernet has a finite number of shallow edges, and a finite number ofdeep edges.
Proof. Any hypernet has a finite number of shallow edges by definition. We prove thatany hypernet G has a finite number of deep edges, by induction on minimum level k of
the hypernet.
When k = 0, the hypernet has ho deep edges.
0
When k > 0, each hypernet H that labels a shallow edge of G belongs to Hk−1
(L, M ),and therefore its minimum level is less than k. By induction hypothesis, the labelling
hypernet H has a finite number of deep edges, and also a finite number of shallow edges.
Deep edges of G are given by edges, at any depth, of any hypernet that labels a shallowedge of G. Because there is a finite number of the hypernets that label the shallow edgesof G, the number of deep edges of G is finite.

A.2. Plugging
An interfaced labelled monoidal hypergraph can be given by data of the following form:((V ] I ] O, E), (S, T ), (fL , fM )) where I is the input list, O is the output list, V is the setof all the other vertices, E is the set of edges, (S, T ) defines source and target lists, and(fL , fM ) is labelling functions.
Definition A.5 (Plugging). Let C[χ~1 , χ, χ~2 ] = ((V ]I]O, E), (S, T ), (fL , fM )) and C 0 [χ~3 ] =0 )) be contexts, such that the hole χ and the latter context((V 0 ]I 0 ]O0 , E 0 ), (S 0 , T 0 ), (fL0 , fM
C 0 have the same type and χ~1 ∩ χ~2 ∩ χ~3 = ∅. The plugging C[χ~1 , C 0 , χ~2 ] is a hypernet given
by data ((V̂ , Ê), (Ŝ, T̂ ), (fˆL , fˆM )) such that:V̂ = V ] V 0 ] I ] O

Ê = (E\{eχ }) ] E 0(S(e)(if e ∈ E\{eχ })Ŝ(e) =g ∗ (S 0 (e)) (if e ∈ E 0 )(T (e)(if e ∈ E\{eχ })T̂ (e) =∗0g (T (e)) (if e ∈ E 0 )(if v ∈ V 0 )vg(v) = (S(eχ ))i (if v = (I 0 )i )
(T (eχ ))i (if v = (O0 )i )60(fL (v) (if v ∈ V )fˆL (v) =fL0 (v) (if v ∈ V 0 )(fM (e) (if e ∈ E\{eχ })fˆM (e) =0 (e) (if e ∈ E 0 )fM
where eχ ∈ E is the hole edge labelled with χ, and (−)i denotes the i-th element of a list.
~0 , C 0 , χ~00 ], each edge comes from either C or C 0 . If a path inIn the resulting context C[χ~0 , C 0 , χ~00 ]. Conversely, if a
C does not contain the hole edge eχ , the path gives a path in C[χ~0 , C 0 , χ~00 ] consists of edges from C only, the path gives a path in C.
path in C[χ~0 , C 0 , χ~00 ]. However, if a path in C[χ~0 , C 0 , χ~00 ] consists ofAny path in C 0 gives a path in C[χedges from C 0 only, the path does not necessarily give a path in C 0 . The path indeed givesa path in C 0 , if sources and targets of the hole edge eχ are distinct in C (i.e. the hole edgeeχ is not a self-loop).

A.3. Rooted states
Lemma A.6. Let (X, _) is an abstract rewriting system that is deterministic.

1. For any x, y, y 0 ∈ X such that y and y 0 are normal forms, and for any k, h ∈ N, if
there exist two sequences x _k y and x _h y 0 , then these sequences are exactly thesame.
2. For any x, y ∈ X such that y is a normal form, and for any i, j, k ∈ N such thati 6= j and i, j ∈ {1, . . . , k}, if there exists a sequence x _k y, then its i-th rewritez _ z 0 and j-th rewrite w _ w0 satisfy z 6= w.

Proof. The point (1) is proved by induction on k + h ∈ N. In the base case, when k + h = 0(i.e. k = h = 0), the two sequences are both the empty sequence, and x = y = y 0 . The
inductive case, when k + h > 0, falls into one of the following two situations. The firstsituation, where k = 0 or h = 0, boils down to the base case, because x must be a normal
form itself, which means k = h = 0. In the second situation, where k > 0 and h > 0,
there exist elements z, z 0 ∈ X such that x _ z _k−1 y and x _ z 0 _h−1 y 0 . Because _is deterministic, z = z 0 follows, and hence by induction hypothesis on (k − 1) + (h − 1),these two sequences are the same.
The point (2) is proved by contradiction. The sequence x _k y from x to the normal
form y is unique, by the point (1). If its i-th rewrite z _ z 0 and j-th rewrite w _ w0
satisfy z = w, determinism of the system implies that these two rewrites are the same.
This means that the sequence x _k y has a cyclic sub-sequence, and by repeating thecycle different times, one can yield different sequences of rewrites x _∗ y from x to y.
This contradicts the uniqueness of the original sequence x _k y.
∗•Lemma A.7. If a state Ġ is rooted, a search sequence ?; |Ġ| →Ġ from the initial state?; |Ġ| to the state Ġ is unique. Moreover, for any i-th search transition and j-th searchtransition in the sequence such that i 6= j, these transitions do not result in the same state.

Proof. Let X be the set of states with search or value token. We can define an abstract•
rewriting system (X, _) of “reverse search” by: Ḣ _ Ḣ 0 if Ḣ 0 →Ḣ. Any search sequencecorresponds to a sequence of rewrites in this rewriting system.
••
The rewriting system is deterministic, i.e. if Ḣ 0 →Ḣ and H˙ 00 →Ḣ then Ḣ 0 = H˙ 00 ,−1
because the inverse 7→ of the interaction rules (Fig. 3) is deterministic.
61

If a search transition changes a token to a search token, the resulting search token always
has an incoming operation edge. This means that, in the rewriting system (X, _), initialstates are normal forms. Therefore, by Lem. A.6(1), if there exist two search sequencesfrom the initial state ?; |Ġ| to the state Ġ, these search sequences are exactly the same.
The rest is a consequence of Lem. A.6(2).
Lemma A.8. For any hypernet N , if there exists an operation path from an input to avertex, the path is unique. Moreover, no edge appears twice in the operation path.
Proof. Given the hypernet N whose set of (shallow) vertices is X, we can define an abstract
rewriting system (X, _) of “reverse connection” by: v _ v 0 if there exists an operationedge whose unique source is v 0 and targets include v. Any operation path from an input
to a vertex in N corresponds to a sequence of rewrites in this rewriting system.
This rewriting system is deterministic, because each vertex can have at most one incoming edge in a hypergraph (Def. 3.2) and each operation edge has exactly one source.
Because inputs of the hypernet N have no incoming edges, they are normal forms in thisrewriting system. Therefore, by Lem. A.6(1), an operation path from any input to any
vertex is unique.
The rest is proved by contradiction. We assume that, in an operation path P from an
input to a vertex, the same operation edge e appears twice. The edge e has one source,which either is an input of the hypernet N or has an incoming edge. In the former case, theedge e can only appear as the first edge of the operation path P , which is a contradiction.
In the latter case, the operation edge e has exactly one incoming edge e0 in the hypernet
N . In the operation path P , each appearance of the operation edge e must be precededby this edge e0 via the same vertex. This contradicts Lem. A.6(2).
Lemma A.9. For any rooted state Ġ, if its token source (i.e. the source of the token) does
not coincide with the unique input, then there exists an operation path from the input tothe token source.
∗•
Proof. By Lem. A.7, the rooted state Ġ has a unique search sequence ?; |Ġ| →Ġ. Theproof is by the length k of this sequence.
In the base case, where k = 0, the state Ġ itself is an initial state, which means the
input and token source coincide in Ġ.
• k−1•
In the inductive case, where k > 0, there exists a state Ġ0 such that ?; |Ġ| →
Ġ0 →
Ġ.
•
0
The proof here is by case analysis on the interaction rule used in Ġ → Ġ.

• When the interaction rules (1a), (1b), (2) or (5b) is used (see Fig. 3), the transition•
Ġ0 →Ġ only changes a token label.
•• When the interaction rule (3) is used, the transition Ġ0 →Ġ turns the token and its
outgoing operation edge eG0 into an operation edge eG and its outgoing token. By
induction hypothesis on Ġ0 , the token source coincides with its input, or there exists
an operation path from the input to the token source, in Ġ0 .

In the former case, in Ġ, the source of the operation edge eG coincides with the
input. The edge eG itself gives the desired operation path in Ġ.
In the latter case, the operation path PG0 from the input to the token source inĠ0 does not contain the outgoing operation edge eG0 of the token; otherwise, theedge eG0 must be preceded by the token edge in the operation path PG0 , which is acontradiction. Therefore, the operation path PG0 in Ġ0 is inherited in Ġ, becoming apath PG from the input to the source of the incoming operation edge eG of the token.
62In the state Ġ, the path PG followed by the edge eG yields the desired operationpath.
•Ġ changes the token from• When the interaction rule (4) is used, the transition Ġ0 →a (k + 1)-th outgoing edge of an operation edge e to a (k + 2)-th outgoing edge of thesame operation edge e, for some k ∈ N. In Ġ0 , the token source is not an input, andtherefore, there exists an operation path PG0 from the input to the token source, by
induction hypothesis.

The operation path PG0 ends with the operation edge e, and no outgoing edge ofthe edge e is involved in the path PG0 ; otherwise, the edge e must appear more thanonce in the path PG0 , which is a contradiction by Lem. A.8. Therefore, the path PG0
is inherited exactly as it is in Ġ, and it gives the desired operation path.
• When the interaction rule (5a) is used, by the same reasoning as in the case ofrule (4), Ġ0 has an operation path PG0 from the input to the token source, where theincoming operation edge eG0 of the token appears exactly once, at the end. Removing
the edge eG0 from the path PG0 yields another operation path P from the input inĠ0 , and it also gives an operation path from the input to the token source in Ġ.

Lemma A.10. For any state Ġ with a t-token such that t 6= ?, if Ġ is rooted, then there• ∗• +exists a search sequence ?; |Ġ| →hĠi?/t →Ġ.
∗•Proof. By Lem. A.7, the rooted state Ġ has a unique search sequence ?; |Ġ| →Ġ. Theproof is to show that a transition from the state hĠi?/t appears in this search seqeunce,and it is by the length k of the search sequence.
Because Ġ does not have a search token, k = 0 is impossible, and therefore the base•case is when k = 1. The search transition ?; |Ġ| →Ġ must use one of the interaction rules(1a), (1b), (2) and (5b). This means ?; |Ġ| = hĠi?/t .
k−1•
In the inductive case, where k > 0, there exists a state Ġ0 such that ?; |Ġ| →•Ġ.
The proof here is by case analysis on the interaction rule used in Ġ0 →

•
Ġ.
Ġ0 →

• When the interaction rule (1a), (1b), (2) or (5b) is used, ?; |Ġ| = hĠi?/t .
• Because Ġ does not have a search token, the interaction rules (3) and (4) can be•never used in Ġ0 →Ġ.
• When the interaction rule (5a) is used, Ġ0 has a value token, which is a (k + 1)-thoutgoing edge of an operation edge e, for some k ∈ N. The operation edge e becomes
the outgoing edge of the token in Ġ. By induction hypothesis on Ġ0 , we have
∗

+

•
•
•
?; |Ġ| →hĠ0 i?/X →
Ġ0 →
Ġ.

(A)

If k = 0, in Ġ0 , the token is the only outgoing edge of the operation edge e. BecausehĠ0 i?/X is not an initial state, it must be a result of the interaction rule (3), whichmeans the search sequence (A) is factored through as:
∗

+

•
•
•
•
?; |Ġ| →hĠi?/t →hĠ0 i?/X →
Ġ0 →
Ġ.

If k > 0, for each m ∈ {0, . . . , k}, let N˙m be a state with a search token, such that|N˙m | = |Ġ0 | and the token is an (m + 1)-th outgoing edge of the operation edge e.
This means Ṅk = hĠ0 i?/X . The proof concludes by combining the following internallemma with (A), taking k as m.
63• h ˙
Nm ,Lemma A.11. For any m ∈ {0, . . . , k}, if there exists h < k such that ?; |Ġ| →
• ∗
• + ˙
then it is factored through as ?; |Ġ| → hĠi?/t → Nm .

Proof. By induction on m. In the base case, when m = 0, the token of N˙m is thefirst outgoing edge of the operation edge e. This state is not initial, and therefore
must be a result of the interaction rule (3), which means• ∗•?; |Ġ| →hĠi?/t →N˙m .

In the inductive case, when m > 0, the state N˙m is not an initial state and must bea result of the interaction rule (4), which means∗••
˙ iX/? →?; |Ġ| →
hNm−1
N˙m .
• ∗
˙ iX/? , consists of h−1 <The first half of this search sequence, namely ?; |Ġ| →hNm−1
k transitions. Therefore, by (outer) induction hypothesis on h − 1, we have
• ∗
• +
•
˙ →
˙ iX/? →?; |Ġ| →
Nm−1
hNm−1
N˙m .
• ∗
˙ , consists of less than k transitions. Therefore,
The first part, namely ?; |Ġ| →Nm−1
by (inner) induction hypothesis on m − 1, we have
• ∗
• +
• +
•
˙ →
˙ iX/? →?; |Ġ| →hĠi?/t →
Nm−1
hNm−1
N˙m .

Lemma A.12.
1. For any state Ṅ , if it has a path to the token source that is not an operation path,then it is not rooted.
˙ with one hole edge, such
2. For any focus-free hypernet H and any focussed context C[χ]˙that C[H]is a state, if the hypernet H is one-way and the context C˙ has a path to˙
the token source that is not an operation path, then the state C[H]is not rooted.
˙ χ]; G;
~ H)
~ of an output-closed pre-tepmlate C, if the context
3. For any C-specimen (C[~˙C[~χ] has a path to the token source that is not an operation path, then at least one
˙ G]~ and C[˙ H]
~ is not rooted.
of the states C[
Proof of the point (1). Let P be the path in Ṅ to the token source that is not an operation
path. The proof is by contradiction; we assume that Ṅ is a rooted state.
Because of P , the token source is not an input. Therefore by Lem. A.9, the state Ṅ
has an operation path from its unique input to the token source. This operation pathcontradicts the path P , which is not an operation path, because each operation edge has
only one source and each vertex has at most one incoming edge.
Proof of the point (2). Let P be the path in C˙ to the token source that is not an operationpath.
˙
If the path P contains no hole edge, it gives a path in the state C[H]to the token sourcethat is not an operation path. By the point (1), the state is not rooted.
64

Otherwise, i.e. if the path P contains a hole edge, we give a proof by contradiction; we
˙assume that the state C[H]is rooted. We can take a suffix of the path P , so that it gives
˙ and moreover, gives a patha path from a target of a hole edge to the token source in C,0
˙
P from a source of an edge from H to the token source in C[H].
This implies the token
˙
source is not an input, and therefore by Lem. A.9, the state C[H] has an operation pathfrom its unique input to the token source. This operation path must have P 0 has a suffix,
meaning P 0 is also an operation path, because each operation edge has only one sourceand each vertex has at most one incoming edge. Moreover, H must have an operation
path from an input to an output, such that the input and the output have type ? and thepath ends with the first edge of the path P 0 . This contradicts H being one-way.
Proof of the point (3). Let P be the path in C˙ to the token source that is not an operation
path.
˙ G]
~ and C[˙ H]
~ to theIf the path P contains no hole edge, it gives a path in the states C[
token source that is not an operation path. By the point (1), the states are not rooted.
Otherwise, i.e. if the path P contains a hole edge, we can take a suffix of P that gives
˙ so that the path P 0
a path P 0 from a source of a hole edge e to the token source in C,
does not contain any hole edge. We can assume that the hole edge e is labelled with χ1 ,without loss of generality. The path P 0 gives paths PG0 and PH0 to the token source, in00
˙ 1 , G\{G~˙~
contexts C[χ1 }] and C[χ1 , H\{H1 }], respectively. The paths PG and PH are notan operation path, because they start with the hole edge e labelled with χ1 .
Because C is output-closed, G1 or H1 is one-way. By the point (2), at least one of the
˙ G]~ and C[˙ H]
~ is not rooted.
states C[
Lemma A.13. If a rewrite transition Ġ → Ġ0 is stationary, it preserves the rooted property, i.e. Ġ being rooted implies Ġ0 is also rooted.
Proof. The stationary rewrite transition Ġ → Ġ0 is in the form of C[ ;i H] → C[?;i H 0 ],where C is a focus-free simple context, H is a focus-free one-way hypernet, H 0 is a focusfree hypernet and i ∈ N. We assume C[ ;i H] is rooted, and prove that C[?;i H 0 ] is rooted,• ∗i.e. ?; C[H 0 ] →C[?;i H 0 ]. By Lem. A.10, there exists a number k ∈ N such that:
k

+

•
•
?; C[H] →C[?;i H] →C[ ;i H].

The rest of the proof is by case analysis on the number k.
• When k = 0, i.e. ?; C[H] = C[?;i H], the unique input and the i-th source of thehole coincide in the simple context C. Therefore, ?; C[H 0 ] = C[?;i H 0 ], which means
C[?;i H 0 ] is rooted.
k−1••• When k > 0, there exists a state Ṅ such that ?; C[H] →Ṅ →C[?;i H]. By thefollowing internal lemma (Lem. A.14), there exists a focussed simple context C˙N ,whose token is not entering nor exiting, and we have two search sequences:k−1•?; C[H] →k−1•?; C[H 0 ] →•C˙N [H] →C[?;i H],C˙N [H 0 ].

•The last search transition C˙N [H] →C[?;i H], which yields a search token, must use
the interaction rule (3) or (4). Because the token is not entering nor exiting in thesimple context C˙N , either of the two interaction rules acts on the token and an edge65

of the context. This means that the same interaction is possible in the state C˙N [H 0 ],yielding:• k−1 ˙•?; C[H 0 ] →CN [H 0 ] →C[?;i H 0 ],which means C[?;i H 0 ] is rooted.

m•
Lemma A.14. For any m ∈ {0, . . . , k − 1} and any state Ṅ such that ?; C[H] →
k−m
•
Ṅ →
C[?;i H], the following holds.
(A) If there exists a focussed simple context C˙N such that Ṅ = C˙N [H], the token of
the context C˙N is not entering.
(B) If there exists a focussed simple context C˙N such that Ṅ = C˙N [H], the token of
the context C˙N is not exiting.
• m(C) There exists a focussed simple context C˙N such that Ṅ = C˙N [H], and ?; C[H 0 ] →0C˙N [H ] holds.

Proof. Firstly, because search transitions do not change an underlying hypernet, if
there exists a focussed simple context C˙N such that Ṅ = C˙N [H], |C˙N | = C necessarily
holds.
The point (A) is proved by contradiction; we assume that the context C˙N has anentering token. This means that there exist a number p ∈ N and a token labelt ∈ {?, X, } such that C˙N = C[t;p H]. By Lem. A.10, there exists a number h suchthat h ≤ m and:
• h
• k−h
?; C[H] →C[?;p H] →C[?;i H].
($)
We derive a contradiction by case analysis on the numbers p and h.
– If p = i and h = 0, the state C[?;i H] must be initial, but it is a result of asearch transition because k − h > 0. This is a contradiction.
– If p = i and h > 0, two different transitions in the search sequence ($) result inthe same state, because of h > 0 and k − h > 0, which contradicts Lem. A.7.
– If p 6= i, by Def. 6.2, there exists a state Ṅ 0 with a rewrite token such that•
C[?;p H] →Ṅ 0 . This contradicts the search sequence ($), because k − h > 0 andsearch transitions are deterministic.

The point (B) follows from the contraposition of Lem. A.12(2), because H is oneway and Ṅ is rooted. The rooted property of Ṅ follows from the fact that searchtransitions do not change underlying hypernets.
The point (C) is proved by induction on m ∈ {0, . . . , k − 1}. In the base case, whenm = 0, we have ?; C[H] = Ṅ , and therefore the context ?; C can be taken as C˙N .
This means ?; C[H 0 ] = C˙N [H 0 ].
In the inductive case, when m > 0, there exists a state Ṅ 0 such that
m−1•?; C[H] →k−m••
Ṅ 0 →Ṅ →C[?;i H].

˙ 0 such that
By the induction hypothesis, there exists a focussed simple context CN
0˙
Ṅ = CN 0 [H] andm−1•?; C[H] →0• m−1?; C[H ] →

k−m

•
•
˙ 0 [H] →CNṄ →˙ 0 [H ].
CN
066

C[?;i H],Our goal here is to find a focussed simple context C˙N , such that Ṅ = C˙N [H] and•˙ 0 [H 0 ] →CNC˙N [H 0 ].
•˙ 0 [H] →In the search transition CN
Ṅ , the only change happens to the token and its
˙ 0 [H]. By the points (A) and (B), theincoming or outgoing edge e in the state CN
˙ 0 , which means the edge e musttoken is not entering nor exiting in the context CN
be from the context, not from H.
•
˙ 0 [H] →Now that no edge from H is changed in CN
Ṅ , there exists a focussed simple•
˙˙
˙ 0 [H 0 ] →context CN such that Ṅ = CN [H], and moreover, CNC˙N [H 0 ].

A.4. Accessible paths and stable hypernets
A stable hypernet always has at least one edge, and any non-output vertex is labelled with?. It has a tree-like shape.
Lemma A.15 (Shape of Stable Hypernets).
1. In any stable hypernet, if a vertex v 0
is reachable from another vertex v such that v 6= v 0 , there exists a unique path fromthe vertex v to the vertex v 0 .
2. Any stable hypernet has no cyclic path, i.e. a path from a vertex to itself.
3. Let C : ? ⇒ ⊗m
i=1 `i be a simple context such that: its hole has one source and at least
one outgoing edge; and its unique input is the hole’s source. There are no two stablehypernets G and G0 that satisfy G = C[G0 ].
Proof. To prove the point (1), assume there are two different paths from the vertex v tothe vertex v 0 . These paths, i.e. non-empty sequences of edges, have to involve an edge
with more than one source, or two different edges that share the same target. However,neither of these is possible in a stable hypernet, because both a passive operation edge
and an instance edge have only one source and vertices can have at most one incomingedge. The point (1) follows from this by contradiction.
If a stable hypernet has a cyclic path from a vertex v to itself, there must be infinitely
many paths from the input to the vertex v, depending on how many times the cycle isincluded. This contradicts the point (1).
The point (3) is also proved by contradiction. Assume that there exist two stablehypernets G and G0 that satisfy G = C[G0 ] for the simple context C. In the stable hypernet
G, a vertex is always labelled with ? if it is not an output. However, in the simple context
C, there exists at least one target of the hole that is not an output of the context but notlabelled with ? either. This contradicts C[G0 ] being a stable hypernet.
A stable hypernet can be found as a part of representation of a value.
Lemma A.16. Let ~x be a sequence of k variables and ~a be a sequence of h atoms. For
any derivable type judgement ~x | ~a ` v : ? where v is a value, its representation can be
decomposed as (~x | ~a ` v : ?)† = C[G] using a stable hypernet G : ? ⇒ ⊗m
i=1 `i and a simple
context C : ? ⇒ ?⊗k ⊗ ⊗h whose unique input coincides with a (unique) source of its hole.
Proof. By induction on the definition of value.
When the value v is an atom, in the representation (~x | ~a ` v : ?)† , only an instanceedge can comprise a stable hypernet.

67

When the value is v ≡ φX (v1 , . . . , vm ; ~s), by induction hypothesis, a stable hypernet Gi
can be extracted from (a bottom part of) representation of each eager argument vi . The
stable hypernet G that decomposes the representation (~x | ~a ` v : ?)† can be given by
all these stable hypernets G1 , . . . , Gm together with the passive operation edge φX that is
introduced in the representation.
When the value is v ≡ bind x → t in v 0 , or v ≡ new a ( t in v 0 , by induction hypothesis,
representation of the value v 0 includes a stable hypernet G0 . The stable hypernet itself
decomposes the representation (~x | ~a ` v : ?)† in the required way.
Lemma A.17. For any state Ṅ , and its vertex v, such that the vertex v is not a targetof an instance edge or a passive operation edge, if an accessible path from the vertex v isstable or active, then the path has no multiple occurences of a single edge.
Proof. Any stable or active path consists of edges that has only one source. As a consequence, except for the first edge, no edge appears twice in the stable path. If the stable
path is from the vertex v, its first edge also does not appear twice, because v is not atarget of an instance edge or a passive operation edge.
Lemma A.18. For any state Ṅ , and its vertex v, such that the vertex v is not a targetof an instance edge or a passive operation edge, the following are equivalent.
˙(A) There exist a focussed simple context C[χ]and a stable hypernet G, such that Ṅ =
˙
˙
C[G],
where the vertex v of Ṅ corresponds to a unique source of the hole edge in C.
(B) Any accessible path from the vertex v in Ṅ is a stable path.
Proof of (A) ⇒ (B). Because no output of a stable hypernet has type ?, any path from˙
the vertex v in C[G]gives a path from the unique input in G. In the stable hypernet G,
any path from the unique input is a stable path.
Proof of (B) ⇒ (A). In the state Ṅ , the token target has to be a source of an edge, whichforms an accessible path itself. By Lem. A.17, in the state Ṅ , we can take maximal stable
paths from the vertex v, in the sense that appending any edge to these paths, if possible,
does not give a stable path.
If any of these maximal stable paths is to some vertex, the vertex does not have type?; this can be confirmed as follows. If the vertex has type ?, it is not an output, so it
is a source of an instance, token, operation or contraction edge. The case of an instanceor passive operation edge contradicts the maximality. The other case yields a non-stable
accessible path that contradicts the assumption (B).
Collecting all edges contained by the maximal stable paths, therefore, gives the desired
hypernet G. These edges are necessarily all shallow, because of the vertex v of Ṅ . The
˙
focussed context C[χ],whose hole is shallow, can be made of all the other edges (at any
depth) of the state Ṅ .
Lemma A.19. Let Ṅ be a state, where the token is an incoming edge of an operationedge e, whose label φ takes at least one eager arguments. Let k denote the number of eager
arguments of φ.
For each i ∈ {1, . . . , k}, let sw i (Ṅ ) be a state such that: both states sw i (Ṅ ) and Ṅ havethe same token label and the same underlying hypernet, and the token in sw i (Ṅ ) is thei-th outgoing edge of the operation edge e.
For each i ∈ {1, . . . , k}, the following are equivalent.
(A) In Ṅ , any accessible path from an i-th target of the operation edge e is a stable(resp. active) path.
(B) In sw i (Ṅ ), any accessible path from the token target is a stable (resp. active) path.
68

Proof. The only difference between Ṅ and sw i (Ṅ ) is the swap of the token with the operation edge e, and these two edges form an accessible path in the states Ṅ and sw i (Ṅ ),individually or together (in an appropriate order). Therefore, there is one-to-one correspondence between accessible paths from an i-th target of the edge e in Ṅ , and accessible
paths from the token target in sw i (Ṅ ).
When (A) is the case, in Ṅ , any accessible paths from an i-th target of the edge e does
not contain the token nor the edge e; otherwise there would be an accessible path that
contains the token and hence not stable nor active, which is a contradiction. This means
that, in sw i (Ṅ ), any accessible path from the token target also does not contain the token
nor the edge e, and the path must be a stable (resp. active) path.
When (B) is the case, the proof takes the same reasoning in the reverse way.
Lemma A.20. Let Ṅ be a rooted state with a search token, such that the token is not an
incoming edge of a contraction edge.
+•
1. Ṅ →
hṄ iX/? , if and only if any accessible path from the token target in Ṅ is astable path.
+•
2. Ṅ →
hṄ i /? , if and only if any accessible path from the token target in Ṅ is anactive path.
∗•
Proof of the forward direction. Let t be either ‘X’ or ‘ ’. The assumption is Ṅ →hṄ it/? .
We prove the following, by induction on the length n of this search sequence:• any accessible path from the token target in Ṅ is a stable path, when t = X, and• any accessible path from the token target in Ṅ is an active path, when t = .
In the base case, where n = 1, because the token is not an incoming edge of a contraction
edge, the token target is a source of an instance edge, or an operation edge labelled withφ ∈ Ot that takes no eager argument. In either situation, the outgoing edge of the token
gives the only possible accessible path from the token target. The path is stable whent = X, and active when t = .
In the inductive case, where n > 1, the token target is a source of an operation edge eφlabelled with an operation φ ∈ Ot that takes at least one eager argument.
Let k denote the number of eager arguments of φt , and i be an arbitrary number in{1, . . . , k}. Let sw i (Ṅ ) be the state as defined in Lem. A.19. Because Ṅ is rooted,
by Lem. A.10, the given search sequence gives the following search sequence (proof by
induction on k − i):
∗

+

+

+

•
•
•
•
?; |Ṅ | →Ṅ →sw i (Ṅ ) →hsw i (Ṅ )iX/? →hṄ it/? .
+•By induction hypothesis on the intermediate sequence sw i (Ṅ ) →hsw i (Ṅ )iX/? , any accessible path from the token target in sw i (Ṅ ) is a stable path. By Lem. A.19, any accessible
path from an i-th target of the operation edge eφ in Ṅ is a stable path.
In Ṅ , any accessible path from the token target is given by the operation edge eφfollowed by an accessible path, which is proved to be stable above, from a target of eφ .
Any accessible path from the token target is therefore stable when t = X, and active whent= .

Proof of the backward direction. Let t be either ‘X’ or ‘ ’. The assumption is the following:• any accessible path from the token target in Ṅ is a stable path, when t = X, and69

• any accessible path from the token target in Ṅ is an active path, when t = .
∗•Our goal is to show Ṅ →hṄ it/? .
In the state Ṅ , the token target has to be a source of an edge, which forms an accessible
path itself. By Lem. A.17, we can define r(Ṅ ) by the maximum length of stable paths from• ∗the token target. This number r(Ṅ ) is well-defined and positive. We prove Ṅ →hṄ it/?
by induction on r(Ṅ ).
In the base case, where r(Ṅ ) = 1, the outgoing edge of the token is the only possible
accessible path from the token target. The outgoing edge is not a contraction edge by theassumption, and hence it is an instance edge, or an operation edge labelled with φ ∈ Ot•
that takes no eager argument. We have Ṅ →hṄ it/? .
In the inductive case, where r(Ṅ ) > 1, the outgoing edge of the token is an operationedge eφ labelled with φ ∈ Ot that takes at least one eager argument. Any accessible pathfrom the token target in Ṅ is given by the edge eφ followed by a stable path from a targetof eφ .
Let k denote the number of eager arguments of φt , and i be an arbitrary number in{1, . . . , k}. Let sw i (Ṅ ) be the state as defined in Lem. A.19.
By the assumption, any accessible path from an i-th target of the operation edge eφ inṄ is a stable path. Therefore by Lem. A.19, in sw i (Ṅ ), any accessible path from the token
target is a stable path. Moreover, these paths in Ṅ and sw i (Ṅ ) correspond to each other.
By Lem. A.17, we can define r(sw i (Ṅ )) by the maximum length of stable paths from thetoken target. This number r(sw i (Ṅ )) is well-defined, and satisfies r(sw i (Ṅ )) < r(Ṅ ). By
induction hypothesis on this number, we have:∗•sw i (Ṅ ) →hsw i (Ṅ )iX/? .

Combining this search sequence with the following possible search transitions concludes
the proof:•Ṅ →sw 1 (Ṅ ),•hsw i (Ṅ )iX/? →sw i+1 (Ṅ ),•hsw k (Ṅ )iX/? → hṄ it/? .

(when k 6= 1 and i < k)A.5. Parametrised (contextual) refinement and equivalence~0 , χ, χ~00 ] and C2 such that C1 [χ~0 , C2 , χ~00 ] isLemma A.21. For any focus-free contexts C1 [χ~0 , C2 , χ~00 ] is also binding-free.
defined, if both C1 and C2 are binding-free, then C1 [χ~0 , C2 , χ~00 ], and eχ denote the hole edge of C1 labelled with χ.
Proof. Let C denote C1 [χThe proof is by contradiction. We assume that there exists a path P in C, from a sourceof a contraction, atom, box or hole edge e, to a source of a hole edge e0 . We derive acontradiction by case analysis on the path P .
• When e0 comes from C1 , and the path P consists of edges from C1 only, the path P
gives a path in C1 that contradicts C1 being binding-free.
• When e0 comes from C1 , and the path P contains an edge from C2 , by finding thelast edge from C2 in P , we can take a suffix of P that gives a path from a target ofthe hole edge eχ to a source of a hole edge, in C1 . Adding the hole edge eχ at the
beginning yields a path in C1 that contradicts C1 being binding-free.
70• When both e and e0 come from C2 , and the path P gives a path in C2 , this contradicts
C2 being binding-free.
• When both e and e0 come from C2 , and the path P does not give a single path in C2 ,there exists a path from a source of the hole edge eχ to a source of the hole edge eχ ,in C1 . This path contradicts C1 being binding-free.
• When e comes from C1 and e0 comes from C2 , by finding the first edge from C2 in P ,we can take a prefix of P that gives a path from a source of a contraction, atom, box
or hole edge to a source of the hole edge eχ , in C1 . This path contradicts C1 being
binding-free.

Lemma A.22. For any set C of contexts that is closed under plugging, and any preorder
Q on natural numbers, the following holds.
˙ Q and C are reflexive.
• Q˙ Q and C are transitive.
• Q˙ Q and 'C• 'Q are equivalences.
C˙
˙ Q and 'C
Proof. Because 'Q are defined as a symmetric subset of Q and Q , respectively,C˙
˙ Q and 'C'
Q are equivalences if Q and Q are preorders.
˙ Q is a direct consequence of those of the preorder Q.
Reflexivity and transitivity of 
For any focus-free hypernet H, and any focus-free context C[χ] ∈ C such that ?; C[H] is˙ Q ?; C[H] because of reflexivity of ˙ Q.
a state, ?; C[H] For any focus-free hypernets H1 , H2 and H3 , and any focus-free context C[χ] ∈ C,C
such that H1 C
Q H2 , H2 Q H3 , and both ?; C[H1 ] and ?; C[H3 ] are states, our goal is˙ Q ?; C[H3 ]. Because H1 C H2 and H2 C H3 , all three hypernets
to show ?; C[H1 ] QQ
H1 , H2 and H3 have the same type, and hence ?; C[H2 ] is also a state. Therefore, we˙ Q ?; C[H2 ] and ?; C[H2 ] ˙ Q ?; C[H3 ], and the transitivity of ˙ Q implies
have ?; C[H1 ] ˙?; C[H1 ] Q ?; C[H3 ].

Lemma A.23. For any set C of contexts that is closed under plugging, and any preorder
Q on natural numbers, the following holds.
C
1. For any hypernets H1 and H2 , H1 'C
Q∩Q−1 H2 implies H1 'Q H2 .

2. If all compute transitions are deterministic, for any hypernets H1 and H2 , H1 'C
Q H2Cimplies H1 'Q∩Q−1 H2 .
Proof. Because (Q ∩ Q−1 ) ⊆ Q, the point (1) follows from the monotonicity of contextual
equivalence.
For the point (2), H1 'C
Q H2 means that any focus-free context C[χ] ∈ C, such that˙ Q ?; C[H2 ] and ?; C[H2 ] ˙ Q ?; C[H1 ]. If?; C[H1 ] and ?; C[H2 ] are states, yields ?; C[H1 ] 
the state ?; C[H1 ] terminates at a final state after k1 transitions, there exists k2 such that
k1 Q k2 and the state ?; C[H2 ] terminates at a final state after k2 transitions. Moreover,there exists k3 such that k2 Q k3 and the state ?; C[H1 ] terminates at a final state after k3transitions.
Because search transitions and copy transitions are deterministic, if all compute transitions are deterministic, states and transitions comprise a deterministic abstract rewriting71system, in which final states are normal forms. By Lem. A.6, k1 = k3 must hold. This
˙ Q∩Q−1 ?; C[H2 ]. Similarly, we can infer ?; C[H2 ] ˙ Q∩Q−1means k1 Q ∩ Q−1 k2 , and ?; C[H1 ] C?; C[H1 ], and hence H1 'Q∩Q−1 H2 .

A.6. Proof for Sec. 6.4
Lemma A.24. Let C be a set of contexts, and Q0 be a binary relation on N such that, forany k0 , k1 , k2 ∈ N, (k0 + k1 ) Q0 (k0 + k2 ) implies k1 Q0 k2 . Let C be a pre-template that is a12
˙
trigger and implies contextual refinement C
Q0 . For any single C-specimen (C[χ]; H ; H )of C, the following holds.
• k ˙
• k ˙
˙ 2] →
˙ 1] →
1. For any k ∈ N, ?; |C|[HC[H 1 ] if and only if ?; |C|[HC[H 2 ].

˙ 1 ] and C[H˙ 2 ] is2. If compute transitions are all deterministic, and one of states C[H
1
2
˙
˙
˙
rooted, then the other state is also rooted, and moreover, C[H ] Q0 C[H ].
Proof of the point (1). Let (p, q) be an arbitrary element of a set {(1, 2), (2, 1)}. We prove
• k ˙
• k ˙
˙ p] →
˙ q] →
that, for any k ∈ N, ?; |C|[HC[H p ] implies ?; |C|[HC[H q ]. The proof is by caseanalysis on the number k.
˙ p ] is initial, and by Lem. 7.5(1), C[H˙ q ] is also initial. Note that C• When k = 0, C[His a trigger and hence output-closed.
• k ˙˙ q] →• When k > 0, by the following internal lemma, ?; |C|[HC[H q ] follows fromk•˙ p] →
˙ p ].
?; |C|[HC[HLemma A.25. For any m ∈ {0, . . . , k}, there exists a focussed context Ċ 0 [χ] such˙ and the following holds:
that |Ċ 0 | = |C|• m 0• k−m ˙˙ p] →?; |C|[HĊ [H p ] →C[H p ],• m 0
˙ q] →?; |C|[HĊ [H q ].

˙ as Ċ 0 .
Proof. By induction on m. In the base case, when m = 0, we can take ?; |C|In the inductive case, when m > 0, by induction hypothesis, there exists a focussed
˙ and the following holds:
context Ċ 0 [χ] such that |Ċ 0 | = |C|• m−1 0• k−m+1 ˙
˙ p] →?; |C|[HĊ [H p ] →C[H p ],
• m−1 0˙ q] →?; |C|[HĊ [H q ].

˙ ∈ C, (Ċ 0 ; H 1 ; H 2 ) is a single C-specimen of C, which yields rooted
Because |Ċ 0 | = |C|
states. Because k − m + 1 > 0, Ċ 0 cannot have a rewrite token. The rest of the proof
is by case analysis on the token of Ċ 0 .

– When Ċ 0 has an entering search token, because C is a trigger, Ċ 0 [H r ] → hĊ 0 [H r ]i /?
for each r ∈ {p, q}. Because hĊ 0 [H r ]i /? = hĊ 0 i /? [H r ], and search transitions
are deterministic, we have the following:• m−1 0•• k−m ˙˙ p] →?; |C|[HĊ [H p ] →hĊ 0 i /? [H p ] →C[H p ],m−1•
˙ q] →?; |C|[H•Ċ 0 [H q ] →hĊ 0 i /? [H q ].

˙
We also have |hĊ 0 i /? | = |Ċ 0 | = |C|.
72

– When Ċ 0 has a value token, or a non-entering search token, because C is outputclosed, by Lem. 7.5(3), there exists a focussed context C˙00 such that |C˙00 | = |Ċ 0 |and Ċ 0 [H r ] → C˙00 [H r ] for each r ∈ {p, q}. The transition Ċ 0 [H r ] → C˙00 [H r ],for each r ∈ {p, q}, is a search transition, and by the determinism of searchtransitions, we have the following:• ˙00• k−m ˙• m−1 0˙ p] →
C[H p ],Ċ [H p ] →C [H p ] →?; |C|[H• m−1 0• ˙00
˙ q] →?; |C|[HĊ [H q ] →C [H q ].

˙ 1 ] and C[H˙ 2 ] is rooted, by the point (1), theProof of the point (2). If one of states C[H• k ˙˙ r] →
other state is also rooted, and moreover, there exists k ∈ N such that ?; |C|[HC[H r ]
for each r ∈ {1, 2}.
˙ 1 ] →k1 Ṅ1 ,Our goal is to prove that, for any k1 ∈ N and any final state Ṅ1 such that C[H˙ 2 ] →k2 Ṅ2 . Assuming
there exist k2 ∈ N and a final state Ṅ2 such that k1 Q0 k2 and C[H1k1
˙
C[H ] → Ṅ1 , we have the following:• k ˙
˙ 1] →?; |C|[HC[H 1 ] →k1 Ṅ1 ,• k ˙
˙ 2] →?; |C|[HC[H 2 ].

˙
Because C implies contextual refinement CQ0 , and |C| ∈ C, we have state refinement
˙ 1] 
˙ 2 ]. Therefore, there exist l2 ∈ N and a final state Ṅ2 such that˙ Q0 ?; |C|[H?; |C|[H˙ 2 ] →l2 Ṅ2 .
(k + k1 ) Q0 l2 and ?; |C|[H
The assumption that compute transitions are all deterministic implies that all transitions, including intrinsic ones, are deterministic. Following from this are l2 ≥ k and thefollowing:• k ˙
˙ 1] →?; |C|[HC[H 1 ] →k1 Ṅ1 ,• k ˙
˙ 2] →?; |C|[HC[H 2 ] →l2 −k Ṅ2 .

By the assumption on Q0 , (k + k1 ) Q0 l2 implies k1 Q0 (l2 − k).

73