Memoryful Geometry of Interaction II
Recursion and Adequacy
Koko Muroya

Naohiko Hoshino

Ichiro Hasuo

University of Tokyo, Japanmuroykk@is.s.u-tokyo.ac.jp

RIMS, Kyoto University, Japannaophiko@kurims.kyoto-u.ac.jp

University of Tokyo, Japanichiro@is.s.u-tokyo.ac.jp

Abstract
A general framework of Memoryful Geometry of Interaction (mGoI)
is introduced recently by the authors. It provides a sound translationof lambda-terms (on the high-level) to their realizations by stream
transducers (on the low-level), where the internal states of the latter(called memories) are exploited for accommodating algebraic effects of Plotkin and Power. The translation is compositional, hence“denotational,” where transducers are inductively composed using
an adaptation of Barbosa’s coalgebraic component calculus.
In the current paper we extend the mGoI framework and provide a systematic treatment of recursion—an essential feature of
programming languages that was however missing in our previous
work. Specifically, we introduce two new fixed-point operators in
the coalgebraic component calculus. The two follow the previous
work on recursion in GoI and are called Girard style and Mackiestyle: the former obviously exhibits some nice domain-theoretic
properties, while the latter allows simpler construction. Their equivalence is established on the categorical (or, traced monoidal) levelof abstraction, and is therefore generic with respect to the choiceof algebraic effects. Our main result is an adequacy theorem of ourmGoI translation, against Plotkin and Power’s operational semantics
for algebraic effects.
Categories and Subject Descriptors D.3 [Formal Definitions andTheory]: Semantics; F.3 [Semantics of Programming Languages]:
Algebraic approaches to semantics
General Terms Theory
Keywords Geometry of Interaction, monad, algebraic effect, adequacy

1.

Introduction

Geometry of interaction (GoI) introduced by Girard is a semantics
of linear logic [11]. The aim of GoI project is to mathematicallyunderstand dynamical process of cut-elimination. In other words, via
Curry-Howard correspondence, GoI project aims to mathematicallyunderstand dynamical process of program execution. This is likegame semantics that interprets programs by dialogue between two
players [1, 17].

This paper is a second step towards our prospect of developing GoI-based compilation technique for effectful programming languages. Our prospect is motivated by Ghica’s Geometry of Synthesis[7] where Ghica applied the idea of GoI and game semantics to givea semantics-directed compiler. In our first step [16], we introduced
GoI semantics called memoryful GoI (mGoI) for Moggi’s computational lambda calculus equipped with algebraic effects. Our goalin this paper is to show that mGoI introduced in our previous work
can accommodate recursion. Main contributions of this paper are as
follows.
• We give two mGoI interpretation of recursion.

One is Girard style interpretation. Interpretation of recursion
is given as limits of approximating chains as given in [12].
This modeling style is much like the one in domain theory
and is easy to mathematically deal with.
The other is Mackie style interpretation. Interpretation of recursion is given by feedback loops as given in [22]. Mackiestyle is much simpler than Girard style and is easy to implement.
• We show that these two interpretations of recursion are the same.

Coincidence of these styles enables us to enjoy advantages ofeach of them. In this paper, we give interpretation of recursion in
Mackie style because of its simplicity, and we use Girard style
to show adequacy of mGoI interpretation.

• We prove adequacy of mGoI interpretation with respect to theoperational semantics given by Plotkin and Power [25].

Our framework is applicable to a wide class of computational effects. For example, mGoI can model nondeterministic choice, probabilistic choice, global states, interactive I/O, exceptions and their
combinations. The generality of mGoI is achieved by a categorical framework of GoI called GoI situation introduced by Abramsky,
Haghverdi and Scott in [2].
Construction of mGoI semantics for the computational lambda
calculus is as follows:
A monad T : Set → Set
The Kleisli category SetT
T -transducers
GoI situationmGoI semantics for the computational λ-calculus
Our starting point is a monad on the category Set of sets andfunctions. Given a monad T : Set → Set, we construct a categoryof sets and T -transducers. Roughly speaking, T -transducers are “T branching” Mealy machines: when T is the powerset monad P, a
P-transducer is a nondeterministic Mealy machine; when T is thesubdistribution monad D, a D-transducer is a probabilistic Mealy
machine; when T is an exception monad E, a E-transducer is a
Mealy machine that may raise errors.
By constructing a GoI situation on the category of sets and T transducers, we obtain GoI semantics for the lambda calculus. What
we clarified in our previous work is that the monad T induces interpretation of computational effects. For example, we interpret nondeterministic choice 0 t 1 by a P-transducer, which is a nondeterministic Mealy machine, whose transition diagram is given by
q/0: sl o

q/0



s0

q/1

/ sr dq/1 .

We explain how this P-transducer behaves by using mGoI interpretation of (λx. x + x) (0 t 1). Interpretation of this term is givenby the following interactive communication between λx. x + x and
0 t 1:
1. λx. x + x requires output of the left argument x.
2. 0 t 1 nondeterministically answers 0 or 1 and stores its choice.
3. λx. x + x requires output of the right argument x.
4. 0 t 1 answers its first choice.
5. λx. x + x outputs the sum of the first answer and the second
answer from 0 t 1.
As a result, λx. x + x nondeterministically outputs 0 or 2. This isexactly the call-by-value evaluation result of (λx. x + x) (0 t 1).
The important point in this dialogue is that 0 t 1 memorizes its
first choice by using states. Use of this memorization mechanism isessential. Without memorization, (λx. x + x) (0 t 1) may output 1
because 0 t 1 may answer 0 to the first question and 1 to the second
question from λx. x + x. We note that we have similar problems forcall-by-name situation.
1.1

Related Works

Recursion in GoI There already exist some works on interpretingrecursion in GoI. The earliest one is Girard’s GoI II [12]. Girard’s
idea is similar to the one in domain theory, i.e., fixed points are
given as limits of approximating ω-chains. In this paper, we callthis interpretation of recursion Girard style. Results in GoI II are
generalized in terms of unique decomposition category in [13].
We can find another style of interpreting recursion in [22] where
Mackie employed feedback loops to interpret recursion. We call thisinterpretation of recursion Mackie style. We can also find Mackiestyle fixed point operator in [15, 19]. In this paper, we show thatthese two styles are the same in mGoI semantics.
GoI as Mathematical Framework for Implementation While theoriginal motivation of GoI stems from mathematical investigation in
proof theory, the dynamical aspect of GoI provides practical applications. In GoI semantics, we model programs by means of interactive dialogue, and we can understand GoI semantics as translationof high-level languages into low-level languages. Danos and Regnier
presented this basic idea of applying GoI to implementation of functional programming languages in [4]. Developing their idea, Mackie
gave an implementation of PCF [22] where implementation of PCF
is given by simulating interactive dialogue by means of an assembly language. GoI-based implementation inherits some features of
GoI: simple run-time systems and compositional interpretation ofprograms. Furthermore, soundness of GoI semantics assures correctness of GoI-based implementation by construction. Recently, in theseries of works [7–10], Ghica applied the idea of GoI and game semantics to give a semantics-directed compiler for programming languages based on Reynolds’ Syntactic Control of Interference. Ghica
also pointed simplicity of compilation results of programs: circuits
generated by compilation consist of a few basic circuits connected

through wirings. Dal Lago and Schöpp applied GoI to design a functional programming language for computation with sublinear space[3]. Their design is based on an observation that space-efficient computation can naturally be organized into interactive dialogue.
Call-by-value and Computational Effects GoI semantics is callby-name in nature: arguments are evaluated only if they are called
in interactive dialogue. Therefore, in order to model call-by-value
computation, we need to suitably adapt GoI interpretation. There areseveral approaches to call-by-value GoI. An early approach given in[6] is to employ jumping mechanism to enforce call-by-value evaluation. In [29], Schöpp employed cps-translation with some refinement to achieve efficient implementation of call-by-value computation. Later, this approach is reformulated in terms of typed closure conversion [30]. In this paper, we employ cps-translation, andtherefore, our approach is close to Schöpp’s approach (without refinement for efficiency). Recently, another approach to call-by-value
GoI is proposed in [19].
Schöpp also studied combination of GoI and effects in [28],where he introduced GoI semantics for a functional programming
language INTML[WEC]. We can embed a restriction of the enriched effect calculus, which is introduced by Egger, Møgelberg andSimpson [5], into INTML[WEC], which can accommodate computational effects through this embedding. Our basic idea in this paper is similar to Schöpp’s approach: modeling computational effects
by means of computational effects in interactive dialogue. Differences between our work and Schöpp’s work are: while the computational lambda calculus allows to use effects at any type, it is notclear how to use computational effects at any type in INTML[WEC];
while control operators and locally scoped states can be modeledin Schöpp’s approach, we restrict our attention to algebraic effects.
Precise comparison is future work.
1.2

Organization of the Paper

First in Section 2 we describe our target language LΣ and its operational semantics. They are slight adaptations of those introducedin [25]. In Section 3 we give algebraic operations on monads, thatmodel algebraic effects in a uniform way. We also state the requirement of our framework on monads in this section. In Section 4 werecall the component calculus used in the mGoI framework. It is
extended in Section 5 by two styles of fixed point operators. Theirproperties are investigated in this section as well. Finally we givea translation of the language LΣ to transducers, as well as its adequacy, in Section 6; and illustrate the translation and execution of
the resulting transducer in Section 7 using an example.

2.

Target Language and Operational Semantics

This section is devoted to our target language LΣ and its operationalsemantics. They are slight adaptations of those given by Plotkin &Power [25]; differences are introduction of coproduct types τ + τ
and replacement of the base type bool by a coproduct type 1 + 1.
2.1

The Target Language LΣ

The language LΣ extends the call-by-value computational λ-calculus[23] with algebraic operations, product/coproduct types and arithmetic primitives. It is parametrized by an algebraic signature Σ
whose element is an operation op that comes with its arity ar(op). In
this paper we assume all arities are finite.1 For an operation op ∈ Σ
we often write op0 if its arity is zero and op+ if positive.
Example 2.1. Here are examples of algebraic signatures taken from[26].
1 Readers are referred to [26] for accommodation of countable arities.

• The signature Σexcept = {raisee | e ∈ E} is for excep-

tions: the set E specifies exceptions and each nullary operation
raisee () raises an exception e.
• The signature Σndet = {t} is for nondeterminism, where thebinary operation t represents nondeterministic choice.
• The signature Σprob = {tp | p ∈ [0, 1]} is for probabilistic
choice: in M tp N, M is chosen with probability p; and N is withprobability 1 − p.
• The signature Σglstate = {lookupl | l ∈ Loc} ∪ {updatel,v |l ∈ Loc, v ∈ Val } is for actions on global states, where
Loc is a set of locations and Val is a finite set of values. In
lookupl (Mv1 , . . . , Mv|Val| ), one of the arguments is chosen according to a value stored by a global state of location l. In
updatel,v (M), M is executed after updating a global state of location l with a value v.

R ::= (λx : σ. M) V | rec(f : σ → τ, x : σ). M| op+ (M1 , . . . , Mar(op) ) | fst(hV, Vi) | snd(hV, Vi)| case(inlτ,σ (V), x. M, y. M) | case(inrτ,σ (V), x. M, y. M)|V+V
If a closed term M is not a value, it is decomposed into either the form
E[R] or E[op0 ()], where E, R and/or op0 are uniquely determined.
For closed redexes, transition relations are defined as in Figure 2.
The unlabeled “pure” transition relation → corresponds to the ordiop
nal β-reduction; and a labeled “effectful” transition relation →i rep+resents reduction of a term op (M1 , . . . , Mar(op) ) to one argument
Mi , according to an effect generated by op+ . Additionally for a termop0 (), a labeled “effectful termination” predicate ↓op is defined by
op0 () ↓op .

The types τ , terms M and values V of LΣ are defined by thefollowing BNF’s:(λx : σ. M) V → M[V/x]τ ::= unit | nat | τ → τ | τ × τ | τ + τ

fst(hV1 , V2 i) → V1

M ::= x ∈ Var | λx : σ. M | M M | rec(f : σ → τ, x : σ). M+

0| op (M1 , . . . , Mar(op) ) | op () | ∗ | fst(M) | snd(M) | hM, Mi| inlτ,σ (M) | inrτ,σ (M) | case(M, x. M, y. M) | n ∈ N | M + M
V ::= x ∈ Var | λx : σ. M | ∗ | hV, Vi | inlτ,σ (V) | inrτ,σ (V)rec(f : σ → τ, x : σ). M → (λx : σ. M)[rec(f : σ → τ, x : σ). M/f]snd(hV1 , V2 i) → V20case(inlτ,σ (V), x. N, x . N0 ) → N[V/x]case(inrτ,σ (V), x. N, x0 . N0 ) → N0 [V/y0 ]n+m→n+m

opi+

op (M1 , . . . , Mar(op) ) → Mi (i = 1, . . . , ar(op))
Figure 2: Transition Relations for Closed Redexes|n∈Nwhere Var is a (countable) set of variables, N is the set of natural
numbers and op ∈ Σ is an operation. Substitution M[N/x] is definedas usual and a term is called closed if it has no free variables.
A type judgment Γ ` M : τ , where Γ = x1 : τ1 , . . . , xm : τm ,is inductively defined by the typing rules shown in Figure 1. They
are standard except those for operations in Σ; note that nullary
operations op0 () can be arbitrarily typed. In the paper we assume
any term M is well-typed, i.e. there exists a derivable type judgmentΓ ` M : τ.
Γ, x : σ ` M : τΓ`M:σ→τ Γ`N:σΓ ` xi : τi Γ ` λx : σ. M : σ → τΓ`M N:τΓ, f : σ → τ, x : σ ` M : τΓ ` rec(f : σ → τ, x : σ). M : σ → τUsing the transition relations and predicates, we define the small
step operational semantics for a closed term, that is not a value, byΓ ` Mi : τ (i = 1, . . . , ar(op))

Both small and medium step operational semantics are uniquelydetermined for each closed term.

Γ ` op+ (M1 , . . . , Mar(op) ) : τΓ ` op0 () : τ Γ ` ∗ : unitΓ`M:τ ×σΓ`M:τ ×σ Γ`M:τ Γ`N:σΓ ` fst(M) : τ Γ ` snd(M) : σΓ ` hM, Ni : τ × σ
Γ`M:τ
Γ`M:σ
Γ ` inlτ,σ (M) : τ + σ Γ ` inrτ,σ (M) : τ + σΓ ` M : τ + τ 0 Γ, x : τ ` N : σ Γ, x0 : τ 0 ` N0 : σΓ ` case(M, x. N, x0 . N0 ) : σΓ ` M : nat Γ ` N : nat
Γ ` n : nat
Γ ` M + N : nat
Figure 1: Typing Rules of LΣ

R→M
E[R] → E[M]R →i Mopop0 () ↓op

opi

E[op0 ()] ↓op

E[R] → E[M]and define the medium step operational semantics for a closed term
M by
def.

M ⇒ V ⇐⇒ M →∗ V
op

def.

op

M ⇒i N ⇐⇒ ∃L. M →∗ L →i Ndef.

M ⇓op ⇐⇒ ∃L. M →∗ L ↓opdef.

M ⇑ ⇐⇒ ∃ infinite sequence M → M0 → · · · .

Lemma 2.2. (I) Any closed term M of type τ satisfies just one of thefollowing:• M ≡ V for a (unique closed) value V;• M → N for a unique closed term N of type τ ;op• M →i Ni for a unique operation op+ and a unique familyar(op){Ni }i=1 of closed terms of type τ ; and• M ↓op for a unique operation op0 .

(II) Any closed term M of type τ satisfies just one of the following:• M ⇒ V for unique (closed) value V of type τ ;op• M ⇒i Ni for a unique operation op+ and a unique familyar(op)

2.2

Operational Semantics

For LΣ we define two kinds of operational semantics: the small step
one and the medium step one. They are specified via decompositionof terms into evaluation contexts E and redexes R, defined by thefollowing BNF’s.
E ::= [−] | E M | V E | fst(E) | snd(E) | hE, Mi | hV, Ei| inlτ,σ (E) | inrτ,σ (E) | case(E, x. M, y. M) | E + M | V + E{Ni }i=1 of closed terms of type τ ;• M ⇓op for a unique operation op0 ; and• M ⇑.

Additionally the notion of effect values is introduced with theintention of defining a big step operational semantics. The notion isformalized using continuous Σ-algebras. A continuous Σ-algebra
A is an ω-cppo (i.e. ω-cpo with the least element Ω), with each
operation op ∈ Σ identified as a continuous function from thear(op)-fold product of A to A. Especially for a set X, there exists
the free continuous Σ-algebra CT Σ (X) over it.
Let Valτ be the set of values of type τ . For a closed term M oftype τ , its effect value |M| is defined as a limit of its “finite approximations” in the free continuous Σ-algebra CT Σ (Valτ ) over Valτ .
We refer readers to [25] for the precise definition, but intuitively aneffect value |M| ∈ CT Σ (Valτ ) can be understood as a Σ-branching(possibly infinite) tree over the set Valτ ∪ {Ω} that is equal to:Vop+

if M ⇒ Vop

if M ⇒i Ni for each i ∈ 1, . . . , ar(op)|N1 | · · · |Nar(op) |

3.

op0

if M ⇓opΩ

if M ⇑|N|

if M → N .

Algebraic Operations on Monads

Our framework, as well as the mGoI framework [16], accommodates
algebraic effects in a uniform way: it exploits their categorical abstraction by monads and algebraic operations [23, 25]. Namely ourframework is parametrized by a monad T on Set, where Set is thecategory of sets and functions.
3.1

MonadsA monad T on Set induces the Kleisli category SetT equipped
with: the finite coproduct structure (+, ∅), the countable coproductstructure inherited from Set (see e.g. [21]), and the premonoidal
structure [27]. In order to accommodate recursion, our framework
requires these structures to satisfy some domain-theoretic properties
stated in Requirement 3.1 below.

Example 3.2. Here are our leading examples of monads that satisfy Requirement 3.1. Note that all the monads T given below areequipped with partiality: it is often obtained by adding 1 = {∗}and induces an ω-cppo structure of each set T X. Hence a Cppoenrichment of the category SetT is given in the pointwise manner.
• The exception monad EX = 1 + E + X for a set E.
• The powerset monad PX = {A ⊆ X}.
• The subdistribution monadP
DX = {d : X → [0, 1] | x∈X d(x) ≤ 1}.
• A global state monad SX = (1 + X × S)S for a set S.
• A writer monad T X = 1 + M × X for a monoid M .
• An I/O monad T A = µX. (1 + O × X + X I + A) for sets
I and O. By regarding sets I and O as ω-cpo’s with discreteorders, for any ω-cppo X, FA X := (1 + O × X + X I + A)
becomes an ω-cppo with the least element ∗ ∈ 1. Hence FA is an
endofunctor on Cppo. The monad sends a set A to the carrierof a final FA -coalgebra in Cppo.
3.2

Algebraic Operations

Following [25, 26] operations in Σ are modeled by algebraic operations on a monad T that serve as interfaces of algebraic effects. We
use one equivalent definition of algebraic operations investigated in[26], with finite arities; here X n denotes a n-fold product of a set
X, for n ∈ N.
Definition 3.3 (algebraic operations on T [26]). Let (×, 1, ⇒) be
the cartesian closed structure of Set and n ∈ N be a natural
number. For a monad T on Set, a family {αA,B : (A ⇒ T B)n →(A ⇒ T B)}A∈Setop ,B∈SetT of Set-arrows is an n-ary algebraic
operation on T if it is natural in A ∈ Setop and B ∈ SetT .
The following examples are algebraic operations on some of themonads listed in Example 3.2. They are used in our framework tomodel operations shown in Example 2.1.

Requirement 3.1. Throughout the paper a monad T on Set isrequired to satisfy the followings.

Example 3.4. Here are algebraic operations on some of the monads
listed in Example 3.2.

• The Kleisli category SetT is Cppo-enriched, i.e.

• For a set E and each element e ∈ E, a 0-ary algebraic operation

every homset SetT (X, Y ) is an ω-cppo with the least element ⊥; andcompositions ◦T of SetT are continuous.
• Compositions ◦T are additionally strict in the restricted form:
for any SetT -arrow f : X →T Y and Set-arrow g : Y → Z it
holds that f ◦T ⊥ = ⊥ and ⊥ ◦T g ∗ = ⊥. Here (−)∗ , the Kleisli
inclusion from Set to SetT , assigns a SetT -arrow A →T B toeach Set-arrow A → B by post-composing the unit of T .
• The finite coproduct structure (+, ∅) of SetT is Cppo-enriched,i.e. cotuplings [−, −]T are continuous.
• The premonoidal structure ⊗ of SetT is continuous and strict:
namely, for any set X, the maps X ⊗ (−) and (−) ⊗ X on
homsets of SetT are continuous and strict.

The first three conditions of this requirement are precisely what
are given in [16, Lemma 4.3] as a sufficient condition for monads
that can be used in the mGoI framework. It is also shown in [16,Lemma 4.3] that these conditions ensures the existence of a trace
operator tr of the monoidal category (SetT , 0, +): the operator
tr is defined exploiting the Cppo-enrichment of SetT . Here we
additionally require the last condition in order to accommodate
recursion. Requirement 3.1 not only supports the development of
a component calculus but also ensures its desired domain-theoretic
properties.
A monad T , as a parameter of our framework, models computational effects in a uniform way as proposed in [23]; we can instantiate it to model various effects.

raise e on the exception monad E is equivalently given by thefamily {A → 1+E+A}A∈Set of constant functions that always
returns e.
• A 2-ary algebraic operation ⊕ on the powerset monad P performs nondeterministic choice. For two functions f, g : A →PB it takes pointwise unions: (f ⊕ g)(a) = f (a) ∪ g(a).
• For any p ∈ [0, 1], a 2-ary algebraic operation ⊕p on the subdistribution monad D performs probabilistic choice. For two functions f, g : A → DB it superposes distributions in a pointwisemanner: (f ⊕p g)(a)(b) = p × f (a)(b) + (1 − p) × g(a)(b).
• Let Val be a finite set and Loc be a set. For their elementsv ∈ Val and l ∈ Loc, a |Val |-ary algebraic operation lookup land a 1-ary algebraic operation update l,v on the global statemonad SX = (1+X ×Val Loc )Val
states.

4.

Loc

perform actions on global

Component Calculus in the mGoI Framework

In this section we recall the component calculus over transducers
that is given in the mGoI framework [16].
Transducers, to which our framework translates terms, are precisely called T -transducers: they are “effectful” extension of (sequential) transducers or Mealy machines.
Definition 4.1 (T -transducers [16, Definition 4.1]). For sets A andB, a T -transducer (X, c, x) from A to B consists of a set X, afunction c : X × A → T (X × B) and an element x ∈ X.

We write (X, c, x) : A _ B when a T transducer (X, c, x) is from A to B. A T transducer (X, c, x) : A _ B can be understoodas an “effectful” transition function c with input
A, output B, a state space X and an initial statex ∈ X. On this intuition we depict it as in Figure 3.
The component calculus over T -transducers
provides some primitive T -transducers and a setof operators on T -transducers.
4.1

e0 hi, ni = n

BcA
Figure 3: A
T -transducer(X, c, x) :A_B

d(i, hj, ni) = hhi, ji, ni

c0 hgi, ni = inlhi, ni0c0 hdi, ni = inrhi, ni

d hhi, ji, ni = (i, hj, ni)
w = !∗N

Another class of underlying functions includes the following
functions:kn : N → N
sum : N + N + N → N + N + N

Primitive T -transducers

and four retractions(dereliction)c̃A : F A + F A ∼= F A : c˜0 A(contraction)w̃A : ∅ C F A : w̃0 A(weakening)(digging)(2)

where a set F X is defined by N × X for each set X. The first three
are in Set (and hence in SetT ) and the last one is in SetT . Letinji `inl
inr
A −→ A + B ←−− B and A −−→
i Ai be injections in Set and!A : ∅ → A be the unique Set-arrow from the initial object ∅ to A.
The retractions in (2) are defined as below.
ẽA := inj0e˜0 A := [idA ]i∈Nd˜A := u × Ac̃A := φ × A

d̃0 A := v × A
c˜0 A := ψ × Aw̃A := !N×A

A∗
w̃0 A := trF
F A,∅ ([idF A , idF A ] )We also use their adaptation as listed below: we take N as A andcompress N × N to N via the bijection u : N × N ∼= N : v in order
to fit the retractions to our use in the translation.
e : N C N : e0(dereliction)
0∼
d:N×N=N:d(digging)c : N + N C N : c0
w :∅CN:w

0(contraction)(weakening)

Their definition can be concretely expressed as below. We write gfor φ ◦ inlN,N , d for φ ◦ inrN,N and h−, −i for u(−, −).2e(n) = h0, nic(inlhi, ni) = hgi, ni

2 g is for left and d is for right, in French. See e.g. [20, 24].

w0 = trNN,∅ ([idN , idN ]∗ )h := (φ + N) ◦ (N + σ) ◦ (ψ + N) ◦ σ◦ (φ + N) ◦ (N + σ) ◦ (ψ + N)

Each SetT -arrow f : A →T B (i.e. function f : A → T B) can belifted to a T -transducer J(f ) := (1, f, ∗) : A _ B, where 1 = {∗}∼=is the terminal object of Set and isomorphisms 1 × A →
A and
∼
=
1 × B → B are omitted. The resulting T -transducer Jf performs
the same computation as the function f without changing its internal
state.
Primitive T -transducers used in our framework are all either inthe form J(f ) : A _ B for some SetT -arrow f : A →T B orin the form J(g ∗ ) : A _ B for some Set-arrow g : A → B.
Here (−)∗ is the Kleisli inclusion from Set to SetT . For notational
simplicity, in depictions of a primitive T -transducer J(f ) we simply
write its underlying function, e.g. we write f for J(f ) and g forJ(g ∗ ) (see e.g. Figure 5). We here give the underlying functions ofour primitive T -transducers.
One class of underlying functions consists of retractions in Set
and SetT , that are pairs of arrows f : X C Y : g such that g ◦ f =idX holds. Namely we use: two chosen bijections in Set
∼N:ψ
∼N:v
(1)
φ:N+N=
u : FN =ẽA : A C F A : e˜0 A
d˜A : F F A ∼= F A : d̃0 Ac(inrhi, ni) = hdi, ni: N+N→N+N∼=
where σ : N + N →N + N is a swapping isomorphism. In thetranslation, kn is used for the constant term n; sum is for thearithmetic operation +; and h serves as a CPS-like construct that“forces” call-by-value evaluation. They concretely act on natural
numbers as below.

sum(inj0 (n)) = inj2 (n)h(inl(gn)) = inl(dgn)sum(inj2 hi, ni) = inj1 hhi, ni, nih(inl(dgn)) = inl(gn)sum(inj1 hhi, ni, mi) = inj0 hi, n + mi
kn hi, mi = hi, nih(inl(ddn)) = inr(n)h(inr(n)) = inl(ddn)

4.2

Operators on T -transducers

The mGoI framework gives the following operators on T -transducers:(a) sequential composition ◦; (b) binary parallel composition ; (c)the countable copy operator F ; (d) the trace (or feedback) operator
Tr; (e) binary application •; and (f) the operator α for each algebraic
operation α on T .
Figure 4 shows depictions of how these operators act on T transducers. Here we only give intuitive descriptions, for the lackof space; the reader is referred to [16, Section 4.2] for their precise
definitions.
C
d
B
c

B
c
A

A

(a) Sequential
Composition ◦
B
C

A

N×C

N×C

c

d

A

(d) TrC
A,B (X, c, x) :A_B(b) Binary Parallel
Composition 

B

c

D
d
C

(e) Binary Application •

c

N×B
N×A

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

B

c1

α
...

A

B

cn
A

A

(f) α{(Xi , ci , xi )}i∈n :A_B

Figure 4: Operators on T -transducers

Sequential Composition ◦ Sequential composition (Y, d, y) ◦(X, c, x) : A _ C of two T -transducers (X, c, x) : A _ B and(Y, d, y) : B _ C has a state space X × Y and an initial statehx, yi. It runs first (X, c, x) and then (Y, d, y) by passing output of
the former to input of the latter.
Binary Parallel Composition  Binary parallel composition(X, c, x)  (Y, d, y) : A + C _ B + D of two T -transducers(X, c, x) : A _ B and (Y, d, y) : C _ D has also a state space
X × Y and an initial state hx, yi. It runs either (X, c, x) or (Y, d, y)according to input: namely it runs (X, c, x) if input is in A and(Y, d, y) if in C.

Countable Copy Operator F A T -transducer F (X, c, x) : N ×
A _ N × B can be understood as countably many copies of a T transducer (X, c, x) : A _ B. Given input hi, ai ∈ N × A, it runs
the i-th copy of (X, c, x) with input a; and it outputs hi, bi ∈ N × B
if the i-th copy of (X, c, x) outputs b.
Trace Operator Tr Trace TrC
A,B (X, c, x) : A → B of a T transducer (X, c, x) : A + C _ B + C has the same state space andinitial state as (X, c, x). Given input in A, it runs (X, c, x) repeatedly until output in B is generated, by passing output in C to input.
Its “effectful” transition function is defined using the trace operator
tr of the category SetT .
Binary Application • Using these four operators above, binary
application (X, c, x) • (Y, d, y) : A _ B of two T -transducers(X, c, x) : A + N × C _ B + N × C and (Y, d, y) : C _ C
is defined to be
N×C((J(id∗B )  F (Y, d, y)) ◦ (X, c, x)) .
TrA,BBinary application • is an adaptation of the operator • defined in[16]. It is used to translate function application.
Lifted Algebraic Operations α Finally for an n-ary algebraic operation α on T and a family {(Xi , ci , xi ) : A _ B}i∈n of T transducers, a T -transducer α{(Xi , ci , xi )}i∈n : A _ B has a state
space 1 + X1 + · · · + Xn and an initial state ∗ ∈ 1. Here the set n
is the n-fold coproduct of 1.
The operator α introduces a fresh initial state ∗ ∈ 1 and effectfultransitions from the state ∗ to each states in {xi }i∈n that are initialstates of T -transducers {(Xi , ci , xi )}i∈n , respectively. After making an effectful transition from its initial state ∗ to a state xi , theT -transducer α{(Xi , ci , xi )}i∈n sticks to its choice and behaves inthe same way as (Xi , ci , xi ). In other words a T -transducer exploits
its internal states to memorize the result of its effectful transitions.
4.3

The “Category” of Transducers

We have introduced the component calculus over T -transducers thatis used in the original mGoI framework; one natural question iswhat axioms it satisfies. An answer given in [16], following theprevious observations in [? ], is a categorical one via the behavioral
equivalence.
Definition 4.2 (homomorphism between T -transducers [16, Definition 5.1]). For two T -transducers (X, c, x), (Y, d, y) : A _ B, afunction h : X → Y is a homomorphism from (X, c, x) to (Y, d, y)if (h∗ ⊗ B) ◦T c = d ◦T (h∗ ⊗ A) holds in SetT (equivalently
T (h × B) ◦ c = d ◦ (h × A) holds in Set) and h(x) = y holds.

arrows: resumptions, that are equivalence classes of T transducers modulo the behavioral equivalence, with identities given by J(id∗ ) and compositions by ◦is indeed a category and has a traced symmetric monoidal structure (, ∅, Tr).
• The operator F , defined for sets by F X := N × X, is a traced

symmetric monoidal functor on Res(T ). This fact enables us to
identify a T -transducer F (X, c, x) : F (A + C) _ F (B + D)with F (X, c, x) : F A + F C _ F B + F D, as done e.g. in
Figure 5 & 7.

• Moreover the data (Res(T ), F, N), together with primitive T -transducers lifted from the retractions in (1) and (2), induces a
GoI situation [2]. This means the primitive T -transducers liftedfrom the left-hand side functions of retractions in (2) satisfies
monoidal naturality.

• [16, Theorem 5.3] Operators α are natural and Tr distributes

over them up to the behavioral equivalence.

Figures in this section can be therefore seen as string diagrams in
Res(T ).
It is also possible to think of a “category” Trans(T ) of T transducers (without quotienting modulo the behavioral equivalence); however this is more like a bicategory since axioms like
associativity of ◦ are satisfied only up to isomorphisms.

5.

Definition 4.3 (behavioral equivalence [16, Definition 5.2]). Two
T -transducers (X, c, x), (Y, d, y) : A _ B are behavioral equivalent if there exists a T -transducer (Z, e, z) : A _ B and two
homomorphisms, from (X, c, x) to (Z, e, z) and from (Y, d, y) to(Z, e, z).
The behavioral equivalence enables us to abstract away fromstate spaces of T -transducers. For example two T -transducers(X, c, x) : A _ B and J(id∗B ) ◦ (X, c, x) : A _ B have different
state spaces (namely X and X × 1) but their transition functions are
identified after composing an obvious isomorphism X ∼= X × 1.
By choosing the isomorphism as a homomorphism between the two
T -transducers we can identify them via the behavioral equivalence.
All the operators ◦, , Tr and F as well as α respect the
behavioral equivalence. The axioms satisfied by these operators canbe described categorically; what follows is a summary of the facts
shown in [16].
• The category Res(T ), defined by

objects: sets

Extending the Component Calculus

In the previous section we have recalled the component calculus
over T -transducers from the mGoI framework; now in this section it
is extended so that our framework can accommodate recursion.
In the mGoI framework, binary application • of T -transducers isused in translating function application to T -transducers. Our goal
here is to introduce a new operator that can be used in translating recursion as infinitely many self-applications of some function. Hencethe new operator is designed to give infinitely many “self-binaryapplications” of a given T -transducer.
We extend the component calculus in three steps by introducing
first countable parallel composition n∈N , second the Girard style
fixed point operator FixG and finally the Mackie style fixed point
operator FixM . Figure 5 shows depictions of how these new operators act on T -transducers.
B1
c1

B2
...
c2

A1

A2

(a) Countable
n∈N

ParallelA

A

Composition

N×A

e˜0
N×A
c˜0
N×A

N×A

N×A

c

A

c

c

c

...

N×A

N×A

(b) FixG (X, c, x) : A _ A

c̃

c

d˜
N2 × A

N2 × A
d˜0

ẽ

A

N×A

(c) FixM (X, c, x) :A_A

Figure 5: New Operators on T -transducers

5.1

Countable Parallel Composition n∈N

As a first step we extend binary parallel composition  to the countable one n∈N ; this is straightforward, and possible because Set
has countable coproducts and SetT inherits
par` them. Countable`allel composition n∈N {(Xn , cn , xn )} :n∈N An _n∈N Bnof a family Q{(Xn , cn , xn ) : An _ Bn }n∈N of T -transducers has astate space n∈N Xn , whose element is an infinite list hy1 , y2 , . . .i,and has an initial state hx1 , x2 , . . .i.
Countable parallel composition n∈N can be seen as a generalization of the countable copy operator F . Namely for any T transducer (X, c, x) : A _ B, a T -transducer F (X, c, x) can be
identified with a T -transducer n∈N {(X, c, x)}. Here the former’s
input/output N × C is identified with a N-fold countable coproductof C and the former’s state space X N is with a N-fold countableproduct of X.
5.2

Girard Style Fixed Point Operator FixG

On top of the component calculus, i.e. operators on T -transducers
described so far, we define the Girard style fixed point operator FixG
on T -transducers.
Definition 5.1 (Girard style fixed point operator FixG ). For a T transducer (X, c, x) : A + N × A _ A + N × A, a T -transducer
FixG (X, c, x) : A _ A is defined byn∗FixG (X, c, x) := TrN
A,A (n∈N {F (X, c, x)}n∈N ◦ J(swap ))where N is the set defined to be(N × A + N × A) + (N × N × A + N × N × A)
+ (N × N × N × A + N × N × N × A)
+ ···`and swap is the function defined to be idA + n∈N σ : N → N∼=
using swapping isomorphisms {σ : R + S →S + R}R,S∈Set in
Set.
The following proposition shows that the operator FixG indeed
gives what serves as infinitely many “self-binary-applications” of atransducer, as we intended. Namely the operator FixG gives a fixed
point with respect to binary application •: that is why we call FixGa “fixed point” operator.
Proposition 5.2. For any T -transducer (X, c, x) : A + N × A _A + N × A, a T -transducer FixG (X, c, x) : A _ A satisfies the
behavioral equivalence(X, c, x) • FixG (X, c, x) ' FixG (X, c, x) .
Proof. The behavioral equivalence follows from the equational
properties (up to behavioral equivalence) listed in Section 4.3, ofthe component calculus. Especially we take advantage of trace axioms [14, 18] satisfied by the trace operator Tr.

• Additionally a T -transducer (X, ⊥, x) : A _ B for each least

element ⊥ ∈ SetT (X × A, X × B) gives a minimal element.

This partial order E is quite “raw”: two T -transducers can be ordered only if they have the same state spaces and the same initialstates. The order E forces us to remain aware of state spaces, while
the behavioral equivalence ' (see Definition 4.3) enables us to abstract away state spaces and to perform equational reasoning up to
behavioral equivalence. To our knowledge there seems no way torelate E to the behavioral equivalence '. In spite of this inconvenience, the order E has enough power to support the proof of adequacy.
The conditions stated in Requirement 3.1 imply the following
domain-theoretic properties of our component calculus with respect
to the order E.
Lemma 5.3. Operators of the component calculus satisfy the following, up to (not behavioral equivalence but) the exact equality =.
sequential composition ◦binary parallel composition 
countable copy operator F
trace operator Tr
binary application •lifted algebraic operation αcountable parallel composition n∈N
Girard style fixed point operator FixG

continuity
X
X
X
X
X
X
X
X

strictness
X?1
X?2
X
X
X?3
×
X?2
X

?1 In the restricted form: (Y, d, y)◦(X, ⊥, x) = (X ×Y, ⊥, hx, yi)
and (X, ⊥, x) ◦ (Z, e∗ , z) = (Z × X, ⊥, hz, xi), for any T transducers (X, c, x) and (Y, d, y), and for any T -transducer(Z, e∗ , z) whose transition function is lifted from a Set-arrowe.
?2 If all arguments have ⊥ as transition functions.
?3 In the restricted form: (X, ⊥, x) • (Y, d, y) = (Z, ⊥, z) for any
T -transducer (Y, d, y) and any T -transducer (X, ⊥, x) whosetransition function is ⊥, where Z and z is respectively the state
space and the initial state of (X, ⊥, x) • (Y, d, y).
Proof. The properties shown in the table are consequences of theconditions stated in Requirement 3.1. Note that the conditions imply
the facts in the category SetT listed below. Once we observe them
the properties of the component calculus can be easily confirmed bydefinitions of operators.
• Continuity of countable cotuplings [{−}n∈N ]T is inherited bythat of (finite) cotuplings [−, −]T .

5.3

Induced ω-cpo Structure on Transducers

The operator FixG gives not only a fixed point with respect tobinary application • but also a least fixed point with respect to anω-cpo structure on T -transducers, that is induced by the Cppoenrichment of the category SetT .
As guaranteed by Requirement 3.1, each homset of SetT hasan ω-cppo structure (SetT (A, B), v, ⊥). This structure induces anω-cpo structure (Trans(T )(A, B), E) in the following way, where
Trans(T )(A, B) denotes a set of T -transducers from A to B.
• A relation E on T -transducers, defined bydef.

(X, c, x) E (Y, d, y) ⇐⇒ X = Y ∧ x = y ∧ c v dfor two T -transducers (X, c, x), (Y, d, y) : A _ B, is a partial
order.
• For an ω-chain (X, c1 , x) E (X, c2 , x) E · · · of T -transducers

from A to B, its supremum supi∈ω (X, ci , x) : A _ B is givenby (X, supi∈ω ci , x).

• Both finite and countable cotuplings are strict in the sense of[⊥, ⊥]T = ⊥ and [{⊥}n∈N ]T = ⊥. It is because of therestricted strictness of composition ◦T .
• The trace operator tr is continuous and strict by its definition
that takes advantage of Cppo-enrichment of SetT .
• Continuity of algebraic operations on T follows from continuityof composition ◦T and cotuplings [−, −]T .

The last fact can be confirmed using the bijective correspondence of an n-ary algebraic operation α on T and a SetT -arrow(called generic effects) β : 1 →T n, studied in [26]. Namely
for a family {fi : A →T B}i∈n of SetT -arrows, a SetT -arrowα{fi }i∈N : A →T B can be equivalently given byβ⊗A∼[{fi }i∈n ]T=
A −−−→T n × A →−−−−−−→T B
T A + ··· + A −using the corresponding generic effect β.
Based on these properties the operator FixG is characterized asa supremum (or a least fixed point) of its finite approximants.

A
⊥
A

A

N×A

⊥

⊥

...

c

E

N×A

A

N×A

A

⊥

...

⊥

c

E

N×A

N×A

A

c

⊥

...

E ···

N×A

(i)

Figure 6: The ω-chain of Finite Approximants FixG (X, c, x)(i)Definition 5.4 (finite approximant FixG ). For a T -transducer(X, c, x) : A + N × A _ A + N × A and i ∈ ω, a T -transducer(i)FixG (X, c, x) : A _ A is defined by
(i)

n (i)
∗
FixG (X, c, x) := TrN
A,A (n∈N {F (cn )}n∈N ◦ J(swap ))(i)where N and swap are defined as in Definition 5.1; and cn : A +N × A _ A + N × A is the T -transducer defined by (X, c, x) if
n < i and (X, ⊥, x) otherwise, for each i ∈ ω and n ∈ N.
Proposition 5.5. For any T -transducer (X, c, x) : A + N × A _(i)
A+N×A, a family {FixG (X, c, x) : A _ A}i∈ω of T -transducers
forms an ω-chain
(0)

(1)

FixG (X, c, x) E FixG (X, c, x) E · · ·as depicted in Figure 6. Moreover a T -transducer FixG (X, c, x) : A _A satisfies the behavioral equivalence(i)FixG (X, c, x) ' sup(FixG (X, c, x)) .
i∈ω

5.4

Mackie Style Fixed Point Operator FixM

So far, in this section, the Girard style fixed point operator FixG has
been introduced with the intention of using it in translating recursion. As shown in Proposition 5.2 & 5.5, the operator FixG enjoys
properties that are essential in the proof of adequacy; especially it
is characterized as a supremum of its finite approximants. Therefore
by the operator FixG recursion can be translated as a supremum offinite approximants. This approach to interpret recursion in GoI ismuch like the one by Girard [12]; that is why we call FixG “Girard
style” fixed point operator.
On the other hand there exists another approach to interpret
recursion in GoI: that is the one by Mackie [22] where recursion
is interpreted by a loop and a single “box” in a proof net. In our
setting this approach corresponds to interpreting recursion using an
operator that is defined by the single use of the trace operator Tr andthe single use of countable copy operator F , in particular without
any use of countable parallel composition n∈N . The last operator
FixM on T -transducers, introduced in our framework, is defined insuch a way: therefore we call the operator “Mackie style” fixed point
operator. See Figure 5 for its depiction.
Definition 5.6 (Mackie style fixed point operator FixM ). For a T transducer (X, c, x) : A + N × A _ A + N × A, a T -transducer
FixM (X, c, x) : A _ A is defined by
FixM (X, c, x) :=
∗
˜∗
˜0 ∗
˜0 ∗
TrA+A
A,A ((J(e )  J(idA+A )) ◦ (J(c )  J(d )) ◦ F (X, c, x)∗◦ (J(c̃∗ )  J(d̃0 )) ◦ (J(ẽ∗ )  J(σ ∗ )))∼=where σ is a swapping isomorphism A + A →A + A in Set.

The next theorem shows that the Girard and Mackie style fixed
point operators actually coincide.

Theorem 5.7 (coincidence of two styles of fixed point operator).
The following behavioral equivalence
FixG (X, c, x) ' FixM (X, c, x)
holds for any T -transducer (X, c, x) : A + N × A _ A + N × A.
Proof. The proof exploits: 1) naturality of the trace operator Tr; and2) monoidal naturality (in A) of the retractions/isomorphismsẽA : A C F A : e˜0 A , d˜A : F F A ∼= F A : d̃0 A
0∼˜c̃A : F A + F A = F A : c A .

andThe latter is exploited e.g. in deriving the following behavioral
equivalences of transducers.
N×A

c˜0
N×A

N×A
N×A

c̃

c

N×A
c˜0
N×A

c̃

N×A

N×A

'

N×A

c

c

N×A

N×A

N×N×N
d˜0
N×N

c

N×A

'

N×N
d˜
N×N×N

N×N×N

c
N×N×N

We use the above behavioral equivalences for the purpose oftranslating a bunch of (X, c, x)’s in FixG (X, c, x) into a single
F (X, c, x) in FixM (X, c, x).

6.

Translation to Transducers and Its Adequacy

Finally in this section, on top of our extended component calculus,
we define a translation of terms of LΣ to transducers. To achieveadequacy of the translation we exploit the properties of primitives
and operators of our component calculus.
6.1

Translation to Transducers

In order to translate a term of our target language LΣ , the first stepis to choose an appropriate monad T that satisfies Requirement 3.1
and supports the algebraic signature Σ.
Definition 6.1. We say a monad T on Set supports an algebraic
signature Σ if, for each operation op ∈ Σ, it has an ar(op)-ary
algebraic operation op on it.
For the algebraic signatures listed in Example 2.1, we use the monads listed in Example 3.2. Operations in these algebraic signatures
can be modeled by algebraic operations listed in Example 3.4.
Example 6.2. Here we show how the algebraic signatures listed in
Example 2.1 are supported by the monads listed in Example 3.2.
• For a set E, the exception monad E = 1 + E + (−) supports

Σexcept = {raisee | e ∈ E}. For each operation raisee ∈Σexcept we can take a 0-ary algebraic operation raise e on E.
• The powerset monad P supports Σndet where the operation t ismodeled by the 2-ary algebraic operation ⊕ on P.
• Similarly the subdistribution monad D supports Σprob where
each operation tp is modeled by the 2-ary algebraic operation⊕p on D.

• For a set Loc and a finite set Val , the state monad SX = (1 +Loc Val Loc(−) × Val )supports Σglstate . Each operation lookupl
is modeled by the |Val |-ary algebraic operation lookup l andeach operation updatel,v is by the 1-ary algebraic operation
update l,v on S.

Let T be a monad that supports Σ. We now give a translation L−Mof terms of LΣ to T -transducers. It is given using depictions such as
Figure 3–5. Moreover it is an extension of the translation given by
the mGoI framework [16].
Definition 6.3 (translation L−M). For each type judgment Γ ` M : τ
where Γ = x1 : τ1 , . . . xm : τm , we inductively define a T transducermNLΓ ` M : τ M =

N

N

...

N

LΓ ` M : τ M

N

...

:
N

m
a
i=0

N_

m
a

N

i=0

m

as in Figure 7, where labels of edges (either N or N × N) are omitted
for visibility.
In translation of recursion depicted in Figure 7 we implicitly use the
Mackie style fixed point operator FixM . Due to Theorem 5.7 wecan also use the Girard style fixed point operator FixG as depicted
in Figure 8.
The Categorical Model Much like the translation of the original
mGoI framework in [16], the translation L−M of our framework
is backed up by a categorical model (whose definition we do notgive here). Our translation L−M can be extracted by a categoricalinterpretation on the model PerΦ0 that is the Kleisli category of
the strong monad Φ0 on the cartesian closed category Per. The
model is a modification of the one used in the mGoI framework: thecategory Per is the same; and the monad Φ0 is modified to reflectthe ω-cpo structure of T -transducers. Its construction is done bycombination of categorical GoI [2] and realizability techniques, as in[16]. Proposition 5.2 & 5.5 ensures that the Girard style fixed point
operator FixG indeed yields a (categorical) fixed point operator in
the model PerΦ0 .
6.2

Adequacy of Translation L−M

Let T be a monad that supports the algebraic signature Σ. The
statement of adequacy connects operational semantics reviewed in
Section 2.2 and the translation L−M extracted from denotationalsemantics. In order to give the statement we start with “collecting”
the execution results of terms of LΣ via both T -transducers andeffect values. In this section we restrict ourselves to closed termsof base type nat: we simply say a “term” to indicate such a term,
and write LMM for L` M : natM.
For a term M, we can observe that running the T -transducer
LMM : N _ N with input in the form ddhi, mi yields output in theform ddhi, ni, where i and m are arbitrary natural numbers andn corresponds to an evaluation result of the term (see Section 4.1
for the notation). Therefore we take the set T N as the collection ofevaluation results, fixing a retraction enc : Valnat C N : dec suchthat
enc(n) = ddh0, ni

dec(ddhi, ni) = n .

For a term M, let (X, c, x) : N _ N be a T -transducer LMM. We
collect execution results from the T -transducer by taking
0
LMM† := ((πX,N)∗ ◦T c)(x, enc(m)) ∈ T N

0where πX,N
: X × N → N is the second projection and m denotes afixed natural number. This procedure (−)† runs a T -transducer andgathers its output. Additionally (−)† ignores the resulting internal
states that record the branching history of program execution, orthe history of effect occurrences during program execution. Indeed
we have the equality (X, c, x)† = (Y, d, y)† for two behavioral
equivalent T -transducers (X, c, x) ' (Y, d, y) : A _ B.
Next we define interpretation of effect values. Recall that effectvalues for terms are formulated as elements of the free continuous
Σ-algebra CT Σ (Valnat ) over the set Valnat . On the other hand,for each operation op ∈ Σ, the monad T has an ar(op)-ary algebraic operation op on it. This means that the set T N, which isisomorphic to SetT (1, N), is a continuous Σ-algebra. Therefore wecan lift the function enc∗ : Valnat → T N to a unique morphism
J−K : CT Σ (Valnat ) → T N that is a strict continuous function preserving the operations specified by Σ. When the monad T is equal
to the powerset monad P, this interpretation corresponds to forgetting branching structures of effect values (i.e. branching structuresof program execution): for example two effect values (1 t 2) t 3 and1 t (2 t 3) are identified as a set {enc(1), enc(2), enc(3)} ⊆ PN
where t ∈ Σndet is the nondeterministic choice operation.
Now we can state adequacy of the translation L−M.

Theorem 6.4 (adequacy). Any closed term M of base type natsatisfies J|M|K = LMM† .

6.3

Proof of Adequacy

To prove Theorem 6.4 we introduce a language LΣ following [25].
In this language all occurrences of recursion are restricted to finite
depth. Namely LΣ is made from the target language LΣ , by replacing the term constructor rec with rec(i) for each i ∈ N and byadding a constant Ωτ for each type τ . In the definition of the small
step operational semantics, transitions
rec(i+1) (f : σ → τ, x : σ). M→ (λx : σ. M)[rec(i) (f : σ → τ, x : σ). M/f]rec(0) (f : σ → τ, x : σ). M → λx : σ. Ωτreplace the one for rec shown in Figure 2. This excludes any infinite
sequence M → M0 → · · · of pure transitions, hence M ⇑ no longer
appears in the medium step operational semantics. Effect values aredefined in the same way as LΣ , except that we define |E[Ωτ ]| to be Ω.
On the other hand the translation LΓ ` rec(i) (f : σ → τ, x : σ). MM(i)
is given like Figure 8 where we use the i-th approximant FixG of
the Girard style fixed point operator instead of FixG .
Theorem 6.4 is a consequence of Lemma 6.5 below that states
adequacy of the translation L−M with respect to the language LΣ .
The proof goes as follows. For a term M of LΣ and i ∈ N, let M(i) bea term of LΣ obtained from M by replacing all occurrences of recwith rec(i) . For effect values we can prove
J|M|K = supJ|M(i) |Ki∈ωin T N as in [25]. On the other hand Proposition 5.5 ensures the
behavioral equivalence
LMM ' supLM(i) M .
i∈ω

Therefore it holds that
J|M|K = supJ|M(i) |K = sup(LM(i) M† ) = (supLM(i) M)† = LMM† .
i∈ω

i∈ω

i∈ω

The third equality is easily confirmed by the definition of (−)† andcontinuity of composition ◦T of SetT .

...

LΓ ` ∗ : unitM =

h

w

w0

w0

...

i−1

...

LΓ ` xi : τi M =

w
h

φ

...

w ... ww

w0 . . . w0

w0

...

φ

ψ

w

LΓ ` fst(M) : τ M =

w0

...

...

w

LΓ ` M : τ × σM

h
w0

...

φ

ψ
ψ

i−1

...
u

d

φ

LΓ ` λx : σ. M : σ → τ M =

φ

d

φ

ψ

LΓ ` snd(M) : σM =

...

...

w

LΓ ` M : τ × σMψLΓ, x : σ ` M : τ M

h

...
c

d0

v

...

c

d0

φ
ψ

LΓ ` hM, Ni : τ × σM =...

φLΓ ` M : τ M
...

φ

φ

ψ

...

...

ψ

LΓ ` N : σM

h
φ

...

φ

ψ
ψ

e
ψ

ψ

...

ψ

h
w0

...

φ

c

c

c0

c0
...

ψ
...

LΓ ` M N : τ M =LΓ ` M : σ → τ M

LΓ ` N : σM

...

φ

φ

LΓ ` inlτ,σ (M) : τ + σM =

φ
e0

c0

c0

ψ

φ

w

ψ

LΓ ` M : σM

h
w0

φ
ψ

ψ
ψ

...

φ

LΓ ` inrτ,σ (M) : τ + σM =

...
d

φ

ψ

c0
d

φ

LΓ ` M : τ M

h
w0

φ

...

φ

w

ψ

ψ

ψ
ψ

...

LΓ ` case(M, x. N, x0 . N0 ) : σM =
...
φ

...

ψ

φ

...

d

LΓ, f : σ → τ, x : σ ` M : τ M

h

φ

...

...

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

φ

ψ

c

c

ψ
ψ

c

φ

c

ψ

v

d0

c

d0

...

d0

ψ

...

φ

LΓ ` M : τ + τ 0 M

φ

φ

...

...

...

LΓ, x0 : τ 0 ` N0 : σMLΓ, x : τ ` N : σM
...

...

ψ

ψ

φ
ψ

φ

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

c0

ψ

op+
. . . LΓ ` Mar(op) : τ M
...

c0
...

...

... ...

c0φ... ...
...

c0

...

LΓ ` n : natM =

h

w

w

w0

w0

kn
...

...
0

LΓ ` op () : τ M =

w

...

w

op0
w0

...

w0

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

w

w

w0

w0

sum

h

...

(if x 6≡ y)...

cLΓ, x : nat ` x + x : natM =Figure 7: Inductive Definition of the Translation L−M

h

w

w

w0

w0

sum
c0

...

N
φ
N
φ

LΓ ` rec(f : σ → τ, x : σ). M : σ → τ M =N

φw∪ {( d
u

d ...

w0

ψ
N

ψ
N

φ

FixG

h

c ...

c

LΓ, f : σ → τ, x : σ ` M : τ M
ψc0 . . . c0v

d0 . . . d0v

d0 . . . d0...

ud ... d, inrτ,σ (N)) | (d, N) ∈ Rσ } .

ψ

N

d

For a type environment Γ = x1 : τ1 , . . . , xm : τm , a binary relationRΓ is defined by Rτ1 × · · · × Rτm .
For a type judgment Γ ` M : τ and T -transducers c1 , . . . , cm : N _N, let LMM[~c] : N _ N be a T -transducer defined by
LMM[~c] := (· · · ((LMM •0 c1 ) •0 c2 ) · · · •0 cm ) .

We prove by induction on M that it satisfies(LMM[~c], M[~V/Γ]) ∈ Rτ
Figure 8: Translation of Recursion by FixG

Lemma 6.5 (adequacy with respect to LΣ ). For the language LΣ ,any closed term M of base type nat satisfies J|M|K = LMM† .
Proof. The proof utilizes a logical relation between T -transducers
and closed terms. Let Termτ be the set of closed terms of typeτ . For a binary relation R ⊆ Trans(T )(N, N) × Valτ , a binary
relation R ⊆ Trans(T )(N, N) × Termτ is defined to be the least
binary relation such thatfor any (~c, ~V) ∈ RΓ . We note that if (x, M) ∈ Rnat , then J|M|K = x† .
In fact, by the definition of Rnat , it is easy to see that the relation
Rnat is a subset of {(x, M) | J|M|K = x† }. The statement ofLemma 6.5 is a consequence of (3). In the proof of (3), propertiesof the component calculus summarized in Section 4.3 are exploited.
Here, we only give outline of a proof for the case when M is equal torec(i+1) (f : τ → σ, x : τ ). N. We define a transducer di to be(i)FixG ((J(φ∗ )  J(u∗ )) ◦ LN[~c]M ◦ (J(ψ ∗ )  J(v ∗ ))).

We first prove((J(ψ ∗ ) ◦ di+1 ◦ J(φ∗ )) • c0 ,(λx : τ. N[rec(i) (f : τ → σ, x : τ ). N/f])[~V/Γ] U) ∈ Rσ

• (d, M) ∈ R if (c, M) ∈ R and c ' d• (J(h∗ ) •0 c, V) ∈ R for any (c, V) ∈ R, where h is fromfor any (c , U) ∈ Rτ . Since Rτ →σ is closed under behavioral
equivalence and reductions, it is enough to check

Section 4.1(LNM[~c, di , c0 ],opieach i = 1, . . . , ar(op)• (op{}, M) ∈ R if M ↓op• (J(⊥), E[Ωτ ]) ∈ R for any type τ .

Note that a binary relation R is closed under behavioral equivalence.
The operator •0 in the above is linear binary application on T transducers defined by(N[rec(i) (f : τ → σ, x : τ ). N/f])[~V, U/Γ, x]) ∈ Rτfor any (c0 , U) ∈ Rτ . We can prove this by induction on i. Now, by
the definition of Rτ →σ and (4), it follows that
(J(ψ ∗ ) ◦ di+1 ◦ J(φ∗ ),(λx : τ. N[rec(i) (f : τ → σ, x : τ ). N/f])[~V/Γ])is in Rτ →σ , and therefore,(J(h∗ ) •0 (J(ψ ∗ ) ◦ di+1 ◦ J(φ∗ )),∗(X, c, x) •0 (Y, d, y) := TrC
A,B ((J(idB )  (Y, d, y)) ◦ (X, c, x))

for two T -transducers (X, c, x) : A+C _ B+C and (Y, d, y) : C _C. It is a “linear” version of binary application • (from Section 4.2)
where the countable copy operator F is excluded.
For each type τ a binary relation Rτ ⊆ Trans(T )(N, N)×Valτ
is inductively defined by
Runit = {(J(id∗N ), ∗)}Rnat = {(J(k∗n ), n) | n ∈ N}
Rσ→τ = {(J(ψ ∗ ) ◦ r ◦ J(φ∗ ), V)| ∀(d, U) ∈ Rσ . (r • d, V U) ∈ Rτ }Rτ ×σ = {(J(φ∗ ) ◦ (c  d) ◦ J(ψ ∗ ), hV, Ui)| (c, V) ∈ Rτ , (d, U) ∈ Rσ }
N
φ
N
φ
N

φ
w

Rτ +σ = {( c

w0
ψ

N
ψ
N

ψ
N

, inlτ,σ (M)) | (c, M) ∈ Rτ }(4)0

• (c, M) ∈ R if M → N and (c, N) ∈ R• (op{c1 , . . . , car(op) }, M) ∈ R if M → Ni and (ci , Ni ) ∈ R for(3)(rec(i+1) (f : τ → σ, x : τ ). N)[~V/Γ]) ∈ Rτ →σ .
Since the left component is behaviorally equivalent to LMM[~c],(Lrec(i+1) (f : τ → σ, x : τ ). MM[~c],(rec(i+1) (f : τ → σ, x : τ ). N)[~V/Γ])is in Rτ →σ .

7.

Executing Transducers

In this section we illustrate execution of transducers using the following example termP ≡ (rec(flipLoop, x). Q) 0 : nat
where Q ≡ x t0.4 (flipLoop (x + 1)).
The term P is a closed term of the language LΣprob , where Σprob
is the algebraic signature for probabilistic choice and supportedby the subdistribution monad D (see Example 6.2). This term P
intuitively flips an unfair coin repeatedly until we observe head,counting how many tails we observe. Indeed the effect value |P|can be seen as the infinite binary tree shown in Figure 9 and its
t0.4
t0.4

0

1

t0.4

1
2

..

.

Figure 9: The Effect Value |P|interpretation J|P|K ∈ DN is equal to the distribution over N suchthat J|P|K(enc(n)) = 0.4 × 0.6n for each n ∈ N.
As a consequence of Theorem 6.4 we can say that the Dtransducer LPM : N _ N, depicted in Figure 10, outputs enc(n)with probability 0.4 × 0.6n for each n ∈ N. The execution of LPM
Exit
ψ
c0

φ

u

h
ψ

e

d
ψ

φ

LPM =

LQM

v

L0M
φ
d0

c

e0
ψ

φ
Enter

where LQM =LxM

an electronic edition), and enters a copy of LQM as many times as thesubterm flipLoop is recursively called (i.e. the coin results in tail).
Each copy of the transducer LQM has the state space that is isomorphic to the set {∗, L, R}; the transition diagram is given by

t0.4

LflipLoop (x + 1)M

Figure 10: The D-transducer LPM : N _ N

can be visualized using a token that moves around the depiction
along edges, updating the data (a natural number) carried by thetoken: it enters from the edge labeled with “Enter” carring the dataenc(m), where m is a fixed natural number, and exits along the edge
labeled with “Exit” with data enc(n) and probability 0.4 × 0.6n foreach n ∈ N.
The way in which the token travels around captures dynamics
of the evaluation of the term P in some sense. For example we
can observe that the token enters a copy of the “subtransducer”
LQM as many times as the coin is flipped (i.e. the recursive function
rec(flipLoop, x). Q is called). Note that the transducer LQM is
within the dashed box in Figure 10 and hence “copied” by theoperator F (see Section 4.2). Each copy has an index given by anatural number and, in fact, the token enters a different copy of LQM
for each time: namely it inters the g0-th copy for the first time, thedhg0, g0i-th copy for the second, the dhdhg0, g0i, g0i-th copy forthe third and so on. In this course, the token goes along the pathindicated by the bold red arrows in Figure 10 (colors are available in

;Lo

0.4



∗

0.6

/Rd

1

where labels denote probabilities. The copies of LQM indeed record
the history of probabilistic choices using their internal states: forexample if the coin results in tail twice and in head at the third time(i.e. the term P is evaluated to 2), internal states of the copies resultin as below.
indexinternal stateg0
Rdhg0, g0i
R
dhdhg0, g0i, g0i
L∗othersReaders can see how exactly the token moves around using ourtool TtT 3 —short for “Terms to Transducers.” The tool automaticallytranslates a given term of the language LΣprob and visualize execution of the resulting transducer by showing how a token moves
around and updates its data.

8.

Concluding Remark

In this paper we established a framework that gives GoI semantics
for effectful programming language. Our framework accommodates
various algebraic effects in a uniform way by employing categoricalformalization of GoI and algebraic effects. This generality is inherited from the framework in our previous work; what is new in ourcurrent work is to accommodate recursion. Notably we gave two
ways to interpret recursion—by Girard style and by Mackie style—and they were proved to be coincide. Additionally adequacy of ourinterpretation was proved. Our framework inherits another featurefrom the mGoI framework: that is, GoI interpretation of programs
is given as transducers. In particular we gave the translation from
effectful terms to transducers by means of a component calculus,
even for recursion, with our prospect of developing a compilation
technique for effectful programs and implementing them directly tohardware.
Let us give a remark on two styles of fixed point operator ontransducers. In extracting a compilation technique from our framework and implementing it, one difficulty would arise from the useof countable copy operator F and countable parallel composition
n∈N of the component calculus. The reason is that they both can
inflate state spaces of transducers to infinite ones. From this point ofview we would like to say that the Mackie style fixed point operator is a little more acceptable than the Girard style one, because theformer includes only one occurrence of F while the latter includes
one occurrence of n∈N and many occurrences of F . Therefore,
although the Girard style fixed point operator exhibits convenientdomain-theoretic properties, we would prefer the Mackie style fixed
point operator in implementing our framework. That is why we used
the Mackie style fixed point operator in the translation (Figure 7) ofrecursion.

Acknowledgments
The authors are supported by the JSPS-INRIA Bilateral Joint Research Project “CRECOGI,” and by Grant-in-Aid No. 15K11984,
JSPS. K.M. and I.H. are supported by Grants-in-Aid No. 24680001& 15KT0012, JSPS; N.H. is supported by Grant-in-Aid No. 26730004,
JSPS.
3 http://koko-m.github.io/TtT/

References[1] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF.
Information and Computation, 163(2):409–470, 2000.
[2] S. Abramsky, E. Haghverdi, and P. J. Scott. Geometry of Interaction
and linear combinatory algebras. Math. Struct. in Comp. Sci., 12(5):625–665, 2002.
[3] U. Dal Lago and U. Schöpp. Type inference for sublinear spacefunctional programming. In Programming Languages and Systems,
volume 6461 of Lecture Notes in Computer Science, pages 376–391.
Springer Berlin Heidelberg, 2010.
[4] V. Danos and L. Regnier. Local and asynchronous beta-reduction (ananalysis of girard’s execution formula). In Logic in Computer Science,
1993. LICS ’93., Proceedings of Eighth Annual IEEE Symposium on,
pages 296–306, 1993.
[5] J. Egger, R. E. Møgelberg, and A. Simpson. Enriching an effectcalculus with linear types. In E. Grädel and R. Kahle, editors, Computer
Science Logic, volume 5771 of Lecture Notes in Computer Science,
pages 240–254. Springer Berlin Heidelberg, 2009.
[6] M. Fernández and I. Mackie. Call-by-value λ-graph rewriting without
rewriting. In A. Corradini, H. Ehrig, H.-J. Kreowski, and G. Rozenberg, editors, Graph Transformation, volume 2505 of Lecture Notes in
Computer Science, pages 75–89. Springer Berlin Heidelberg, 2002.
[7] D. Ghica. Geometry of Synthesis: a structured approach to VLSI
design. In POPL 2007, pages 363–375. ACM, 2007.
[8] D. R. Ghica and A. I. Smith. Geometry of synthesis II: from games
to delay-insensitive circuits. Electr. Notes Theor. Comput. Sci., 265:
301–324, 2010.
[9] D. R. Ghica and A. I. Smith. Geometry of synthesis III: resource management through type inference. In T. Ball and M. Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL 2011, Austin, TX, USA, January 2628, 2011, pages 345–356. ACM, 2011.
[10] D. R. Ghica, A. I. Smith, and S. Singh. Geometry of Synthesis IV:
compiling affine recursion into static hardware. In ICFP, pages 221–
233, 2011.
[11] 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.
[12] J. Y. Girard. Geometry of interaction 2: Deadlock-free algorithms.
In Proceedings of the International Conference on Computer Logic,
COLOG-88, pages 76–93, New York, NY, USA, 1990. Springer-Verlag
New York, Inc. ISBN 0-387-52335-9.
[13] E. Haghverdi. Towards a geometry of recursion. Theor. Comput. Sci.,
412(20):2015–2028, Apr. 2011. ISSN 0304-3975. .

[14] M. Hasegawa. On traced monoidal closed categories. Math. Struct. in
Comp. Sci., 19(2):217–244, 2009.
[15] N. Hoshino. A modified GoI interpretation for a linear functional
programming language and its adequacy. In FoSSaCS 2011, volume6604 of Lect. Notes Comp. Sci., pages 320–334. Springer, 2011.
[16] N. Hoshino, K. Muroya, and I. Hasuo. Memoryful Geometry of Interaction: from coalgebraic components to algebraic effects. In CSL-LICS
2014, page 52. ACM, 2014.
[17] J. Hyland and C.-H. Ong. On full abstraction for PCF: I, II, and III.
Information and Computation, 163(2):285–408, 2000.
[18] A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Math.
Proc. Cambridge Phil. Soc., 119(3):447–468, 1996.
[19] U. D. Lago, C. Faggian, B. Valiron, and A. Yoshimizu. Parallelism andsynchronization in an infinitary context. In LICS, 2015.
[20] O. Laurent. A token machine for full Geometry of Interaction. In TLCA,
pages 283–297, 2001.
[21] S. Mac Lane. Categories for the working mathematician. Springer,
1998.
[22] I. Mackie. The Geometry of Interaction machine. In POPL 1995, pages
198–208. ACM, 1995.
[23] E. Moggi. Computational lambda-calculus and monads. Tech. Report,
pages 1–23, 1988.
[24] 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.
[25] G. Plotkin and J. Power. Adequacy for algebraic effects. In FoSSaCS
2001, volume 2030 of Lect. Notes Comp. Sci., pages 1–24. Springer,
2001.
[26] G. Plotkin and J. Power. Algebraic operations and generic effects. Appl.
Categorical Struct., 11(1):69–94, 2003.
[27] J. Power and E. Robinson. Premonoidal categories and notions ofcomputation. Math. Struct. in Comp. Sci., 7(5):453–468, 1997.
[28] U. Schöpp. Computation-by-interaction with effects. In H. Yang, editor, Programming Languages and Systems, volume 7078 of Lecture
Notes in Computer Science, pages 305–321. Springer Berlin Heidelberg, 2011.
[29] U. Schöpp. Call-by-value in a basic logic for interaction. In J. Garrigue,
editor, Programming Languages and Systems, volume 8858 of Lecture
Notes in Computer Science, pages 428–448. Springer International
Publishing, 2014.
[30] U. Schöpp. From call-by-value to interaction by typed closure conversion. In APLAS, 2015. To appear.