Memoryful Geometry of Interaction
From Coalgebraic Components to Algebraic Effects
Naohiko Hoshino
RIMS, Kyoto University
naophiko@kurims.kyoto-u.ac.jp

Abstract
Girard’s Geometry of Interaction (GoI) is interaction based semantics of linear logic proofs and, via suitable translations, of functional programs in general. Its mathematical cleanness identifies
essential structures in computation; moreover its use as a compilation technique from programs to state machines—“GoI implementation,” so to speak—has been worked out by Mackie, Ghica andothers. In this paper, we develop Abramsky’s idea of resumption
based GoI systematically into a generic framework that accounts
for computational effects (nondeterminism, probability, exception,
global states, interactive I/O, etc.). The framework is categorical:
Plotkin & Power’s algebraic operations provide an interface tocomputational effects; the framework is built on the categorical axiomatization of GoI by Abramsky, Haghverdi and Scott; and, byuse of the coalgebraic formalization of component calculus, we describe explicit construction of state machines as interpretations offunctional programs. The resulting interpretation is shown to besound with respect to equations between algebraic operations, aswell as to Moggi’s equations for the computational lambda calculus. We illustrate the construction by concrete examples.
Categories and Subject Descriptors D.3 [Formal Definitions andTheory]: Semantics; F.3 [Semantics of Programming Languages]:
Algebraic approaches to semantics
General Terms Theory
Keywords Geometry of interaction, monad, algebraic effect1.

Introduction

Geometry of Interaction (GoI) is introduced by Girard [10] as
semantics of proofs—i.e. programs, under the Curry-Howardcorrespondence—for the study of dynamics and invariants of thecut elimination process (i.e. program execution). Girard’s original
presentation of GoI is in the language of C ∗ -algebras; Mackie’s
alternative presentation [25] as token machines initiated anotherimportant application of GoI, namely as a compilation technique.
There GoI provides translation of programs into state machines;
and the machines’ execution results are invariant under cut elimination. Dynamics in such machines can be understood as a math-Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. Copyrights for components of this work owned by others than ACM
must be honored. Abstracting with credit is permitted. To copy otherwise, or republish,
to post on servers or to redistribute to lists, requires prior specific permission and/or afee. Request permissions from permissions@acm.org.
CSL-LICS 2014, July 14–18, 2014, Vienna, Austria.
Copyright c 2014 ACM 978-1-4503-2886-9. . . $15.00.
http://dx.doi.org/10.1145/2603088.2603124

Koko Muroya

Ichiro Hasuo

Dept. Computer Science, University of Tokyo
muroykk@is.s.u-tokyo.ac.jp ichiro@is.s.u-tokyo.ac.jp

ematical counterpart of control flow in program execution, and in
this way, GoI connects mathematics (denotational semantics), program evaluation (operational semantics) and state based computation (low-level languages/implementations). Applications of GoI
are widespread: implementation of (imperative) functional programming languages [8, 9, 25]; relationship to Krivine abstract
machines [7] and to defunctionalization [30]; optimal graph reduction for the lambda calculus [11]; and the design of a functional
programming language for sublinear space [6].
Categorical GoI
This remarkable level of integration in GoI—of operational anddenotational/structural semantics—is further exemplified by its
categorical axiomatics (categorical GoI) developed by Abramsky,
Haghverdi and Scott [2]. There a general construction is given froma traced monoidal category—together with additional constructs,
altogether called a GoI situation—to a combinatory algebra. One
can then apply the realizability construction (see e.g. [24]) thatturns a combinatory algebra (an “untyped” model) into a categorical model of a typed calculus, from which one extracts realizers as
concrete interpretations. The latter are sound by construction.
In a big picture, the current work is one of the attempts to instantiate this general methodology of categorical GoI to concrete situations. Our starting point is the previous work [14] where we extend the above workflow by a step prior to it. The extension comesfrom the following observation (a folklore result, see Lemma 4.3;
see also [18]): many traced monoidal categories arise as a Kleisli
category of a monad with a suitable order structure. The resulting
extended workflow is as follows.
(a Set-monad T whose Kleisli category is Cppo-enriched)
Kleisli construction
7−→(a traced monoidal category)
categorical GoI [2]7−→realizability &realizer extraction

7−→(a combinatory algebra)(1)(a GoI interpretation of a typed calculus)

In [14] we pursued use of this extended general workflow that isparametrized by T : in order to interpret a calculus with a certain
additional feature, we start with a monad T equipped with the samefeature, and the generic constructions would yield a suitable GoI
interpretation. In [14], specifically, we considered a calculus forquantum computation.
Effects and Resumption Based GoI
However, following this naive scenario turned out to be far fromstraightforward: in [14] we ended up using a complicated continuation monad that keeps track of all the measurement outcomes. In
fact the same kind of difficulty is already with nondeterminism—
one of the most basic computational effects—as we exhibit now.
Here we shall speak on the intuitive level, using the game-theoreticterms of queries and answers instead of the categorical language
for GoI.
Consider the call-by-value evaluation of the program(λx : nat. x + x) (0 t 1)

(2)

where the subterm 0 t 1 returns 0 or 1 nondeterministically. Thenthe whole program is expected to return 0 or 2. However, the usual
GoI interpretation of (2) may return an unexpected value 1, as theresult of the following interaction.
1. We ask the value of the left occurrence of x in x + x.
2. The subterm 0 t 1 answers 0 or 1 nondeterministically.
3. We ask the value of the right occurrence of x in x + x.
4. The subterm 0 t 1 answers 0 or 1 nondeterministically.
5. We add the values of the left x and the right x.
The difficulty is as follows. After the first query 2), the nondeterminism in the subterm 0 t 1 is resolved, with the subterm reduced
to 0 or 1. The second query 4) must stick to this choice; however,most instances of GoI—presented in terms of C ∗ -algebra, tokenmachines or categories—lack such an explicit “memory” mechanism. The lack of memories in GoI causes similar difficulties withother computational effects. Even more, it seems to be also thereason why additive connectives are far less trivial to interpret in
GoI: additive slices—a common tool for additive connectives in
GoI [23, 33]—indeed have a strong flavor of memories. In the previous example (2) one may wonder if the call-by-value evaluation
strategy is to blame. This is unlikely; see Remark 1.1.
The memory mechanism needed in the above example can beprovided in the form of a Mealy machine, or a (nondeterministic)transducer. The term 0 t 1 is now interpreted as
q/0: x0 o

q/0



x0t1

q/1

/ x1 dq/1(3)

where the machine can initially respond to a query q with 0 or
1; however, after that the machine sticks to the same choice byremembering the state by means of its internal state. For more
examples of Mealy-like machines, see Section 7.
The idea of using such memories (or states) in GoI is not new.
In [1, 2], an instance of categorical GoI is given by the categoryof resumptions—roughly speaking, a resumption from a set A to
B is a “stateful computation” from A to B; more precisely it is asuitable equivalence class (e.g. modulo bisimilarity) of transducers
from A to B. In [2] it is also characterized as an element of a final
coalgebra.
Remark 1.1. Lack of memories in effectful situations causes difficulties in GoI regardless of evaluation strategies. Consider theequation (t t s) u = t u t s u; we expect it to hold regardlessof evaluation strategies. In the GoI interpretation of (t t s) u, whenu receives a query from the t part in t t s, we must make sure thatthe response goes back to t, not to s. It is not clear how to enforce
this without using memories, as one would see trying to interpretthe program in (any presentation of) GoI.
Contributions—from Coalgebraic Components to Algebraic
Effects
Building on Abramsky’s idea of resumption based GoI, the current
paper aims at a generic framework that yields GoI interpretations—or rather GoI implementations, since they are given concretely asstate based transducers like in (3)—of calculi with various computational effects.
More specifically: we model an effect by a monad T following Moggi [26]; and as an syntactic interface we use algebraic operations like t for the powerset monad P, following

Plotkin & Power [28]. Concrete interpretations are given by (statebased) transducers with the same effect T , much like the nondeterministic one in (3). Assuming that T comes with a suitable
Cppo structure—many effects qualify by the slight modificationof adding partiality—we show that the category Res(T ) of T resumptions is traced monoidal. Then the general workflow in (1),starting from its second step, yields a GoI interpretation of a calculus, with transducers as realizers. The resulting interpretation
is sound with respect to the algebraic axioms (e.g. associativityof t) as well as Moggi’s equations for the computational lambda
calculus.
This overall procedure—from a monad T and algebraic operations to a GoI interpretation in the form of T -transducers—we wish
to call memoryful GoI, emphasizing the role of memories (“memories” here are the same as “internal states”; the choice is to distinguish from the global “state” monad). A novelty is the use ofmemories (in the form of internal states of transducers) that allows
us to describe interpretations of algebraic effects in a generic yet
concrete manner.
We describe the construction of transducers concretely in termsof coalgebraic component calculus. Component calculi are heavily
studied in software engineering (see e.g. [4]) as means of composing software components. A major concern there is compositionality, much like in the study of process calculi (see e.g. [3]); and successful (co)algebraic techniques have been developed for the latter [21, 32] as well as for the former [5]. We rely on the categoricalformalization of component calculi in [5, 15] where components
are coalgebras; categorical genericity is needed since our transducers are parametrized by a monad T . In this way, the current work
pursues “some convergence and unification”—suggested in the paper [1], from which we draw inspirations—of GoI and coalgebra,
in program semantics.
Organization of This Paper In Section 2 we recall categorical
GoI, and in Section 3 we summarize notations used in this paper.
In Section 4 we introduce component calculus on transducers; inSection 5 we quotient components by behavioral equivalence anddefine a traced symmetric monoidal category of sets and resumptions. In Section 6, we sketch construction of categorical models of
the computational lambda calculus based on categorical GoI withtransducers; the resulting GoI interpretation is described in Section 7 with concrete examples. Due to space limitation, some proofs
and argument in this paper are deferred to an extended version.

2.

Categorical Geometry of Interaction

We recall a categorical formulation of GoI called GoI situation introduced by Abramsky, Haghverdi and Scott and pin down the obstacle explained in the introduction in mathematical terms. A crucial notion in their categorical axiomatics is that of traced symmetric monoidal category.
Definition 2.1. A traced symmetric monoidal category is a symmetric monoidal category (C, ⊗, I) with a family of maps
trC
A,B : C(A ⊗ C, B ⊗ C) → C(A, B)
subject to certain conditions (see [13, 20]).
Definition 2.2. Let C be a traced symmetric monoidal category.
A traced symmetric monoidal functor F : C → C is a strong
symmetric monoidal functor such that
C
−1
C
trF
F A,F B (mB,C ◦ F f ◦ mA,C ) = F (trA,B (f ))for all C-morphisms f : A ⊗ C → B ⊗ C where mA,B : F A ⊗F B → F (A ⊗ B) is the coherence isomorphism of F .
For example, the category (Rel, +, ∅) of sets and relations
forms a traced symmetric monoidal category: for a Rel-morphism

f : A + C → B + C, we define the trace operator trC
A,B (f ) : A →B by the execution formula[n
trC
fCB ◦ fCC
◦ fAC
A,B (f ) = fAB ∪n≥0where fXY : X → Y is the restriction of f to a relation between
X and Y .
Definition 2.3. A GoI situation is a list (C, U, F, φ, ψ, u, v) consisting of a traced symmetric monoidal category (C, ⊗, I), a Cobject U and a traced symmetric monoidal functor F : C → C withretractions φ : U ⊗ U C U : ψ and u : F U C U : v together with thefollowing retractionsn : I C U : n0eA : A C F A : e0A

cA : F A ⊗ F A C F A : c0A

for the canonical bijections. We write >A : A → 1 and ⊥A : ∅ →A for the unique maps. For sets I and A, we write AI for the I-foldproduct of A.
Let (T, η, µ) be a monad on Set. In order to distinguish maps
from morphisms in the Kleisli category SetT , we write f : A →T
B when f is a SetT -morphism from A to B. Since T is a monadon Set, we have tensorial strengths
stA,B

T A × B −−−−→ T (A × B),

For SetT -morphisms f : A →T B and g : B →T C, a map
h : A → B and a set D, we define SetT -morphisms g ◦T f , f ⊗D,
D ⊗ f and h∗ byg ◦T f = µC ◦ T g ◦ f : A →T C,

dA : F F A C F A : d0Af ⊗ D = stB,D ◦ (f × D) : A × D →T B × D,

0wA : I C F A : wA

D ⊗ f = st0D,B ◦ (D × f ) : D × A →T D × B,

such that eA , dA , cA and wA are natural in A.
The retraction (φ, ψ) and (n, n0 ) provides GoI interpretation of themultiplicative fragment of linear logic, and the traced symmetricmonoidal functor F with the remaining retractions provide GoI
interpretation of the exponential fragment of linear logic. In [2],a GoI situation is shown to yield a linear combinatory algebra; via
the Girard translation, we obtain an SK-algebra that is a model of
intuitionistic logic.
Proposition 2.4. Let (C, U, F, φ, ψ, u, v) be a GoI situation. The
set C(U, U ) with the binary application a • b on C(U, U ) given bya • b = trU
U,U ((U ⊗ (u ◦ F b ◦ v)) ◦ ψ ◦ a ◦ φ)forms an SK-algebra: there exist S, K ∈ C(U, U ) such thatS • a • b • c = a • c • (b • c),K •a•b=awhere we assume that the binary application is left associative.
On the categorical level, the obstacle in the introduction stems
from the fact that the trace operator tr on Rel does not preserve
the union of relations:CC
trC
A,B (f ∪ g) = trA,B (f ) ∪ trA,B (g) ∪ gCB ◦ fAC ∪ · · · (4)Failure of preservation of the trace results in failure of the equation:(a ∪ b) • c 6= (a • c) ∪ (b • c)(5)

in the SK-algebra (Rel(U, U ), •) constructed from a GoI situation(Rel, U, F, φ, ψ, u, v). The unexpected value returned by the program (2) appears in the extra summands in (4).
Remark 2.5. In the original definition of GoI situation in [2], theretractions (e, e0 ), (d, d0 ), (c, c0 ) and (w, w0 ) are required to bemonoidal natural transformations. In this paper, we only require
the injection side of retractions to be natural since this is enoughto prove Proposition 2.4. This relaxation is needed in our concrete
examples. We also note that since we do not require e, d, c and w to
be monoidal, the retraction pairs (e, e0 ), (d, d0 ), (c, c0 ) and (w, w0 )do not give rise to pointwise natural transformations. Pointwise
naturality is required in [2] to construct weak linear category.

3.

Notations

We summarize several notations used in this paper. Let Set be thecategory of sets and maps (i.e. functions). We write
inlA,B

inrA,B

A −−−−→ A + B ←−−−− B,γ

A + A −−A→A

for the injections and the codiagonal map. We write
σA,B

A × B −−−→ B × A,

δA,B,C

st0A,BA × T B −−−−→ T (A × B).

A × B + A × C −−−−−→ A × (B + C)h∗ = ηB ◦ h : A →T B.
The first construction is the composition of Kleisli morphisms. The
second and the third constructions are the premonoidal products in
SetT . See [29] for premonoidal category, although further familiarity will not be needed. For SetT -morphisms f : A →T B andg : C →T D such that(f ⊗ D) ◦T (A ⊗ g) = (B ⊗ g) ◦T (f ⊗ C),
we write f ⊗ g for (f ⊗ D) ◦T (A ⊗ g); this happens when T
is a commutative monad. The last construction (−)∗ is the Kleisli
inclusion from Set to SetT , which lifts the (finite) coproducts(∅, +, inl, inr) of Set to (finite) coproducts (∅, +, inl∗ , inr∗ ) of
SetT .
For legibility, we omit some obvious isomorphisms in the remainder of this paper. For example, we write ηA for a map from
1 × A to T (1 × A) obtained by composing ηA with obvious isomorphisms.

4.

Transducers and a Component Calculus

4.1

Transducer

Transducers are “functions with internal states.”
Definition 4.1. Let T be a monad on Set. For sets A and B,
a T -transducer from A to B is a pair (X, c) consisting of a set
X together with a SetT -morphism c : X × A →T X × B.
A pointed T -transducer is a triple (X, c, x) consisting of a T transducer (X, c) and a map x : 1 → X. We often drop theword ‘pointed’ in ‘pointed T -transducer.’ When (X, c, x) is a T transducer from A to B, we write (X, c, x) : A _ B.

A T -transducer (X, c, x) is a machine consisting of a set of(internal) states X, an initial state x and a transition rule c. For
example, when T is the identity functor, an equation c(y, a) =(y 0 , a0 ) means that if an input is a and the current internal state of
the machine is y, then the machine outputs a0 and the next internal
state is y 0 . The monad T enables us to consider various effects oftransition rules: when T is the powerset monad, transition rules arenondeterministic.
Requirement 4.2. Throughout the paper we require that the symmetric monoidal category (SetT , +, ∅) has a trace operator tr thatsatisfies the following restricted uniformity [12]: for all h : C →D, f : A + C →T B + C and g : A + D →T B + D, if
D(B + h∗ ) ◦T f = g ◦T (A + h∗ ), then trC
A,B (f ) = trA,B (g).
It is typical in particle style GoI [2] that the underlying traced
symmetric monoidal category of a GoI situation is a Kleisli category with a trace operator that is uniform in the above restrictedsense. The next lemma is useful for checking Requirement 4.2. Wewrite Cppo for the category of pointed complete posets (cpo) andcontinuous maps. We consider Cppo-enrichment with respect tothe symmetric monoidal structure given by the finite products. A
Cppo-enriched cocartesian category C is a Cppo-enriched category whose underlying category has finite coproducts such that the
coproduct f + g : A + B → C + D is continuous on f and g.
Lemma 4.3. If the Kleisli category SetT is a Cppo-enriched cocartesian category such that the bottom morphisms ⊥A,B : A →T
B satisfy the following conditions:

For T -transducers (X, c, x) : A _ B and (Y, d, y) : B _ C,
we define a “composition”(Y, d, y) ◦ (X, c, x) : A _ C

to be (X × Y, e, x × y) where e is a SetT -morphism from X ×
Y × A to X × Y × C given by∗∗(X ⊗ d) ◦T (X ⊗ σB,Y) ◦T (c ⊗ Y ) ◦T (X ⊗ σY,A).

This is the sequential composition of machines:C• f ◦T ⊥A,B = ⊥A,B 0 for all f : B →T B 0• ⊥A,B ◦T g ∗ = ⊥A0 ,B for all g : A0 → A(Y,d,y)(Y, d, y) ◦ (X, c, x) =B
(X,c,x)then (SetT , +, ∅) satisfies Requirement 4.2.

A

In the following examples, we can use Lemma 4.3 to check Requirement 4.2: we combine partiality with the standard definitionsof monads so that the Kleisli categories are enriched over Cppo.

We note that this is an intuitive representation of the composition
and is inept for rigorous reasoning. For example, the composition
of T -transducers fails to be associative in the strict sense.

Example 4.4. We give leading examples of monads that satisfy
Requirement 4.2.

4.2.2

Monoidal ProductWe define a “monoidal product”• The lift monad LA = 1 + A.
• The (full) powerset monad PA = 2A and the countable pow-

(X, c, x)  (Y, d, y) : A + C _ B + D

of T -transducers (X, c, x) : A _ B and (Y, d, y) : C _ D to be(X × Y, e, x × y) where

erset monad Pω A = {a ⊆ A | a is countable}.
• The probabilistic subdistribution monade : X × Y × (A + C) →T X × Y × (B + D)

P
DA = d : A → [0, 1] | a∈A da ≤ 1

is a unique SetT -morphism such that

where [0, 1] is the unit interval.
• A global state monad SA = (1 + A × V L )V

L

where V and L

are (countable) sets.
• A writer monad T A = 1 + M × A where M is a monoid.
• An exception monad EA = 1 + E + A where E is a set.
• A continuation monad T A = RA ⇒ R where R is a pointed
cpo and RA ⇒ R is the set of continuous maps from the A-foldproduct of R to R.
• An I/O monad T A = νD. (O × D + D I + A)⊥ where O and
I are (countable) sets.
In the last example, we regard a set as a cpo with the discrete order,
and D⊥ is the pointed cpo obtained by adding a bottom element toa cpo D. For an endo-functor F on Cppo, the fixed point νD. F D
denotes a final F -coalgebra in Cppo.
4.2

A Component Calculus

We shall extend some constructions on SetT to constructions on
T -transducers, namely the sequential composition f ◦T g, the traced
symmetric monoidal structure (SetT , +, ∅, tr) and algebraic operations on T . These extensions will organize T -transducers into a“traced symmetric monoidal category,” on which we will define a“GoI situation.” Here the quotation marks (“so to speak”) are because the equational axioms of traced symmetric monoidal category and GoI situation hold only up-to suitable equivalences between T -transducers. In Section 5, we will (properly) introduce a
traced symmetric monoidal category and a GoI situation as quotients of the “traced symmetric monoidal category” and the “GoI
situation” in this section.
4.2.1

Identity and Composition

For a set A, we define an “identity” on A to be the obvious one-state
T -transducer(1, ηA , id1 ) : A _ A.
Generalizing the above “identity,” we have a construction J froma SetT -morphism f : A →T B to a T -transducer Jf : A _ B
defined by (1, f, id1 ). For a map g : A → B, we define a T transducer J0 g : A _ B as the composition of J and the Kleisli
inclusion, namely (1, g ∗ , id1 ).

∗e ◦T (X ⊗ Y ⊗ inl∗A,C ) = (σY,X⊗ inl∗B,D )∗◦T (Y ⊗ c) ◦T (σX,Y⊗ A),e ◦T (X ⊗ Y ⊗ inr∗A,C ) = (X ⊗ Y ⊗ inr∗B,D ) ◦T (X ⊗ d).
The “monoidal product”  is the parallel composition of machines:(X,c,x)(Y,d,y)(X, c, x)  (Y, d, y) =.
The T -transducers (X, c, x) and (Y, d, y) behave independently
following their own internal states.
4.2.3

Trace

For a T -transducer (X, c, x) : A + C _ B + C, we define a T transducer TrC
A,B (X, c, x) : A _ B to be


X×C
∗
∗
X, trX×A,X×B ((δX,B,C)−1 ◦T c ◦T δX,A,C), x .
Here δ is the bijection in Section 3 and tr is the trace operatorof SetT . The operator Tr is a “trace operator” with respect tothe “symmetric monoidal structure” (, ∅). Checking that trace
axioms are indeed “satisfied” is laborious but doable; see [15]. The“trace operator” introduces feedback:
B

C

A

B
TrC
A,B

(X,c,x)7−→

C(X,c,x)AC

The internal states enable us to memorize history of feedbacking.
Let L be the lifting monad given in Example 4.4. Then the internal
states of an L-transducer
given by({0, 1, · · · , n}, c, 0) : {0} + {0} _ {0} + {0}((0, inr{0}+{0} (0)) (i < n)(0, inl{0}+{0} (0)) (i = n)((i + 1, inr{0}+{0} (0)) (i < n)(0, inl{0}+{0} (0))(i = n)c(i, inl{0}+{0} (0)) =c(i, inr{0}+{0} (0)) =For T -transducers (X, c, x), (Y, d, y) : N _ N, we define a T transducer (X, c, x) • (Y, d, y) : N _ N to bememorizes number of feedback loops.
4.2.4

GoI Situation

TrNN,N ((N  (J0 u ◦ F (Y, d, y) ◦ J0 v)) ◦ J0 ψ ◦ (X, c, x) ◦ J0 φ).

Let N be the set of natural numbers. We define maps
$n,X : X N → X N × X,

κn : 1 → N,

f N : AN → B N

to be the constant map κn (∗) = n, the permutation that picks then-th element, and the N-fold product of a map f : A → B.
For a set A, we define a set F A to be N × A, and for a T transducer (X, c, x) : A _ B, we define a T -transducer

Since (N, F, J0 φ, J0 ψ, J0 u, J0 v) is a “GoI situation,” the set of
T -transducers with the binary application (−) • (−) forms an “SKalgebra” by Proposition 2.4. The binary application consists ofparallel composition plus hiding:F (X, c, x) : F A _ F B(X, c, x) • (Y, d, y) =to be (X N , c0 , xN ) whose transition map

J0 ψ

J0 u

(X,c,x)F (Y,d,y)

J0 φ

J0 v

c0 : X N × N × A →T X N × N × B.
Hiding means that we can not observe interaction between J0 u ◦F (Y, d, y) ◦ J0 v and J0 ψ ◦ (X, c, x) ◦ J0 φ from outside.

is a unique SetT -morphism such thatc0 (−, n, −) : X N × A →T X N × N × B =∗∗(($n,X)−1 ⊗ κ∗n ⊗ B) ◦T (X N ⊗ c) ◦T ($n,X⊗ A)

for all natural numbers n. The construction F , which corresponds
to the linear exponential comonad of linear logic, introduces aparallel composition of countably infinite copies:


B
B
B
(X,c,x) ···(X,c,x)(X,c,x)F (X, c, x) =.
A
AAEach (X, c, x) in F (X, c, x) behaves independently.
We choose bijections φ : N + N ∼= N : ψ and u : F N ∼= N : v in
Set, which induce the following “retractions”∼ N : J0 ψ,∼ N : J0 v.
J0 φ : N + N =J0 u : F N =The list (N, F, J0 φ, J0 ψ, J0 u, J0 v) forms a “GoI situation.” Infact, we have the following “retractions”

Remark 4.5. Since we work in untyped setting (at the transducer
level), it is straightforward to extend our results to model polymorphic calculi. For modeling computational lambda calculi without
polymorphism, you can choose typed approach, which will simplify our framework.
4.2.5

Algebraic Operation

We extend algebraic operations on the monad T to operations on
T -transducers. We first recall the definition of algebraic operation,
which is a mathematical interface to computational effects.
Definition 4.6 ([28]). Let T be a strong monad on a cartesianclosed category (C, 1, ×, ⇒) with countable products, and let I bea countable set. An I-ary algebraic operation on T is a family of
C-morphisms{αA,B : (A ⇒ T B)I → (A ⇒ T B)}A,B∈C

J0 ⊥N : ∅ C N : J(trNN,∅ (γN∗ ))J0 (κ1 × A) : A C F A : J0 (>N × A)
J0 (u × A) : F F A ∼= F A : J0 (v × A)

(dereliction)such that(digging)

αA0 ,B 0 ◦ cpI ◦ ∆ = cp ◦ ((B ⇒ T B 0 ) × αA,B × (A0 ⇒ A))A∗
J0 ⊥F A : ∅ C F A : J(trF
F A,∅ (γF A ))∼ F A : J0 (ψ × A)
J0 (φ × A) : F A + F A =(weakening)

where(contraction)

cp : (B ⇒ T B 0 ) × (A ⇒ T B) × (A0 ⇒ A) → (A0 ⇒ T B 0 )where we omit several obvious “isomorphisms.”
We illustrate how these “retractions” act on T -transducers. We
note that a pair of T -transducers000(Y, d, y) : A0 _^A : (Y , d , y )induces a translation of T -transducers:(X, c, x) : A _ A 7−→(Y 0 , d0 , y 0 ) ◦ (X, c, x) ◦ (Y, d, y) : A0 _ A0 .

For a T -transducer (X, c, x) : A _ A, dereliction pulls out the first(X, c, x) in F (X, c, x), and digging sorts F (X, c, x) into a bunchof bunches of (X, c, x)’s:
..

..

.

..

.

.

diggingdereliction

7−→

···

7−→

,

.

Weakening discards F (X, c, x) completely, and contraction sorts
F (X, c, x) into a pair of F (X, c, x)’s:
..

..

.
weakening

7−→

∅

..

.

.

..

∆ : (B ⇒ T B 0 ) × (A ⇒ T B)I × (A0 ⇒ A) →((B ⇒ T B 0 ) × (A ⇒ T B) × (A0 ⇒ A))I
is the C-morphism that is diagonal in the first argument and thethird argument. We write ary(α) for I.
We define AlgOpT to be the category of algebraic operations
on T : an object is a countable set, and a morphism from I to I 0 is afamily of C-morphisms
0{αA,B : (A ⇒ T B)I → (A ⇒ T B)I }A,B∈C
such that the family {πj A,B ◦ αA,B }A,B∈C is an I-ary algebraic
operation for all j ∈ I 0 where πj A,B is the j-th projection from0(A ⇒ T B)I to A ⇒ T B. The category AlgOpT has countableproducts given by the disjoint sum.
Example 4.7. We give examples of algebraic operations.

.

• A binary algebraic operation ⊕ on P given bycontraction

7−→,is the (Kleisli) composition, and.

The construction of GoI situation is essentially equivalent to thosein [2]. For operational description of GoI situation, see [16].

(f ⊕A,B g)(a) = f (a) ∪ g(a)where we use an infix notation. We will use the operation ⊕ tointerpret the t construct in the introduction.

• A binary algebraic operation ⊕p on D given by(f ⊕pA,B g)(a) = p · f (a) + (1 − p) · g(a)where p is a real number in the unit interval [0, 1].
• A state monad SX = (1 + X × V L )V

L

for a countable set of
locations L and a countable set of values V has the following
algebraic operations
lookup`,A,B : SetS (A, B)V → SetS (A, B),
updatev,`,A,B : SetS (A, B) → SetS (A, B)
for each ` ∈ L and v ∈ V given by((lookup`,A,B (f ))(a))(s) = (fs(`) (a))(s),((updatev,`,A,B (f ))(a))(s) = (f a)(s[v/`])
where the state s[v/`] ∈ V L is given by s[v/`](`0 ) = s(`0 ) for` 6= `0 and s[v/`](`) = v.

For other examples of algebraic operations, see [28].
For a monad T on Set, an I-ary algebraic operation α on T anda family of T -transducers {(Xi , ci , xi ) : A _ B}i∈I , we define
αA,B {(Xi , ci , xi )}i∈I : A _ B

to be a T -transducer (1 + Y, d, inl1,Y ) consisting of a coproduct
`
inji
Y =
−− Xi and a unique SetT -morphism d fromi∈I Xi ←(1 + Y ) × A to (1 + Y ) × B satisfying
d ◦T (inl∗1,Y ⊗ A) = αA,(1+Y )×B {c0i }i∈Id ◦T ((inr∗1,Y ◦T inj∗i ) ⊗ A) = ((inr∗1,Y ◦T inj∗i ) ⊗ B) ◦T ci
where c0i is a SetT -morphism from A to (1 + Y ) × B given by(inr∗1,Y ⊗ B) ◦T (inj∗i ⊗ B) ◦T ci ◦T (x∗i ⊗ A).
Intuitively, the construction αA,B introduces branching at the(fresh) initial state. A T -transducer αA,B {(Xi , ci , xi )}i∈I memorizes the first branching information using its internal states, and after the first branching, the behavior of αA,B {(Xi , ci , xi )}i∈I in thei-th branching follows the i-th T -transducer (Xi , ci , xi ) for eachi ∈ I. For example, the nondeterministic Mealy machine in (3) isthe same as the following P-transducer({x0 }, c0 , x0 )⊕{q},{0,1} ({x1 }, c1 , x1 ) : {q} → {0, 1}
where ({xi }, ci , xi ) : {q} _ {0, 1} are P-transducers given byci (xi , q) = (xi , i) for i = 0, 1.

5.

Behavioral Equivalence

We have presented “GoI situation” on the “traced symmetricmonoidal category” of sets and T -transducers. Precisely speaking, they are not so in a strict sense: in order to satisfy the equational axioms of traced symmetric monoidal category and GoI
situation, T -transducers must be suitably quotiented. For example, (X, c, x) ◦ (1, ηA , id1 ) is not equal to (X, c, x), and we need
to identify them. In this paper, we use behavioral equivalence, anotion common in coalgebra [19]. Intuitively, two (pointed) T transducers are behaviorally equivalent if the initial states are connected by a zigzag of homomorphisms.
Definition 5.1. Let (X, c, x) and (Y, d, y) be T -transducers from
A to B. A homomorphism from (X, c, x) to (Y, d, y) is a map
h : X → Y such that (h∗ ⊗B)◦T c = d◦T (h∗ ⊗A) and h◦x = y.
Definition 5.2. For T -transducers (X, c, x) and (Y, d, y) from A
to B, we say that (X, c, x) is behaviorally equivalent to (Y, d, y)
if there is a T -transducer (Z, e, z) : A _ B and homomorphisms from (X, c, x) to (Z, e, z) and from (Y, d, y) to (Z, e, z).
When (X, c, x) is behaviorally equivalent to (Y, d, y), we write(X, c, x) 'TA,B (Y, d, y).

A zigzag of homomorphisms can be reduced to a cospan used in theprevious definition, since the category of T -transducers (identified
as coalgebras) has pushouts. See [19].
Up to the behavioral equivalence, we can drop the quotation marks in Section 4.2. It is easy to check that constructions◦, , Tr, F, • and α are compatible with the behavioral equivalence. Below we abuse notations: we use , Tr, F and • for operators on T -transducers as well as those on equivalence classes ofT -transducers.
We define a category Res(T ) by
• Objects are sets.
• Morphisms from A to B are 'T
A,B -equivalence classes of T -transducers from A to B.
For a T -transducer (X, c, x) : A _ B, we write [(X, c, x)] for
the Res(T )-morphism from A to B represented by (X, c, x). The
identity on A is [(1, ηA , id1 )], and the composition of a Res(T )morphism [(X, c, x)] from A to B and a Res(T )-morphism[(Y, d, y)] from B to C is [(Y, d, y) ◦ (X, c, x)].
The category Res(T ) with (, ∅, Tr) is a traced symmetricmonoidal category. The coherence isomorphisms of the symmetricmonoidal category (Set, +, ∅) induce coherence isomorphisms of(Res(T ), , ∅). The following list
(Res(T ), N, F, [J0 φ], [J0 ψ], [J0 u], [J0 v])
is a GoI situation, and (Res(T )(N, N), •) is an SK-algebra.
Theorem 5.3. Let α be an I-ary algebraic operation on T . The
operator α is natural, and Tr is distributive over α modulo the
behavioral equivalence:• For each T -transducer (X, c, x) : B _ B 0 , for each familyof T -transducers {(Yi , di , yi ) : A _ B}i∈I and for each map
h : A0 → A, it holds that(X, c, x) ◦ αA,B {(Yi , di , yi )}i∈I ◦ J0 h
'TA0 ,B 0 αA0 ,B 0 {(X, c, x) ◦ (Yi , di , yi ) ◦ J0 h}i∈I .

• For each family of T -transducers {(Xi , ci , xi )}i∈I from A+C

to B + C, it holds that
TrC
A,B (αA+C,B+C {(Xi , ci , xi )}i∈I )'TA,B αA,B {TrC
A,B (Xi , ci , xi )}i∈I .

(6)Let α be an I-ary algebraic operation on T . The following
behavioral equivalence is a consequence of Theorem 5.3:
αN,N {(Xi , ci , xi )}i∈I • (Y, d, y)'TN,N αN,N {(Xi , ci , xi ) • (Y, d, y)}i∈I(7)

where {(Xi , ci , xi )}i∈I and (Y, d, y) are T -transducers from N to
N. In fact, we have
αN,N {(Xi , ci , xi )}i∈I • (Y, d, y)= TrNN,N ((Z, e, z) ◦ J0 ψ ◦ αN,N {(Xi , ci , xi )}i∈I ◦ J0 φ)'TN,N TrNN,N (αN,N {(Z, e, z) ◦ J0 ψ ◦ (Xi , ci , xi ) ◦ J0 φ}i∈I )'TN,N αN,N {TrNN,N ((Z, e, z) ◦ J0 ψ ◦ (Xi , ci , xi ) ◦ J0 φ)}i∈I= αN,N {(Xi , ci , xi ) • (Y, d, y)}i∈I
where we write (Z, e, z) for N  (J0 u ◦ F (Y, d, y) ◦ J0 v). The firstequivalence follows from naturality of α, and the second equivalence follows from distributivity of Tr over α. The behavioral
equivalences (6) and (7) are the equivalences that we wish to holdas we observed at the end of Section 2.

6.

Realizability and Categorical Models

In the next section, we exemplify GoI interpretation of algebraic
effects. The purpose of this section is to sketch how to derive them:
we use realizability technique. For details of arguments and proofs
in this section are deferred to an extended version.
From the SK-algebra (Res(T )(N, N), •), we can utilize therealizability construction and constructs a cartesian closed category
Per(T ) consisting of partial equivalence relations on the SKalgebra Res(T )(N, N) and realizable maps. See [17] for a precise
definition of the category of partial equivalence relations. Since
the category Per(T ) has countable products, we can consider
algebraic operations with countable arities on monads on Per(T ).
The next theorem is our main theorem, from which soundnessof GoI interpretation that we are going to give follows.
Theorem 6.1. The cartesian closed category Per(T ) has a strong
monad Φ and an identity-on-object countable-product-preserving
faithful functor (−)† : AlgOpT → AlgOpΦ .
We only give a definition of ΦR for R in Per(T ). Let h be a map
from N to N given by• If t ≈ s and τ is the base type nat, then LtM 'T
N,N LsM.

where [LtM] is the Res(T )-morphism represented by LtM, and wewrite t ≈ s when the equation holds in the extension of thecomputational lambda calculus. For example, we havev (3 t 5) ≈ v 3 t v 5,3t5t3≈3t5≈5t3

for any value v when the extension of the computational lambda
calculus has nondeterminism.

7.

GoI Interpretation of Algebraic Effects

7.1

Memoryless GoI Interpretation

For comparison, we first present (memoryless) GoI interpretationof the following programs:(λxy : nat. x + y) 5 3(λx : nat. x + x) 3.

We write g for φ ◦ inlN,N , d for φ ◦ inrN,N like [23] and hn, mi foru(n, m). For i ∈ N, we define a map ki : N → N byφ ◦ (φ + N) ◦ (N + ς) ◦ (ψ + N) ◦ ς ◦ (φ + N) ◦ (N + ς) ◦ (ψ + N) ◦ ψ

ki hm, ni = hm, ii,

where ς : N + N → N + N is the swapping. We derived h using
combinatory completeness: the map h represents a term λx. λk. k xof the untyped linear lambda calculus [31]. We say that an object R
in Per(T ) is closed when (αN,N {ai }i∈ary(α) , αN,N {a0i }i∈ary(α) )is in R for each {(ai , a0i ) ∈ R}i∈ary(α) and for each algebraic
operation α on T . We define ΦR by\
ΦR = {S ∈ Per(T ) | R0 ⊆ S and S is closed}

and we define maps sum, cpy : N + N + N → N + N + N by

0

0

0

where R = {([J0 h] • a, [J0 h] • a ) | (a, a ) ∈ R}.
By Theorem 6.1, the Kleisli category Per(T )Φ is a categorical model of the computational lambda calculus, i.e., there is a
canonical interpretation of the computational lambda calculus in
Per(T )Φ . The interpretation, which we call categorical interpretation, is sound with respect to the standard equational theory of
the computational lambda calculus [26]. We can interpret algebraic
effects using algebraic operations on Φ induced by algebraic operations on T via (−)† . For example, when we need nondeterminism,
we can start from the powerset monad; when we need global states,
we can start from a global state monad.
We sketch extraction of GoI interpretation—i.e. extraction of
concrete T -transducers as realizers—from the categorical interpretation of the computational lambda calculus extended with algebraic effects and a base type nat. For simplicity, we only consider
closed terms.
1. We choose a monad T on Set that satisfies Requirement 4.2.
2. We interpret the computational lambda calculus in the Kleisli
category Per(T )Φ as in [26, 28] where we interpret algebraic
effects by algebraic operations on Φ derived from algebraic
operations on T via (−)† , and we interpret nat by a natural
number object of Per(T ).
3. The categorical interpretation of a closed term t of a type τ bijectively corresponds to an equivalence class of a partial equivalence relation ΦJτ K where Jτ K is the categorical interpretationof the type τ . We choose a Res(T )-morphism on N that represents the equivalence class, and then, we extract a T -transducer
LtM : N _ N that represents the Res(T )-morphism on N.

We call the T -transducer LtM GoI interpretation of a term t.
We extracted GoI interpretation so that the next theorem holds.
Theorem 6.2 (Soundness). For closed terms t and s of type τ ,• If t ≈ s, then ([LtM], [LsM]) ∈ ΦJτ K.

sum(inj1 (n)) = inj2 (n)sum(inj2 (n)) = inj3 hn, 0i
sum(inj3 hhn, mi, li) = inj1 hn, m + li
cpy(inj1 hn, mi) = inj3 hgn, micpy(inj2 hn, mi) = inj3 hdn, micpy(inj3 hgn, mi) = inj1 hn, micpy(inj3 hdn, mi) = inj2 hn, mi
where inji : N → N + N + N is the i-th injection. The map cpy isfrom contraction in the GoI situation.
In (memoryless) GoI interpretation, we interpret a closed term
as a partial map from N to N. The following diagrams present GoI
interpretation of programs:
LnM = kn : N * N,L(λxy : nat. x + y) 5 3M = sumL(λx : nat. x + x) 3M = sum

k3

k5

cpy

: N * N,k3

: N * N.

If we input hn, mi to L(λxy : nat. x + y) 5 3M, then we get an
output hn, 8i as a result of the following interactive computation
between sum, k3 and k5 .
1. sum receives an input hn, mi from the leftmost port and outputs hn, mi from the middle port to ask a value of x.
2. k5 answers hn, 5i to sum.
3. sum receives an input hn, 5i from the middle port and outputs
hhn, 5i, 0i from the rightmost port to ask a value of y.
4. k3 answers hhn, 5i, 3i to sum.
5. sum outputs hn, 8i from the leftmost port.
As a whole, GoI interpretation is sound with respect to β-equality:
L(λxy : nat. x + y) 5 3M is equal to k8 . Similarly, we can checkthat the GoI interpretation L(λx : nat. x + x) 3M is equal to k6 . Theinteractive computation illustrates how sum and cpy work: sum
computes sum, and cpy copies data.

7.2

Memoryful GoI Interpretation of Global State

GoI interpretation of the computational lambda calculus (i.e. callby-value calculus) in Section 7.2 and Section 7.3 follows from thegeneral scheme that we developed in this paper. In this section, we
present GoI interpretation of the computational lambda calculus extended with global states. We have a countably infinite set Loc oflocation names, and each location stores a natural number. Existence of global states enables us to fetch a natural number stored at
a location ` ∈ Loc and update a value stored at a location `:! ` : nat,φ

GoI Interpretation of core fragment For a type judgment(Γ = x1 : τ1 , · · · , xn : τn ),we inductively define an S-transducer

···
w

w

w0

w0
···

w

···

w

sum

h

w0

···

w0

LΓ ` t + s : natM = LΓ ` (λxy : nat. x + y) t s : natM
i−1
···

···
w

Lx1 : τ1 , · · · , xn : τn ` xi : τi M =

w

w

w0

w0

···

h
w0

w
···

···

w0
···

where w0 : N →S ∅ and w : ∅ →S N are unique SetS -morphisms,
and h : N + N → N + N is ψ ◦ h ◦ φ. Here h is from Section 6, andw and w0 are from weakening of the GoI situation in Section 4.2.4.
The combinator h corresponds to the unit of the monad Φ.
For Γ ` t : τ ⇒ σ and Γ ` s : τ , we define LΓ ` t s : σM by
φ

c

c

ψ

LΓ ` t s : σM =LΓ`s:τ M

···

φ
φ

c0

c0

e0
ψ

···
d0

d0
···

where d and d0 are S-transducers from N to N given by d =u ◦ (u × N) ◦ F v ◦ v and d0 = u ◦ F u ◦ (v × N) ◦ v. They are from
digging of the GoI situation in Section 4.2.4. The dashed line box
is an application of the “strong monoidal” F given in Section 4.2.4
followed by composition of the following isomorphismu⊗···⊗u···

GoI interpretation of algebraic effects Let Per(T )-objects L
and N be countably infinite coproducts of terminal object 1. The
algebraic operations in Example 4.7 induce algebraic operations
on Φ, which induce the following Per(S)Φ -morphisms
asg : L × N →Φ 1

called generic effects in [28]. Interpretation of dereferencing ! ` andassignment ` := n are derived from drf and asg respectively. For
simplicity, we give GoI interpretation of ! ` and ` := n for a fixedlocation ` and a fixed value n.
We interpret − ` ! ` : nat by an S-transducer
drf ` = ({x` , x1 , x2 , · · · }, c, x` ) : N _ N
where the SetS -morphism c on {x` , x1 , x2 , · · · } × N is given by(c(x` , n))(s) = (xs(`) , Ls(`)M(n), s),(c(xm , n))(s) = (xm , LmM(n), s).
Initially, the S-transducer drf ` looks up the global state s and behaves as an S-transducer Ls(`)M. At the same time, the S-transducer
drf ` stores the value s(`) locally using its internal state. Thereafter,
drf ` looks up its internal state: if an internal state is xn , then drf `behaves following LnM without referring to global states.
We interpret − ` ` := n : unit by an S-transducerasg`,n = ({xrun , xdone }, c0 , xrun ) : N _ N(c0 (xrun , m))(s) = (xdone , L1M(m), s[n/`])(c0 (xdone , m))(s) = (xdone , L1M(m), s).

···LΓ`t:τ ⇒σMLΓ,x:τ `t:σMhwhere the SetS -morphism c0 on {xrun , xdone } × N is given by

···
e

ψ

d

···

ψ

drf : L →Φ N

kn

LΓ, x : nat, y : nat ` x + y : natM =···F (N ⊗ · · · ⊗ N) −→ F N ⊗ · · · ⊗ F N −→ N ⊗ · · · ⊗ N.

where N⊗(n+1) is the (n+1)-fold tensor product of N, i.e., (n+1)fold direct sum of N. First, we give GoI interpretation of constants,
variables, the term application and the lambda abstraction. We
interpret natural numbers, summation and variables as follows:hLΓ ` λx : τ. t : τ ⇒ σM =∼=LΓ ` t : τ M : N⊗(n+1) _ N⊗(n+1)

LΓ ` n : natM =d` := 3 : unit.

We extract GoI interpretation of global states from the categoricalinterpretation in Per(S)Φ where Φ is the monad in Theorem 6.1
Loc
for T = S given by SA = (1 + A × NLoc )N . This is a
global state monad in Example 4.4 where V = N and L =Loc. In this section and the next section, we often confuse a map
f : N → N with a T -transducer J0 f : N _ N and a SetT morphism g : N →T N with a T -transducer Jg : N _ N.
Γ`t:τ

where we write e for u ◦ (κ1 × N), e0 for (>N × N) ◦ v, c foru ◦ (φ × N) ◦ (v + v) and c0 for (u + u) ◦ (ψ × N) ◦ v. Here we omit
some obvious bijections like N × (N + N) ∼= N × N + N × N.
These S-transducers are from dereliction and contraction of the
GoI situation given in Section 4.2.4. We note that the component
cpy consists of c and c0 .
For Γ, x : τ ` t : σ, we define LΓ ` λx : τ. t : τ ⇒ σM by

Initially, ({xrun , xdone }, c0 , xrun ) updates a global state, and thereafter, ({xrun , xdone }, c0 , xrun ) does nothing. We note that L1M inthe right hand side can be any GoI interpretation of a constant.
For example, the GoI interpretation of the following program
Q = (λx : nat. x + (` := 3); x) (! `) : nat

is also behaviorally equivalent to ({x` , x1 , x2 , · · · }, d, x` ).

where t; s is an abbreviation of (λx : unit. s) t is

ψ

ψ

φ

ψ

Remark 7.1. Some readers may notice symmetries in diagrams inthis paper: the top half of diagrams are mirror images of the bottom
half of diagrams. This phenomenon stems from Int-constructionin the GoI workflow [2, 20] and is also observed in [22].

w0

φ

ψ

7.3
LQM = drf `

sum

h

φ

h

asg`,3

cpy

φ

ψ
φ

φ
w

ψ

.
Here we simplified the canonically derived GoI interpretation. For
example, since φ is the inverse of ψ, we can apply the following
reduction to GoI interpretation:
φ

ψ

7−→

.

These diagrams represent the identity on N + N, and the reduction
does not affect the execution result of GoI interpretation. Correctness of the simplification can be checked by the realizability interpretation. Automatic simplification is future work.
For an input ddhn, mi and a global state s such that s(`) = 2,
the S-transducer behaves as follows:
1. drf ` refers to the global state s and memorizes the value s(`) =2 by means of its internal state.
2. asg`,3 assigns 3 to ` changing its internal state to xdone .
3. sum asks a value of the right occurrence of x in x + x.
4. cpy passes the query from sum to drf ` .
5. drf ` answers 2 to the query following its internal state. In thisstep, drf ` does not refer to the global state s[3/`].

Memoryful GoI Interpretation of Nondeterminism

In this section, we consider nondeterminism. We can extract GoI
interpretation for nondeterminism from the categorical interpretation in Per(P)Φ where Φ is the monad in Theorem 6.1 for T = P.
We interpret the computational lambda calculus as in Section 7.2.
Interpretation of the nondeterministic choice operator t is derived
from the algebraic operation ⊕† on Φ.
We give two examples of GoI interpretation. The first one is
GoI interpretation of the nondeterministic choice 3 t 5. The GoI
interpretation L− ` 3 t 5 : natM : N _ N is a P-transducer
L3M⊕N,N L5M = ({x3t5 , x3 , x5 }, c, x3t5 ) given byc(x3t5 , n) = {(x3 , L3M(n)), (x5 , L5M(n))}
c(x3 , n) = {(x3 , L3M(n))}
c(x5 , n) = {(x5 , L5M(n))}.

The P-transducer L3M⊕N,N L5M behaves like the nondeterministic
Mealy machine (3): initially, the P-transducer L3M⊕N,N L5M nondeterministically chooses L3M or L5M; thereafter L3M⊕N,N L5M sticks tothe same choice referring to its internal state.
We next consider the following program:P = (λx : nat. x + x) (3 t 5) : nat.
We have the following equations:
P = ((λx : nat. x + x) 3) t ((λx : nat. x + x) 5)= (3 + 3) t (5 + 5) = 6 t 10.
GoI interpretation of the program P is

6. cpy passes the answer from drf ` to sum.
7. sum asks a value of the left occurrence of x in x + x.
8. cpy passes the query from sum to drf ` .
9. drf ` answers 2 to the query following its internal state. In thisstep, drf ` does not refer to the global state s[3/`].

φψ

LPM = L3M⊕N,N L5M

We note that without internal states, drf ` can not but refer to a
global state at 5) and 9), which results in a wrong output. We only
sketched computation process for lack of space. For example, weomit some access to asg`,3 .
As a whole, the S-transducerL(λx : nat. x + (` := 3); x) (! `)M : N _ N

is behaviorally equivalent to an S-transducer({x` , x1 , x2 , · · · }, d, x` ) : N _ N

where the SetS -morphismd : {x` , x1 , x2 , · · · } × N → {x` , x1 , x2 , · · · } × N
is given by(d(x` , n))(s) = (xs(`) , Ls(`) + s(`)M(n), s[3/`]),(d(xm , n))(s) = (xm , Lm + mM(n), s).

We can observe that the GoI interpretation of the following program(λx : nat. (` := 3); (x + x)) (! `) : nat

sum

cpy

φ
ψ

.

10. cpy passes the answer from drf ` to sum.
11. sum outputs 4 = 2 + 2.

hHere we also simplified canonically derived GoI interpretation.
The P-transducer LPM behaves as follows:
1. We input ddhn, mi.

2. L3M⊕N,N L5M receives an input gddhn, mi, and the internal
state nondeterministically changes to x3 or x5 . Here we assume that L3M⊕N,N L5M chooses x3 . Then L3M⊕N,N L5M outputs
dgddhn, mi.
3. sum receives hn, mi from the leftmost input port and outputs
hn, mi from the middle port to ask a value of the right occurrence of x in x + x.
4. cpy receives an input hn, mi from the leftmost port and outputs
hgn, mi from the rightmost port to get x.
5. L3M⊕N,N L5M receives ddhgn, mi. Since the internal state is x3 ,it answers ddhgn, 3i
6. cpy receives hgn, 3i from the rightmost port and answers
hn, 3i to sum via the leftmost port.
7. sum receives hn, 3i from the middle port and asks a value ofthe left occurrence of x in x + x by outputting hhn, 3i, 0i fromthe rightmost port.

8. cpy receives hhn, 3i, 0i from the middle port and outputs
hdhn, 3i, 0i from the rightmost port to get x.
9. L3M⊕N,N L5M receives ddhdhn, 3i, 0i. Since the internal state is
x3 , it answers ddhdhn, 3i, 3i.
10. cpy receives hdhn, 3i, 3i and answers hhn, 3i, 3i to sum via
the middle port.
11. sum receives hhn, 3i, 3i from the rightmost port and outputs
hn, 6i from the leftmost port.
12. We get an output ddhn, 6i.
In the computation, the component h controls interaction between
L3M⊕N,N L5M and the sum-cpy fragment.
Similarly, if L3M⊕N,N L5M chooses x5 at the first step, then we
get ddhn, 10i as an output. As a whole, we have the following
behavioral equivalence:L(λx : nat. x + x) (3 t 5)M 'P
N,N L6M⊕N,N L10M = L6 t 10M.

8.

Conclusion

We gave a general GoI/realizability workflow that interprets thecomputational lambda calculus with algebraic effects as concrete
state machines. In other words, our framework equips token machines with internal memories and it allows to handle generic algebraic effects. Our result provides a systematic approach to categorical GoI for algebraic effects. It would be interesting to apply our
results to compiler construction (initial steps are made in [27]), GoI
for additives and quantum lambda calculi.

Acknowledgments
We thank Dan Ghica, Toshiki Kataoka and anonymous reviewers
for useful comments and discussions. The first author is supported
by Grants-in-Aid for Young Scientists (B) No. 26730004, JSPS.
The second and third authors are supported by Grants-in-Aid forYoung Scientists (A) No. 24680001, JSPS, and by Aihara Innovative Mathematical Modeling Project, FIRST Program, JSPS/CSTP.

References[1] S. Abramsky. Retracing some paths in process algebra. In CONCUR ’96: Concurrency Theory, volume 1119 of LNCS, pages 1–17.
Springer Berlin Heidelberg, 1996.
[2] S. Abramsky, E. Haghverdi, and P. Scott. Geometry of interaction andlinear combinatory algebras. Math. Struct. in Comp. Sci., 12:625–665,
2002.
[3] L. Aceto, W. Fokkink, and C. Verhoef. Structural operational semantics. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook ofProcess Algebra, pages 197–292. Elsevier, 2001.
[4] C. Baier, M. Sirjani, F. Arbab, and J. J. M. M. Rutten. Modelingcomponent connectors in Reo by constraint automata. Science ofComputer Programming, 61(2):75–113, 2006.
[5] L. S. Barbosa. Towards a calculus of state-based software components.
Journal of Universal Computer Science, 9(8):891–909, 2003.
[6] U. Dal Lago and U. Schöpp. Functional programming in sublinear
space. In Programming Languages and Systems, volume 6012 of
LNCS, pages 205–225. Springer Berlin Heidelberg, 2010.
[7] V. Danos and L. Regnier. Reversible, irreversible and optimal λmachines: Extended abstract. ENTCS, 3(0):40–60, 1996.
[8] O. Fredriksson and D. R. Ghica. Seamless distributed computing fromthe geometry of interaction. In C. Palamidessi and M. D. Ryan, editors,
Trustworthy Global Computing, volume 8191 of Lecture Notes in
Computer Science, pages 34–48. Springer Berlin Heidelberg, 2013.
[9] D. R. Ghica. Geometry of synthesis: a structured approach to VLSI
design. In M. Hofmann and M. Felleisen, editors, POPL, pages 363–
375. ACM, 2007. ISBN 1-59593-575-4.

[10] J.-Y. Girard. Geometry of interaction 1: Interpretation of system F. In
S. V. R. Ferro, C. Bonotto and A. Zanardo, editors, Logic Colloquium’88 Proceedings of the Colloquium held in Padova, volume 127 ofStudies in Logic and the Foundations of Mathematics, pages 221–260.
Elsevier, 1989.
[11] G. Gonthier, M. Abadi, and J.-J. Lévy. The geometry of optimallambda reduction. In R. Sethi, editor, POPL, pages 15–26. ACM Press,
1992. ISBN 0-89791-453-8.
[12] M. Hasegawa. The uniformity principle on traced monoidal categories. ENTCS, 69(0):137–155, 2003. CTCS’02.
[13] M. Hasegawa. On traced monoidal closed categories. Math. Struct. in
Comp. Sci., 19:217–244, 4 2009. ISSN 1469-8072.
[14] I. Hasuo and N. Hoshino. Semantics of higher-order quantum computation via geometry of interaction. In LICS, pages 237–246, 2011.
[15] I. Hasuo and B. Jacobs. Traces for coalgebraic components. Mathematical Structures in Computer Science, 21:267–320, 4 2011.
[16] N. Hoshino. A modified GoI interpretation for a linear functional
programming language and its adequacy. In M. Hofmann, editor,
FOSSACS, volume 6604 of Lecture Notes in Computer Science, pages
320–334. Springer, 2011.
[17] B. Jacobs, editor. Categorical Logic and Type Theory, volume 141 ofStudies in Logic and the Foundations of Mathematics. Elsevier, 19999.
[18] B. Jacobs. From coalgebraic to monoidal traces. ENTCS, 264(2):125–
140, 2010.
[19] B. Jacobs. Introduction to coalgebra. towards mathematics of statesand observations, Version 2.0 2012.
[20] A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119:
447–468, 4 1996.
[21] B. Klin. Bialgebraic methods and modal logic in structural operationalsemantics. Information and Computation, 207(2):237–257, 2009.
[22] Y. Lafont. Interaction combinators. Information and Computation,
137(1):69–101, 1997. .
[23] O. Laurent. A token machine for full geometry of interaction. In
TLCA, pages 283–297, 2001.
[24] J. Longley. Realizability Toposes and Language Semantics. PhD
thesis, University of Edinburgh, 1994.
[25] I. Mackie. The geometry of interaction machine. In R. K. Cytron
and P. Lee, editors, POPL, pages 198–208. ACM Press, 1995. ISBN
0-89791-692-1.
[26] E. Moggi. Computational lambda-calculus and monads. Technical
Report ECS-LFCS-88-66, Laboratory for Foundations of Computer
Science, 1988.
[27] K. Muroya, T. Kataoka, I. Hasuo, and N. Hoshino. Compiling effectful terms to transducers: Prototype implementation of memoryful
geometry of interaction. Submitted, 2014.
[28] G. Plotkin and J. Power. Algebraic operations and generic effects.
Applied Categorical Structures, 11(1):69–94, 2003.
[29] J. Power and E. Robinson. Premonoidal categories and notions ofcomputation. Mathematical Structures in Computer Science, 7:453–
468, 10 1997.
[30] U. Schöpp. On interaction, continuations and defunctionalization.
In TLCA, volume 7941 of LNCS, pages 205–220. Springer Berlin
Heidelberg, 2013.
[31] A. Simpson. Reduction in a linear lambda-calculus with applications
to operational semantics. In G. Jürgen, editor, RTA, volume 3467 of
LNCS, pages 219–234. Springer Berlin Heidelberg, 2005.
[32] D. Turi and G. Plotkin. Towards a mathematical operational semantics.
In LICS, pages 280–291. IEEE Computer Society, 1997.
[33] A. Yoshimizu, I. Hasuo, C. Faggian, and U. Dal Lago. Measurements
in proof nets as higher-order quantum circuits. In ESOP, 2014. To
appear.