A Graph-Rewriting Perspective of the Beta-Law
Dan R. Ghica1 , Koko Muroya1,2 , and Todd Waugh Ambridge1
1University of Birmingham
RIMS, Kyoto University

2xThis preliminary report studies a graphical version of
Plotkin’s call-by-value equational theory, in particular its
soundness with respect to operational semantics. Although an equational theory is useful in safe programtransformation like compiler optimisation, proving its
soundness is not trivial, because it involves analysis ofinteraction between evaluation flow and a particular subprogram of interest. We observe that soundness can beproved in a direct and generic way in the graphical setting,using small-step semantics given by a graph-rewriting abstract machine previously built for evaluation-cost analysis. This would open up opportunities to think of a costsensitive equational theory for compiler optimisation, andto prove contextual equivalence directly in the presence oflanguage extensions.

?
?
x†

D=Cm!

x(λx. t)

†=t

†

t

λ(t u)††u†=D!
@Figure 1: Graph Representation of Terms

1

Call-by-Value Equational TheA graph-equation formula G =g H between graphs G
ory, Graphicallyand H of the same interface is given by the following rules,
as well as the rules that make the graph-equation =g anequivalence.

We first transfer Plotkin’s call-by-value equational theory [5] to a graphical setting, assuming the graph representation of terms that is inductively defined in Fig. 1.
We aim at the very basic lambda-calculus, whose terms
are defined by t, u ::= x | λx.t | t u Both variables andabstractions are referred to as values. A term with nofree variables is said to be closed.
A graph G is directed, and may have n open incomingedges (“input”) and m open outgoing edges (“output”),
in which case we say the graph G has interface (n, m)
and may write G(n, m). Nodes have specific degrees determined by labels, of which λ and @ are taken from thesyntactical constructs (i.e. abstraction and application),and !, ?, D and Cm are taken from the exponential fragment of proof nets [1]. We use bold edges/nodes to represent a bunch of edges/nodes. A Cm -labelled node hasm inputs.
A dashed box, called !-box, delimits a graph of interface
G(1, n) and comes with one !-labelled node connected tothe unique input and n ?-labelled nodes connected to theoutputs. This !-box structure, taken from proof nets, isused to manage duplicable sub-graphs. In particular, it
is used to represent only and all values, which captures
the fact that only a value can be substituted and hence
copied in the call-by-value evaluation.
The graph representation t† of a term t has always oneinput (“root”), and each of its output corresponds to one
occurrence of a free variable of t. In the representation(λx.t)† of abstraction, where the bound variable m appears m times in t, all m edges corresponds to occurrencesof x are connected to a Cm -labelled node.

G ≺χ H(χ-rule)
G =g H

G =g H(Cong)
G[G] =g G[H]A basic χ-rule is given by a relation ≺χ between graphsof the same interface, parameterised by χ ∈ {λ, C, D, ?}.
All these relations are inspired by cut elimination of proofnets [1]. The λ-rule models elimination of constructs λ(abstraction) and @ (application), and the C-rule models
duplication of a value (i.e. a !-box). The other rules, Drules and ?-rules together models replacement of a single
occurrence of a variable with a value. The congruence rule(Cong) involves a graph-context G that is a graph withexactly one special node (“hole”) of label  and arbitrary
interface. Replacing the hole with a graph G yields agraph G[G]. We illustrate these rules by an example, inAppendix A.
The difference between our graphical theory andPlotkin’s syntactical theory [5] lies in basic rules. Outof the two syntactical basic rules, the α-rule λx.t =sλy.(t[y/x]) (where y is not free in t) becomes trivial in
the graphical theory. Difference of variable names does
not change the shape of graph representation (recall thatvariables labelling edges in Fig. 1 are auxiliary). The
other syntactical basic rule, the β-rule (λx.t) v =s t[v/x]
is now decomposed into four graphical basic rules (λ, C, Dand ?). This amounts to extend the lambda-calculus andthe syntactical theory with explicit substitutions t[x ← u].
The decomposition in particular discloses duplication ofvalues as the C-rule.
1

2

Proving Soundnesssituations. The first situation is when the evaluation control physically enters the sub-graph of interest, and theThe key property of an equational theory is soundness, second is when the evaluation control triggers a rewriting
consistency with operational semantics. It ensures that that affects the sub-graph.
two terms equated by the theory are contextually equivaThis proof idea is realised by the following notion oflent, i.e. indistinguishable in any contexts under the op- U-simulation, a variant of simulation. We give a generational semantics.
eral definition for a state transition system → with disWe turn the soundness theorem of the syntactical the- tinguished final states, where (·)+ denotes the transitiveory [5, Thm. 5] graphical, by introducing a graphical ver- closure. It is adapted from the one we used to prove asion of contextual equivalence. Like a context C is given version of beta-equivalence in the presence of an exotic
as a term with one “hole”, a graph-context G is defined language extension [2].
as a graph with exactly one special node (“hole”) of label  and arbitrary interface. Replacing the hole (n, m) Definition 2.3 (U-simulation). A binary relation R onwith a graph G(n, m) of matching interface yields a graph states is a U-simulation, if it satisfies the following twoconditions. (I) If σ1 R σ2 and a transition σ1 → σ10 isG[G].
0We state soundness below with a black-box operational possible, then (i) there exists a graph state σ2 such that00+0
semantics for now: let ⇓g be an “evaluation” relation be- σ2 → σ2 and σ1 R σ2 , or (ii) there exists a sequence0∗ 00
00
tween graphs of interface (1, 0). Recall that closed terms σ1 → σ1 of (possibly no) transitions such that σ1 R σ2 .
(II) If σ1 R σ2 and no transition is possible from the graphare represented by graphs of this interface (1, 0).
state σ1 , no transition is possible from the graph state σ2
Definition 2.1 (Graph-contextual equivalence). Two either. Moreover σ1 is a final state if and only if σ2 is agraphs G1 (n, m) and G2 (n, m) are graph-contextually final state.
equivalent, written as G1 ∼=g G2 , if for any graph conIntuitively, a U-simulation R is the ordinary simulationtext G[] that makes two graphs G[G1 ] and G[G2 ] of interface (1, 0), G1 ⇓g H1 for some graph H1 (1, 0) if and between two states (the condition (I-i) in the above defionly if G2 ⇓g H2 for some graph H2 (1, 0), and moreover nition), “Until” the left sequence of transitions is reduced
to the right sequence (the condition (I-ii)) up to the relaH1 =g H2 .
tion R itself. This is typically when the evaluation control
Theorem 2.2 (Soundness). For any graphs G and H of visits a sub-graph of interest. The sub-graph may not beinterface (1, 0), if G =g H then G ∼=g H.
visited, which resembles the weak until operator of linear
What matters in proving soundness, in particular con- temporal logic. The sub-graph may be duplicated by atextual equivalence, is formulation of the operational se- rewriting step, which is captured by the transitive closure+mantics ⇓g . In the usual syntactical setting, small-step R in the condition (I-i).
Our graph-rewriting abstract machine [3] is given as
semantics is not preferred, because it makes control flowadeterministic
state transition system →, whose stateof evaluation explicit by decomposing a program into aσ=((G,e),δ)consistsof a graph G(1, 0), its selected
context and a sub-term under evaluation. It tends to be“control”
edge
eand
additional
data δ that is a few stacks
hard to analyse interaction between a particular sub-term
usedtoguidethecontrolflow.
Agraph G(1, 0) induces aand the control flow. Plotkin indeed uses compositional
unique“initial”
state
Init(G)anda unique “final” state
big-step semantics, which is proved to be equivalent toFinal(G).
Theevaluation
relation⇓g is defined by G ⇓gsmall-step semantics.
Hiff
there
existsasequence
Init(G)→∗ Final (H).
However, our observation is that one can prove conThanks to the following property, the soundness proof
textual equivalence directly using small-step semantics,
boils
down to a routine work to show that each basic relain a graphical setting. We use in particular the graphtion≺χ , which gives a basic χ-rule of the graph-equational
rewriting abstract machine, previously developed for
1 theory, induces a U-simulation ≺χ .
evaluation-cost analysis [3], as small-step semantics.
This has a potential benefit of designing a cost-sensitive
equational theory, which could be used for compiler optimisation.
The graph-rewriting machine works on graph representation of a whole program, and notably models controlof evaluation as a selected edge of the graph. Evaluation is modelled by two kinds of machine steps: searching steps where the evaluation control is moved aroundthe graph to detect a redex, and rewriting steps where agraph-rewriting rule is applied, resembling reduction of a
sub-term.
This low-level, less-structured nature of the machine
enables us to analyse the interaction between the evaluation control and a particular sub-graph, and hence toprove contextual equivalence, in a simple, step-wise way.
Namely, the interaction boils down to the following twoProposition 2.4. Let ≺ be a binary relation on graphswith the same interface, and its lifting ≺ on graph states
be defined as follows: ((G[G1 ], `), δ) ≺ ((G[G2 ], `), δ) iff
G1 ≺ G2 and the position ` is in the graph-context G[].
If the lifting ≺ is a U-simulation, the binary relation ≺implies the graph-contextual equivalence ∼=, i.e. G ≺ H ⇒G∼= H for any graphs G and H.

Using the graph-rewriting abstract machine, contextual
equivalence can be proved not only directly but also in ageneric way using U-simulations. We expect the graphical perspective would also be useful in the presence oflanguage extensions like ground-type operations, conditional statements and effects. In situations with variouseffects, contextual equivalence is commonly proved via asound and complete method, e.g. logical relation [4] andenvironmental bisimulation [6]. We have seen our method
1 The graph-rewriting abstract machine can be executed on arbitrary closed terms, using our on-line visualiser: https://koko-m. applies to a version of the beta-law for a particular ingithub.io/GoI-Visualiser/ .
stance of language extension [2].
2References[1] Jean-Yves Girard. Linear logic. Theor. Comp. Sci.,
50:1–102, 1987.
[2] Koko Muroya, Steven Cheung, and Dan R. Ghica. Thegeometry of computation-graph abstraction. In LICS
2018, 2018. To appear.
[3] Koko Muroya and Dan R. Ghica. Efficient implementation of evaluation strategies via token-guided graphrewriting. In WPTE 2017, 2017.
[4] Andrew M. Pitts. Reasoning about local variables
with operationally-based logical relations. In LICS
1996, pages 152–163. IEEE Computer Society, 1996.
[5] Gordon Plotkin. Call-by-name, call-by-value and thelambda-calculus. Theor. Comp. Sci., 1(2):125–259,1975.
[6] Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii.
Environmental bisimulations for higher-order languages. In LICS 2007, pages 293–302. IEEE Computer
Society, 2007.

A

Example of Graphical Equation

To illustrate the four kinds of basic rules (λ, C, D and ?),we take as an example two terms T1 and T2 below,
T1 = (λx.(λu.u x) (λu.u x)) (λy.y)
T2 = (λu.u (λy.y)) (λu.u (λy.y))which are beta-equivalent in Plotkin’s call-by-value equational theory.
Given a basic relation ≺χ (χ ∈{λ, C, D, ?}), let a relation 4χ between graphs of the sameinterface be defined by G[G1 ] 4χ G[G2 ] iff G1 ≺χ G2 .
There exists the following chain of relations between
graph representations (T1 )† and (T2 )† of the two terms:(T1 )† = G0 4D G1 4λ G2 4C G3(4? )2 G4 (4? )2 G5 (4D )2 G6 = (T2 )† ,as shown in Fig. 2. First, the basic relation ≺D eliminatesa !-box structure with a D-labelled node connected to itsinput (i.e. to a !-labelled node), which amounts to detect
an abstraction in the function part of an application. Second, the basic relation ≺λ eliminates a connected pair ofa λ-labelled node and an @-labelled node. The rest of
the chain models substitution. The basic relation ≺C duplicates a !-box, i.e. representation of a value. The basic
relation ≺? lets one !-box absorb another !-box connected
to one of its output (i.e. to a ?-labelled node), which models replacement of a variable with a value, together withthe basic relation ≺D . The formula (T1 )† =g (T2 )† canbe proved using the basic rules and the congruence ruleaccordingly, together with transitivity.

3

C2?

!

C2?

?

?

!

D

D?

?
D@?

C1@?

4D

D?

D!

D?

λλC1!
D@C1?

!

C1!

D
D

D?

λ(T1 )† =D

D!

C1?

?

!

D

D@!

C1!

λ!

!

D!

λλ!

!

λ!

D@@!

λD@@

C1

C1C1?

D?

?

DD!

!

λ!

C24λ?

4C?

!

?

D

D
D?

D?

@?
@C1?
D

D
D@!

!
?

!

D

D

D?

!
?

?

?
Dλ!

!

D!

λC1λλ!

!

!

C1!

@!

C1

λλ!

!

D
D@@

C1

C1

C1?

?

?

D

D

D

D!

(4? )2!

λλ!

!

!

!

(4? )2!
?

D

D

DD?
@@!

λ!

!

D

D@
C1

λλ!

!

@

C1?

D

D!

!
λ!
D!

= (T2 )†!

D?
@@
C1

C1
λλ!

!

!

D?

C1?

λ?

D!
D!

D

C1

D!

@!

C1

λ@D!

?

D

(4D )2

λ!
DD?
C1!

λ?
D!

C1?

D@Figure 2: A Chain of Relations that Witnesses (T1 )† =g (T2 )†4