Memoryful GoI with Recursion
Koko Muroya

Naohiko Hoshino

Ichiro Hasuo

University of Tokyo
Email: muroykk@is.s.u-tokyo.ac.jp

RIMS, Kyoto University
Email: naophiko@kurims.kyoto-u.ac.jp

University of Tokyo
Email: ichiro@is.s.u-tokyo.ac.jp

Abstract—In this preliminary report we extend our frameworkof memoryful Geometry of Interaction (mGoI) [Hoshino, Muroya &Hasuo, CSL-LICS 2014] by recursion. The mGoI framework provides a sound translation from λ-terms to transducers; notably it
accommodates algebraic effects introduced by Plotkin and Power;
and the translation, defined in terms of a coalgebraic component
calculus, is extracted from categorical semantics (hence correct-byconstruction). In our current extension, recursion is additionallyaccommodated by introducing a new “fixed point” operator in
the component calculus.

machines) by effects specified by a monad T . Here we follow[8] and model algebraic effects by a monad T on the category
Set of sets and functions.

I. G O I I NTERPRETATIONA T -transducer (X, c, x) : A _ B can be seen asBan (T -effectful) transition function c with input A,
coutput B, a set of internal states X and an initial
Astate x. It shall be presented, in diagrams, as inFig. 1. a T Fig. 1.

Girard’s Geometry of Interaction (GoI) [1] is originallyintroduced as semantics of linear logic proofs and, via theCurry-Howard correspondence (and the Girard transformation),
it has been successfully applied to denotational semantics ofhigher-order functional programs. The resulting semantics giveso-called “GoI interpretation” of programs; one of its notablefeatures is that GoI interpretation of function application isgiven by interactions of a function and its arguments.
Many representations of GoI interpretation have been studied so far: the original one by elements of a C ∗ -algebra (ora dynamic algebra) that can be seen as “valid paths” on typederivation trees [1]; the one by token machines [2]; and thecategorical one by arrows in a traced symmetric monoidal
category [3]. The second one by token machines plays animportant role in bridging the gap between mathematical interpretation and low-level implementation. Namely it provides
techniques of compilation and high-level synthesis, such as acompilation technique [2] and a high-level synthesis technique[4] that enables hardware acceleration of programs by FPGA.
We wish to contribute to this sequence of work by enable
GoI interpretation to accommodate computational effects.
II. M EMORYFUL G O I
In the previous work [5] we developed the memoryful GoI(mGoI) framework that extends GoI interpretation of programs.
Notably it accommodates algebraic effects—computational effects with algebraic operations as a syntactic interface, introduced by Plotkin and Power [6], [7]. Their examples include:
nondeterminism, with a nondeterministic choice operation t
as an algebraic operation; probability, with a probabilistic
choice operation tp for any p ∈ [0, 1]; and global states, withoperations lookup and update.

Definition II.1 (T -transducers [5, Definition 4.1]). For sets
A and B, a T -transducer (X, c, x) from A to B (written as(X, c, x) : A _ B) consists of a set X, a function c : X ×A →T (X × B) and an element x ∈ X.

transducer

In the mGoI framework, T -transducers are com- (X, c, x) :A_B
bined via a component calculus over them. It consists of primitive T -transducers (as basic building blocks) andthe following operators on T -transducers: a) sequential composition ◦; b) binary parallel composition ; c) the trace operator
Tr; d) the countable copy operator F ; e) the operator α foreach algebraic operation α on T .1 On top of these operators
an auxiliary operator is defined: f) binary application •.2 The
last is a well-known construction called parallel compositionand hiding and is used here to translate function application.
In Fig. 2 are graphical presentation of these operators; we referreaders to [5] for their precise definitions.
CdBcBcAADBCA

cd(c) Tr(X, c, x) :A_B(b) binary parallel
composition (a) sequential
composition ◦Bc

N×B
N×A(d) F (X, c, x) :N×A_N×B

B

B

c1c2

AA

C

B

α...

A(e) α{(Xi , ci , xi )}i∈I :
A_B

N×C

N×CcdA(f) binary application •Fig. 2. Operators on T -transducers

A. Component Calculus over Transducers
The mGoI interpretation of a program is given by T transducers—an extension of Mealy machines (or sequential

1 We identify algebraic operations with their interpretations, as in [6].
2 Binary application • presented here is an adaptation of that in [5].

Lemma III.1. Let (X, c, x) : A + N × A _ A + N × A be aT -transducer. The T -transducer Fix(X, c, x) : A _ A satisfies
In our mGoI framework, to be precise, the provided interprethe behavioral equivalencetation L−M is from a type judgment Γ ` M : τ to a T -transducer(X, c, x) • Fix(X, c, x) ' Fix(X, c, x).
mmaaLΓ ` M : τ M :N_N .
Here the behavioral equivalence ' [5, Definition 5.2] is usedi=0i=0for (equational) reasoning on T -transducers; it enables us toHere N is the set of natural numbers. The interpretation is de- abstract away from internal state spaces of T -transducers.
With this extension of the component calculus the translation
fined inductively on the type derivations, using the component
L−M can be extended to recursion: the following definition iscalculus introduced in the above.
In [9] we presented a prototype implementation—TtT, short precisely what is given in [5], except recursion that is new.
for “Terms to Transducers”—of the translation L−M. Given a Definition III.2 (translation L−M). For each type judgment Γ `closed term M of type τ , the tool first generates a Haskell pro- M : τ where Γ = x : τ , . . . x : τ , we inductively define a11mmgram that implements a transition function of the T -transducer T -transducerL` M : τ M; and then it produces a simulation result of themexecution of the transducer. We believe that the tool serves asmm
NN ...
Naaa first step towards high-level synthesis (that translates a λLΓ ` M : τ M:N_LΓ ` M : τ M =N
term to hardware design like on FPGA)—much like in [4] but
NN ...
Ni=0i=0
now with algebraic effects.
mSome further comments are in order on: 1) a categorical as in Fig. 4. In Fig. 4, α is an n-ary algebraic operation on Tmodel behind the translation L−M; and 2) prospects of accom- that is the interpretation of op; and all the T -transducers othermodating recursion. In fact the translation L−M is extracted than those in the form LΓ ` M : τ M are primitives (see [5] forfrom a categorical model PerΦ —a Kleisli category of a strong their definitions).
monad Φ on a cartesian closed category Per—built on T transducers and the component calculus. It is an instance of The translation L−M is sound with respect to the equational
the class of models, that is provided in [6], of the Moggi’s theory given in [6]. The latter is (an almost full fragment of)computational λ-calculus [8] with algebraic operations and the Moggi’s equational theory of computational λ-calculus,
arithmetic primitives. In [6] a class of models that accommo- extended by algebraic operations, arithmetic primitives anddates recursion is studied as well; the key is a fixed point recursion.
operator on a categorical model. However it was not clear, Theorem III.3 (soundness of L−M). For closed terms M and N
at the time of writing our previous paper [5], how to obtain a of the base type nat, ` M = N : nat implies L` M : natM 'fixed point operator on the categorical model PerΦ and extend L` N : natM.
the translation L−M to recursion.
For simplicity we have restricted to algebraic operations withfinite arities; accommodating countable arities is straightforIII. T RANSLATION OF R ECURSION
ward (much like in [5], [10]). On top of soundness, we expect
Here we report our ongoing work that introduces recursion adequacy to hold too, against the operational semantics in [6].
to the mGoI framework in [5].
Extension of our implementation tool TtT with recursion isfuture work, too.
A. Extension of Component Calculus and Translation
B. The Categorical Model
Our approach is to extend the component calculus shown in
The translation L−M extended with recursion (Def. III.2) isFig. 2: binary parallel composition  is extended to a countablebackedup by a categorical model, too—this fact underlies
one i∈I ; and on top of the calculus, a “fixed point” operator
Thm.
III.3.
Starting from the model PerΦ used in [5], weFix is introduced. It is presented in Fig. 3.
use its modification PerΦ0 (whose details we do not describehere); then we can show that the construction Fix in Lem. III.1
AN×A
indeed yields a (categorical) fixed point operator in PerΦ0 . In.
.
.
showing the latter, the following is a key technical lemma.
cccc
B. Translation from Terms to Transducers

Lemma III.4. Let Cppo be the category of pointed ω-cpo’s(i.e. with the least element ⊥) and continuous maps. Assume
that the Kleisli category SetT satisfies the following:
Fig. 3. Fix(X, c, x) : A _ A. Here one dashed box means countable• it is Cppo-enriched (with a partial order v) and has
duplication of a component.
Cppo-enriched (countable) cotupling;
It indeed gives a fixed point with respect to binary application• its compositions ◦T is strict, in the restricted sense as•.
in [5, Lem. 4.3];

AN×Aits premonoidal structures X ⊗ −, − ⊗ X are locallycontinuous and strict, for any X ∈ Set.
The Cppo-enrichment of SetT induces the following ωcpo structure on T -transducers. A partial order E on T transducers (X, c, x), (Y, d, y) : A _ B is defined by•def.

(X, c, x) E (Y, d, y) ⇐⇒ X = Y ∧ x = y ∧ c v d .

Minimal T -transducers with respect to E are given by(Z, ⊥, z) for any set Z. Now for a T -transducer (X, c, x) : A+N × A _ A + N × A, the T -transducer Fix(X, c, x) : A _ A
is a supremum of the following ω-chain.
A

⊥
A

A

N×A

⊥
N×A

⊥

...

Ec
AA

N×A⊥

⊥

...

E

N×A

N×AcAc

⊥

...

E ...

i−1...

LΓ ` xi : τi M =h...

w ... www0 . . . w0w0...

ww0...
i−1...

φeψccψ
...

LΓ ` M N : τ M =LΓ ` M : σ ⇒ τ MLΓ ` N : σM...

φφe0c0ψ

c0...

N×A...

ACKNOWLEDGMENT
The authors are supported by the JSPS-INRIA Bilateral Joint
Research Project CRECOGI; K.M. and I.H. are supported by
Grants-in-Aid No. 24680001 & 15K11984, JSPS; and N.H. issupported by Grant-in-Aid No. 26730004, JSPS.
R EFERENCES[1] J.-Y. Girard, “Geometry of Interaction I: interpretation of system F,” inLogic Colloquium 1988, ser. Studies in Logic & Found. Math., vol. 127.
Elsevier, 1989, pp. 221–260.
[2] I. Mackie, “The Geometry of Interaction machine,” in POPL 1995.
ACM, 1995, pp. 198–208.
[3] S. Abramsky, E. Haghverdi, and P. J. Scott, “Geometry of Interaction
and linear combinatory algebras,” Math. Struct. in Comp. Sci., vol. 12,no. 5, pp. 625–665, 2002.
[4] D. Ghica, “Geometry of Synthesis: a structured approach to VLSI
design,” in POPL 2007. ACM, 2007, pp. 363–375.
[5] N. Hoshino, K. Muroya, and I. Hasuo, “Memoryful Geometry of Interaction: from coalgebraic components to algebraic effects,” in CSL-LICS
2014. ACM, 2014, p. 52.
[6] G. Plotkin and J. Power, “Adequacy for algebraic effects,” in FoSSaCS
2001, ser. Lect. Notes Comp. Sci., vol. 2030. Springer, 2001, pp. 1–24.
[7] ——, “Semantics for algebraic operations,” Elect. Notes in Theor. Comp.
Sci., vol. 45, pp. 332–345, 2001.
[8] E. Moggi, “Computational lambda-calculus and monads,” Tech. Report,pp. 1–23, 1988.
[9] K. Muroya, T. Kataoka, I. Hasuo, and N. Hoshino, “Compiling effectfulterms to transducers: prototype implementation of memoryful Geometryof Interaction,” in LOLA 2014, 2014.
[10] G. Plotkin and J. Power, “Algebraic operations and generic effects,” Appl.
Categorical Struct., vol. 11, no. 1, pp. 69–94, 2003.

udφLΓ ` λx : σ. M : σ ⇒ τ M =d...

LΓ, x : σ ` M : τ M

h...

ψd0v

d0...

...

LΓ ` n : natM =hw

w

w0w0kn...

...
w

LΓ, x : nat, y : nat ` x + y : natM =w0...

...
ww

sumhw0w0...

c0... ...
...

LΓ ` op(M1 , . . . , Mn ) : τ M =LΓ ` M1 : τ M

...

α...

LΓ ` Mn : τ M

...

...

... ...

LΓ ` rec(f : σ ⇒ τ, x : σ. M ) : σ ⇒ τ M =
u

d ...

dφ

c ...

chFixw0(if x 6≡ y)cLΓ, x : nat ` x + x : natM =w

sumhLΓ, f : σ ⇒ τ, x : σ ` M : τ M
ψc0 . . . c0v

d0 . . . d0v

d0 . . . d0ud ... d...

Fig. 4. inductive definition of the translation L−M