The Geometry of Computation-Graph Abstraction
Koko Muroya

University of Birmingham, UK

Steven W. T. Cheung

University of Birmingham, UK

Abstract
The popular library TensorFlow (TF) has familiarised the mainstream of machine-learning community with programming language concepts such as data-flow computing and automatic differentiation. Additionally, it has introduced some genuinely new
syntactic and semantic programming concepts. In this paper westudy one such new concept, the ability to extract and manipulate
the state of a computation graph. This feature allows the convenient
specification of parameterised models by freeing the programmerof the bureaucracy of parameter management, while still permitting
the use of generic, model-independent, search and optimisation
algorithms. We study this new language feature, which we call
‘graph abstraction’ in the context of the call-by-value lambda calculus, using the recently developed Dynamic Geometry of Interaction
formalism. We give a simple type system guaranteeing the safetyof graph abstraction, and we also show the safety of critical language properties such as garbage collection and the beta law. The
semantic model suggests that the feature could be implemented ina general-purpose functional language reasonably efficiently.
CCS Concepts •Theory of computation → Semantics and reasoning; •Software and its engineering → Formal language definitions;
Keywords Geometry of Interaction, semantics of programming
languages, TensorFlow
ACM Reference format:
Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica. 2018. The Geometryof Computation-Graph Abstraction. In Proceedings of LICS ’18: 33rd Annual
ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom,
July 9–12, 2018 (LICS ’18), 24 pages.
DOI: 10.1145/nnnnnnn.nnnnnnn

1

TF as a programming language

TensorFlow (TF) is a popular and successful framework for machine learning, based on a data-flow model of computation [1].
It is programmable via an API, available in several mainstream
languages, which is presented as a shallowly embedded domainspecific language (DSL). As a programming language, TF has several
interesting features. First of all, it is a data-flow language, in which
the nodes are mathematical operations (including matrix operations), state manipulation, control flow operations, and various
low-level management operations. The programmer uses the hostlanguage, which can be Python, Java, Haskell etc., to construct a
language term (‘computation graph’). The graphs are computationally inert until they are activated in a ‘session’, in which they can
perform or be subjected to certain operations. Two such operations
are essential, execution and training. The execution is the usual
modus operandi of a data-flow graph, mapping inputs to outputs.
Training is the wholesale update of the stateful elements of a computation graph so that a programmer-provided error measure (‘loss
LICS ’18, Oxford, United Kingdom
2018. 978-x-xxxx-xxxx-x/YY/MM. . . $15.00
DOI: 10.1145/nnnnnnn.nnnnnnn

Dan R. Ghica

University of Birmingham, UK

function’) is minimised. The optimisation algorithm computing the
new state of the computation graph is also user provided, but it
may use automatic differentiation.
Many ingredients of TF are not new, in particular data-flow [8]and automatic differentiation [12]. However, the language quietly
introduced a striking new semantic idea, in order to support thetraining mode of operation of a computation graph, the wholesale
update of the stateful elements of a data-flow graph. To enable
this operation, the state elements of the graph can be collected
into a single vector (‘tensor’). These parameters are then optimised
by a generic algorithm, such as gradient descent, relative to thedata-flow graph itself and some loss function.
We are dissecting TF’s variable update into two simpler operations. The first one, which is the focus of this paper, is turning astateful computation graph into a function, parameterised by its
former state. We call this ‘graph abstraction’ (abs). The second
step is the actual update, which in the case of TF is imperative. In
this paper we will consider a functional update, realised simply byapplying the abstracted graph to the optimised parameters.
For the sake of simplicity and generality, we study graph abstraction in the context of a pure higher-order functional language
for transparent data-flow computation. In this language ‘sessions’are not required because computation graphs are intrinsic in thesemantics of the language. A term will be evaluated as a conventional computation or will result in the construction of a data-flow
graph, depending on its constituent elements. Consequently, any
term of the language can participate in the formation of data-flow
graphs, including lambda abstractions and open terms.
The blending of data-flow into a functional language is an ideawith roots in functional reactive programming [19], although oursemantic model is more akin to self-adjusting computation [2]. The
new feature is the ability to collect certain elements of the graph(‘variables’ in TF lingo, ‘cells’ in our terminology) into a single
data-structure, in order to update it as a whole. The way this ishandled in our language is by deprecating a data-flow graph into alambda expression with the collected cell vector as its argument.

x = tf . placeholder ( ” float ” )a = tf . Variable (1)b = tf . Variable (0)# C o n s t r u c t c o m p u t a t i o n graph f o r l i n e a r model
model = t f . add ( t f . m u l t i p l y ( x , a ) , b )with t f . S e s s i o n ( ) as s :s . run ( i n i t )# T r a i n t h e models . run ( o p t i m i s e r , d a t a , model , l o s s f u n c t i o n )# Compute y u s i n g t h e u p d a t e d m o d e l
y = s . run ( a ) ∗ 7 + s . run ( b )Figure 1. Linear regression in TF

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica

We call our calculus ‘idealised tensor flow’ (ITF). Let us see
how a basic example is handled in TF vs. ITF. For readability, we
use a simplified form of the Python bindings of TF. The programis a parameterised linear regression model, optimised then usedby applying it to some value (7), as in Fig. 1. The corresponding
program in ITF is given below:
let a = {1}
let b = {0}family of type- and name-indexed graph abstractions ATa ( f ,x ).t.
Graph abstraction as discussed in the introduction is defined assyntactic sugar abs t ≡ (A ( f ,x ).( f ,x )) t.
Let A ⊂fin A be a finite set of names, Γ a sequence of typed
variables x i :Ti , and p~ a sequence of elements of the field F (i.e. avector over F). We write A ` Γ if A is the support of Γ. The typejudgements are of shape: A | Γ | p~ ` t : T , and type derivation rules
are given below.
A ` Γ, T
A | Γ, x : T , ∆ | − ` x : T

let model x = a × x + b
let (model 0 ,p) = abs modelA | Γ |−`p :F

let model 00 = model 0 p 0~ ` t 2 : T2
A |Γ |q# : T1 → T2 → T~ ` t1 # t2 : T
A | Γ | p~, q

let y = model 7p ∈For, more concisely

A | Γ | p ` {p } : F

let (model 0 ,p) = abs (λx .{1} × x + {0})let y = model 0 (optimiser data p model 0 loss f unction) 7
In both TF and ITF a data-flow network corresponding to theexpression a × x + b is created, where a and b are variables (cells
respectively, indicated by {−}). New values of a and b are computedby an optimiser parameterised by the model, training data, anda loss function. As it is apparent, in TF the computation graphis constructed explicitly by using constructors such as tf.add andtf.multiply instead of the host language operators (+, ×). In contrast,in ITF a term is turned into a graph whenever cells are involved.
Another key difference is that in TF the variables are updated
in place by the optimiser, whereas in ITF the let ( f ,p) = abs tconstruct ‘abstracts’ a data-flow graph t into a regular function f ,while collecting the default values of its cells in a vector p.

ITF

Let F be a (fixed) set and A be a set of names (or atoms). Let(F, +, −, ×, /) be a field and {(Va , +a , ×a , •a )}a ∈A an A-indexed family of vector spaces over F. The types T of the languages are definedby the grammar T ::= F | Va | T → T . We refer to the field type
F and vector types Va as ground types. Besides the standard algebraic operations contributed by the field and the vector spaces, we
provide a family of fold operations folda , which are always overthe bases of the vector space indexed by a:0, 1,p : F+, −, ×, / : F → F → F~ `u :T
A |Γ |q~ `tu :TA | Γ | p~, q

A | Γ | p~ ` t 1 : T1

00

2

0

A | Γ | p~ ` λx T .t : T 0 → T

A | Γ | p~ ` t : T 0 → Tp ∈F

let p 0 = optimiser data p model 0 loss f unction

A | Γ, x : T 0 | p~ ` t : T(field constants)(operations of the field F)+a : Va → Va → Va

(vector addition)

×a : F → Va → Va(scalar multiplication)•a : Va → Va → F,(dot product)

folda : (Va → Va → Va ) → Va → Va

(fold)All vector operations are indexed by a name a ∈ A, and symbols +and × are overloaded. The role of the name a will be discussed later.
Throughout the paper, we use $ to refer to a ground-type operation(i.e. $ ∈ {+, −, ×, /, +a , ×a , •a | a ∈ A}), and # to refer to a primitive
operation (i.e. # ∈ {+, −, ×,/, +a , ×a , •a , folda | a ∈ A}).
Terms t are defined by the grammar t ::= x | λx T .t | t t | p | t #t | {p} | ATa ( f ,x ).t, where T is a type, f and x are variables, andp ∈ F is an element of the field. We identify t folda u with folda t u.
The novel syntactic elements of the language are cells {p} and a

A, a | Γ, f : Va → T 0, x : Va | p~ ` t : T

A ` Γ, T 0, T

0A | Γ | p~ ` ATa (f , x ).t : T 0 → T

Note that the rules are linear with respect to the cells p~. In a
derivable judgement A | Γ | p~ ` t : T , the vector p~ gives thecollection of all the cells in the term t.
0Graph abstraction ATa ( f ,x ).t serves as a binder of the name aand, therefore, it requires in its typing a unique vector type Vacollecting all the cells. Because of name a, this vector type cannot
be used outside of the scope of the graph abstraction. An immediate
consequence is that variables f and x used in the abstraction of agraph share the type Va , so that this type cannot be involved inother graph abstractions. This is a deliberate restriction, because
abstracting different graphs results in vectors of parameters of
unknown, at compile-time, sizes. Mixing such vectors would be asource of unsafe behaviour.

3

Graph-rewriting semantics

We first present an abstract machine, with roots in the Geometryof Interaction [11], which will be used to interpret the language.
The state of the machine is a graph with a selected edge (token) annotated with extra information. The token triggers graph rewriting
in a deterministic way by selecting redexes, and it also propagates
information through the graph. This abstract machine is a variant of the Dynamic GoI (DGoI) machine, which has been used togive uniform, cost-accurate models for call-by-need and call-byvalue computation [14, 15]. The graph-rewriting style of the DGoI
will prove to be a convenient execution model which matches thedata-flow-graph intuitions of TF and ITF. The interpretation is ‘operational’, in the sense that computational costs of its steps are at
most linear in the size of the program.
3.1

Graphs and graph states

A graph is defined by a set of nodes and a set of edges. The nodes
are partitioned into proper nodes and link nodes. A distinguishedlist of link nodes forms the input interface and another list of link
nodes forms the output interface. Edges are directed, with at least
one endpoint being a link node. An input link (i.e. a link in the
input interface) is the source of exactly one edge and the target of
no edge. Similarly an output link (i.e. a link in the output interface)is the source of no edge and the target of exactly one edge. Everyother link must be the source of one edge and the target of anotherone edge. A graph may contain adjacent links, but we identify
them as a single link, by the notion of ‘wire homeomorphism’ [13]The Geometry of Computation-Graph Abstraction

C

#

P

A

F

F

F !(Va ! T ) !Va

(~
p) ‡

Figure 2. Connection of edges

G(1, 0)H(1, n)=p0 ... pn 1

where

where H (1,n) contains no -nodes, p~ ∈ Fn , and cells are aligned left
to right according to the ordering. A graph is said to be definitive if
it contains no -nodes and all its output links have the cell type F.
The graph-rewriting semantics works on composite graphs.
!

!

used in a graphical formalisation of string diagrams. We may write
G (n,m) to indicate that a graph G has n links in the input interface
and m links in the output interface. From now on we will refer toproper nodes as just ‘nodes’, and link nodes as ‘links’.
Links are labelled by enriched types T̃ , defined by T̃ ::= T | !T | F
where T is any type of terms. Adjacent links are labelled with thesame enriched types, to be coherent with the wire homeomorphism.
If a graph has only one input, we call it ‘root’, and say the graph hasenriched type T̃ if the root has the enriched type T̃ . We sometimes
refer to enriched types just as ‘types’, while calling the enriched
type F ‘cell type’ and an enriched type !T ‘argument type’. Notethat the types used by the labels are ignored during execution, butthey make subsequent proofs easier.
Nodes are labelled, and we call a node labelled with X an ‘X node’. We have several sorts of labels. Some represent the basic
syntactic constructs of the lambda calculus: λ (abstraction), @ (application), p ∈ F (scalar constants), p~ ∈ Fn (vector constants), and# (primitive operations). Node P handles the decomposition of avector in its elements (coordinates). Node A indicates the graphabstraction. Nodes !, ?, D, and C play the same role as exponential
nodes in proof nets [10], handling sharing and copying for argument types. Adaptations of these nodes, namely , , and , arefor sharing (but not copying) of cells. Note that we use generalised
contractions (C, ) of any input arity, which includes weakening.
We sometimes write W (resp. ) to emphasise a contraction C(resp. ) has no inputs and hence is weakening.
We use the following diagrammatic conventions. Link nodes are
not represented explicitly, and their labels are only given when theycannot be easily inferred from the rest of the graph. By graphicalconvention, the link nodes at the bottom of the diagram represent
the input interface and they are ordered left to right; the link nodes
at the top of the diagram are the output, ordered left to right. A
double-stroke edge represents a bunch of edges running in parallel
and a double stroke node represents a bunch of nodes.
The connection of edges via nodes must satisfy the rules in Fig. 2,
where !T~ denotes a sequence !T1 , . . . , !Tm of enriched types, and# : T1 → T2 → T is a primitive operation. The outline box in
Fig. 2 indicates a sub-graph G (1,n 1 + n 2 ), called a !-box. Its input
is connected to one !-node (‘principal door’), while the outputs
are connected to n 1 ?-nodes (‘definitive auxiliary doors’), and n 2-nodes (‘provisional auxiliary doors’).
A graph context is a graph with exactly one distinguished nodethat has label ‘’ and any interfaces. We write a graph context
as G[] and call the unique extra -node ‘hole’. When a graph G
has the same interfaces as the -node in a graph context G[], we
write G[G] = G[/G] for the substitution of the hole by the graph
G. The resulting graph G[G] indeed satisfies the rules in Fig. 2,
thanks to the matching of interfaces.

=

(~
p) ‡

Definition 3.1 (Graph states). A graph state σ = ((G,e),δ ) consists of a composite graph G = H ◦ (p~) ‡ with a distinguished link e,
and token data δ = (d, f ,S,B) that consists of a direction d ::= ↑ | ↓,a rewrite flag f ::=  | λ | $ | ? | ! | F(n), a computation stack
S ::=  | @ : S | ? : S | λ : S | p : S | p~ : S, and a box stack
B ::=  | e 0 : B, where p ∈ F, p~ is a vector over F, n is a natural
number, and e 0 is a link of the graph G.
In the definition above we call the link e of (G,e) the ‘position’of the token. The rewrite flag determines the applicable graphrewriting. The computation stack tracks intermediate results ofprogram evaluation and the box stack tracks duplications. We callλ, scalar and vector constants ‘token values’. Together, the two
stacks determine the trajectory of the token, which models the flowof program evaluation.
3.2

Transitions

We define a relation on graph states called transition ((G,e),δ ) →((G 0 ,e 0 ),δ 0 ). Transitions are either pass or rewrite.
Pass transitions occur if and only if the rewrite flag is . Thesetransitions do not change the overall graph but only the token, as
shown in Fig. 3. In particular, the stacks are updated by changing
only a constant number of top elements. In the figure, only the nodetargeted by the token is shown, with token position and direction
indicated by a black triangle. The symbol ‘−’ denotes any token
value, k = k 1 $ k 2 , X ∈ { , , , D}, Y ∈ { , , } and Z ∈ {C, }.
The order of evaluation is right-to-left. A left-to-right applicationis possible, but more convoluted for ordinary programs where theargument is often of ground type. An abstraction node (λ) either
returns the token with a value λ at the top of the computation stackor triggers a rewrite, if @ is at the top of the computation stack,hence no a downward pass transition for application. The token
never exits an application node (@) downward due to rewrite rules
which eliminate λ-@ node pairs.
A ground-type operation ($) is applied to top two values of thecomputation stack, yielding a value k = k 1 $ k 2 , in its downward
pass transition. The downward pass transition over a fold operation
raises the rewrite flag F(n), using the size of the token value p~ ∈ Fn .
When passing a Z -node (i.e. C or ) upwards, the token pushes theold position e to the box stack. It uses the top element e 0 of thebox stack as a new position when moving downwards the Z -node,requiring e 0 to be one of the inputs of the node. The other nodes (?,A and P) only participate in rewrite transitions.
Rewrite transitions are written as
C

D
F

T
!T

D?!

p~
Va

T
!T
!Va

!

p
F

F

C

!
!T

T2
F

!

T

F

!

T1 ! T2

!

G

!

?
!

F

!T~

Finally, we say a graph G (1, 0) is composite, if its -nodes satisfy
the following: (i) they are outside !-boxes; (ii) there is a uniquetotal order on them; and (iii) their outputs are connected to (scalar)constant nodes. Each connected pair of a -node and a constant nodeis referred to as ‘cell’. A composite graph G (1, 0) can be uniquely
decomposed as below, and written as G = H ◦ (p~) ‡ :

D?!

D

T2

C

@

T1

!

!T

!

!T

!

T1 ! T2 !T1

!

T2

!

!

?

!

F !T1

!T~

LICS ’18, July 9–12, 2018, Oxford, United Kingdom((G[G],e), (d, f ,S,B)) → ((G[G 0 ],e 0 ), (d, f 0 ,S,B 0 ))

!

!

C

D ? !

C

W

C

?

LICS ’18, July 9–12, 2018, Oxford, United Kingdomp⇤, ? : S, B⇤,

: S, B, S, B

F

F

⇤,

!

!

@

@

#

#

X

X

⇤, S, B?, S, B⇤, S, B⇤, ? : S, B⇤, S, B⇤, ? : S, B⇤, S, B⇤, S, B

!

!

@

@

#

#

Y

Y

⇤, S, B⇤, S, B⇤, S, B⇤, ? : S, B⇤, S, B⇤, S, Bp⇤, ? : S, B ⇤, p : S, B

p~⇤, @ : S, B

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghicap~⇤, ? : S, B ⇤, p~ : S, B$⇤, k1 : k2 : ? : S, B

: p~ : S, B F(n), S, B⇤,

: S, B ⇤, @ : S, B

$

Z

Z

Z

Z

⇤, k : S, B⇤, S, B⇤, S, e : B⇤, S, e0 : B⇤, S, B

Figure 3. Pass transitions$, S, Bk⇤, S, B

Z2 Z1$$, S, B

Z2

G

$

~en 1
H1n :=!

⇤, S, BF

W G

F (0), S, B⇤, S, BD@!

Figure 4. Rewrite transitions: computation@?

and they apply to states where the rewrite flag is not , i.e. to whichpass transitions never apply. They replace the (sub-)graph G with
G 0 , keeping the interfaces, move the position, and modify the box
stack, without changing the direction and the computation stack.
We call the sub-graph G ‘redex’, and a rewrite transition ‘f -rewrite
transition’ if a rewrite flag is f before the transition.
The redex may or may not contain the token position e, but it
is always defined relative to it. We call a rewrite transition ‘local’
if its redex contains the token position, and ‘remote’ if not. Fig. 4,
Fig. 7b and Fig. 7c define local rewrites, showing only the redexes.
We explain some rewrite transitions in detail.
The rewrites in Fig. 4 are computational in the sense that they
are the common rewrites for CBV lambda calculus extended withconstants (scalars and vectors) and operations. The first rewrite is
the elimination of a λ-@ pair, a key step in beta reduction. Following
the rewrite, the incoming output link of λ will connect directly tothe argument, and the token will enter the body of the function.
Ground-type operations ($) also reduce their arguments, if they
are constants k 1 and k 2 , replacing them with a single constantk = k 1 $ k 2 . If the arguments are not constant-nodes (Z 1 and Z 2 in
the figure), then they are not rewritten out, leading to the creationof computation (data-flow) graphs when cells are involved.
Rewrite rules for the fold operations are in Fig. 5. Once therewrite flag F(n) is raised, the sub-graph G above the fold node (F)is recursively unfolded n times. This yields G itself with a weakening(W) if n = 0, and a graph Hnn otherwise. If n > 0, for any 0 < i < n,the i-th unfolding Hin inserts an application to the basis ~en−i ∈ Fn ,noting that the bases themselves are not syntactically available.
The rewrites in Figs. 7a–7c define three classes of rewrites involving !-boxes. They govern duplication of sub-graphs, and the
behaviour of graph abstraction, including application of its result
function. They are triggered by rewrite flags ‘?’ or ‘!’ whenever thetoken reaches the principal door of a !-box.
The first class of the !-box rewrites are remote rules, in which therewrites apply to parts of the graphs that have not been reached by
the token yet. A redex of a remote rule is determined relative to the

G

!

C

G

?

~en i

!
F

Hnn

Hin := D

Hin 1

!
@

F (n), S, B⇤, S, B?

⇤, S, B

Z1

?

$

@
, S, B

k2

?

k1

!
@

Figure 5. Rewrite transition: unfolding over the bases
token position, namely as a sub-graph of E in Fig. 6 that consists of
a !-box H , whose principal door is connected to either a A-node, aP-node with more than one inputs, a C-node, or another !-box. The
principal door of the !-box H has to satisfy the following: (i) the
node is ‘box-reachable’ (see Def. 3.2 below) from one of definitive
auxiliary doors of the !-box G (in Fig. 6), and (ii) the node is in thesame ‘level’ as one of definitive auxiliary doors of the !-box G, i.e.
the node is in a !-box if and only if the door is in the same !-box.
Definition 3.2 (Box-reachability). In a graph, a node/link v is boxreachable from a node/link v 0 if there exists a finite sequence of
directed paths p0 , . . . ,pi such that: (i) if i > 0, for any 0 ≤ j < i, thepath p j ends with the root of a !-box and the path p j+1 begins withan output link of the !-box, and (ii) the path p0 begins with v andthe path pi ends with v 0 .
We call the sequence of paths in the above definition ‘box-path’.
Box-reachability is more general than normal graph reachability,
since it may involve a !-box whose doors are not connected.
In order to define the remote rewrite rules let us introduce somenotation. We write G[X /Y ] for a graph G in which all Y -nodes are
replaced with X -nodes of the same signature, and write G[ϵ/Y ] fora graph G in which all Y -nodes (which must have one input andone output) are replaced with links. The remote rewrite rules are
given in Fig. 7a.

A

D

H

!

!

F !(Va ! T )

!Va

F

p~

!

!

!(Va ! T )

!Va

H

!
H

0

?

?

!

!

G

G

!T

!T

!

!

?, S, B?, S, B

C
C
?

?

?

C

!
!T

!T

!T

?

!

⇡sup(T ) · H?

⇡sup(T ) · H

!

!

H

⇡{a} · H

!
!Va
P

•

G

G

?

H

...

?

H

!

0

?

C

!

?

?

?

D

?
!

?

?

W

H[C/ , ?/ , D/ ]

?

C

H

H

?

?

?

!

?

H

?

W

?

?

G

G[C/ , ✏/ ]

?

P

?

G

(~
p) ‡

?

(~
p) ‡

LICS ’18, July 9–12, 2018, Oxford, United Kingdom?

The Geometry of Computation-Graph Abstraction

~e0

...

⇡{a} · H
•

!

!F

~en 1

!
!F

!F

!

!

?, S, B!, S, B(b) Rewrite transitions: merging !-boxes(a) Remote rules: graph abstraction, absorption, contraction, projection

G

?
!

!

!

!

D

Y

Y

C

?

G

?

G

⇡sup(T ) · G

...

!

!
!T

!, S, B⇤, S, B!, S, B⇤, S, B⇡sup(T ) · G!, S, e : B

?

?

?

?

G

C

G

...

⇡sup(T ) · G

!
!T

!T

!, S, B(c) Rewrite transitions: copying closed !-boxes

Figure 7. Rewrite transitions: !-boxes

F

?

?
G

?

?

F

E'

G

!

!

?, S, B?, S, B

Figure 6. Remote rules triggering
The top left remote rule is graph abstraction, that takes into
account the sub-graph G ◦ (p~) ‡ outside its redex (i.e. the !-box H ,its doors and the A-node). The sub-graph G ◦ (p~) ‡ contains exactly
all nodes that are graphically reachable, in a directed way, fromauxiliary doors ( ) of the !-box H . It is indeed a composite graph,with G containing only -nodes or -nodes, due to the typing. The
cells (p~) ‡ may not be all the cells of the whole graph, but a uniqueand total order on them can be inherited from the whole graph.
Upon applying the graph abstraction rule, the two input edgesof the A-node will connect to the result of graph abstraction, afunction and arguments. The function is created by replacing thecells (p~) ‡ with a projection (P), inserting a λ-node and a dereliction( ). A copy of the cells used by other parts of the graph is left
in place, which means the sub-graph G ◦ (p~) ‡ is left unchanged.
Another copy is transformed into a single vector node (p~) and linked
to the second input of graph abstraction, which now has access tothe current cell values. The unique and total ordering of cells (p~) ‡is used in introducing the P-node and the p~-node, and makes graphabstraction deterministic.
Note that the graph abstraction rule is the key new rule of thelanguage, and the other remote rules are meant to support andcomplement this rule. These remote rules can involve nodes only
reached by box-reachability, because we want all parameters of amodel to be extracted in graph abstraction, including those contributed, potentially, by its free variables. A ‘shallow’ local versionof graph abstraction would be simpler and perhaps easier to implement but not as powerful or interesting.
The bottom left remote rule eliminates a contraction node (C),and replicates the !-box H connected to the contraction. The bottom
right rule handles vector projections. Any graph H handling avector value with n dimensions is replicated n times to handle each
D

E

?

?

C

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica

coordinate separately. The projected value is computed by applying
the dot product using the corresponding standard base. In these tworules, the names in H are refreshed using the name permutation
action π N , where N ⊆ A, defined as follows: all names in N arepreserved, all other names are replaced with fresh (globally to thewhole graph) names.
Names indexing the vector types must be refreshed, because asa result of copying, any graph abstraction may be executed several times, and each time the resulting computation graphs andcells must be kept distinct from previously abstracted computationgraphs and cells. This is discussed in more depth in Appendix B, noting that in general types are ignored during execution but including
them in the graphs makes proofs easier.
The top right remote rule cause an ‘absorption’ of the !-box
H into the !-box H 0 it is connected to. Because the ?-nodes of!-boxes arise from the use of global or free variables, this boxabsorption process models that of closure-creation in a conventional
operational semantics. The !-box H 0 in Fig. 7a is required not to be
the !-box where the token position is.
The local version of absorption, where the lower !-box has thetoken position in it, belongs to the second class of !-box rewrites
shown in Fig. 7b. After this local absorption is exhaustively applied,
the rewrite flag changes from ‘?’ to ‘!’, and the last class of rewrites,shown in Fig. 7c are enabled. These rules handle copying of sharedclosed values, i.e. !-boxes accompanied by no ?-nodes.
The first two rules in Fig. 7c (Y < {D, C}) change rewrite mode topass mode, by setting the rewrite flag to . The third rewrite copies
a !-box. It requires the top element e of the box stack to be one of
input links of the contraction node (C). The link e determines the
copy of the !-box G that has the new token position in. As in the
remote duplication rule, names are refreshed in the new copies.
All transitions presented so far are well-defined.
Proposition 3.3 (Form preservation). All transitions send a graphstate to another graph state, in particular a composite graph G ◦ (p~) ‡to a composite graph G 0 ◦ (p~) ‡ of the same type.
Proof. Transitions make changes only in definitive graphs, keeping
the cells (p~) ‡ which contains only constant nodes and -nodes.
Transitions do not change redex interfaces.
!

Recall that we identify adjacent links in a graph as a single link,using wire homeomorphism. All transitions can be made consistent
with wire homeomorphism by incorporating the ‘identity’ passtransition that only changes the token position along a link.
All the pass transitions are deterministic and so are local rewrites.
Remote and copying rewrites are not deterministic but are confluent,
as no redexes are shared between rewrites. Therefore, the overall
beginning-to-end execution is deterministic.
Definition 3.4 (Initial/final states and execution). Let G be a composite graph with root e. An initial state Init (G) on the graph G
is given by ((G,e), (↑, ,? : , )). A final state Final(G,κ) on thegraph G, with a token value κ, is given by ((G,e), (↓, ,κ : , )).
An execution on the graph G is any sequence of transitions fromthe initial state Init (G).
Proposition 3.5 (Determinism of final states). For any graph state
σ , the final state Final(G,κ) such that σ →∗ Final(G,κ) is unique up
to name permutation, if it exists.
Proof. See Appendix A.

Corollary 3.6 (Determinism of executions). For any initial state
Init (H ), the final state Final(G,κ) such that Init (H ) →∗ Final(G,κ)
is unique up to name permutation, if it exists.
3.3

Translation of terms to graphs
A derivable type judgement A | Γ | p~ ` t : T is inductively translated
to a composite graph (A | Γ | p~ ` t : T ) † , as shown in Fig. 8,
where names in type judgements are omitted. The top left graphin the figure shows the general pattern of the translation, where(A | Γ | p~ ` t : T ) † has three components: weakening nodes (W),cells Pt = (p~) ‡ , and the rest G t . The translation uses variables
as additional annotations for links, to determine connection of
output links. In the figure, the annotation !Γ denotes the sequencex 0 : !T0 , . . . ,xm−1 : !Tm−1 of variables with enriched types, madefrom Γ = x 0 : T0 , . . . ,xm−1 : Tm−1 , and !∆ is made from ∆ in thesame way. The other annotations are restrictions of !Γ. Let FV(u) be
the set of free variables of a term u. The annotation !Γ1 , appearing
in inductive translations of typing rules with one premise, is the
restriction of !Γ to FV(t ), and !Γ0 is the residual. The annotations !Γt ,!Γt t 0 and !Γt 0 , in translations of typing rules with two premises, arerestrictions of !Γ to FV(t )\FV(t 0 ), FV(t ) ∩ FV(t 0 ) and FV(t 0 )\FV(t ),respectively. Note that the translation is not compositional in thecomponent of weakening nodes (W).
3.4Soundness

The first technical result of this paper is soundness, which expresses
the fact that well typed programs terminate correctly, which means
they do not crash or diverge. The challenge is, as expected, dealing
with the graph abstraction and related rules.
Theorem 3.7 (Soundness). For any closed program t such that A |− | p~ ` t : T , there exist a graph G and a token value κ such that:
Init ((A | − | p~ ` t : T ) ‡ ) →∗ Final(G,κ).
Our semantics produces two kinds of result at the end of theexecution. One, intensional result, is the graph G. It will involvethe cells of values p~ and computation depending on them, which
are not reduced during execution. The other one, extensional result,is the value κ carried by the token as it ‘exits’ the graph G. The
value κ will always be either a scalar, or a vector, or the symbol λindicating a function-value result.
The proof is given in Appendix G. It uses logical predicates on
definitive graphs, to characterise safely-terminating graphs inductively on types. The key step is to prove that graph abstraction
preserves the termination property of a graph, which involves ananalysis of sub-graphs that correspond to data-flow (i.e. groundtype computation only with cells, constants and ground-type operations). Graph abstraction enables more rewrites to be applied toa graph, by turning non-duplicable cells into duplicable function
arguments of ground types. Thanks to the call-by-value evaluation, the newly enabled rewrites can only involve the data-flow
sub-graphs and hence do not break the termination property.

4

Programming in ITF

Let us consider a more advanced example which will show how thetreatment of cells and graph abstraction in ITF reduces syntactic
overhead and supports our semantic intuitions. We create a linear model for a set of points in the plane corresponding to (x,y)
measurements from some instrument. The model must represent
the relationship between y and x not pointwise but as a confidence

The Geometry of Computation-Graph Abstraction

LICS ’18, July 9–12, 2018, Oxford, United Kingdom
p

Pt ! 1 ! 0( |W` p : F)† := p

FW

( | p ` {p} : F)† :=

D

Gt

!

!

( | p~ ` t : T )† :=

!

W

F

T
Pt ! 1 ! 0
Gt0( | p~ ` xT .t : T 0 ! T )† :=(if x 62 f v(t))

W

0

T !T

! 1

Pt

T !T

! 0

! 1
Pt

A
?
Gt

?
W

!

A
?

W ?
Gt

0

( | p~ ` ATa (f, x).t : T 0 ! T )† :=(if f 2 f v(t), x 62 f v(t))

D

T0 ! T

T0 ! T! t0 ! 0Pt

Pt0 ! t ! tt0

W

!

D

! tt0

! 0

Pt

W

?

?

Gt 0

?

?

( | p~, ~q ` folda t t0 : Va )† :=

Gt

Gt 0

!

!

!

?

?

?

! t ! tt0

! t0 ! 0?

( | p~, ~q ` t $ t : T ) :=

Gt

Gt 0

!

!

D

D

0

? ?

! t0 ! 0

C

C

C

Pt 0

?

?
0

?

?

( | p~ ` ATa (f, x).t : T 0 ! T )† :=(if f, x 2 f v(t))( | p~, ~q ` t t0 : T )† := Gt` x : T )† := W D W|( , x : T,

W

T

0

Pt Pt 0 ! t

Gt

W

†

W

?

0

( | p~ ` xT .t : T 0 ! T )† :=(if x 2 f v(t))!Γ !T !Δ

! 1! 0

Pt

?

@

F

$

T

T

T

? ?
W

Figure 8. Inductive translationinterval. Concretely, let us look at two (parameterised) such models: linear regression with confidence interval (CI) and weighted
regression (WR) [4]. The first model is suitable when training data
has measurement errors independent of the value of x, while thesecond model is suitable when errors vary linearly with x.1
Let pair = λx .λy.λz.z x y be the Church-encoding of pairs and let
f = λa.λb.λx .a ×x +b be a generic linear function with unspecified
parameters a and b. Let opt ci and opt wr be generic learning
functions that can be applied to some model m and seed p, definedelsewhere, suitable for CI and WR, respectively, incorporating thereference data points, suitable loss functions, and optimisation
algorithms.
An ITF program for the confidence-interval model is shown
below, emphasising each step in the construction.
let a = {1}let ci = pair ( f a {1}) ( f a {2})let (pcim,p) = abs ci(confidence interval)(parameterised CI model)

1 These examples and more can be explored in the online visualiser: https://cwtsteven.

github.io/GoI-TF-Visualiser/

let pci = opt ci pcim

(learn CI parameters)

let cim = pcim pci(concrete CI model)

The model consists of a pair of linear functions which share thesame slope (a) but may have different intercepts. The graph abstraction turns the computation graph ci into a conventional function
pcim which will take three parameters. However, the number ofparameters of the function is hidden into the vector type of theargument. The generic optimisation function opt ci will computethe best values for the parameters (pci) which can be then used tocreate a concrete model cim which can be then used, as a regularfunction, in the subsequent program.
In contrast, the weighted-regression model is a pair of independent linear functions. The structure of the program is otherwise
similar.
let wr = pair ( f {1} {0}) ( f {1} {0})(weighted regression)let (pwrm,p) = abs wr(parameterised WR model)

let pwr = opt wr pwrm

(learn WR parameters)

let wrm = pwrm pwr(concrete WR model)

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica

P

P

C
1

1

2

?

?

¡

¡

¡

?

?

C
¿

¿

¿

¿

¿
¿

f’

f’

!

!

¿

f’

¿

!

?

1

?
?

0

¡

?

f’
!

pair’

pair’

¡

¡
¿

¿

¿

¿

f’

f’

!

!

?

?

?

?

?

!

f’

f’

!

!

pair’
!
D

!

[1;0;1;0]

?

?

A
?

A

?

λ

pair’

[1;1;2]

!
?

G

G

!

!

!
?

?
?

G

G

!

!

Figure 9. Graph-abstracting the CI model

These codes can be written more concisely, e.g.
let ci = (λa.pair ( f a {1}) ( f a {2})) {1}
let cim = (A(pcim,p).pcim (opt ci pcim)) ci
let wr = pair ( f {1} {0}) ( f {1} {0})let wrm = (A(pwrm,p).pwrm (opt wr pwrm)) wr
This relatively simple example illustrates several key features of
ITF. First, there is no distinction between regular lambda terms anddata-flow graphs. A higher-order computation graph is constructed
automatically. Second, cells are treated as references rather thanas constants, ensuring that the programmer has a grasp on how
many parameters can be adjusted by the optimiser. For CI there arethree parameters, the (shared) slope and two intercepts, whereas
for WR there are four parameters, two slopes and two intercepts.
Third, cells are collected into parameters of the graph-abstracted
function not just from the term to which abs is applied, but fromits free variables as well.
The key step in both examples is the graph abstraction. Figs. 910 show how the two models differ. The !-box G represents the
programming context when graph abstraction is triggered. Preabstraction the computation graphs of CI share a cell, resulting postabstraction in a function with a shared argument. In contrast, theWR computation graph and resultant function involve no sharing.
In the absence of graph abstraction, the obvious alternatives ina functional setting, such as explicitly parameterising models with
vectors involves error-prone index manipulation to control sharing([k 0 ; . . . ; km ] is a vector and p[i] is element access), for example:
let f p x = p[0] × x + p[1]let ci p = pair ( f [p[0]; p[1]]) ( f [p[0]; p[2]])let cim = ci (opt ci ci)
let wr p = pair ( f [p[0]; p[1]]) ( f [p[2]; p[3]])The alternatives are comparably awkward.

¡

¿
¿

!

!

let wrm = wr (opt wr wr )

0

¿

λ

!

1

¿

D

?

?

?

Figure 10. Graph-abstracting the WR model

5

Contextual equivalence

Usually programs (closed ground-type terms) are equated if andonly if they produce the same values. However in the presence ofcells, this is not enough. For example, evaluating programs {1} + 2,
1 + 2 and 1 + {2} yields the same token value (3) but different final
graphs, which can be made observable by graph abstraction.
Definition 5.1 (Token-value equivalence). Two composite graphs
G 1 (0, 1) and G 2 (0, 1) are token-value equivalent, written as G 1 =G
˙ 2,
if there exists a token value κ such that the following are equivalent: Init (G 1 ) →∗ Final(G 10 ,κ) for some composite graph G 10 , andInit (G 2 ) →∗ Final(G 20 ,κ) for some composite graph G 20 .
We lift token-value equivalence to a congruence by definition,
just like the usual program equivalence is lifted to open terms.
Definition 5.2 (Graph-contextual equivalence). Two graphs G 1 (n,m)
and G 2 (n,m) are graph-contextually equivalent, written as G 1  G 2 ,if for any graph context G[] that makes two composite graphs
G[G 1 ] and G[G 2 ] of ground type, the token-value equivalenceG[G 1 ]=G[G˙2 ] holds.
The graph-contextual equivalence  is indeed an equivalence
relation, and also a congruence with respect to graph contexts.
We say a binary relation R on graphs implies graph-contextual
equivalence, if R ⊆ .
In the DGoI machine, the token always moves along a node,
and a redex can always be determined as a sub-graph relative tothe token position. This locality of the machine behaviour enables
us to give some instances of the graph-contextual equivalence bymeans of the following variant of simulation, ‘U-simulation’. Let(·) + stand for the transitive closure of a binary relation.
Definition 5.3 (U-simulation). A binary relation R on graph states
is a U-simulation, if it satisfies the following two conditions. (I) If
σ1 R σ2 and a transition σ1 → σ10 is possible, then (i) there exists agraph state σ20 such that σ2 → σ20 and σ10 R + σ20 , or (ii) there exists
a sequence σ10 →∗ σ2 of (possibly no) transitions. (II) If σ1 R σ2
and no transition is possible from the graph state σ1 , then there
exist composite graphs G 1 and G 2 and a token value κ such that
σ1 = Final(G 1 ,κ) and σ2 = Final(G 2 ,κ).

The Geometry of Computation-Graph Abstraction

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

Intuitively, a U-simulation is the ordinary simulation between
two transition systems (the condition (I-i) in the above definition),‘Until’ the left sequence of transitions is reduced to the right sequence (the condition (I-ii)). The reduction may not happen, which
resembles the weak until operator of linear temporal logic. The condition (I-i) involves the transitive closure R + , in case the reduction
steps are multiplied.
Proposition 5.4. Let R be a U-simulation. If σ1 R σ2 , then there
exists a token value κ such that the following are equivalent: σ1 →∗Final(G 1 ,κ) for some composite graph G 1 , and σ2 →∗ Final(G 2 ,κ)for some composite graph G 2 .
Proof. See Appendix H.

We will use U-simulations to see if some rewrites on graphs,
which may or may not be triggered by the token, imply the graphcontextual equivalence.
Proposition 5.5. Let ≺ be a binary relation on graphs with thesame interface, and its lifting ≺ on graph states defined as follows:((G[G 1 ],e),δ ) ≺ ((G[G 2 ],e),δ ) iff G 1 ≺ G 2 and the position e is in
the graph-context G[]. If the lifting ≺ is a U-simulation, the binary
relation ≺ implies the graph-contextual equivalence .
Proof. We assume G 1 ≺ G 2 , and take an arbitrary graph context G[] that makes two composite graphs G[G 1 ] and G[G 2 ].
The lifting ≺ relates initial states on these composite graphs, i.e.
G[G 1 ] ≺ G[G 2 ]. Therefore, if it is a U-simulation, these two graphs
are token-value equivalent G[G 1 ]=G[G˙2 ], by Prop. 5.4. We canconclude the graph-contextual equivalence G 1  G 2 .
Finally, the notion of contextual equivalence of terms can be
defined as a restriction of the graph-contextual equivalence, tograph-contexts that arise as translations of (syntactical) contexts.
Definition 5.6 (Contextual equivalence). Two terms A | Γ | p~ ` ti :T 0 (i = 1, 2) in the same derivable type judgement are contextuallyequivalent, written as A | Γ | p~ ` t 1 ≈ t 2 : T 0 , if for any context
Ch·iT such that the two type judgements A | Γ | q~ ` Chti i : T(i = 1, 2) are derivable for some vector q~ and some ground type T ,the token-value equivalence (A | Γ | q~ ` Cht 1 i : T ) † =(A˙| Γ | q~ `Cht 2 i : T ) † holds.
5.1

Garbage collection

Large programs generate sub-graphs which are unreachable andunobservable during execution (garbage). In the presence of graphabstraction the precise definition is subtle, and the rules for garbage
collection are not obvious. We show safety of some forms of garbage
collection, as below.
Proposition 5.7 (Garbage collection). Let ≺W , ≺W 0 and ≺GC bebinary relations on graphs, defined by
?

?
W0

G

!

GC

W

W

W

C

C

W

W

C

C

X0

where the X -node is either a W-node, or a P-node with no input. They
altogether imply the graph-contextual equivalence, i.e. ≺W ∪ ≺W 0
∪ ≺GC implies the graph-contextual equivalence.

Sketch of proof. The relation ≺W ∪ ≺W 0 ∪ ≺GC lifts to a U-simulation,
where the condition (I-ii) in Def. 5.3 is not relevant. We then use
Prop. 5.5.

5.2

Beta equivalence

We can prove a form of beta equivalence, where the function argument is a closed value without cells. The substitution t[u/x]is defined as usual. The proof is by making U-simulations out ofspecial cases of λ-rewrites and !-rewrites, and is also by the garbage
collection shown above.
Proposition 5.8 (Beta equivalence). Let v be a value defined by
the grammar v ::= p | λx T .t | ATa ( f ,x ).t. If the type judgement
A0 | − | − ` v : T 0 is derivable, the contextual equivalence A | Γ |0p~ ` (λx T .t ) v ≈ t[v/x] : T holds.
Sketch of proof. See Appendix H.1.

6

Conclusion and related work

Machine learning can take advantage of a novel programming
idiom, which allows functions to be parameterised in such a waythat a general purpose optimiser can adjust the values of parameters
embedded inside the code. The nature of the programming language
design challenge is an ergonomic one, making the bureaucracy ofparameter management as simple as possible while preserving
soundness and equational properties. In this paper we do not aim
to assess whether the solution proposed by TF reflects the best
design decisions, but we merely note that automating parameter
management requires certain semantic enhancements which are
surprisingly complex.
The new feature is the extraction of the variable-dependencies
of a computation graph (the parameters) into a single vector, which
can be then processed using generic functions. Moreover, we place
this feature in an otherwise pure, and quite simple, programming
language in order to study it semantically (ITF). Our contribution
is to provide evidence that this rather exotic feature is a reasonableaddition to a programming language: typing guarantees safety of
execution (soundness), garbage collection is safe, and a version of
the beta law holds. Moreover, the operational semantics does not
involve inefficient (worse than linear) operations, indicating a goodpotential for implementability. Reaching a language comparable
in sophistication and efficiency with TF is a long path, but we aremaking the first steps in that direction [3]. The advantages of using
a stand-alone language, especially when there is evidence that it
has a reasonably well behaved semantics, are significant, as EDSLs
suffer from well known pitfalls [18].
Other than TF, we only know of one other language which
supports the ability to abstract on state (‘wormholing’), with asimilar motivation but with a different application domain, data
science [17]. For keeping the soundness argument concise the language lacks recursion, but sound extensions of GoI-style machineswith this feature have been studied in several contexts and we
do not think it presents insurmountable difficulties [5, 16]. Further extensions of the language, in particular effects, pose serious
challenges however.
We chose to give a semantics to ITF using the Dynamic Geometryof Interaction (DGoI) [14, 15], a novel graph-rewriting semantics
initially used to give cost-accurate models for various reduction
strategies of the lambda calculus. The graph model of DGoI is
already, in a broad sense, a data-flow graph with higher-order

LICS ’18, July 9–12, 2018, Oxford, United Kingdom
features, which is a natural fit for the language we aim to model.
The semantics of call-by-value lambda calculus is based on the
one in [15], where it is shown to be efficient, in a formal sense.
In this paper we do not formally analyse the cost model of ITF
but we can see, at least informally, that the operations involved inhandling language extensions such as cells, computation graphs,
and graph abstraction are not computationally onerous. Some of
the more expensive operations, such as box-reachability, could be
implemented in constant time using ‘jump links’ between the endpoints of a path, thus trading off space and time costs. The idea ofjumping can be found in the GoI literature [7, 9].
Pragmatically speaking, even though the infrastructure required
to support computation graphs and graph abstraction involves a
non-negligible overhead, the impact of this overhead on the runningcost of a typical machine-learning program as a whole is negligible.
This is because the running cost of machine-learning programs isdominated by the learning phase, realised by the optimisers. This
phase involves only ‘conventional’ functions, the result of graphabstraction, in which all the overhead can be simply discarded assuperfluous. This overhead is only required in the model creation
phase, which is not computationally intensive.
This paper represents a first step in the study of ITF, focussingon what we believe to be the most challenging semantic feature of
the language. In the future we plan to study the execution modeof the graphs, by propagating automatically changes to the cells
through the graph, much like in incremental or self-adjusting computation, and the way such features interact with graph abstraction.
Finally, in the longer term, to develop a usable functional counterpart of TF we also aim to incorporate a safe version of automaticdifferentiation, as well as probabilistic execution.

References[1] Martı́n Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen,
Craig Citro, Greg S Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, et al.
2016. Tensorflow: Large-scale machine learning on heterogeneous distributed
systems. arXiv preprint arXiv:1603.04467 (2016).
[2] Umut A. Acar, Matthias Blume, and Jacob Donham. 2013. A consistent semantics
of self-adjusting computation. J. Funct. Program. 23, 3 (2013), 249–292.
[3] Steven Cheung, Victor Darvariu, Dan R. Ghica, Koko Muroya, and Reuben N. S.
Rowe. 2018. A functional perspective on machine learning via programmableinduction and abduction. In FLOPS 2018. (forthcoming).
[4] William S Cleveland. 1979. Robust locally weighted regression and smoothing
scatterplots. Journal of the American statistical association 74, 368 (1979), 829–836.
[5] Ugo Dal Lago, Claudia Faggian, Benoı̂t Valiron, and Akira Yoshimizu. 2015.
Parallelism and synchronization in an infinitary context. In LICS 2015. IEEE,
559–572.
[6] Vincent Danos and Laurent Regnier. 1989. The structure of multiplicatives. Arch.
Math. Log. 28, 3 (1989), 181–203.
[7] Vincent Danos and Laurent Regnier. 1996. Reversible, irreversible and optimallambda-machines. Elect. Notes in Theor. Comp. Sci. 3 (1996), 40–60.
[8] Jack B Dennis. 1974. First version of a data flow procedure language. In Programming Symposium. Springer, 362–376.
[9] Maribel Fernández and Ian Mackie. 2002. Call-by-value lambda-graph rewriting
without rewriting. In ICGT 2002 (LNCS), Vol. 2505. Springer, 75–89.
[10] Jean-Yves Girard. 1987. Linear logic. Theor. Comp. Sci. 50 (1987), 1–102.
[11] Jean-Yves Girard. 1989. Geometry of Interaction I: interpretation of system F.
In Logic Colloquium 1988 (Studies in Logic & Found. Math.), Vol. 127. Elsevier,
221–260.
[12] Andreas Griewank et al. 1989. On automatic differentiation. Mathematical
Programming: recent developments and applications 6, 6 (1989), 83–107.
[13] Aleks Kissinger. 2012. Pictures of processes: automated graph rewriting formonoidal categories and applications to quantum computing. arXiv preprint
arXiv:1203.0202 (2012).
[14] Koko Muroya and Dan R. Ghica. 2017. The dynamic Geometry of Interaction
machine: a call-by-need graph rewriter. In CSL 2017 (LIPIcs), Vol. 82.
[15] Koko Muroya and Dan R. Ghica. 2017. Efficient implementation of evaluation
strategies via token-guided graph rewriting. In WPTE 2017.
[16] Koko Muroya, Naohiko Hoshino, and Ichiro Hasuo. 2016. Memoryful Geometryof Interaction II: recursion and adequacy. In POPL 2016. ACM, 748–760.

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica[17] Tomas Petricek. Retrieved 2017. Design and implementation of a live coding
environment for data science. (Retrieved 2017). http://tomasp.net/academic/
drafts/live/live.pdf.
[18] Josef Svenningsson and Emil Axelsson. 2015. Combining deep and shallow embedding of domain-specific languages. Computer Languages, Systems & Structures
44 (2015), 143–165. https://doi.org/10.1016/j.cl.2015.07.003[19] Zhanyong Wan and Paul Hudak. 2000. Functional reactive programming fromfirst principles. ACM sigplan notices 35, 5 (2000), 242–252.

The Geometry of Computation-Graph Abstraction

A

Determinism

The only sources of non-determinism are the choice of fresh names
in replicating a !-box and the choice of ?-rewrite transitions (Fig. 7aand Fig. 7b). Introduction of fresh names has no impact on execution, as we can prove ‘alpha-equivalence’ of graph states.

LICS ’18, July 9–12, 2018, Oxford, United Kingdom
Uniqueness. The name a is not free, and is bound by exactly
one A-node.
Scope. Bound names do not appear in types of input links ofthe graph G. Moreover, if the A-node that binds the namea is in a !-box, the name a appears only strictly inside the!-box (i.e. in the !-box, but not on its interfaces).

Proposition A.1 (‘Alpha-equivalence’ of graph states). The binary
relation ∼α of two graph states, defined by ((G,e),δ ) ∼α ((π ·G,e),δ )for any name permutation π , is an equivalence relation and a bisimulation.

The name permutation action accompanying rewrite transitions(Fig. 7a and Fig. 7c) is an explicit way to preserve the above requirement in transitions.

Proof. Only rewrite transitions that replicate a !-box (in Fig. 7a andFig. 7c) involve name permutation. Names are irrelevant in all theother transitions.


Proposition B.3 (Preservation of bound-name criterion). In anytransition, if an old state meets the bound-name criterion, so does a
new state.

We identify graph states modulo name permutation, namely thebinary relation ∼α in the above proposition. Now non-determinism
boils down to the choice of ?-rewrites, which however does notyield non-deterministic overall executions.

Proof. In a ?-rewrite transition that eliminates a A-node, the namea ∈ A bound by the A-node turns free. As the name a is not boundby any other A-nodes, it does not stay bound after the transition.
The transition does not change the status of any other names, andtherefore preserves the uniqueness and scope of bound variables.
Duplication of a !-box, in a rewrite transition involving a C-nodeor a P-node applies name permutation. The scope of bound names
is preserved by the transition, because if an A-node is duplicated, alllinks in which the name bound by the A-node appears are duplicatedtogether. The scope also ensures that, if an A-node is copied, thename permutation makes each copy of the node bind distinct names.
Therefore the uniqueness of bound names is not broken by thetransition.
Any other transitions do not change the status of names.
Proposition A.2 (Determinism). If there exists a sequence((G,e),δ ) →∗ ((G 0 ,e 0 ), (d 0 , ,S 0 ,B 0 )),any sequence of transitions from the state ((G,e),δ ) reaches the state((G 0 ,e 0 ), (d 0 , ,S 0 ,B 0 )), up to name permutation.
Proof. The applicability condition of ?-rewrite rules ensures thatpossible ?-rewrites at a state do not share any redexes. Therefore ?rewrites are confluent, satisfying the so-called diamond property: if
two different ?-rewrites ((G,e),δ ) → ((G 1 ,e 1 ),δ 1 ) and ((G,e),δ ) →((G 2 ,e 2 ),δ 2 ) and are possible from a single state, both of the data δ 1
and δ 2 has rewrite flag ?, and there exists a state ((G 0 ,e 0 ),δ 0 ) suchthat ((G 1 ,e 1 ),δ 1 ) → ((G 0 ,e 0 ),δ 0 ) and ((G 2 ,e 2 ),δ 2 ) → ((G 0 ,e 0 ),δ 0 ).
Corollary A.3 (Prop. 3.5). For any graph state σ , the final state
Final(G,κ) such that σ →∗ Final(G,κ) is unique up to name permutation, if it exists.
Corollary A.4 (Cor. 3.6). For any initial state Init (G), the final state
Final(G,κ) such that Init (G) →∗ Final(G,κ) is unique up to namepermutation, if it exists.

B

ValidityThis section investigates a property of graph states, validity, whichplays a key role in disproving any failure of transitions. It is basedon three criteria on graphs.
In the lambda calculus one often assumes that bound variables
in a term are distinct, using the alpha-equivalence, so that betareduction does not cause unintended variable capturing. We startwith an analogous criterion on names.
Definition B.1 (Bound/free names). A name a ∈ A in a graph issaid to be:
1. bound by an A-node, if the A-node has input types Va → T )and !Va , for some type T .
2. free, if a p~-node has input type Va or a P-node has output
type Va .
Definition B.2 (Bound-name criterion). A graph G meets thebound-name criterion if any bound name a ∈ A in the graph G
satisfies the following.

The second criterion is on free names, which ensures each freename indicates a unique vector space Fn .
Definition B.4 (Free-name criterion). A graph G meets the freename criterion if it comes with a ‘validation’ map v : FRG → N,from the set FRG of free names in the graph G to the set N of natural
numbers, that satisfies the following.
• If a p~-node has input type Va , the vector p~ has the size v (a),i.e. p~ ∈ Fv (a)• If a P-node has output type !Va , it has v (a) input links, i.e.
n = v (a).
The validation map is unique by definition. We refer to the combination of the bound-name criterion and the free-name criterionas ‘name criteria’.
Proposition B.5 (Preservation of name criteria). In any transition,
if an old state meets both the bound-name criterion and the free-namecriterion, so does a new state.
Proof. With Prop. B.3 at hand, we here show that the new state
fulfills the free-name criterion.
A free name is introduced by a ?-rewrite transition that eliminates a A-node. The name was bound by the A-node and not free
before the transition, because of the bound-name criterion (namely
the uniqueness property). Therefore the validation map can besafely extended.
The name permutation, in rewrite transitions that duplicate a!-box, applies for both bound names and free names. It introduces
fresh free names, without changing the status of names, and therefore the validation map can be extended accordingly.

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica

Some computational rewrite rules (Fig. 4) act on links with vector
type Va , however they have no impact on the validation map. Anyother transitions also do not affect the validation map.

The last criterion is on the shape of graphs. It is inspired by
Danos and Regnier’s correctness criterion [6] for proof nets.
Definition B.6 (Covering links). In a graph G (1,n), a link e iscovered by another link e 0 , if any box-path (see Def. 3.2) from theroot of the graph G to the link e contains the covering link e 0 .
Definition B.7 (Graph criterion). A graph G (1,n) fulfills the graphcriterion if it satisfies the following.
Acyclicity Any box-path, in which all links have (not necessarily the same) argument types, is acyclic, i.e. nodes orlinks appear in the box-path at most once. Similarly, any
directed path whose all links have the cell type F is acyclic.
Covering At any λ-node, its incoming output link is coveredby its input link. Any input link of A-node or P-node iscovered by a ?-node.
!

Proposition B.8 (Preservation of graph criterion). In any transition, if an old state meets the graph criterion, so does a new state.
Proof. An @-rewrite transition eliminates a pair of a λ-node andan @-node, and connects two acyclic box-paths of argument types.
The resulting box-path being a cycle means that there existed abox-path from the free (i.e. not connected to the λ-node) output linkof the @-node to the incoming output link of the λ-node before thetransition. This cannot be the case, as the incoming output link musthave been covered by the input link of the λ-node. Therefore the@-rewrite does not break the acyclicity condition. The condition
can be easily checked in any other transitions.
The covering condition is also preserved. Only notable case forthis condition is the graph abstraction rule that introduces a λ-nodeand a P-node.
Finally the validity of graph states is defined as below. The
validation map of a graph is used to check if the token carries
appropriate data to make computation happen.
Definition B.9 (Queries and answers). Let d : A → N be a map
from a finite set A ⊂fin A of names to the set N of natural numbers.
For each type T̃ , two sets QryT̃ and Ansd are defined inductivelyT̃
as below.
AnsdF = AnsdF := F!

QryF = Qry F := {?},!

QryT1 →T2 := {?, @}, Fd (a)
d
AnsV
:= 
∅
a

AnsTd1 →T2 := {λ}Qry!T := QryT ,Ansd!T := AnsTd .

QryVa := {?},

(if a ∈ A)
(otherwise)

Definition B.10 (Valid states). A state ((G,e), (d, f ,S,B)) is valid
if the following holds.
1. The graph G fulfills the name criteria and the graph criterion.
2. If d = ↑ and the position e has type ρ, the computation stack
S is in the form of X : S 0 such that X ∈ Qryρ .
3. Let v be the validation map of the graph G. If d = ↓ andthe position e has type ρ, the set Ansvρ is not empty, andthe computation stack S is in the form of X : S 0 such thatX ∈ Ansvρ .

Proposition B.11 (Preservation of validity). In any transition, if
an old state is valid, so is a new state.
Proof. Using Prop. B.5 and Prop. B.8, the proof boils down to checkthe bottom two conditions of validity. Note that no rewrite transitions change the direction and the computation stack. When thetoken passes a $-node downwards, application of the primitive
operation $ preserves the last condition of validity. All the otherpass transitions are an easy case.
In an execution, validity of intermediate states can be reduced
to the criteria on its initial graph.
Proposition B.12 (Validity condition of executions). For any execution Init (G 0 ) →∗ ((G,e),δ ), if the initial graph G 0 meets the namecriteria and the graph criterion, the state ((G,e),δ ) is valid.
Proof. The initial state Init (G 0 ) has the direction ↑, and its computation stack has the top element ?. Since any type ρ satisfies? ∈ Qryρ , the criteria implies validity at the initial state Init (G 0 ).
Therefore the property is a consequence of Prop. B.11.
C

Stability

This section studies executions in which the underlying graph isnever changed.
Definition C.1 (Stable executions/states). An execution Init (G) →∗((G,e),δ ) is stable if the graph G is never changed in the execution.
A state is stable is there exists a stable execution to the state itself.
A stable execution can include pass transitions, and rewrite transitions that just lower the rewrite flag, as well. Since the only sourceof non-determinism is rewrite transitions that actually change agraph, a stable state comes with a unique stable execution to thestate itself.
The stability property enables us to backtrack an execution incertain ways, as stated below.
Proposition C.2 (Factorisation of stable executions).
1. If an execution Init (G) →∗ ((G,e),δ ) is stable, it can befactorised as Init (G) →∗ ((G,e 0 ),δ 0 ) →∗ ((G,e),δ ) where
the link e 0 is any link covering the link e.
2. If an execution Init (G) →∗ ((G,e), (↓, ,X : S,B)) is stable,
it can be factorised as Init (G) →∗ ((G,e), (↑, ,? : S,B)) →∗((G,e), (↓, ,X : S,B)).
Proof of Prop. C.2.1. The proof is by induction on the length of thestable execution Init (G) →∗ ((G,e),δ ). When the execution has
null length, the last position e is the root of the graph G, and theonly link that can cover it is the root itself.
When the execution has a positive length, we examine eachpossible transition. Rewrite transitions that only lower the rewrite
flag are trivial cases. Cases for pass transitions are the straightforward use of induction hypothesis, because for any link and a node,
the following are equivalent: (i) the link covers one of outgoing
output links of the node, and (ii) the link covers all input links ofthe node.
Proof of Prop. C.2.2. The proof is by induction on the length n of
the stable execution Init (G) →n ((G,e), (↓, ,X : S,B)).
As the first state and the last state cannot be equal, base cases
are for single transitions, i.e. when n = 1. Only possibilities are

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

D ? !

CD?!

→l ((G, out (Z )), (↓, ,X : S,B 0 ))→ ((G, in(Z )), (↓, ,X : S,B)).
Moreover the state ((G, out (Z )), (↑, ,? : S,B 0 )) must be the resultof a pass transition over the Z -node. This means we have thefollowing further factorisation if Z , !,Init (G) →m−1 ((G, in(Z )), (↑, ,? : S,B))

Proof. The proof is by looking at how factorisation is given in the
proof of Prop. C.2.2. Note that, since we are ruling out argument
types, i.e. enriched types of the form of !T , the factorisation neverencounters !-nodes (hence nor -nodes).
?

C

Init (G) →m ((G, out (Z )), (↑, ,? : S,B 0 ))Proposition C.3 (Stable executions, intensionally). Any stable execution of the form Init (G) →h ((G,e), (↑, ,? : S,B)) →k ((G,e), (↓, ,X :S,B)) satisfies the following.
• If the position e has a ground type or the cell type F, the last
k transitions of the stable execution involve nodes labelledwith only {p, p~, $, , , | p ∈ F, p~ ∈ Fn , n ∈ N}.
• If the position e has a function type, i.e. T1 → T2 , it is the
input of a λ-node, and k = 1.
CD!

pass transitions over a λ-node, a p-node or a p~-node, all of which isin the form of ((G,e), (↑, ,? : S,B)) → ((G,e), (↓, ,X : S,B)).
In inductive cases, we will use induction hypothesis for any
length that is less than n. If the last transition is a pass transition
over a λ-node, a p-node or a p~-node, the discussion goes in thesame way as in base cases. All the other possible last transitions
are: pass transitions over a node labelled with !, , , or ; andrewrite transitions that do not change the underlying graph but
discard the rewrite flag $.
If the last transition is a pass transition over a Z -node such thatZ ∈ {!, , , , }, the last position (referred to as in(Z )) is input tothe Z -node, and the second last position (referred to as out (Z )) is
output of the Z -node. Induction hypothesis (on n − 1) implies thefactorisation below, where n = m + l + 1:!

The Geometry of Computation-Graph Abstraction

The fundamental result is that stability of states is preserved byany transitions. This means, in particular, rewrites triggered by
the token in an execution can be applied beforehand to the initialgraph without changing the end result. Another (rather intuitive)
insight is that, in an execution, the token leaves no redexes behindit.
Proposition C.4 (Preservation of stability). In any transition, if an
old state is stable, so is a new state.
Proof. If the transition does not change the underlying graph, it
clearly preserves stability. If not, the preservation is a direct consequence of Lem. C.5 and Lem. C.6 below.
→ ((G, out (Z )), (↑, ,? : S,B 0 ))→l ((G, out (Z )), (↓, ,X : S,B 0 ))→ ((G, in(Z )), (↓, ,X : S,B))

Lemma C.5 (Stable executions in graph context). If all positions ina stable execution Init (G[G]) →∗ ((G[G],e),δ ) are in the graph context G, there exists a stable execution Init (G[G 0 ]) →∗ ((G[G 0 ],e),δ )for any graph G 0 with the same interfaces as the graph G.

and the one below if Z = !.
Init (G) →m−3 ((G, in(Z )), (↑, ,? : S,B))→ ((G, out (Z )), (↑, ?,? : S,B))→ ((G, out (Z )), (↑, !,? : S,B))→ ((G, out (Z )), (↑, ,? : S,B 0 ))→l ((G, out (Z )), (↓, ,X : S,B 0 ))→ ((G, in(Z )), (↓, ,X : S,B))
If the last transition is a rewrite transition that discards therewrite flag $, it must follow a pass transition over a $-node. Letin, out 1 and out 2 denote input, left output and right output, respectively, of the $-node. We obtain the following factorisation wheren = m +l 2 +l 1 + 3 and k = k 1 $ k 2 , using induction hypothesis twice(on n − 2 and n − l 1 − 3).
Init (G) →m−1 ((G, in), (↑, ,? : S,B))→ ((G, out 2 ), (↑, ,? : ? : S,B))→l2 ((G, out 2 ), (↓, ,k 2 : ? : S,B))→ ((G, out 1 ), (↑, ,? : k 2 : ? : S,B))→l1 ((G, out 1 ), (↓, ,k 1 : k 2 : ? : S,B))→ ((G, in), (↓, $,k : S,B))→ ((G, in), (↓, ,k : S,B))

Inspecting the proof of Prop. C.2.2 gives some intensional characterisation of graphs in stable executions. We say a transition‘involves’ a node, if it is a pass transition over the node or it is a
rewrite transition whose (main-)redex contains the node.

Proof. The proof is by induction on the length of the stable execution Init (G[G]) →∗ ((G[G],e),δ ). The base case for null length istrivial. Inductive cases are respectively for all possible last transitions. When the last transition is a pass transition, the single node
involved by the transition must be in the graph context G[]. Therefore the last transition is still possible when the graph G is replaced,
which enables the straightforward use of induction hypothesis.
When the last transition is a ‘stable’ rewrite transition that simply changes the rewrite flag f to , we need to inspect its redex.
Whereas a part of the redex may not be inside the graph context
G[], we confirm below that the same last transition is possible forany substitution of the hole, by case analysis of the rewrite flag f .
Once this is established, the proof boils down to the straightforward
use of induction hypothesis. Possible rewrite flags are ground-type
operations $, and symbols ? and ! for !-box rewrites.
If the rewrite flag is $, the redex consists of one $-nodes with
two nodes connected to its output. The rewrite flag must havebeen raised by a pass transition over the $-node, which means the$-node is in the graph context G[]. Moreover, by Lem. C.2.2, thetwo other nodes in the redex are also in the graph context G[].
Therefore the stable rewrite transition, for the rewrite flag $, is notaffected by substitution of the hole.
If the rewrite flag is ?, the redex is a !-box with all its doors.
Since the rewrite flag must have been raised by the pass transition
over the principal door, the principal has to be in the graph context
G[]. All the auxiliary doors of the same !-box are also in thegraph context G[], by definition of graphs. The stable rewrite
transition for the rewrite flag ? is hence possible, regardless of any

LICS ’18, July 9–12, 2018, Oxford, United Kingdom
substitution of the hole, while the !-box itself may be affected by
the substitution. If the rewrite flag is !, the redex is a !-box, allits doors, and a node connected to its principal door. This case issimilar to the last case. The connected node, to the principal door,
is also in the graph context because the token must have visitedthe node before passing the principal door.
Lemma C.6 (Stabilisation of actual rewrites). Let((G[G],e),δ ) → ((G[G 0 ],e 0 ),δ 0 )Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica
for the last state, otherwise the rewrite flag $ must have beenraised and have triggered the change of the graph. As the links
in(k 1 ) and in(k 2 ) are the only ones outside the graph context G[G]and the link in($) is input of the redex G, the prefix execution isentirely in the graph context G[]. We can take in($) as e 0 and(↑, ,? : S 0 ,B 0 ) as δ 0 . The rewrite of the redex does not change
the position, which means e 0 = e 0 = in($). The resulting graph G 0
consists of one constant node (k), and we have a single transition((G[G 0 ],e 0 )), (↑, ,? : S 0 ,B 0 )) → ((G[G 0 ],e)), (↓, ,k : S 0 ,B)) tothe result state of the rewrite.
When the rewrite flag is F(n), the redex is a F-node with one!-box connected to its right output link. By Lem. C.2.2, the stable
execution Init (G[G]) →∗ ((G[G],e),δ ) is in the form of:

be a rewrite transition, where G is the redex replaced with a different graph G 0 . If the rewrite transition follows the stable execution
Init (G[G]) →∗ ((G[G],e),δ ), there exist an input link e 0 of the hole
 (equivalently of G and G 0 ) and token data δ 0 such that:∗0 0• the stable execution can be factorised as Init (G[G]) →∗ ((G[G],e 0 ),δ 0 ) →∗ Init (G[G]) → ((G[G], in), (↑, ,? : S ,B ))((G[G],e),δ ), where all positions in the first half sequence→ ((G[G], out 2 ), (↑, ,? : ? : S 0 ,B 0 ))are in the graph context G[]→∗ ((G[G], out 2 ), (↓, , p~ : ? : S 0 ,B 0 ))• there exists a sequence ((G[G 0 ],e 0 ),δ 0 ) →∗ ((G[G 0 ],e 0 ),δ 0 )→ ((G[G], out 1 ), (↑, ,? : p~ : ? : S 0 ,B 0 ))in which the graph G[G 0 ] is never changed.
Proof. The proof is by case analysis of the rewrite flag of the data δ .
Note that we only look at rewrites that actually change the graph.
When the rewrite flag f is λ, the redex contains a connected
pair of an @-node and a λ-node. We represent the outgoing outputof the λ-node by out (λ), one output of the @-node connected tothe λ-node by in(λ), the other output of the @-node by out (@),
and the input of the @-node by in(@). Lem. C.2.2 implies that thestable execution Init (G[G]) →∗ ((G[G],e),δ ) can be factorised as
below, for some element X of the computation stack.
Init (G[G]) →∗ ((G[G], in(@)), (↑, ,S,B))→ ((G[G], out (@)), (↑, ,? : S,B))→∗ ((G[G], out (@)), (↓, ,X : S,B))→ ((G[G], in(λ))), (↑, , @ : S,B)
→ ((G[G], out (λ)), (↑,λ,S,B))
The four links out (λ), in(λ), out (@) and in(@) cannot happen in thestable prefix execution Init (G[G]) →∗ ((G[G], in(@)), (↑, ,S,B)),
except for the last state, otherwise the rewrite flag λ must have beenraised in this execution, causing the change of the graph. The otherlink in the redex, the incoming output of the λ-node, neither appears
in the prefix execution, as no pass transition is possible at the link.
Therefore the prefix execution contains only links in the graphcontext G[], and we can take e 0 as in(@) and (↑, ,S,B) as δ 0 . The
rewrite yields the state ((G[G 0 ],e 0 ), (↑, ,S,B)) = ((G[G 0 ],e 0 ),δ 0 ).
When the rewrite flag f is $, the redex is a $-node with twoconstant nodes (k 1 and k 2 ) connected. Let in($), in(k 1 ) and in(k 2 )denote the unique input of these three nodes, respectively. The
stable execution Init (G[G]) →∗ ((G[G],e),δ ) is actually in thefollowing form, where k = k 1 $ k 2 .
Init (G[G]) →∗ ((G[G], in($)), (↑, ,? : S 0 ,B 0 ))→ ((G[G], in(k 2 )), (↑, ,? : ? : S 0 ,B 0 ))→ ((G[G], in(k 2 )), (↓, ,k 2 : ? : S 0 ,B 0 ))→ ((G[G], in(k 1 )), (↑, ,? : k 2 : ? : S 0 ,B 0 ))→ ((G[G], in(k 1 )), (↓, ,k 1 : k 2 : ? : S 0 ,B 0 ))→ ((G[G], in($)), (↓, $,k : S 0 ,B))
The links in($), in(k 1 ) and in(k 2 ) cannot appear in the stable prefix
execution Init (G[G]) →∗ ((G[G], in($)), (↑, ,? : S 0 ,B 0 )), except→∗ ((G[G], out 1 ), (↓, ,λ : p~ : ? : S 0 ,B 0 ))→ ((G[G], in), (↑, F(n),? : S 0 ,B))
where in, out 2 and out 1 denote the input, the right output and theleft output of the F-node, respectively, and p~ ∈ Fn . Any links in theredex, i.e. the three interface links of the F-node and links in theconnected !-box, are covered by the link in. Therefore by Lem. C.2.1,
these links do not appear in the prefix execution Init (G[G]) →∗((G[G], in), (↑, ,? : S 0 ,B 0 )) except for the last in. The last state of
the prefix execution has the same token position and token data as
the result of the rewrite.
The rewrite flag ? is raised by a pass transition over a !-node,
principal door of a !-box. The pass transition is the last one of thestable execution Init (G[G]) →∗ ((G[G],e),δ ), i.e.
Init (G[G]) →∗ ((G[G], in),δ ) → ((G[G], out),δ )where in and out are respectively the input and output of the !node. Since any ?-rewrite leaves the !-node in place and keeps
the position and data of the token, we have a pass transition((G[G 0 ], in),δ ) → ((G[G 0 ], out),δ ) to the resulting state of therewrite. It remains to be seen whether the stable prefix execution
Init (G[G]) →∗ ((G[G], in),δ ) is entirely in the graph context G[].
First, the links in and out cannot appear in the prefix execution
except for the last, otherwise there must have been a non-stable?-rewrite. When the rewrite flag ? triggers the contraction rule(bottom-right in Fig. 7a) or the absorption rule (left in Fig. 7b),
any links in the redex are covered by the link in, by definition ofgraphs. Therefore by Lem. C.2.1, these links neither appear in theprefix execution. When the projection rule (top-right in Fig. 7a)occurs, the interface links of the P-node do not appear in the prefix
execution, as there is no pass transition over the P-node. Since theinput link of the P-node covers all the other links in the redex, byLem. C.2.1, no links in the redex have been visited by the token.
The case of the graph abstraction rule (left in Fig. 7a) is similar tothe projection case. Recall that the redex for the graph abstraction
rule excludes the sub-graph (G ◦ (p~) ‡ in the figure) that stays thesame. In graph abstraction case, all links in the redex do not appear
in the prefix execution, while the unchanged sub-graph is includedby the graph context G[] by assumption.
Finally for the rewrite flag !, the stable execution Init (G[G]) →∗((G[G],e),δ ) ends with several pass transitions, including one overThe Geometry of Computation-Graph Abstraction

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

a !-node, and a rewrite transition that sets the rewrite flag:

D.1

Init (G[G]) →∗ ((G[G],e 0 ),δ 0 ) →∗ ((G[G], in), (↑, ,S,B))→ ((G[G], out), (↑, ?,S,B)) → ((G[G], out), (↑, !,S,B))
where e 0 is an input link of the redex G, and in and out are respectively the input and output of the !-node. Inspecting each !-rewrites
yields a stable sequence ((G[G 0 ],e 0 ),δ 0 ) →∗ ((G[G 0 ], out), (↑, !,S,B))
to the result state of the rewrite. The inspection also confirms thatthe stable prefix execution Init (G[G]) →∗ ((G[G],e 0 ),δ 0 ) is entirely in the graph context G, as below.
In the first two rewrites of Fig. 7c, the link e 0 is the only inputof the redex and it covers the whole redex. As the link e 0 cannot
appear in the stable prefix execution, neither any link in the redex,
by Lem. C.2.1. In the last rewrite of Fig. 7c, the input link e 0 of theredex covers the whole redex except for the other input links. The
uncovered input links, in fact, must have not been visited by thetoken, otherwise the token has proceeded to a !-node and triggered
copying.

Since stability is trivial for initial states, we can always assume
stability at any states in an execution.

Proof of Prop. D.1

First we assume that the state has rewrite flag . Failure of passtransitions can be caused by either of the following situations: (i)the position is eligible but the token data is not appropriate, or (ii)the position is not eligible.
The situation (i) is due to the wrong top elements of a computation/box stack. In most cases, it is due to the single top elementof the computation stack, or top elements of the box stack, which
can be disproved easily by validity, or respectively, stability. The
exception is when the token points downwards at the left output
of a primitive operation node (#), and the top three elements ofthe computation stack have to be checked. Let in, out 1 and out 2
denote the input, the left output and the right output of the $-node,
respectively. By stability and Lem. C.2.2, the state is the last stateof a stable execution of the following form.
Init (G) →∗ ((G, out 1 ), (↑, ,? : S,B)) →∗ ((G, out 1 ), (↓, ,X 1 : S,B))
The intermediate state has to be the result of a pass transition, i.e.
Init (G) →∗ ((G, out 2 ), (↓, ,S,B)) → ((G, out 1 ), (↑, ,? : S,B))→∗ ((G, out 1 ), (↓, ,X 1 : S,B)).

Since the last state is valid, the graph G fulfills the criteria (Def. B.2,
Proposition C.7 (Stability of executions). In any execution Init (G 0 ) →∗ Def. B.4 and Def. B.7) and any states in this execution is valid byProp. B.12. Therefore the computation stack S is in the form of((G,e),δ ), the state ((G,e),δ ) is stable.
S = X 2 : S 0 , and using Lem C.2.2 again yields:
Proof. This is a consequence of Prop. C.4, since any initial states
Init (G) →∗ ((G, out 2 ), (↑, ,? : S 0 ,B))
are trivially stable.
→∗ ((G, out 2 ), (↓, ,X 2 : S 0 ,B))D

→ ((G, out 1 ), (↑, ,? : X 2 : S 0 ,B))

Productivity and safe termination

By assuming both validity and stability, we can prove productivity: namely, a transition is always possible at a valid and stableintermediate state.
Proposition D.1 (Productivity). If a state is valid, stable and not
final, there exists a possible transition from the state.
Proof in Sec. D.1.



We can obtain a sufficient condition for the safe termination ofan execution, which is satisfied by the translation of any program.
Proposition D.2 (Safe termination). Let Init (G 0 ) be an initial state
whose graph G 0 meets the name criteria and the graph criterion. If
an execution Init (G 0 ) →∗ ((G,e),δ ) can be followed by no transition,
the last state ((G,e),δ ) is a final state.
Proof. This is a direct consequence of Prop. B.12, Prop. C.7 and
Prop. D.1.

Proposition D.3 (Safe termination of programs). For any closed
program t such that − | − | p~ ` t : T , if an execution on thetranslation (− | − | p~ ` t : T ) ‡ can be followed by no transition, thelast state of the execution is a final state.
Proof. The translation (− | − | p~ ` t : T ) ‡ fulfills the name criteria
and the graph criterion, which can be checked inductively. Notethat all names in the translation are bound. This proposition ishence a consequence of Prop. D.2.
→∗ ((G, out 1 ), (↓, ,X 1 : X 2 : S 0 ,B)).
The first intermediate state, again, has to be the result of a passtransition, i.e.
Init (G) →∗ ((G, in), (↑, ,S 0 ,B)) → ((G, out 2 ), (↑, ,? : S 0 ,B))→∗ ((G, out 2 ), (↓, ,X 2 : S 0 ,B))
→ ((G, out 1 ), (↑, ,? : X 2 : S 0 ,B))→∗ ((G, out 1 ), (↓, ,X 1 : X 2 : S 0 ,B)).
Since the first intermediate state of the above execution is valid, thecomputation stack S 0 is in the form of S 0 = ? : S 00 , which means
S = X 1 : X 2 : ? : S 00 . Moreover validity ensures that the elements
X 1 and X 2 are values and eligible for a pass transition from the laststate. In particular, vector operations +, × and · are always given
two vectors of the same size.
We move on to the situation (ii), where the token position is not
eligible to pass transitions. To disprove this situation, we assume avalid, stable and non-final state from which no pass transition ispossible, and derive contradiction.
The first case is the state ((G,e), (↓, ,S,B)) where the positione is the incoming output of a λ-node. By the graph criterion, theposition is covered by the outgoing output out (λ) of the λ-node,and Lem. C.2 implies the following stable execution.
Init (G) →∗ ((G, out (λ)), (↑, f ,S 0 ,B 0 )) →∗ ((G,e), (↓, ,S,B))
Due to stability, the intermediate state ((G, out (λ)),δ ) must be theresult of a pass transition over the λ-node. However the transition
sets λ as the rewrite flag f , which triggers elimination of the λ-nodeand contradicts stability.

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

to the state. The graph criterion (Def. B.7) implies the Z -node belongs to an acyclic box-path of argument types. By typing, any
maximal acyclic box-path ends with either a λ-node or a !-node,and the token must visit this node in the second half of the stable
execution. This implies contradiction as follows. If the last nodeof the maximal box-path is a λ-node, the token must visit the incoming output link of the λ-node, from which the token cannot
been proceeded. If the last node is a !-node, the token must pass
the !-node and trigger rewrites that eliminate the Z -node.
This completes the first half of the proof, where we assume thestate has rewrite flag . In the second half, we assume that thestate has a rewrite flag which is not , and show the graph of thestate contains an appropriate redex for the rewrite flag.
When the rewrite flag is λ, by stability, the token must be at theoutgoing output of a λ-node which is connected to the left output
of an @-node. Therefore the λ-rewrite is possible. For the rewrite
flag F(n), stability implies that a !-box with no definitive auxiliary
doors (?) must be connected to the right output of a F-node. Rewrite
transitions for rewrite flags $ and F(n) are exhaustive.
When the rewrite flag is !, by stability, the state is the result of
the ?-rewrite that only changes the rewrite flag. This means thetoken is at the root of a !-box with no definitive auxiliary doors(?-nodes). Transitions for the rewrite flag ! are exhaustive for theclosed !-box.
When the rewrite flag is ?, the token is at the root of a !-box,
which we here call ‘inhabited !-box’. By typing, output links ofdefinitive auxiliary doors of the inhabited !-box can be connected to
C-nodes, P-nodes, A-nodes, !-nodes, ?-nodes or λ-nodes. However?-nodes and λ-nodes are not the case, as we see below in two steps.
First, we assume that a definitive auxiliary door of the inhabited!-box is connected to another ?-node. This means that the inhabited!-box is inside another !-box, and therefore the token position isE

Provisional contexts and congruence ofexecution

To deal with shared cells that arise in an execution, we introduce
another perspective on composite graphs which takes -nodes into
account.
Definition E.1 (Provisional contexts). A graph context of the form(~p) ‡H(n, m)⇤denoted by P[], is a provisional context if it satisfies the following.
• The graph H (n,m) consists solely of -nodes, and p~ ∈ Fm .
• For any graph G (1,n) that fulfills the graph criterion, thegraph P[G] also fulfills the graph criterion.
C

Init (G) →∗ ((G, out (Z )), (↑, ,S,B)) →∗ ((G, out (Z )), (↓, ,S,B))

C

to the state. The only transitions that can yield the intermediate
state, at the left output of the @-node, are rewrite transitions thatchange the graph, which is contradiction.
The third case is the state ((G,e), (↑, ,S,B)) where the positione is the input of a ?-node, an auxiliary door of a !-box. Since thelink e is covered by the root of the !-box, by Lem. C.2.1, the token
has visited its principal door, i.e. !-node. This visit must have raised
rewrite flag ?. Because of the presence of the ?-node, the rewrite
flag must have triggered a rewrite that eliminates the ?-node, whichis contradiction.
The fourth case is when the position e is one of the interface(i.e. either input or output) links of an A-node or a P-node. By thecovering condition of the graph criterion, this case reduces to theprevious case.
The last case is the state ((G, out (Z )), (↓, ,S,B)) where the position out (Z ) is the output of an Z -node, for Z ∈ {D, C, ?}. If Z = ?,i.e. the node is an auxiliary door of a !-box, the position is coveredby the root of the !-box. This reduces to the previous case. If not,i.e. Z ∈ {D, C}, Lem. C.2.2 gives the stable execution

C

Init (G) →∗ ((G,e), (↑, ,? : S 0 ,B)) →∗ ((G,e), (↓, ,λ : S 0 ,B))

covered by the root of the outer !-box. By Lem. C.2.1, the token
must have visited the principal door of the outer !-box and triggered
the change of the graph, which contradicts stability.
Second, we assume that a definitive auxiliary door of the inhabited !-box is connected to the incoming output link of a λ-node.
This λ-node cannot be inside the inhabited !-box, since no !-box has
incoming output. Clearly there exists a box-path from the token
position to the incoming output of the λ-node. Therefore the token
position, the unique input of the !-box, is covered by the input ofthe λ-node; otherwise the graph criterion is violated. This covering
implies that the token must have passed the λ-node upwards andtriggered its elimination, by Lem. C.2.1, which contradicts stability.
Now, if a !-node is connected to a definitive auxiliary door of the
inhabited !-box, the !-node is a principal door of another !-box, andthe !-box may have definitive auxiliary doors. Output links of thesedefinitive auxiliary doors, again, can be only connected to C-nodes,
P-nodes, A-nodes, or !-nodes, which are principal doors of other!-boxes. This means there can be chains of !-boxes starting from theinhabited !-box, where a principle door of a !-box is connected to adefinitive auxiliary door of another !-box via C-nodes and P-nodes.
Since the graph of any valid graph state has no output and satisfies
the acyclicity property (in Def. B.7), these chains must be acyclic,
and hence they must end with !-boxes without definitive auxiliary
doors. Therefore, when the rewrite flag ? is raised, there is always
a possible remote rule.
The last remark for the rewrite flag ? is about the replacement of
nodes in the graph abstraction rule. Typing of links ensures that the
replacement never fails and produces a correct graph. In particular
the sub-graph G in Fig. 7a only consists of -nodes and -nodes.
Finally, in conclusion, the state with rewrite flag ? is always eligible
for at least one of the rules in Fig. 7a and Fig. 7b.
?

The second case is the state ((G,e), (↓, ,S,B)) where the positione is the left output of an @-node. By validity the computation stack
S is in the form of S = λ : S 0 , and Lem. C.2.2 gives the stable
execution

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica

In the above definition, the second condition implies that thegraph H contains no loops. We sometimes write P[]n to makeT̃
explicit the input type and the number of output links of the hole.
Note that a graph P[G], where P[] is a provisional context and
G is a definitive graph, is a composite graph. As an extension of
Prop. 3.3, we can see a provisional context is preserved by transitions.

The Geometry of Computation-Graph Abstraction

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

!

F
!

k F

G0 (1, 1 + k)

G[] =
where the graph H (n + k,m) consists of all reachable nodes from
output links of the hole . By the assumption on the graph context
G[], all the output links of the hole  have the cell type F. Therefore typing ensures the graph H in fact consists of only -nodes and-nodes. We can turn the graph H ◦ (p~) ‡ to a provisional context
P[], by dropping all -nodes and adding k weakening nodes ( ),as below.
!

C

?

W

?

H[✏/ ]W⇤

be a single transition of the assumed execution Init (P[G]) →∗((P[G 0 ],e 0 ), (d, f ,S 0 ,B 0 )). For any computation stack S 0 and any
box stack B 0 , there exists a sequence ((G[H ],e), (d, f ,S :: S 0 ,B ::B 0 )) →∗ ((G[H 0 ],e 00 ), (d 0 , f 0 ,S 0 :: S 0 ,B 0 :: B 0 )) of transitions froma stable state, where the position e 00 is one of those corresponding
to e 0 .
The proof of the weak simulation follows from the fact that thepresence of the graph G 0 below the graph G does not raise any extra
rewriting, so long as the token data is taken from the execution on
the graph P[G].
Finally, if T is a function type, replacing the element ? with theelement @ in the sequence (1) only affects a pass transition over a
λ-node, which sends the computation stack ? : S to λ : S.
The execution Init (P[G]) →∗ ((P[G 0 ],e 0 ), (d, f ,S 0 ,B 0 )), in fact,
can contain at most one pass transition over a λ-node which changes
the computation stack ? :  to λ : . To make the second such transition happen, some other transition has to remove the top elementof the computation stack λ : , however by stability (Prop. C.7),
no transition can do this. Moreover, such pass transition can be
only the last transition of the execution. Any transitions that canpossibly follow the pass transition, which sets direction ↓ and computation stack λ : , are pass transitions over !-nodes, -nodes,-nodes or -nodes; the existence of these nodes contradicts withthe type T = T1 → T2 of the underlying graph.
Since the sequence (1) weakly simulates the execution, where theweakness comes from only -nodes, we can conclude that there isno occurrence, or exactly one occurrence at the last, in the sequence(1), of the pass transition which is affected by the replacement of
the element ? with the element @. Therefore if the sequence (1)contains no such pass transition, the sequence (2) can be directly
obtained by replacing the element ? with the element @. Otherwise,
cutting the last transition of the sequence (1) just does the job, as
the transition does not change the underlying graph and the token
position.

?

?

(~
p) ‡

P[] =((P[H ],e), (d, f ,S,B)) → ((P[H 0 ],e 0 ), (d 0 , f 0 ,S 0 ,B 0 ))We say the provisional context P[] is ‘induced’ by the graphcontext G[].
Proposition E.3 (Congruence of execution). Let G[G] be a composite graph where G (1,n) is a definitive graph of type T , and e
be the root of the hole of the graph context G[]. Assume an execution Init (P[G]) →∗ ((P[G 0 ],e 0 ), (d, f ,S 0 ,B 0 )), where the provisional
context P[] is induced by the graph context G[]. Then, for any
stacks S and B, there exists a sequence((G[G],e), (↑, ,? : S,B)) →∗ ((G[G 0 ],e 0 ), (d, f ,S 00 ,B 00 ))(1)

F

Data-flow graphs

This section looks at graphs consisting of specific nodes. The restriction on nodes rules out some rewrites, especially @-rewrites
for function application and the graph abstraction rule.
Definition F.1 (Data-flow graphs). A data-flow graph is a graphwith no -nodes, that satisfies the following.
!

⇤

Weak simulation. Let?

H(n + k, m)nProof. By the way the provisional context P[] is induced by thegraph context G[], any link of the graph P[G] has at least one(canonically) corresponding link in the graphs G, H and (p~) ‡ . A link
may have several corresponding links, because of -nodes dropped
in the induced provisional context P[]. The sequence (1) is given
as a consequence of the following weak simulation result, where
weakness is due to -nodes.

D

(~
p) ‡

(2)

of transitions, for some token data δ 0 .

!

CSince our operational semantics is based on low-level graphicalrepresentation and local token moves, rather than structured syntactical representation, any structural reasoning requires extra care.
For example, evaluation of a term of function type is not exactly
the same, depending on whether the term appears in the argument
position or the function position of function application t u. The
token distinguishes the evaluation using elements ? and @ of acomputation stack, which is why we explicitly require terminationin definition of PT1 →T2 . Moreover congruence of execution is nottrivial.
To prove a specific form of congruence, we begin with ‘extracting’a provisional context out of a graph context. Let G[] be a graphcontext, such that for any definitive graph G (1,n) of type T , thegraph G[G] is a composite graph. We can decompose the graphcontext G[] as((G[G],e), (↑, , @ : S,B)) →∗ ((G[G 0 ],e 0 ),δ 0 )?

Proof. In addition to Prop. 3.3, no transition changes existing nodes. Therefore a provisional context is preserved in any transition.
of transitions, where S 00 = S 0 ::S and B 00 = B 0 ::B. The decomposition ::replaces the bottom element  of the first stack with the second stack.
Moreover, if T is a function type, there also exists a sequence?

Proposition E.2 (Provisional context preservation). When a transition sends a graph G to a graph G 0 , if the old graph G can be
decomposed as P[H ] where P[] is a provisional context and H (1,n)
is a definitive graph, the new graph G 0 can be also decomposed as
P[H 0 ] for some definitive graph H 0 (1,n), using the same provisional
context.

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica• The first sub-graph D 0 (n 0 ,n 1 ) is a data-flow graph.
• If k > 0, there exists a unique number h such that 0 < h ≤ k.
For each i = 1, . . . ,h − 1, the sub-graph D i (ni ,ni+1 )can contain only C-nodes, P-nodes, -nodes or !-boxes
with their doors, where these !-boxes are data-flow graphs.
Input links of the sub-graph D i (ni ,ni+1 ) are connected to
output links of the previous sub-graph D i−1 (ni−1 ,ni ), via ni
parallel ?-nodes. These delimiting parallel doors (?) belong
to the same !-box, whose principal door (!) is not includedin the whole sequence of sub-graphs.
For each j = h, . . . ,k, the sub-graph D j (n j ,n j+1 ) solely
consists of -nodes. Input links of the sub-graph D j (n j ,n j+1 )are connected to output links of the previous sub-graph
D j−1 (n j−1 ,n j ), via n j parallel -nodes. These delimiting
parallel doors ( ) belong to the same !-box, whose principal
door (!) is not included in the whole sequence of sub-graphs.
• The final sub-graph D k (nk ,nk +1 ) satisfies either one of thefollowing: (i) all its output links have the cell type F andconnected to -nodes, or (ii) all its output links are input!

!

Proof. The first observation is that any transition sends a data-flow
graph, composed with a graph (p~) ‡ , to a data-flow graph with thesame graph (p~) ‡ .
Given a composite graph G ◦ (p~) ‡ where G is a data-flow graph,
we define a partial ranking map ρ which assigns natural numbers
to some links of G. The ranking is only defined on links which arereachable from the root of G and labelled with either a ground typeor an argument type, as follows: ρ (e) := 0 if e is input of a p-node(p ∈ F), a q~-node (~q ∈ Fk ) or a -node; ρ (e) := max (ρ (e 1 ), ρ (e 2 ))+1
if e is input of a $-node, and e 1 and e 2 are output links of the $-node;and ρ (e) := ρ (e 0 ) + 1 if e is input of a !-node, a ?-node, a D-nodeor a C-node, and e 0 is the corresponding output link. This ranking
on reachable links is well-defined, as the composite graph G ◦ (p~) ‡meets the graph criterion.
Since the state ((G ◦ (p~) ‡ ,e), (↑, ,S,B)) is stable and the positione has ground type, the ranking ρ of the composite graph G ◦ (p~) ‡Definition F.5 (Data-flow chains). In a graph G, a data-flow chain
D is given by a sequence D 0 (n 0 ,n 1 ), . . . ,D k (nk ,nk +1 ) of k + 1 subgraphs, where k is a natural number, that satisfies the following.

?

Proposition F.3. Let G (1,n) be a data-flow graph, with a link e ofground type which is reachable from the root of G. For any vectorp~ ∈ Fn , if a state ((G ◦ (p~) ‡ ,e), (↑, ,S,B)) is stable and valid, there
exists a data-flow graph G 0 (1,n) that agrees with G on the link e,
and a computation stack S 0 , such that ((G ◦ (p~) ‡ ,e), (↑, ,S,B)) →∗((G 0 ◦ (p~) ‡ ,e), (↓, ,S 0 ,B)).

Graph abstraction enables us to replace a computation graphswith a regular function, parameterised explicitly by what used tobe the cells of the computation graph. This replacement is not at
all simple; in an execution, it can happen inside a !-box, or happen
outside a !-box before the resulting graph gets absorbed by the!-box. Moreover, it can change the number of cells extracted bygraph abstraction. Our starting point to formalise this idea of
replacement is the notion of ‘data-flow chain’. It is a sequence of
sub-graphs, which are partitioned by auxiliary doors and essentiallyrepresenting data flow.

?

CD!

We can directly prove soundness of data-flow graphs.

Corollary F.4 (Soundness of data-flow graphs). If a data-flow
graph G (1,n) meets the name criteria and the graph criterion, forany vector p~ ∈ Fn , there exist a data-flow graph G 0 (1,n) and a token
value κ such that Init (G ◦ (p~) ‡ ) →∗ Final(G 0 ◦ (p~) ‡ ,κ).

C

Proof. The second case, where T = T1 → T2 , is a direct consequenceof Prop. C.3. For the first case, where T is a ground type, Prop. C.3
tells us that the stable execution Init (G ◦ (p~) ‡ ) →∗ Final(G ◦ (p~) ‡ ,κ)only involves nodes labelled with {p, p~, $, , , | p ∈ F, p~ ∈ Fn , n ∈N}. It boils down to show that any reachable node from the rootof the graph G is involved by the stable execution. We can show
this by induction on the maximum length of paths from the root
to a reachable node. The base case is trivial, as the root of thegraph G coincides with an input link of the reachable node. In the
inductive case, induction hypothesis implies that any reachable
node is connected to a reachable node which is involved by thestable execution. By Prop. C.2.2 and labelling of the involved node,
the stable execution contains a transition that passes the token
upwards over the involved node, and hence makes the reachable
node of interest involved by the following transition.
C?

1. When T is a ground type, the graph G is a pure data-flow
graph.
2. When T is a function type, i.e. T = T1 → T2 , the root of thegraph G is the input of a λ-node.

C
C

Proposition F.2 (Final graphs intensionally). Let G ◦ (p~) ‡ be acomposite graph of (non-enriched) type T . If a final state Final(G ◦(p~) ‡ ,κ) is stable, the definite graph G satisfies the following.

D?

Data-flow graphs intensionally characterises graphs of final
states. Graphs of final states play the role of ‘values’, since oursemantics implements (right-to-left) call-by-value evaluation.

!

CD

In particular, a data-flow graph is called pure if these reachable
nodes are not labelled with {!, ?, , D, C}.

is defined on the position e. The proof is by induction on the rank
ρ (e).
Base cases are when ρ (e) = 0. If the position e is input of a-node, the graph criterion implies an acyclic directed path fromthe -node to a -node. Intermediate nodes of this path are only
-nodes, and the proof is by induction on the number of these-nodes. Otherwise, the position e is input of a constant node (por q~), and the proof is by one pass transition over the node.
In inductive cases, induction hypothesis is for any natural number that is less than ρ (e). When the position e is input of a D-node,
the graph criterion implies an acyclic directed path from the Dnode to a !-node, with only C-nodes as intermediate nodes. Thismeans, from the state ((G ◦(p~) ‡ ,e), (↑, ,S,B)), the token goes along
the directed path, reaches the !-node, and trigger rewrites. These
rewrites eliminate all the nodes in the path, and possibly include
remote rules that eliminate other ?-nodes and C-nodes. When theserewrites are completed, the position e and its type are unchanged,
but its rank ρ (e) is strictly decreased. Therefore we can use induction hypothesis to prove this case. The last case, when the position e
is input of a $-node, boils down to repeated but straightforward useof induction hypothesis, which may be followed by a $-rewrite. D• All its input links have ground types.
• Any reachable (in the normal graphical sense) nodes from
input links are labelled with {p, p~, $, !, ?, , D, C, , | p ∈F, p~ ∈ Fn , n ∈ N}.

D

The Geometry of Computation-Graph Abstraction

!

Pnk+1

Dk

Dk

?

?

…

…

?

?

Dk

D0

LICS ’18, July 9–12, 2018, Oxford, United Kingdom
Definition F.7 (Data-flow replacements of states). Two stable andvalid states ((G◦(p~) ‡ ,e), (d, f 1 ,S 1 ,B 1 )) and ((H ◦(~q ) ‡ ,e), (d, f 2 ,S 2 ,B 2 ))are related by a binary relation ∝ if the following holds.
• The definitive graphs satisfy G ∝ H .
• The position e is either an input link of the data-flow chain
replaced by ∝, or (strictly) outside the data-flow chain.
• Two stable executions to these states give the exactly same
sequence of positions.
• The rewrite flags f 1 and f 2 may only differ in numbers n ofF(n).
• The validation maps vG and v H of these states, respectively,
satisfy that: vG (a) = 0 implies v H (a) = 0, for any a ∈ A on
which they both are defined.
As usual, we use ∝∗ to denote the reflexive and transitive closureof the relation ∝.

?

Proposition F.8. If

Dk 1q ) ‡ ,e), (↑, f 2 ,S 2 ,B 2 ))((G ◦ (p~) ‡ ,e), (↑, f 1 ,S 1 ,B 1 ))∝∗ ((H ◦ (~?

holds, a sequence…

((G ◦ (p~) ‡ ,e), (↑, f 1 ,S 1 ,B 1 ))→∗ ((G 0 ◦ (p~‡ ),e), (↓, ,S 10 ,B 10 ))?

(3)

implies a sequence

D0((H ◦ (~q ) ‡ ,e), (↑, f 2 ,S 2 ,B 2 ))→∗ ((H 0 ◦ (~q ) ‡ ,e), (↓, ,S 20 ,B 20 ))We refer to input of the first sub-graph D 0 as input of the data-flow
chain D, and output of the last sub-graph D k as output of the dataflow chain D. Fig. 11 illustrates some forms of data-flow chains.
We define a binary relation ∝ between definitive graphs thatapplies single replacement of a data-flow chain. It is lifted to abinary relation ∝ on some states.
Definition F.6 (Data-flow replacement of graphs). Let G (1,n) andH (1,m) be two definitive graphs, that contain data-flow chains DG
and DH , respectively. Two definitive graphs G (1,n) and H (1,m)
satisfies G ∝ H if the following holds.
• Two data-flow chains have the same number of input. The
data-flow chain DH has no more length than the data-flow
chain DG . The data-flow chain DH can have an arbitrary
number of output, whereas the data-flow chain DG has atleast one output.
• Exactly the same set of names appears in both graphs G and
H.
• The graphs G and H only differ in the data-flow chains DG
and DH , and their partitioning auxiliary doors.

such that the resulting states are again related by ∝ .
Proof. The proof is by induction on the length of the sequence (3).
Base cases are when the sequence (3) consists of one pass transition
over a constant node (scalar or vector) or a λ-node, and hencef = . If the transition is over a λ-node, the same transition ispossible at the state ((H ◦ (~q ) ‡ ,e), (↑, f ,S 2 ,B 2 )). If the transition isover a constant node, the constant node may be a part of a dataflow chain replaced by a data-flow chain D in the graph H . By
stability of the state ((H ◦ (~q ) ‡ ,e), (↑, f ,S 2 ,B 2 )), we can conclude
that any partitioning auxiliary doors of the data-flow chain D are-nodes, if they are box-reachable from the position e. This canbe confirmed by contradiction as follows: otherwise the positione must be in a !-box with definitive auxiliary doors (i.e. ?-nodes),which contradicts with stability and the fact f = . This concludes
the proof for base cases.
First inductive case is when the position e is an input link ofa data-flow chain DG , which is replaced with a data-flow chain
DH in the graph H . If the rewrite flag is f = , similar to basecases, we can see that the data-flow chain DH is in fact not partitioned by ?-nodes (but possibly -nodes). Moreover by stability
and the graph criterion, output links of the data-flow chain DH are
not connected to a P-node. This implies that the data-flow chain
DH with partitioning auxiliary doors altogether gives a data-flow
graph. Therefore the sequence (4) can be obtained by Prop. F.4 and
Prop. E.3.
If the rewrite flag f is not equal to , possibilities are f = λ, ?, !.
The λ-rewrite in the graph G sets the rewrite flag  and does notchange the position e. The same λ-rewrite is also possible in thegraph H , and we can use induction hypothesis. If f = ?, there will
be at least one rewrite transitions, in both graphs G and H , until?

links of a single P-node with nk +1 inputs, whose output
link is connected to a λ-node.
• If a node of the graph G is box-reachable from an input linkof the first sub-graph G 0 , it is either (i) in the sub-graphs
D 0 , . . . ,D k , (ii) in auxiliary doors partitioning them, or (iii)box-reachable from an output link of the last sub-graph G k .

(4)

∗

?

Figure 11

LICS ’18, July 9–12, 2018, Oxford, United Kingdom?

Corollary F.9 (Safety of dara-flow replacement). Let G ◦ (p~) ‡ andH ◦ (~q ) ‡ be composite graphs, meeting the name criteria and the graphcriterion, such that G ∝∗ H . If an execution on the graph G ◦ (p~) ‡reaches a final state, an execution on the graph H ◦ (~q ) ‡ also reaches
a final state.

G

Soundness

Our soundness proof uses logical predicates on definitive graphs.
These logical predicates are analogous to known ones on typed
lambda-terms.
Definition G.1 (Logical predicates). Given a term T , a logical predicate PT is on definitive graphs, that meet the name criteria andthe graph criterion, of type T . It is inductively defined as below.
• When T is a ground type, G (1,n) ∈ PT holds if: for any
provisional context P[]Tn , there exist a composite graph H
and a token value κ such that Init (P[G]) →∗ Final(H ,κ).
• When T = T1 → T2 , G (1,n) ∈ PT holds if:
1. for any provisional context P[]Tn , there exists a composite graph H such that Init (P[G]) →∗ Final(H ,λ)2. for any H (1,m) ∈ PT1 , the following graph, denoted by
G@!H , satisfies G@!H ∈ PT2 .

?

the rewrite flag is changed to !. These ?-rewrites may affect thedata-flow chains DG and DH . Since the position e is an input ofthe data-flow chains, these ?-rewrites can only eliminate C-nodes,
P-nodes, or ?-nodes that partition the data-flow chains. Eliminationof C-nodes and P-nodes is where the transitive closure ∝∗ plays arole. It does not change the partitioning structure of the data-flow
chains DG and DH . Elimination of ?-nodes in the graph G must
introduce -nodes, because the replacement ∝ requires the dataflow chain DG to have at least one output. Therefore the ?-rewrites
changes the data-flow chain DG to a new one while keeping its
length. On the other hand, elimination of ?-nodes may not happen
in the graph H , or may decrease the length of the data-flow chain
DH . As a result, after the maximal number of ?-rewrites until therewrite flag is changed to !, resulting graphs are still related by ∝∗and the position e is not changed. Finally if f = !, until the rewrite
flag is changed to , the same nodes (D-nodes and C-nodes) areeliminated in both graphs G and H , and both the data-flow chainsdecrease their length by one, if possible. Once rewrites are done
and the rewrite flag  is set, the position e is still unchanged, andwe use induction hypothesis.
Second inductive case is when the position e is the input of a
F-node, with rewrite flags f 1 = F(n 1 ) and f 2 = F(n 2 ) are raised. If
n 1 = 0, by definition of the relation ∝, it holds that n 2 = 0, and theproof follows from stability. If not, the sequence (3) begins with
non-trivial unfolding of the F-node. The sequence (4) can be provedby induction on n 2 , which is an arbitrary natural number, withn 2 ≤ n 1 being the base case.
Finally, the last inductive case is when the position e is not in
data-flow graphs replaced by ∝∗ . If f =  and the sequence (3)begins with a pass transition, the same transition is possible in
the graph H ◦ (~q ) ‡ , and we can use induction hypothesis. We
use it more than once, when the pass transition is over a $-node.
Possibly the sequence (3) ends with a $-rewrite, which may not be
possible on the other side. However, this is when the position e
becomes an input of a data-flow chain in the resulting graph G 0 ,and the difference of $-rewrites is dealt with by the replacement∝. If f , , discussion in the first inductive case is valid, except
for any ?-rewrites being possible, namely the graph abstraction
rule. We use induction hypothesis once consecutive rewrites are
done. The key fact is that, when the graph abstraction rule applies
to graphs related by the replacement ∝, the resulting graphs areagain related by ∝. The resulting graphs may differ in the size ofextracted vectors and in the number of input links of the introduced
P-nodes. This is dealt with by the replacement ∝ of data-flow chains,in particular, a single constant node itself is a data-flow chain. Note
that, if a P-node with no inputs is introduced on the side of graphG, it is also introduced on the other side, because any data-flow
chain of null output is not replaced by ∝. The graph abstraction ruleis essentially the only transition that is relevant to the conditionof validation maps for the relation ∝, and it does not violate thecondition. This concludes the whole proof.
Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica

G

H
!
@

Proposition G.2 (Deterministic termination). If G (1,n) ∈ PT , forany provisional context P[]Tn , there exist a unique definitive graph
G 0 (1,n) of typeT and a unique token value κ such that Init (P[G]) →∗Final(P[G 0 ],κ).
Proof. This is a direct consequence of Prop. 3.6 and Prop. E.2.



Proposition G.3 (Congruence of termination). Let G[G] be a composite graph where G (1,n) is a definitive graph of type T , and e be theroot of the hole of the graph context G[]. If G (1,n) ∈ PT holds, thenfor any stacks S and B, there exist an element X of a computation
stack and a sequence((G[G],e), (↑, ,? : S,B)) →∗ ((G[G 0 ],e), (↓, ,X : S,B))of transitions. Moreover, if T is a function type, there also exists thefollowing sequence.
((G[G],e), (↑, , @ : S,B)) →∗ ((G[G 0 ],e), (↑, , @ : S,B))
Proof. This is a corollary of Prop. E.3.

The following properties relate logical predicates to transitions,in both forward and backward ways.
Proposition G.4 (Forward/backward reasoning).
Forward reasoning Let G (1,n) be a definitive graph such thatG ∈ PT , and P[]Tn be a provisional context. For any execution Init (P[G]) →∗ ((H 0 ,e),δ ) on the graph P[G], there
exists a definitive graph G 0 (1,n) such that H 0 = P[G 0 ] andG 0 ∈ PT .
Backward reasoning A definitive graph G (1,n) satisfies G ∈PT , if: (i) it meets the name criteria and the graph criterion,and (ii) for any provisional context P[]Tn , there exist a definitive graph G 0 (1,n) ∈ PT and a state ((P[G 0 ],e),δ ) suchthat Init (P[G]) →∗ ((P[G 0 ],e),δ ).

The Geometry of Computation-Graph Abstraction

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

0

∗

0

0

0

Proposition G.5 (Safety of graph abstraction). If G (1,n) ∈ PT
holds, the graph Ĝ given as below

Pm
H(k, m)
!F

!
D

Ĝ =
belongs to PVa →T , where:• the name a ∈ A is any name that does not appear in the graphG0• the graph H (k,m), where k ≤ n and m is arbitrary, consists
solely of C-nodes connected to each other in an arbitrary way,
and fulfills the graph criterion• the graph ϕ(G) is obtained by: (i) choosing k output linksof the graph G arbitrarily, and (ii) replacing any -nodes,-nodes and -nodes with C-nodes, ?-nodes and D-nodes,
respectively, if one of the chosen output links can be reachable
from these nodes via links of only the cell type F.

Init (P [G @!H ]) → ((P [G @!H ],e ), (↓, ,κ : ? : , )) (6)such that Init (P 00 [H ]) →∗ Final(P 00 [H 0 ],κ) for some provisional
context P 00 []Tm and some token value κ. By the assumption of1
G ∈ PT1 →T2 and Prop. E.3, we can continue the execution (5) as:

C

?

!

Init (P 0 [G@!H ]) →∗ ((P 0 [G@!H 0 ],e 0 ), (↓, ,κ : ? : , ))Init (P 0 [G@!H ]) →∗ ((P 0 [G@!H 0 ],e 0 ), (↓, ,κ : ? : , ))→∗ ((P 0 [G 0 @!H 0 ],e),δ )Csuch that there exists a provisional context P 00 []Tm and an execu1
tion Init (P 00 [H ]) →∗ Final(P 00 [H 0 ],κ). Using the assumption on
the graph G, with Prop. E.3, yields its expansion

Proof. It is easy to see the graph Ĝ meets the name criteria and thegraph criterion, given G ∈ PT . Since the graph Ĝ has a λ-node at thebottom, the termination condition of the logical predicate PVa →T
is trivially satisfied. For any graph E ∈ PVa , we prove Ĝ@!E ∈ PT .
Let P 0 []T be any provisional context. By Cor. G.3, an execution on the graph P 0 [Ĝ@!E] first yields the graph P 0 [Ĝ@!E 0 ],where the graph E 0 comes from some execution Init (P0 [E]) →∗Final(P0 [E 0 ],κ) to a final state. Then the token eliminates the pairof the λ-node and the @-node at the bottom of the graph, and triggers the rewrite involving the graph H (C-nodes) and the P-nodeof the graph ϕ(G). This rewrite duplicates the graph E 0 in a !-box,
introducing dot-product nodes and vector nodes. Finally the token
eliminates the D-node and the !-box around the graph ϕ(G). In the
resulting graph, we shall write as P 0 [R], the graph R consists of thegraph ϕ(G), whose output links of type !F are connected to !-boxes,and further, -nodes. The following illustrates the graph R, where-nodes are omitted.
C

Init (P 0 [G@!H ]) →∗ ((P 0 [G@!H 0 ],e 0 ), (↓, ,κ : ? : , ))

k

(G)

(5)

for some token data δ . Since G ∈ PT1 →T2 and H ∈ PT2 by theassumption, we can use induction hypothesis of the forward reasoning and obtain G 0 @!H 0 ∈ PT2 . Using induction hypothesisof the backward reasoning along the execution (6), we conclude
G 0 @!H ∈ PT2 .
In the inductive case of the backward reasoning, we aim toprove G@!H ∈ PT2 for any H (1,m) ∈ PT1 . Let P 0 []Tn+m be any
2provisional context. Since H ∈ PT1 , Cor. G.3 gives an execution,
where the position e 0 is the right output of the @-node,n?

0→∗ ((P 0 [G 0 @!H 0 ],e),δ )

F

D

0

The key ingredient of the soundness proof is ‘safety’ of graphabstraction. This is where we appreciate call-by-value evaluation.

?

Init (P 0 [G@!H ]) →∗ ((P 0 [G@!H 0 ],e 0 ), (↓, ,κ : ? : , ))such that G 0 ∈ PT1 →T2 , arising in an execution Init (P 000 [G]) →∗((P 000 [G 0 ],e),δ ), for some provisional context P 000 []Tn →T . In1
2
duction hypothesis of the forward reasoning implies H 0 ∈ PT1 , andtherefore G 0 @!H 0 ∈ PT2 . We conclude G@!H ∈ PT2 by induction
hypothesis of the backward reasoning.
!

Proof. First of all, Prop. E.2 ensures the decomposition H 0 = P[G 0 ],where G 0 (1,n) is a definitive graph, in the forward reasoning. We
prove the both reasoning simultaneously by induction on the type
T . Base cases of both reasoning, where T is a ground type, relies
on determinism and stability, as we see below.
We begin with the base case of the forward reasoning, where T isa ground type. Given any execution Init (P[G]) →∗ ((P[G 0 ],e),δ )where G (1,n) ∈ PT and P[]Tn is a provisional context, by Prop. G.2,
there exists a unique final state Final(H 00 ,κ) such that Init (P[G]) →∗Final(H 00 ,κ). The uniqueness implies the factorisation Init (P[G]) →∗((P[G 0 ],e),δ ) →∗ Final(H 00 ,κ). Since the state ((P[G 0 ],e),δ ) isstable by Prop. C.7, we have a stable execution Init (P[G 0 ]) →∗((P[G 0 ],e),δ ). As a result we have an execution Init (P[G 0 ]) →∗Final(H 00 ,κ), which proves G 00 ∈ PT .
In the base case of the backward reasoning, where T is a groundtype, G 0 ∈ PT implies an execution Init (P[G 0 ]) →∗ Final(H ,κ) toa unique final state (Prop. G.2). Since the last state of the execution
Init (P[G]) →∗ ((P[G 0 ],e),δ ) is stable by Prop. C.7, there is astable execution Init (P[G 0 ]) →∗ ((P[G 0 ],e),δ ). The uniquenessof the final state Final(H ,κ) gives the sequence ((P[G 0 ],e),δ ) →∗Final(H ,κ) of transitions, which yields an execution Init (P[G]) →∗((P[G 0 ],e),δ ) →∗ Final(H ,κ) and proves G ∈ PT .
In inductive cases of both reasoning, where T = T1 → t 2 , weneed to check two conditions of the logical predicate PT . The first
condition, i.e. termination, is as the same as base cases. The otherinductive condition can be proved using induction hypotheses ofboth properties, together with Prop. E.3 and Cor. G.3, as below.
In the inductive case of the forward reasoning, our goal is toprove G 0 @!H ∈ PT2 for any H (1,m) ∈ PT1 , under the assumptionof the execution Init (P[G]) →∗ ((P[G 0 ],e),δ ) where G (1,n) ∈PT1 →T2 . Let P 0 []Tn+m be any provisional context. Since H ∈ PT1 ,2
Prop. G.3 implies two executions, where the position e 0 is the right
output of the @-node,LICS ’18, July 9–12, 2018, Oxford, United Kingdom

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica
G meets the name criteria and the graph criterion, it belongs to PT .
!F

H0

Hm 1

?

Fk 1
!

!F

F
Fi

!
n

k

!

…

=

F

(G)

F
Fi

p~i

.

!F
?

F

?

?

!

!

!F

!

F0

F

Va

!

…

!T0

!

!Tm 1

F
Gt

G=
Let F~ be these !-boxes. They all have type F, and each of them
contains the graph E 0 , with a dot-product node and a vector node.
Since the provisional context P 0 is arbitrary, we can reduce theproblem to R ∈ PT , using the backward reasoning (Prop. G.4).
If n = 0, the replacement ϕ actually changes nothing on thegraph G, and hence ϕ(G) = G. Therefore, in this case, R ∈ PT
follows from G ∈ PT , by Prop. G.3. We deal with the case wheren > 0 below.
First, as a consequence of Cor. F.9, the execution on the graph
P 0 [R] reaches a final state, given the assumption G ∈ PT . Thisis because, for any provisional context P[]Tn , we have P[G] ∝∗P 0 [R]. Since any name appears in the graph P[G] also appears in
the graph P 0 [R], we can infer Init (P[G])∝∗ Init (P 0 [R]). This means
R ∈ PT when T is a ground type, and the termination condition of
R ∈ PT when T is a function type.
To check the inductive condition of R ∈ PT where T = T1 → T2 ,we need to show R@!F ∈ PT2 for any F ∈ PT1 . By the assumption
G ∈ PT1 →T2 , we have G@!F ∈ PT2 . Using induction hypothesis
F ∈ PV →T . Let Ẽ ∈ PV is aon this graph yields the graph G@!F2bbgraph obtained by renaming E. We can take a provisional context
F )@!Ẽ]P 00 []T2 such that an execution on the graph P 00 [(G@!FF )@!E˜0 ] where the graph E˜0 is a renaming
yields a graph P 00 [(G@!Fof the graph E 0 . By proceeding the execution, we obtain the graph
R 0 , which consists of the graph ϕ(G)@!F and !-boxes connected
to some outputs of ϕ(G), each of which contains the graph E˜0 , a
F ∈ PV →T , thedot-product node and a vector node. Since G@!F2bforward reasoning (Prop. G.4) ensures R 0 ∈ PT2 . Moreover, thegraph R 0 is in fact a renaming of the graph R@!F , therefore wehave R@!F ∈ PT2 .
Finally the soundness theorem, stated below, is obtained as aconsequence of the so-called fundamental lemma of logical predicates.
Theorem G.6 (Thm. 3.7). For any closed program t such that A |− | p~ ` t : T , there exist a graph G and a token value κ such that:
Init ((A | − | p~ ` t : T ) ‡ ) →∗ Final(G,κ).
Proof. This is a corollary of Prop G.7 below.

Proposition G.7 (Fundamental lemma). For any derivable judgement A | Γ | p~ ` t : T , where Γ = x 0 : T0 , . . . ,xm−1 : Tm−1 , and any~ = H 0 , . . . ,Hm−1 such that Hi ∈ PT , if the following graph
graphs H
i

T

Sketch of proof. The first observation is that the translation (A | Γ |p~ ` t : T ) † itself meets the name criterion and the graph criteria.
~ ∈ PΓ , the whole graph again meets the graph criteria. We
Since Hcan always make the whole graph meet the name criteria as well,~ . Note that some names in the translation
by renaming the graphs H(A | Γ | p~ ` t : T ) † are not bound or free, and turns free once we~.
connect the graphs H
The proof is by induction on a type derivation, that goes in a similar way to a usual proof for the lambda calculus. To prove G ∈ PT ,we look at an execution on the graph G using the backward reasoning (Prop. G.4) and the congruence property (Cor. G.3). The only
unconventional cases are: the fold operations fold t u, whose proof
is by induction on the number of bases introduced in unfolding the0operation; and graph abstraction ATa ( f ,x ).t, whose proof relies on
Prop. G.5.
H

Graph-contextual equivalence

Proposition H.1 (Prop. 5.4). Let R be a U-simulation. If σ1 Rσ2 ,then there exists a token value κ such that the following are equivalent: σ1 →∗ Final(G 1 ,κ) for some composite graph G 1 , and σ2 →∗Final(G 2 ,κ) for some composite graph G 2 .
Proof. We first prove (i) implies (ii), by induction on the lengthof the sequence σ1 →∗ Final(G 1 ,κ). In the base case, where σ1 =Final(G 1 ,κ), the condition (II) in Def. 5.3 implies σ2 = Final(G 2 ,κ)for some composite graph G 2 . The inductive case, where σ1 →σ10 →∗ Final(G 1 ,κ) for some state σ10 , has two situations. The
first situation is when the condition (I-i) in Def. 5.3 holds. We canuse the induction hypothesis along the transitive closure R + . The
second situation is when the condition (I-ii) holds and there exists
a sequence σ10 →+ σ2 . Because of the determinism of final states(Prop. 3.5), there exists a sequence from the state σ2 to the same
final state Final(G 1 ,κ).
Second, we prove (ii) implies (i), also by induction on the lengthof the sequence σ2 →∗ Final(G 2 ,κ). In the base case, where σ2 =Final(G 2 ,κ), the state σ1 either reduces to the same final state (thecondition (I-ii)) or is the final state itself (the condition (II)). The
inductive case is where σ2 → σ20 →∗ Final(G 2 ,κ) for some state
σ20 . This implies the state σ2 is not final, and therefore neither
is the state σ1 (by the condition (II)). Given a possible transition
σ1 → σ10 , the first situation is when there exists a state σ200 suchthat σ2 → σ200 and σ 0 1 R + σ200 . The states σ20 and σ200 may not be thesame, but thanks to the determinism (Prop. 3.5), they must resultin the same final state Final(G 2 ,κ). We can then use the induction
hypothesis along the transitive closure R + . The second situation iswhen σ10 →+ σ2 holds, and hence σ1 →∗ Final(G 2 ,κ) holds.
The Geometry of Computation-Graph Abstraction
H.1

Beta equivalence

The proof of beta equivalence is via the so-called substitution lemma,
stated below. Unlike normal substitution lemmas used for call-byvalue evaluation, our version does not require the substitute to be avalue. Instead, we require that the substitute is closed and without
cells. Whether the current requirement can be relaxed is an open
question.
Lemma H.2 (Substitution lemma). For derivable judgements A |Γ,x : T 0 , ∆ | p~ ` t : T and A0 | − | − ` u : T 0 , if x ∈ FV(t ),a judgement A ∪ A0 | Γ, ∆ | p~ ` t[u/x] : T is derivable, and thefollowing graph-contextual equivalence holds:
Gu
! t

!

!

t

! t

!

t

x : !T 0⇠=

Gt
TGt[u/x]T

where graphs G t , Gu and G t [u /x ] are components of translations,and !Γt and !∆t are restrictions of !Γ and !∆ to FV(t ) (see Fig. 8).
Sketch of proof. Let three relations ≺D , ≺C and ≺? on graphs be
defined as in Fig. 12 where the graph G (1, 0) does not contain any
links of cell type F. The first step is to show each of these three
relations lifts to a U-simulation, and hence implies graph-contextual
equivalence (Prop. 5.5).
The second step is by induction on the derivation A | Γ,x : T 0 , ∆ |~p ` t : T . Because we assume x ∈ FV(t ), the only base case is wheret is the variable x. This case can be proved solely by the relation≺D . Inductive cases can be shown by combination of the otherrelations, i.e. ≺C and ≺? .
!

Proposition H.3 (Prop. 5.8). Let v be a value defined by the grammar v ::= p | λx T .t | ATa ( f ,x ).t. If the type judgement A0 | − |− ` v : T 0 is derivable, the contextual equivalence A | Γ | p~ `0
(λx T .t ) v ≈ t[v/x] : T holds.
Sketch of proof. Let ≺β be a relation on graphs, defined by
G

G

!

!

@

such that: (i) the graph G (1, 0) does not contain any links of cell
type F, and (ii) there exists a token value κ such that the final state
Final(G,κ) on the graph G (1, 0) is stable (see Def. C.1). It is easy to
see that the relation ≺β lifts to a U-simulation, with the help of thecongruence property (Cor. E.3). Therefore the relation ≺β implies
graph-contextual equivalence, by Prop. 5.5.
If the bound variable x is not free in t, the proof of the contextual
0
equivalence A | Γ | p~ ` (λx T .t ) v ≈ t[v/x] : T boils down to
the relation ≺β and the garbage collection shown in Prop. 5.7.
Otherwise the proof is combination of the relation ≺β and thesubstitution lemma (Lem. H.2). Note that the component Gv of thetranslation of the value v indeed satisfies the condition (ii) of therelation ≺β .
LICS ’18, July 9–12, 2018, Oxford, United Kingdom

!

!
D

G
D

⇡sup(T ) · G

G

!
C

C

...

⇡sup(T ) · G

!

!
!T

?

G

!
!T

Figure 12?

?

G

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica?

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

?

G

!

?
H

H

!

!