Memoryful GoI
with recursion

室屋 晃子 (東大)CSCAT(鹿児島), March 14, 2015

specific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
The
first
reasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5> --->
TtT Compiler
and TtT Simulator.
| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- dd<42,5> --->We express
transducer
effect T ) as a Haskell prog
Result:5 / aState:
Just (with(Rightthe(*))

Memoryful GoI [Hoshino, —, Hasuo ’14]
effectfulterms

18
The second
speculative
P = reason( xis: nat.
x + x)but(3practical:t 5) : wenatwish to fol-(1)low the path of [3, 4, 10, 11] and use memoryful GoI as a compilawhere
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.
toy tool of TtT will then form a basis of such practical compilers.
The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of areader will be convinced by the following examples.

of the type Td m x a b:
type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
via coalgebraic component
calculus
right, in French, see e.g. [9, 11]), for readability and efficiency.

Transducers, Derived and Executed Consider the term P in (1)with nondeterministic choice t in it. Its translation to a (three-state,nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), after somemanual simplifications, is depicted below (manually).

transducers
LPM =L3M N,N L5M

h

sum

cpy

.

(3)

The figure is a string diagram in the traced monoidal category of

2

1 The word “memory” here is almost synonymous with “internal states”

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
The ones like the former stand for the token’s entrance to and exitfrom a transducer. Specifically, p:[t@x]—with a subterm t0 of t
designated by [t0 ]—means: the token entered to (a copy of) thetransducer Lt0 M, whose current state is x, at its port p. Typical ports
include: Query (a top-level query) and Answer x (an answer tothe previous query on x; see Fig. 2, lines 24 and 44). Similarly,[t@x]:p means the token departed from the port p.
The latter class of expressions like h; k_3; h on Fig. 1, line
5 and phi on Fig. 2, line 3 are referred to as bookkeeping. For
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as purefunctions like h : N + N ! N + N) is found in [8]. As we noted
before, these bookkeeping nodes correspond to logical connectives
Muroyain a proof net; therefore they change the number
carried(U.
byTokyo)theGeometry of Interaction (GoI)•

semantics of•semantics of•token machine presentation [Mackie ’95]{

linear logic proof [Girard ’89],
functional programming“GoI implementation”•

compilation techniques and implementations•[Mackie ’95] [Pinto ’01] [Ghica ’07]

3

Muroya (U. Tokyo)

Geometry of Interaction (GoI)•

token machine semantics( x. x + x) 1

x. x + x
x. x + x1

1

4

Muroya (U. Tokyo)

Geometry of Interaction (GoI)•

token machine semantics( x. x + x) 1

x.x.x
x+x
x. x + x

31
t5

1

4

Muroya (U. Tokyo)

Geometry of Interaction (GoI)•

token machine semantics( x. x + x) 1

x.x.x
x+x
x. x + x

31
t5

1

q

4

Muroya (U. Tokyo)

Geometry of Interaction (GoI)•

token machine semantics( x. x + x) 1

x.x.x
x+x

q

x. x + x

ask (left) x

31
t5

1

4

Muroya (U. Tokyo)

Geometry of Interaction (GoI)•

token machine semantics( x. x + x) 1

x.x.x
x+x

1

x. x + x

ask (left) x

31
t5
answer 1

1

4

Muroya (U. Tokyo)

Geometry of Interaction (GoI)•

token machine semantics( x. x + x) 1

x.x.x
x+x
ask (left) x

x. x + x

1

31
t5
answer 1

ask (right) xq4

Muroya (U. Tokyo)

Geometry of Interaction (GoI)•

token machine semantics( x. x + x) 1

x.x.x
x+x
ask (left) x

x. x + x

1

31
t5
answer 1

ask (right) x
answer 1

1

4

Muroya (U. Tokyo)

Geometry of Interaction (GoI)•

token machine semantics( x. x + x) 1

x.x.x
x+x
ask (left) x

2

x. x + x

1

31
t5
answer 1

ask (right) x
answer 1
answer 2
4

Muroya (U. Tokyo)

Memoryful GoI — Input
effectfulterms

CBV λ-terms with algebraic effects

algebraic operations [Plotkin, Power ’01]
transducers

nondeterministic choice• probabilistic choice• actions on global state

M tN
M tp N

lookupl (v : Val. M )updatel,v (M )•5

Muroya (U. Tokyo)

Memoryful GoI — Output
effectful
terms

transducers

stream transducers (Mealy machines)(X, c : X ⇥ A ! T (X ⇥ B), x0 2 X) : A _ B

x0

a0 /b1x1

a0 /b2x2

string diagram style

c
6

T =P

x0

B
A

automaton stylea0
Muroya (U. Tokyo)

Memoryful GoI — Output
effectfulterms

stream transducers (Mealy machines)(X, c : X ⇥ A ! T (X ⇥ B), x0 2 X) : A _ B

x0transducers

a0Res(T/b1 ) a0 /b2
x1 sets x2
objects:

automaton styleT =Parrows: transducers modulo
behavioral
equivalence[(X, c : X ⇥ A ! T (X ⇥ B), x0 2 X)]' : A _ B
x0

B

string diagram style

c
A
6

a0
Muroya (U. Tokyo)

Memoryful GoI — Output
effectfulterms

stream transducers (Mealy machines)(X, c : X ⇥ A ! T (X ⇥ B), x0 2 X) : A _ B

T = P (x0 , a0 ) 7 ! {(x1 , b1 ), (x2 , b2 )}transducers

T = S = (1 + ( ) ⇥ S)S

computation with
global state

a0 /b1x1

x0

a0 /b2x2

nondeterministic
computation

(x1 , b1 ) 7! 1/4,
(x0 , a0 ) 7 !
(x2 , b2 ) 7! 3/4,

T =D

x0

a0 /b1
1x1 4
7

a0 /b23
4 x2

probabilistic
computation
Muroya (U. Tokyo)

Memoryful GoI — Translation
effectfulterms•

idea: resumptions + categorical GoI••[Abramsky, Haghverdi, Scott ’02]

use coalgebraic component calculus

transducers[Barbosa ’03] [Hasuo, Jacobs ’11]•

composition operations for software components•(many-sorted) process calculus

8

Muroya (U. Tokyo)

Memoryful GoI — Translation
Def. (component calculus)
C

D

C

Tr(C)

D

↵({Ci }i2I )

F(C)

B

C
d

B
c

B
c

A

D
d

B

C

A

B

c
C

A

A

c
c
c

···

B
B
↵
· · · ci · · · cj · · ·AAA(↵: I-ary algebraic operation)

9

Muroya (U. Tokyo)

Memoryful GoI — Translation
Def. (component calculus)
sequential
compositionC

parallelcomposition

D

C

1
1 0
10
X,
X,
X ⇥ Y,ccd@Y ⇥ B !
A @X ⇥ A !
T (X ⇥ B),A···
T (Y ⇥ C),A @X ⇥ A ! T (X ⇥ B),A = @x0 2 X(x0 , y0 ) 2 X ⇥ Y
x0 2 Xy0 2 Y0

1 0

Y,(x0 , y0 )a1 /c1

a2 /c2(x1 , y1 ) (x2 , y2 )

C y0
d
B x0
c

a1 /b1

0D

1
X ⇥ Y,d@Y ⇥ C !
A···
T (Y ⇥ D),A = @(x0 , y0 ) 2 X ⇥ Y
y0 2 Y(x0 , y0 )Y,

c1 /d1(x1 , y0 ) (x0 , y1 )10

B x 0 D y0
c
d
A

C

A
10

Muroya (U. Tokyo)

Memoryful GoI — Translation
Def. (component calculus)

algebraiceffect!-modality
application

Tr(C)
C

B

( (
c

C

( (
A

B
B

c
A

B
B
↵
· · · ci · · · cj · · ·

c

F

=

A

B

B

C

c
c
c

A

A

A

=

Tr

↵({Ci }i2I )

F(C)

A

···

"
a0 /b1
x1

x0

⇤

"

a0 /b2 a0 /b01
y1
x2

y0

a0 /b02y2(↵: I-ary algebraic operation)
11

Muroya (U. Tokyo)

Memoryful GoI — Translation
Def. (component calculus)

algebraiceffect!-modality
application

Tr(C)
C

( (

q
2

A

x. x + x

B
c

q

C

B
B
↵
· · · ci · · · cj · · ·

c

F

C

=

A

A

( (

c

Tr

B

B

=

B

↵({Ci }i2I )

F(C)

B
c

1
cc

A

1

···
q

A

A

A

1

"
a0 /b1
x1

x0

⇤

"

a0 /b2 a0 /b01
y1
x2

y0

a0 /b02y2(↵: I-ary algebraic operation)
11

Muroya (U. Tokyo)

Memoryful GoI — Translation
Def. (component calculus)

algebraiceffect!-modality
application

Tr(C)
C

B

( (
c

C

( (
A

B
B

c
A

B
B
↵
· · · ci · · · cj · · ·

c

F

=

A

B

B

C

c
c
c

A

A

A

=

Tr

↵({Ci }i2I )

F(C)

A

···

"
a0 /b1
x1

x0

⇤

"

a0 /b2 a0 /b01
y1
x2

y0

a0 /b02y2(↵: I-ary algebraic operation)
11

Muroya (U. Tokyo)

Memoryful GoI — Translation
Def. (interpretation L ` t : ⌧ M)

t :: ⌧⌧ M( = x1 : ⌧1 , . . . , xn : ⌧n ),For a type judgement L ` t

we inductively define{n

LL `` tt : ⌧ M =

N N ··· N
L ` t: ⌧M
N N ··· N

12.

Muroya (U. Tokyo)

w

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

h
w

0

···

w

w

0

0

w

w

(c(x` , n))(s) = (xs(`) , Ls(`)M(n), s),(c(xm , n))(s) = (xm , LmM(n), s).

w
···

w0

Memoryful GoI — Translation
···

···

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, and
0w and w 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 byDef. (interpretation L ` t : ⌧ M)
···

e

c

c

Initially, the S-transducer drf ` looks up the global state
haves as an S-transducer Ls(`)M. At the same time, the Sdrf ` stores the value s(`) locally using its internal state. T
drf ` looks up its internal state: if an internal state is xn ,behaves following LnM without referring to global states.
We interpret ` ` := n : unit by an S-transducerasg`,n = ({xrun , xdone }, c0 , xrun ) : N _ N

where the SetS -morphism c0 on {xrun , xdone } ⇥ N is g2

q 1(c0 (xrun , m))(s) = (xdone , L1M(m), s[n/`])x. x + x0

10
where we write e for u (1 ⇥···N), e for (>N ⇥ N) v, c for(c(xdone , m))(s) = (xdone , L1M(m), s).
0u ( ⇥ N)L (v(uN)M v. Here we omit q`t:⌧)+M u) ( L⇥`s:⌧`+t sv): andM =c Lfor
1 q⇠
Initially,({xrun , xdone }, c0 , xrun ) updates a global state,some obvious bijections like N ⇥
(N
+
N)
N
⇥
N
+
N
⇥
N.
···
=
after, ({xrun , xdone }, c0 , xrun ) does nothing. We note t
These S-transducers are from dereliction and0 contraction
of
the
c
c0
GoI situation given in Section 4.2.4. We enotethat the component the right hand side can be any GoI interpretation of a con
0
For example, the GoI interpretation of the following p
cpy consists of c and c0 .
···For , x : ⌧ ` t : , we define L ` x : ⌧. t : ⌧ ) M by
Q = ( x : nat. x + (` := 3); x) (! `) : nat

d

···

d

···

L ` x : ⌧. t : ⌧ ) M =h

L ,x:⌧ `t: M
···

d0

···

d0

where d and d0 are S-transducers from N to N given by d =13u (u ⇥ N) F v v and d0 = u F u (v ⇥ N) v. They
are from

Muroya (U. Tokyo)

`t:⌧is an applicatio
followed by co( = x1 : ⌧1 , · · · , xn : ⌧n ),we inductively define an S-transducer

Memoryful GoI — Translation
L ` t : ⌧ M : N⌦(n+1) _ N⌦(n+1)

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,t : ⌧ M) and the lambda abstraction. We
variables, theL term` application
Def. (interpretationinterpret natural numbers, summation and variables as follows:w

L ` n : natM =

···

w

kn

h

w0

w0
···
w

L , x : nat, y : nat ` x + y : natM =

h

···

w

sum
w0

···

w0

w

i 1
···

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

h
w0

w
···
···

w0

w
w0

w
···

w0

···

where w0 : N !S ; and w : ; !S N are unique SetS -morphisms,
and h : N + N ! N + N is
h14 . Here h is from Section 6, and0

GoI interpreta
and N be cou
algebraic oper
on , which indrf

called genericassignment ` :simplicity, we
location ` and
We interpre

drL ` t + s : natM = L ` ( xy : nat. x + y) t s : natM···

F (N ⌦ · · · ⌦where the Set(

Initially, the S
haves as an Sdrf ` stores thedrf ` looks up
Muroya(U. Tokyo)
behavesfollow

Memoryful GoI — Translation
Thm. (soundness)
For closed terms M and N of type ⌧ ,• ` M = N : ⌧ implies ([LM M]' , [LN M]' ) 2• ` M = N : nat implies LM M ' LN M.

J⌧ Kbehavioral equivalence

Moggi’s equations for computational lambda-calculus• equations for algebraic operations•

M tM =M
E[opr(M1 , . . . , Mn )] = opr(E[M1 ], . . . , E[Mn ])( x. M ) (N1 t N2 ) = ( x. M ) N1 t ( x. M ) N2
15

Muroya (U. Tokyo)

specific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
The
first
reasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5>--->
TtT Compiler
and TtT Simulator.
n| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- N
dd<42,5>
N · · · --->
NWe
expressatransducer
effect T ) as a Haskell prog
L
`
t
:
⌧
M
=
18
Result: 5 /L State:
Just (with(Rightthe
(*))
`
t
:
⌧
M
The second
reasonis
speculative
but
practical:
we
wish
to
folP = ( x : nat. x + x) (3 t 5) : nat(1)of the type Td m x a b:
low the path of [3, 4, 10, 11] and use memoryful GoI as a compilaN N ··· N

Memoryful GoI [Hoshino, —, Hasuo ’14]

where
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.

{

effectful
terms

type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
component
calculus
toy tool of TtT will then form a via
basis of coalgebraicsuch practical compilers.
right, in French, see e.g. [9, 11]), for readability and efficiency.

The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of a

1 The word “memory” here is almost synonymous with “internal states”

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
reader will be convinced by the following examples.
The ones like the former stand for the token’s
entrance to and exit
B
Cfrom a transducer. Specifically, p:[t@x]—with a subterm t0 of t
Transducers, Derived and Executed Consider the term P in (1)BdBto (a copy of) theD [t0 ]—means:
B by
B
···
with nondeterministic choice t in it. Its translation to a (three-state,
Bthe token
designatedentered↵cc···B· cj p.
nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), after somecctransducerc Lt0 M,d whose
current state
is x,· · ·atciits· ·port
Typical portscmanual simplifications, is depicted below (manually).
C (aAtop-levelA x (an answer toinclude:AQuery
query) and AAnswer
C A
the previous query on x; see Fig. 2, lines A
24 and 44). Similarly,
A[t@x]:p means the token departed from the port p.
The latter class of expressions like h; k_3; h on Fig. 1, line
5 and phi on Fig. 2, line 3 are referred to as bookkeeping. For
cpy
sum
h
LPM = L3M N,N L5M
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as purefunctions like h : N + N ! N + N) is found in [8]. As we noted.
(3)
16 before, these bookkeeping nodes correspond to logical connectives
MuroyaThe figure is a string diagram in the traced monoidal category of
in a proof net; therefore they change the number
carried(U.
byTokyo)thetransducers

of the token; a state transition of a token machine
ment of the token, from one position to another. It
he underlying proof net—the “graph” on which theund—is static and remains unchanged.
yless nature of GoI is a big advantage in view
allows us to analyze complicated higher-order
he elementary terms of nodes and edges in graphs
ges in proof nets). The same nature, however, posesns to the use of GoI, too. For example, it is longmmunity that additive connectives in linear logic—
product types like bit = 1 + 1—call for special
pretation that is far from trivial. One solution by solices [9], which can be thought of as an additionalon proof nets.
mple of the limitations of “memoryless GoI” manesence of computational effects. Consider the callion of the term=hence is correct by construction and compositional. The construction of the denotational model relies on the categorical axiomatiza
tion of GoI by Abramsky, Haghverdi and Scott [1, 2]: it allows one
to derive a Cartesian closed category from a traced monoidal category C with suitable additional structures. What we do in [8] is takeas C the category of resumptions, i.e. transducers modulo a suitable“Termsbehavioral equivalence. This in fact is already donein [2]:toour technical novelty is systematic use of componentTransducers”
calculi—those calcul
for composing transducers, formulated in coalgebraic terms—incomposing resumptions.

Prototype Imprementation: TtT
effectful
terms

memoryful GoI( x : nat. x + x) (3 t 5)transducers

: nat

(1)

m 3 t 5 returns 3 or 5 nondeterministically. Obviexpected to yield 6 or 10 (but not 8). However theretation can yield 8 too: in the interaction between. x + x and 3 t 5, the value of the latter is queried
he subterm 3t 5 can answer differently. Here what
e memory mechanism that allows the subterm 3t5
choice that it has made, and to stick to it.

GoI Motivated by a similar (but more complichallenge we encountered in the semantics of aeffectfulterms

Our Tool TtT This is a preliminary report on the implementationof memoryful GoI. Our tool is called TtT—short for “Terms toTransducers”—and is implemented in Haskell. It consists of twoparts: TtT Compiler and TtT Simulator.
TtT Compiler implements the translation sketched in the above
We express a transducer (with the effect T ) as a Haskell programof the type Td m x a b:

TtT Compiler

Haskell programtype

Td m x a b=(x, a) -> m (x, b)

where m is the Haskell monad that corresponds to T , x is the typefor a state space, a is the input type and b the output type.
The transducer obtained from an (effectful) -term is then ex
ecuted by TtT Simulator, in a meticulous way where every move
ment is recorded. Recall that a transducer here is much like a proo

TtT Simulator

simulation
stick to the former so as to distinguish from states as a computational effectresult1 The word “memory” here is almost synonymous with “internal states”; we17

Muroya (U. Tokyo)

4526 6,lines
that
6, 8, 8,10 as possible(duplica-weyields8, 8,
10 yields
as possible
outcomes(duplicaInstead
ofoutcomes
pictorial presentation,onof 8 isfinal
due todifferent
statesofTtT
theSimulatortransducer).
withand observe its dyna
different
statesof the final
transducer).

lation result of LPMTtTfor P in (1) consists o
Prototype
Imprementation:
mulation
Resultspresent actual
simulation
forsuccessfu
sims We present
actualWe
simulation
results
forassimand 10
possibleresults
outcomes,for+ f11)in( Fig.
x. 3 t2.5) w
writtenas 3|_|5in Fig. 1;( x.inx)
1thein1;termFig.
er terms:
3t5, written
asand
3|_|5
Fig.
and(2.(f. fx.0 x),137>--->dd<42,137> --->---|_|5]@ Nothing]
Query:[[3|_|5]@ Nothing ]42,137>--->dd<42,137> --->-.
---[3]|_|5@ * ] [3]|_|5 @ * ]|Query:[;| hh; k_3; h
5| @ * ]:Answer[ [3]|_|5 @ * ]:Answer
42,3>
--->
|
---- dd<42,3> --->@| Just(Left (*))]:Answer[ [3|_|5]@ Just(Left (*)) ]:Answer,3>---> dd<42,3> --->
| ---tate:
Just3 (Left(*))Just (Left (*))
Result:/ State:42,137>--->-.
---- dd<42,137> --->
3|_|[5]@*]|
Query:[ 3|_|[5] @ * ];| hh; k_5; h] @ * ]:Answer|[ 3|_|[5] @ * ]:Answer 18
42,5> --->of 4526 lines that yields 6, 8, 8, 10 as possible outcomes (duplication of 8 is due to different final states of the transducer).

Simulation Results We present actual simulation results for simpler terms: 3t5, written as 3|_|5 in Fig. 1; and ( x. x) 1 in Fig. 2.

1
2
3
4

1
2
3
4
5
6
7
8
9

10
11
12
13
14
15
16
17
18

.
---- dd<42,137> --->|
Query:[ [3|_|5] @ Nothing ]+-.
---- dd<42,137> --->| |Query:[ [3]|_|5 @ * ]| |h; k_3; h| |[ [3]|_|5 @ * ]:Answer| |---- dd<42,3> --->
| | [ [3|_|5] @ Just (Left (*)) ]:Answer| | ---- dd<42,3> --->| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->|
Query:[ 3|_|[5] @ * ]|h; k_5; h|[ 3|_|[5] @ * ]:Answer|---- dd<42,5> --->
| [ [3|_|5] @ Just (Right (*)) ]:Answer| ---- dd<42,5> --->
Result: 5 / State: Just (Right (*))

5
6
7
8
9

10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

Figure 1. Simulation Result for 3 t 5

The convention is as follows. A token carries a natural number naround—or more precisely, an edge e.g. in (3) consists of |N|-many“pipes” and a token goes through the n-th—and this is denoted by---- n --->. Therefore expressions like dd<42,137> in Fig. 1
stand for a certain natural number. We however chose to supplementarily use the dynamic algebra notation (g for left and d forright, in French, see e.g. [9, 11]), for readability and efficiency.
In Fig. 1, between movements ---- n ---> of the token are
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
The ones like the former stand for the token’s entrance to and exitfrom a transducer. Specifically, p:[t@x]—with a subterm t0 of t
designated by [t0 ]—means: the token entered to (a copy of) thetransducer Lt0 M, whose current state is x, at its port p. Typical ports
include: Query (a top-level query) and Answer x (an answer tothe previous query on x; see Fig. 2, lines 24 and 44). Similarly,[t@x]:p means the token departed from the port p.

39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

---- dd<42,137> --->
Query:[ [(\x.x) 1] @ ({_: *}, *) ]phi---- gdd<42,137> --->
Query:[ [\x.x] 1 @ {_: *} ]h
[ [\x.x] 1 @ {_: *} ]:Answer---- dgdd<42,137> --->
psi; psi; phi---- gdd<42,137> --->
Query:[ (\x.x) [1] @ * ]h[ (\x.x) [1] @ * ]:Answer---- dgdd<42,137> --->
psi; e; phi; phi---- dd<0,gdd<42,137>> --->
Query:[ [\x.x] 1 @ {_: *} ]
h; v
0 {
psi
---- dd<42,137> --->
Query:[ (\x.[x]) 1 @ * ]h[ (\x.[x]) 1 @ * ]:Query x---- <42,137> --->
phi
} 0
u; h
[ [\x.x] 1 @ {_: *} ]:Answer---- dd<0,d<42,137>> --->
psi; psi; e’; phi---- dd<42,137> --->
Query:[ (\x.x) [1] @ * ]h; k_1; h[ (\x.x) [1] @ * ]:Answer---- dd<42,1> --->
psi; e; phi; phi---- dd<0,d<42,1>> --->
Query:[ [\x.x] 1 @ {_: *} ]
h; v
0 {
psi
---- <42,1> --->
Answer x:[ (\x.[x]) 1 @ * ]h[ (\x.[x]) 1 @ * ]:Answer---- dd<42,1> --->
phi
} 0
u; h
[ [\x.x] 1 @ {_: *} ]:Answer---- dd<0,gdd<42,1>> --->
psi; psi; e’; phi---- dgdd<42,1> --->
Query:[ (\x.x) [1] @ * ]h[ (\x.x) [1] @ * ]:Answer---- gdd<42,1> --->
psi; phi; phi---- dgdd<42,1> --->
Query:[ [\x.x] 1 @ {_: *} ]h
[ [\x.x] 1 @ {_: *} ]:Answer---- gdd<42,1> --->psi
[ [(\x.x) 1] @ ({_: *}, *) ]:Answer---- dd<42,1> --->
Result: 1 / State: ({_: *}, *)Finally let us speak about making |N|-many copies of a transducer—
which interprets the ! modality that is implicit in the Girard
translation A ! B = ! A ( B. The bookkeeping functionv : N ! N ⇥ N in Fig. 2, line 18, splits |N|-many pipes into
|N| · |N|-many pipes; and lines 19 and 27 mean the token went
to the 0-th bunch of pipes, i.e., to the 0-th copy of the transducer[ (\x.[x]) 1 @ * ]. The state {_: *} that occur e.g. on line
17 stands for the function N ! 1, n 7! *, meaning that the state of
every copy of the transducer is the unique one *.

Acknowledgments

aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa
aaaaa

Thank are due to Ugo Dal Lago, Claudia Faggian, Dan Ghica andAkira Yoshimizu for useful discussions, and to the anonymous referees for useful comments. K.M. and I.H. are supported by Grantsin-Aid for Young Scientists (A) No. 24680001, JSPS; T.K. is supported by Grant-in-Aid for JSPS Fellows; and N.H. is supported by
Grants-in-Aid for Young Scientists (B) No. 26730004, JSPS.

References[1] S. Abramsky. Retracing some paths in process algebra. In CONCUR,
pages 1–17, 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] 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.
[4] 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.
[5] D. R. Ghica, A. I. Smith, and S. Singh. Geometry of synthesis
IV: compiling affine recursion into static hardware. In M. M. T.
Chakravarty, Z. Hu, and O. Danvy, editors, ICFP, pages 221–233.
ACM, 2011. ISBN 978-1-4503-0865-6.

[6] 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.
[7] I. Hasuo and N. Hoshino. Semantics of higher-order quantum computation via geometry of interaction. In LICS, pages 237–246, 2011.
[8] N. Hoshino, K. Muroya, and I. Hasuo. Memoryful geometry ofinteraction: From coalgebraic components to algebraic effects. In
CSL-LICS, 2014. To appear.
[9] O. Laurent. A token machine for full geometry of interaction. In
TLCA, pages 283–297, 2001.
[10] 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.
[11] J. S. Pinto. Implantation Parallèle avec la Logique Linéaire (Applications des Réseaux d’Interaction et de la Géométrie de l’Interaction).
PhD thesis, École Polytechnique, 2001. Main text in English.
[12] G. Plotkin and J. Power. Algebraic operations and generic effects.
Applied Categorical Structures, 11(1):69–94, 2003.

(4,526 lines)

Figure 2. Simulation Result for ( x. x) 1

Muroya (U. Tokyo)

specific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
The
first
reasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5>--->
TtT Compiler
and TtT Simulator.
n| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- N
dd<42,5>
N · · · --->
NWe
expressatransducer
effect T ) as a Haskell prog
L
`
t
:
⌧
M
=
18
Result: 5 /L State:
Just (with(Rightthe
(*))
`
t
:
⌧
M
The second
reasonis
speculative
but
practical:
we
wish
to
folP = ( x : nat. x + x) (3 t 5) : nat(1)of the type Td m x a b:
low the path of [3, 4, 10, 11] and use memoryful GoI as a compilaN N ··· N

Memoryful GoI [Hoshino, —, Hasuo ’14]

where
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.

{

effectful
terms

type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
component
calculus
toy tool of TtT will then form a via
basis of coalgebraicsuch practical compilers.
right, in French, see e.g. [9, 11]), for readability and efficiency.

The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of a

1 The word “memory” here is almost synonymous with “internal states”

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
reader will be convinced by the following examples.
The ones like the former stand for the token’s
entrance to and exit
B
Cfrom a transducer. Specifically, p:[t@x]—with a subterm t0 of t
Transducers, Derived and Executed Consider the term P in (1)BdBto (a copy of) theD [t0 ]—means:
B by
B
···
with nondeterministic choice t in it. Its translation to a (three-state,
Bthe token
designatedentered↵cc···B· cj p.
nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), after somecctransducerc Lt0 M,d whose
current state
is x,· · ·atciits· ·port
Typical portscmanual simplifications, is depicted below (manually).
C (aAtop-levelA x (an answer toinclude:AQuery
query) and AAnswer
C A
the previous query on x; see Fig. 2, lines A
24 and 44). Similarly,
A[t@x]:p means the token departed from the port p.
The latter class of expressions like h; k_3; h on Fig. 1, line
5 and phi on Fig. 2, line 3 are referred to as bookkeeping. For
cpy
sum
h
LPM = L3M N,N L5M
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as purefunctions like h : N + N ! N + N) is found in [8]. As we noted.
(3)
19 before, these bookkeeping nodes correspond to logical connectives
MuroyaThe figure is a string diagram in the traced monoidal category of
in a proof net; therefore they change the number
carried(U.
byTokyo)thetransducers

specific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
recursionThe
firstreasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5> --->
TtT Compiler
and TtT Simulator.
| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- dd<42,5> --->We express
transducer
effect T ) as a Haskell prog
Result:5 / aState:
Just (with(Rightthe(*))

Memoryful GoI with recursion
effectfulterms

18
The second
speculative
P = reason( xis: nat.
x + x)but(3practical:t 5) : wenatwish to fol-(1)low the path of [3, 4, 10, 11] and use memoryful GoI as a compilawhere
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.
toy tool of TtT will then form a basis of such practical compilers.
The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of areader will be convinced by the following examples.

of the type Td m x a b:
type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
via coalgebraic component
calculus
right, in French, see e.g. [9, 11]), for readability and efficiency.

Transducers, Derived and Executed Consider the term P in (1)with nondeterministic choice t in it. Its translation to a (three-state,nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), after somemanual simplifications, is depicted below (manually).

transducers
LPM =L3M N,N L5M

h

sum

cpy

.

(3)

The figure is a string diagram in the traced monoidal category of

20

1 The word “memory” here is almost synonymous with “internal states”

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
The ones like the former stand for the token’s entrance to and exitfrom a transducer. Specifically, p:[t@x]—with a subterm t0 of t
designated by [t0 ]—means: the token entered to (a copy of) thetransducer Lt0 M, whose current state is x, at its port p. Typical ports
include: Query (a top-level query) and Answer x (an answer tothe previous query on x; see Fig. 2, lines 24 and 44). Similarly,[t@x]:p means the token departed from the port p.
The latter class of expressions like h; k_3; h on Fig. 1, line
5 and phi on Fig. 2, line 3 are referred to as bookkeeping. For
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as purefunctions like h : N + N ! N + N) is found in [8]. As we noted
before, these bookkeeping nodes correspond to logical connectives
Muroyain a proof net; therefore they change the number
carried(U.
byTokyo)thespecific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
recursionThe
firstreasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5> --->
TtT Compiler
and TtT Simulator.
| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- dd<42,5> --->We express
transducer
effect T ) as a Haskell prog
Result:5 / aState:
Just (with(Rightthe(*))

Memoryful GoI with recursion
effectfulterms

18
The second
speculative
P = reason( xis: nat.
x + x)but(3practical:t 5) : wenatwish to fol-(1)low the path of [3, 4, 10, 11] and use memoryful GoI as a compilawhere
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.
toy tool of TtT will then form a basis of such practical compilers.
The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of areader will be convinced by the following examples.

of the type Td m x a b:
type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
via coalgebraic component
calculus
right, in French, see e.g. [9, 11]), for readability and efficiency.

Transducers, Derived and Executed Consider the term P in (1)with nondeterministic choice t in it. Its translation to a (three-state,nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), after somemanual simplifications, is depicted below (manually).

transducers
LPM =L3M N,N L5M

h

sum

cpy

.

(3)

The figure is a string diagram in the traced monoidal category of

20

1 The word “memory” here is almost synonymous with “internal states”

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
The ones like the former stand for the token’s entrance to and exitfrom a transducer. Specifically, p:[t@x]—with a subterm t0 of t
designated by [t0 ]—means: the token entered to (a copy of) thetransducer Lt0 M, whose current state is x, at its port p. Typical ports
include: Query (a top-level query) and Answer x (an answer tothe previous query on x; see Fig. 2, lines 24 and 44). Similarly,[t@x]:p means the token departed from the port p.
The latter class of expressions like h; k_3; h on Fig. 1, line
5 and phi on Fig. 2, line 3 are referred to as bookkeeping. For
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as purefunctions like h : N + N ! N + N) is found in [8]. As we noted
before, these bookkeeping nodes correspond to logical connectives
Muroyain a proof net; therefore they change the number
carried(U.
byTokyo)thespecific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
recursionThe
firstreasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5> --->
TtT Compiler
and TtT Simulator.
| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- dd<42,5> --->We express
transducer
effect T ) as a Haskell prog
Result:5 / aState:
Just (with(Rightthe(*))

Memoryful GoI with recursion
effectfulterms

18
The second
speculative
P = reason( xis: nat.
x + x)but(3practical:t 5) : wenatwish to fol-(1)low the path of [3, 4, 10, 11] and use memoryful GoI as a compilawhere
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.
toy tool of TtT will then form a basis of such practical compilers.
The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of areader will be convinced by the following examples.

of the type Td m x a b:
type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
via coalgebraic component
calculus
right, in French, see e.g. [9, 11]), for readability and efficiency.

transducers
L3M N,N L5M

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
The ones like the former stand for the token’s entrance to and exitfrom a transducer. Specifically, p:[t@x]—with a subterm t0 of t
designated by [t0 ]—means: the token entered to (a copy of) thetransducer Lt0 M, whose current state is x, at its port p. Typical ports
include: Query (a top-level query) and Answer x (an answer tothe previous query on x; see Fig. 2, lines 24 and 44). Similarly,[t@x]:p means the token departed from the port p.
The latter class of expressions like h; k_3; h on Fig. 1, line
5 and phi on Fig. 2, line 3 are referred to as bookkeeping. For
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as purefunctions like h : N + N ! N + N) is found in [8]. As we noted
before, these bookkeeping nodes correspond to logical connectives
Muroyain a proof net; therefore they change the number
carried(U.
byTokyo)thefix(F ) = F (F (F (· · · )))Transducers, Derived and Executed Consider the term P in (1)with nondeterministic choice t in it. Its translation to a (three-state,nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), after somemanual simplifications, is depicted below (manually).
LPM =1 The word “memory” here is almost synonymous with “internal states”

h

sum

cpy

.

(3)

The figure is a string diagram in the traced monoidal category of20

specific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
recursionThe
firstreasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5> --->
TtT Compiler
and TtT Simulator.
| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- dd<42,5> --->We express
transducer
effect T ) as a Haskell prog
Result:5 / aState:
Just (with(Rightthe(*))

Memoryful GoI with recursion
effectfulterms

18
The second
speculative
P = reason( xis: nat.
x + x)but(3practical:t 5) : wenatwish to fol-(1)low the path of [3, 4, 10, 11] and use memoryful GoI as a compilawhere
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.
toy tool of TtT will then form a basis of such practical compilers.
The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of areader will be convinced by the following examples.

of the type Td m x a b:
type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
via coalgebraic component
calculus
right, in French, see e.g. [9, 11]), for readability and efficiency.

1 The word “memory” here is almost synonymous with “internal states”

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
The ones like the former stand for the token’s entrance to and exit
Transducers, Derived and Executed Consider the term P in (1)from a transducer. Specifically, p:[t@x]—with a subterm t0 of twith nondeterministic choice t in it. Its translation to a (three-state,
designated by [t0 ]—means: the token entered to (a copy of) the
nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), after sometransducer Lt0 M, whose current state is x, at its port p. Typical ports
manual simplifications, is depicted below (manually).
q
include: Query (a top-level query) and Answer x (an answer to1
the previous query on x; see Fig. 2, lines 24 and 44). Similarly,[t@x]:p means the token departed from the port p.
2
The latter class of expressions like h; k_3; h on Fig. 1, line
5 and phi on Fig. 2, line 3 are referred to as bookkeeping. For
cpy
sum
h
LPM = L3M N,N L5M
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as pureq .
functions like h : N + N ! N + N) is found in [8]. As we notedq1(3)20 before, these bookkeeping nodes correspond to logical connectives
MuroyaThe figure is a string diagram in the traced monoidal category of
in a proof net; therefore they change the number
carried(U.
byTokyo)thetransducers

fix(F ) = F (F (F (· · · )))x. x + x

1specific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
recursionThe
firstreasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5> --->
TtT Compiler
and TtT Simulator.
| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- dd<42,5> --->We express
transducer
effect T ) as a Haskell prog
Result:5 / aState:
Just (with(Rightthe(*))

Memoryful GoI with recursion
effectfulterms

18
The second
speculative
P = reason( xis: nat.
x + x)but(3practical:t 5) : wenatwish to fol-(1)low the path of [3, 4, 10, 11] and use memoryful GoI as a compilawhere
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.
toy tool of TtT will then form a basis of such practical compilers.
The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of areader will be convinced by the following examples.

of the type Td m x a b:
type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
via coalgebraic component
calculus
right, in French, see e.g. [9, 11]), for readability and efficiency.

1 The word “memory” here is almost synonymous with “internal states”

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
The ones like the former stand for the token’s entrance to and exit
Transducers, Derived and Executed Consider the term P in (1)from a transducer. Specifically, p:[t@x]—with a subterm t0 of twith nondeterministic choice t in it. Its translation to a (three-state,
designated by [t0 ]—means: the token entered to (a copy of) the
nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), after sometransducer Lt0 M, whose current state is x, at its port p. Typical ports
manual simplifications, is depicted below (manually).
q
include: Query (a top-level query) and Answer x (an answer to1
the previous query on x; see Fig. 2, lines 24 and 44). Similarly,[t@x]:p means the token departed from the port p.
2
The latter class of expressions like h; k_3; h on Fig. 1, linecc 3 are referredc to as bookkeeping.
5
and
phi
on
Fig.
2,
line
For
cpy
sum
L3M
L5M
h
LPM =
N,N
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as pureq .
functions like h : N + N ! N + N) is found in [8]. As we notedq1(3)20 before, these bookkeeping nodes correspond to logical connectives
MuroyaThe figure is a string diagram in the traced monoidal category of
in a proof net; therefore they change the number
carried(U.
byTokyo)thetransducers

fix(F ) = F (F (F (· · · )))x. x + x

1···specific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
recursionThe
firstreasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5> --->
TtT Compiler
and TtT Simulator.
| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- dd<42,5> --->We express
transducer
effect T ) as a Haskell prog
Result:5 / aState:
Just (with(Rightthe(*))

Memoryful GoI with recursion
effectfulterms

18
The second
speculative
P = reason( xis: nat.
x + x)but(3practical:t 5) : wenatwish to fol-(1)low the path of [3, 4, 10, 11] and use memoryful GoI as a compilawhere
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.
toy tool of TtT will then form a basis of such practical compilers.
The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of areader will be convinced by the following examples.

of the type Td m x a b:
type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
via extended coalgebraic
component
calculus
right, in French, see e.g. [9, 11]), for readability and efficiency.

1 The word “memory” here is almost synonymous with “internal states”

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
The ones like the former stand for the token’s entrance to and exit
Transducers, Derived and Executed Consider the term P in (1)from a transducer. Specifically, p:[t@x]—with a subterm t0 of twith nondeterministic choice t in it. Its translation to a (three-state,
designated by [t0 ]—means: the token entered to (a copy of) the
nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), after sometransducer Lt0 M, whose current state is x, at its port p. Typical ports
manual simplifications, is depicted below (manually).
q
include: Query (a top-level query) and Answer x (an answer to1
the previous query on x; see Fig. 2, lines 24 and 44). Similarly,[t@x]:p means the token departed from the port p.
2
The latter class of expressions like h; k_3; h on Fig. 1, linecc 3 are referredc to as bookkeeping.
5
and
phi
on
Fig.
2,
line
For
cpy
sum
L3M
L5M
h
LPM =
N,N
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as pureq .
functions like h : N + N ! N + N) is found in [8]. As we notedq1(3)21 before, these bookkeeping nodes correspond to logical connectives
MuroyaThe figure is a string diagram in the traced monoidal category of
in a proof net; therefore they change the number
carried(U.
byTokyo)thetransducers

fix(F ) = F (F (F (· · · )))x. x + x

1···

Memoryful GoI with recursion
Def. (component calculus)
C

D

C

Tr(C)

D

↵({Ci }i2I )

F(C)

B

C
d

B
c

B
c

A

D
d

B

C

A

B

c
C

A

A

c
c
c

···

B
B
↵
· · · ci · · · cj · · ·AAA(↵: I-ary algebraic operation)

22

Muroya (U. Tokyo)

Memoryful GoI with recursion
Def. (extended component calculus)

i2I

Ci

countable
parallelcomposition

fixpoint

Fix(C)
N⇥A

A

(

Fix

c1

A1

B2
c2

A2

N⇥A

A

=

B1

(

c

···

A
A
c

A

c

c

···

A
23

Muroya (U. Tokyo)

Memoryful GoI with recursion
Def. (extended component calculus)

i2I

countable
parallelcompositionCi

fixpoint

Fix(C)
N⇥A

A

(

Fix

c1

A1

B2
c2

A2

N⇥A

A

=

B1

(

c

···
c

A
c

c

···

A
c

A

c

c

···

A
23

Muroya (U. Tokyo)

Memoryful GoI with recursion
Lem.
A
A

(

Fix

A

c

N⇥A

(

A

A

=

c

N⇥A

c

c

A

=:

···

Fix(c)

A

A

N⇥A

A

satisfiesc

Fix(c)AA'

Fix(c)

.

A

N⇥A

24

Muroya (U. Tokyo)

Memoryful GoI with recursion
Def. (interpretation L ` t : ⌧ M)

t :: ⌧⌧ M( = x1 : ⌧1 , . . . , xn : ⌧n ),For a type judgement L ` t

we inductively define{n

LL `` tt : ⌧ M =

N N ··· N
L ` t: ⌧M
N N ··· N

25.

Muroya (U. Tokyo)

···

···

w

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

h

w
···

w

w
···

Memoryful GoI with recursion

da calculus (i.e. call7.3 follows from theer. In this section, we
l lambda calculus exly infinite set Loc of
atural number. Exisural number stored at
at a location `:

w

0

···

w0

···

···

e
c

Initially, the S-transducer drhaves as an S-transducer Ls(`
drf ` stores the value s(`) loc
drf ` looks up its internal sta
behaves following LnM witho
We interpret ` ` := nasg`,n = ({xrun

where the SetS -morphism c(c0 (xrun , m))(s)c0where we write e for u (1 ⇥···N), e0 for (>N ⇥ N) v, c for(c(xdone , m))(s)0u ( ⇥ N)L (v(uN)M v. Here we omit`t:⌧)+M u) ( L⇥`s:⌧`+t sv): andM =c Lforsome obvious bijections like N ⇥··· (N + N) ⇠= N ⇥ N + N ⇥ N. Initially, ({xrun , xdone }, c0 , x
after, ({xrun , xdone }, c0 , xru
These S-transducers are from dereliction and0 contraction
of
the
c
c0
GoI situation given in Section 4.2.4. We enotethat the component the right hand side can be an0
For example, the GoI inte
cpy consists of c and c0 .
···For , x : ⌧ ` t : , we define L ` x : ⌧. t : ⌧ ) M by
Q = ( x : nat. x

dt.

from the categoricalonad in Theorem 6.1
Loc
NLoc )N . This is a
V = N and L =often confuse a map_ N and a SetT g : N _ N.

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, and
0w and w 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 byDef. (interpretation L ` t : ⌧ M)

bal Statew0(c(x` , n))(s)(c(xm , n))(s)

···

d

···

L ` x : ⌧. t : ⌧ ) M =h

L ,x:⌧ `t: M
···

d0

···

d0

where d and d0 are S-transducers
26 from N to N given by d =0Muroya (U. Tokyo)

`t:⌧is an applicatio
followed by co( = x1 : ⌧1 , · · · , xn : ⌧n ),we inductively define an S-transducer

Memoryful GoI with recursion
L ` t : ⌧ M : N⌦(n+1) _ N⌦(n+1)

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,t : ⌧ M) and the lambda abstraction. We
variables, theL term` application
Def. (interpretationinterpret natural numbers, summation and variables as follows:w

L ` n : natM =

···

w

kn

h

w0

w0
···
w

L , x : nat, y : nat ` x + y : natM =

h

···

w

sum
w0

···

w0

w

i 1
···

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

h
w0

w
···
···

w0

w
w0

w
···

w0

···

where w0 : N !S ; and w : ; !S N are unique SetS -morphisms,
and h : N + N ! N + N is
h27 . Here h is from Section 6, and0

GoI interpreta
and N be cou
algebraic oper
on , which indrf

called genericassignment ` :simplicity, we
location ` and
We interpre

drL ` t + s : natM = L ` ( xy : nat. x + y) t s : natM···

F (N ⌦ · · · ⌦where the Set(

Initially, the S
haves as an Sdrf ` stores thedrf ` looks up
Muroya(U. Tokyo)
behavesfollow

Memoryful GoI with recursion
Def. (interpretation L ` t : ⌧ M)

J K ⇥ J ) ⌧K ⇥ J K !

J⌧ KJ K ⇥ J ) ⌧K ! J ) ⌧KJ K ) J ) ⌧K ! J K ) J ) ⌧K

J K ! J ) ⌧K

28

Muroya (U. Tokyo)

Memoryful GoI with recursion
Thm. (soundness)
For closed terms M and N of type ⌧ ,• ` M = N : ⌧ implies ([LM M]' , [LN M]' ) 2• ` M = N : nat implies LM M ' LN M.

J⌧ Kbehavioral equivalence

Moggi’s equations for computational lambda-calculus• equations for algebraic operations•

M tM =M
E[opr(M1 , . . . , Mn )] = opr(E[M1 ], . . . , E[Mn ])( x. M ) (N1 t N2 ) = ( x. M ) N1 t ( x. M ) N2

rec(f :) ⌧, x : . M ) = x. M [rec(f :) ⌧, x : . M )/f ]29

Muroya (U. Tokyo)

Memoryful GoI with recursion
Thm. (domain-theoretic characterization of Fix )Under the assumption that
• SetT is a Cppo-enriched category with Cppo-enriched (countable) cotuplings• compositions T of SetT is strict in the restricted form: f T ? = ? and? T (⌘Y g) = ? hold for any f : X ! T Y and g : X ! Y in Set• premonoidal structures X ⌦strict for any X in Set,⌦ X of SetT is locally continuous andit holds that:30

Muroya (U. Tokyo)

Memoryful GoI with recursion
Thm. (domain-theoretic characterization of Fix )
A

A

(

Fix

c

N⇥A

(=

N⇥A

A

A
c

c

is a supremum of an !-chain

···

c

A
A

A

A

A

A

A

A

A

?

?

?

···

E

c
A

?

?

···

A

A

E

c
A

c

?

···

E ···

A

where (X, c : X ⇥ A ! T (X ⇥ B), x0 2 X) E (Y, c : Y ⇥ A ! T (Y ⇥ B), y0 2 Y )def.

(=) X = Y ^ x = y ^ c v d in SetT (X ⇥ A, X ⇥ B)
31

Muroya (U. Tokyo)

specific; currently
it supports
the powerset
monad (nondeterminof simplicity:
it allows
us to analyze
complicatedhigher-order 34ism) and the distribution monad (probability).
computation in the elementary terms of nodes and edges in graphs 5(or: TtT
linksasandedges in proof
The samenature,a Prototype
We nets).
emphasizethat what
ourhowever,tool TtT posescur- 6certainlimitations
use of use
GoI,whatsoever:too. For example,
long 7
rentlydoes is oftonothepractical
after all it istranslatesinan-term—that
may connectives
well be simply
expressed
as 8
known
theeffectfulcommunitythat additivein linearlogic—
Haskell program—to
anotherthat is way
more 9and asimilarly
coproduct types
likeHaskell
bit =program
1 + 1—callfor special
10complicated
and
runs
more
slowly.
Neverthelesswebelieve
thisiscare in GoI interpretation that is far from trivial. One solution by so-11
a worthwhile
venture,the following
three reasons.
calledadditive slices[9],forwhich
can be thoughtof as an additional12
recursionThe
firstreasonistheoretical:
ourmemoryful
GoI framework 13“memory” layer on proof nets.
in [8] seems to be a useful theoretical tool that gives us in- 14
Anotherexample of the limitations of “memoryless GoI” mansights into higher-order computation with effects. Automating the 15
ifestsitself in presenceof computational
effects.
the call-16
translation—that
is painfullycomplicatedwhenConsider
done by hand—by-valueevaluationof theterm
17will hencemeet sometheoreticians’
needs.

+-.gory C------>
withdd<42,137>
suitable additional
structures. What we do in [8] is| |Query:[ [3]|_|5 @ * ]category| |as C theh;k_3; h of resumptions, i.e. transducers modulo a suitequivalence.
This in fact is already done in [2]: our te| |behavioral[ [3]|_|5@ * ]:Answer| |nical ---dd<42,3>---> use of component calculi—those cal
novelty
is systematic| |for [composing[3|_|5] @ transducers,
Just (Left (*))]:Answerin coalgebraic terms—
formulated| | ---- dd<42,3> --->
composing resumptions.
| Result: 3 / State: Just (Left (*))‘-.
---- dd<42,137> --->Our
Tool
TtT This is a preliminary report on the implementa|
Query:[ 3|_|[5] @ * ]Our tool is called TtT—short for “Term|of memoryfulh; k_5; GoI.
himplemented in Haskell. It consists of|Transducers”—and[ 3|_|[5] @ * is]:Answer|parts:---dd<42,5>--->
TtT Compiler
and TtT Simulator.
n| [TtT[3|_|5]@ Just(Right (*))]:Answer sketched in the abCompiler
implements
the translation| ---- N
dd<42,5>
N · · · --->
NWe
expressatransducer
effect T ) as a Haskell prog
L
`
t
:
⌧
M
=
18
Result: 5 /L State:
Just (with(Rightthe
(*))
`
t
:
⌧
M
The second
reasonis
speculative
but
practical:
we
wish
to
folP = ( x : nat. x + x) (3 t 5) : nat(1)of the type Td m x a b:
low the path of [3, 4, 10, 11] and use memoryful GoI as a compilaN N ··· N

Memoryful GoI with recursion

where
subtermto3hardware.
t 5 returns
3 orcase
5 nondeterministically.
Obvitionthe
technique
In ourthis will specifically mean
to thetaketerm
hardwarethat natively
supportsthe(but
effectandHowevercompilingously
is expected
to yield
6 or 10
notT ,8).
thewith T -algebraic
it. Doingfor emerging
comusual -terms
GoI interpretation
caneffects
yield 8to too:in thesointeraction
betweenputing paradigms
probabilistic
andvaluequantumprogrammingwill
the subterms
x. x +likex and
3 t 5, theof thelatter is queried
havepractical
impacts—not
only
becauseprograms Herewill exetwice,
to bigwhich
the subterm
3t
5 can
answerdifferently.
what•cute faster(seememory
e.g. [5]),mechanism
but also because
the compilation(basedis needed
is somethat allows
the subterm
3t5
on denotational semantics) is correct by construction. The current
to remember the choice that •it has made, and to stick to it.

{

effectful
terms

type

for m
3 t(x,
5 b)
Td Figurem x a1. bSimulation= (x,Result
a) ->

where
m is the isHaskell
monad
thatcarries
corresponds
T , x isnthe t
The convention
as follows.
A tokena naturaltonumber
translation
for a statemore
space,
a is thetypeinandb the output
type.
around—or
precisely,
aninputedge e.g.
(3) consistsof |N|-many“pipes”
andtransducer
a token goes
through fromthe n-th—and
this is denotedbythenTheobtainedan (effectful)-term isbased on Geometry---nof--->.
Therefore
expressions
like dd<42,137>
in Fig.
1 mo
ecutedbyInteraction
TtT
Simulator,
in a meticulous
way where
every
stand
forisarecorded.
certain natural
number.
We howeverhere
chose
to supplement
Recallthat a transducer
is muchlike a p
mentarilyusethedynamic
algebranotation
(g
for
left
and
d
for
toy tool of TtT will then form a via
basis of extended
such practical compilers.coalgebraic component calculus
right, in French, see e.g. [9, 11]), for readability and efficiency.

The thirdGoI
reasonMotivatedis: it’s simplyof fun (butto seemore
higher-order“Memoryful”
by aalotsimilarcomplieffectful
computation
in weaction—or
GoI atinwork.
We hope thecated)
technical
challenge
encountered
the semantics
of a

1 The word “memory” here is almost synonymous with “internal states”

In Fig.
1, former
between----fromn --->
token are ef
stick
to thesomovements
as to distinguishstates ofas athecomputational
expressions like Query:[ [3|_|5] @ Nothing ] and h; k_3; h.
reader will be convinced by the following examples.
The ones like the former stand forthe token’s entrance to and exit
B
C
A
Transducers, Derived and Executed Consider the term P in (1)from a transducer. Specifically, p:[t@x]—witha subterm t0 of t
B
d
B
D
B
Bthe token···
A to (a copy of) thewith nondeterministic choice t in it. Its translation to a (three-state,
designatedby [tB0 ]—means:entered↵cc· · · ci · · · cj · · ·cc · ·portsc transducerd·nondeterministic) transducer LPM : 3 ⇥ N ! P(3 ⇥ N), afterBsomec c current
Lt0 M, whosestate is x, at its port
p.c TypicalAc
A Query
manual simplifications, is depicted below (manually).
CA
C (ainclude:A top-level Aquery)A and Answer x (an answer toAA
the previous query on x; see Fig.
A 2, lines 24 and 44). Similarly,[t@x]:p means the token departed from the port p.
The latter class of expressions like h; k_3; h on Fig. 1, line
5 and phi on Fig. 2, line 3 are referred to as bookkeeping. For
cpy
sum
h
LPM = L3M N,N L5M
example, h; k_3; h means the token traversed an h node, a k3
node and then an h node. The definition of these nodes (as purefunctions like h : N + N ! N + N) is found in [8]. As we noted.
(3)
32 before, these bookkeeping nodes correspond to logical connectives
MuroyaThe figure is a string diagram in the traced monoidal category of
in a proof net; therefore they change the number
carried(U.
byTokyo)thetransducers