arXiv:1704.04647v1 [cs.LO] 15 Apr 2017

Effectful Applicative Bisimilarity:
Monads, Relators, and Howe’s Method
(Long Version)
Ugo Dal Lago

Francesco Gavazzo

Paul Blain Levy

Abstract
We study Abramsky’s applicative bisimilarity abstractly, in the context of call-by-value λcalculi with algebraic effects. We first of all endow a computational λ-calculus with a monadic
operational semantics. We then show how the theory of relators provides precisely what is
needed to generalise applicative bisimilarity to such a calculus, and to single out those monads
and relators for which applicative bisimilarity is a congruence, thus a sound methodology for
program equivalence. This is done by studying Howe’s method in the abstract.

1

Introduction

Program equivalence is one of the central notions in the theory of programming languages, and
giving satisfactory definitions and methodologies for it is a challenging problem, for example when
dealing with higher-order languages. The problem has been approached, since the birth of the
discipline, in many different ways. One can define program equivalence through denotational
semantics, thus relying on a model and stipulating two programs to be equivalent if and only if
they are interpreted by the same denotation. If the calculus at hand is equipped with a notion
of observation, typically given through some forms of operational semantics, one could proceed
following the route traced by Morris, and define programs to be contextual equivalent when they
behave the same in every context.
Both these approaches have their drawbacks, the first one relying on the existence of a (not
too coarse) denotational model, the latter quantifying over all contexts, and thus making concrete
proofs of equivalence hard. Handier methodologies for proving programs equivalent have been
introduced along the years based on logical relations and applicative bisimilarity. Logical relations
were originally devised for typed, normalising languages, but later generalised to more expressive
formalisms, e.g., through step-indexing [3] and biorthogonality [6]. Starting from Abramsky’s
pioneering work on applicative bisimilarity [1], coinduction has also been proved to be a useful
methodology for program equivalence, and has been applied to a variety of calculi and language
features.
The scenario just described also holds when the underlying calculus is not pure, but effectful. There have been many attempts to study effectful λ-calculi [36, 32] by way of denotational
semantics [21, 14, 12], logical relations [7], and applicative bisimilarity [27, 10, 9]. But while
the denotational and logical relation semantics of effectful calculi have been studied in the abstract [18, 20], the same cannot be said about applicative bisimilarity and related coinductive
techniques. There is a growing body of literature on applicative bisimilarity for calculi with, e.g.,
nondeterministic [27], and probabilistic effects [10], but each notion of an effect has been studied
independently, often getting different results. Distinct proofs of congruence for applicative bisimilarity, even if done through a common methodology, namely the so-called Howe’s method [19],
do not at all have the same difficulty in each of the cases cited above. As an example, the proof
of the so-called Key Lemma relies on duality results from linear programming [40] when done for
probabilistic effects, contrarily to the apparently similar case of nondeterministic effects, whose

1

W → V ⊕ COMP (V, W )
Z→T1
T n → (R n) ⊕ (T n + 1)
R 0 → λx.x
R n + 1 → COMP (R n, V )

Figure 1: Two Probabilistic Programs.
logical complexity is comparable to that for the plain, deterministic λ-calculus [34, 27]. Finally,
as the third author observed in his work with Koutavas and Sumii [24], applicative bisimilarity
is fragile to the presence of certain effects, like local states or dynamically created exceptions: in
these cases, a sort of information hiding is possible which makes applicative bisimilarity simply
too weak, and thus unsound for contextual equivalence.
The observations above naturally lead to some questions. Is there any way to factor out the
common part of the congruence proof for applicative bisimilarity in the cases above? Where do
the limits on the correctness of applicative bisimilarity lie, in presence of effects? The authors
strongly believe that the field of coinductive techniques for higher-order program equivalence
should be better understood in the abstract, this way providing some answers to the questions
above, given that generic accounts for effectful λ-calculi abound in the literature [32, 36].
This paper represents a first step towards answering the questions above. We first of all
introduce a computational λ-calculus in which general algebraic effects can be represented, and
give a monadic operational semantics for it, showing how the latter coincides with the expected
one in many distinct concrete examples. We then show how applicative bisimilarity can be defined
for any instance of such a monadic λ-calculus, based on the notion of a relator, which allows
to account for the possible ways a relation on a set X can be turned into one for T X, where
T is a monad. We then single out a set of axioms for monads and relators which allow us to
follow Howe’s proof of congruence for applicative bisimilarity in the abstract. Noticeably, these
axioms are satisfied in all the example algebraic effects we consider. The proof of it allows us to
understand the deep reasons why, say, different instances of Howe’s method in the literature seem
to have different complexities.

2

On Coinduction and Effectful λ-Calculi

In this section, we illustrate how coinduction can be useful when proving the equivalence of programs written in higher-order effectful calculi.
Let us start with a simple example of two supposedly equivalent probabilistic functional programs, W and Z, given in Figure 1. (The expression COMP (M, N ) stands for the term λy.M (N y),
and ⊕ is a binary operation for fair probabilistic choice.) Both W and Z behave like the n-th
composition of a function V with itself with probability 21n , for every n. But how could we even
define the equivalence of such effectful programs? A natural answer consists in following Morris
[33], and stipulate that two programs are contextually equivalent if they behave the same when
put in any context, where the observable behaviour of a term can be taken, e.g., as its probability
of convergence. Proving two terms to be contextually equivalent can be quite hard, given the
universal quantification over all contexts on which contextual equivalence is based.
Applicative bisimilarity is an alternative definition of program equivalence, in which λ-terms
are seen as computational objects interacting with their environment by exposing their behaviour,
and by taking arguments as input. Applicative bisimilarity has been generalised to effectful λcalculi of various kinds, and in particular to untyped probabilistic λ-calculi [10], and it is known to
2

W raise → (V ⊕ raisee ) ⊕ COMP (V, W raise )
Z raise → T 1
T n → ((R n) ⊕ raisee ) ⊕ (T n + 1)
R 0 → λx.x
R n + 1 → COMP (R n, V )

Figure 2: Two Probabilistic Programs Throwing Exceptions.
be not only a congruence (thus sound for contextual equivalence) but also fully abstract, at least
for call-by-value evaluation [9]. Indeed, applicative bisimilarity can be applied to the example
terms in Figure 1, which can this way be proved contextual equivalent.
The proof of soundness of applicative bisimilarity in presence of probabilistic effects is significantly more complicated than the original one, although both can be done by following the
so-called Howe’s method [19]. More specifically, the proof that the Howe extension of similarity
is a simulation relies on duality from linear programming (through the Max Flow Min Cut Theorem) when done in presence of probabilistic effects, something that is not required in the plain,
deterministic setting, nor in presence of nondeterministic choice.
Modern functional programming languages, however, can be “effectful” in quite complex ways.
As an example, programs might be allowed not only to evolve probabilistically, but also to have
an internal state, to throw exceptions, or to perform some input-output operations. Consider, as
another simple example, the programs in Figure 2, a variation on the programs from Figure 1
where we allow programs to additionally raise an exception e by way of the raisee command.
Intuitively, W raise and Z raise behave like W and Z, respectively, but they both raise an exception
with a certain probability.
While applicative similarity in presence of catchable exceptions is well-known to be unsound [24],
the mere presence of the raisee command does not seem to cause any significant problem. The
literature, however, does not offer any result about whether combining two or more notions of
computational effect for which bisimilarity is known to work well, should be problematic or not.
An abstract theory accounting for how congruence proofs can be carried out in effectful calculi is
simply lacking.
Even if staying within the scope of Howe’s method, it seems that each effect between those
analysed in the literature is handled by way of some ad-hoc notion of bisimulation. As an example,
nondeterministic extensions of the λ-calculus can be dealt with by looking at terms as a labelled
transition system, while probabilistic extensions of the λ-calculus require a different definition akin
to Larsen and Skou’s probabilistic bisimulation [10]. What kind of transition do we need when,
e.g., dealing with the example from Figure 2? In other words, an abstract theory of effectful
applicative bisimilarity would be beneficial from a purely definitional viewpoint, too.
What could come to the rescue here is the analysis of effects and bisimulation which has been
carried out in the field of coalgebra [39]. In particular, we here exploit the theory of relators, also
known as lax extensions [5, 41].

3

Domains and Monads: Some Preliminaries

In this section, we recall some basic definitions and results on complete partial orders, categories,
and monads. All will be central in the rest of this paper. Due to space constraints, there is no
hope to be comprehensive. We refer to the many introductory textbooks on partial order theory
[13] or category theory [31] for more details.

3

3.1

Domains and Continuous Σ-algebras

Here we recall some basic notions and results on domains that we will extensively use in this work.
The main purpose of this section is to introduce the notation and terminology we will use in the
rest of this paper. We address the reader to e.g. [2] for a deeper treatment of the subject.
Recall that a poset is a set equipped with a reflexive, transitive and antisymmetric relation.
Definition 1. Given a poset D = (D, ⊑D ), an ω-chain in D is an infinite sequence (xn )n<ω of
elements of D such that xn ⊑D xn+1 , for any n ≥ 0.
Definition 2. A poset D = (D, ⊑D ) is an ω-complete partial order, ωCPO for short, if any
ω-chain (xn )n<ω in D has least upper bound (lub) in D. A poset D = (D, ⊑) is an ω-complete
pointed partial order, ωCPPO for short, if it is an ωCPO with a least element ⊥D .
For an ωCPPO D = (D, ⊑D , ⊥D ) we will often omit subscripts, thus writing ⊑ and ⊥ for
⊑
FD and ⊥D , respectively. Given an ω-chain (xn )n<ω we will denote its least upper bound by
{xn | n < ω}. Oftentimes, following the above convention, we will shorten the latter notation
DF
to n<ω xn .
Notice that an ω-chain being a sequence, its elements need not be distinct. In particular, we
say that the chain is stationary if there exists N < ω such that xN +n = xN , for any n < ω.
We will often use the following basics result, stating that if we discard any finite number of
elements at the beginning of a chain, we do not affect its set of upper bounds (and its lub).
Lemma 1. For any ω-chain (xn )n<ω and N < ω the following equality holds:
G
G
xn =
xN +n .
n<ω

n<ω

Definition 3. Let D = (D, ⊑D , ⊥D ), E = (E, ⊑E , ⊥E ) be ωCPPOs. We say that a function
f : D → E is monotone if for all elements x, y in D, x ⊑D y implies f (x) ⊑E f (y). We say it is
continuous if it is monotone and preserves lubs. That is, for any ω-chain (xn )n<ω in D we have:
G
G
f ( {xn | n < ω}) = {f (xn ) | n < ω}.
D

E

Finally, we say it is strict if f (⊥D ) = ⊥E .
Remark 1. (see [2]) It can be easily shown that if a function is continuous then it is also monotone.
However, it should be noticed that to prove that a function f : D → E is continuous, it is necessary
to prove that (f (xn ))n<ω forms an ω-chain in E, for any ω-chain (xn )n<ω in D. That is equivalent
to prove monotonicity of f .
c

c

We denote the set of continuous functions from D to E by D −
→ E and write f : D −
→ E for
c
f ∈D−
→ E.
We will implicitly use the fact that continuous endofunctions on ωCPPOs are guaranteed to
have least fixed points: given a continuous endofunction f : D → D on an ωCPPO D, there
exists an element µf ∈ D such that f (µf ) = µf , and for any x ∈ D, if f (x) = x then µf ⊑ x.
Throughout this work, we will use the notation µf and νf to denote least and greatest fixed point
of a function f , respectively.
ωCPPOs and continuous functions form a category, ωCPPO, which has a cartesian closed
structure. In particular, the cartesian product (of the underlying sets) of ωCPPOs is an ωCPPO
when endowed with the pointwise order (with lubs and bottom element computed pointwise).
Similarly, the set of continuous functions spaces between ωCPPOs is an ωCPPO when endowed
with the pointwise order (again, with lubs and bottom element computed pointwise)1 . Notice
c
that the function space D −
→ E between ωCPPOs D and E is an ωCPPO even if D does not
have a least element (i.e. if D is an ωCPO). As a consequence, since we can regard any set X
1

Let D, E be ωCPPOs define:

4

c

as an ωCPO ordered by the identity relation =X on X 2 , the set X −
→ D = X → D is always an
ωCPPO, for any ωCPPO D. The following well- known result will be useful in several examples.
Lemma 2. Let C, D, E be ωCPPOs. A function f : C × D → E is:
1. Monotone, if it is monotone in each arguments separately.
2. Continuous, if it is continuous in each arguments separately.
Following [36, 37], we consider operations (like ⊕ or raisee in the examples from Section 2) form
a given signature as sources of effects. Semantically, dealing with operation symbols requires the
introduction of appropriate algebraic structures interpreting such operation symbols as suitable
functions. Combining the algebraic and the order theoretic structures just described, leads to
consider algebras carrying a domain structure (ωCPPO, in this paper), such that all function
symbols are interpreted as continuous functions. The formal notion capturing all these desiderata
is the one of a continuous Σ-algebra [15].
Recall that a signature Σ = (F , α) consists of a set F of operation symbols and a map α :
F → N, assigning to each operation symbol a (finite) arity. A Σ-algebra (A, (·)A ) is given by a
carrier set A and an interpretation (·)A of the operation symbols, in the sense that for σ ∈ F , σ A
is a map from Aα(σ) to A. We will write σ ∈ Σ for Σ = (F , α) and σ ∈ F .
Definition 4. Given a signature Σ, a continuous Σ-algebra is an ωCPPO D = (D, ⊑, ⊥) such
that for any function symbol σ in Σ there is an associated continuous function σ D : Dα(σ) → D.
Remark 2. Observe that for a function symbol σ ∈ Σ, we do not require σ D to be strict.
Before looking at monads, we now give various examples of concrete algebras which can be
given the structure of a continuous Σ-algebra for certain signatures. This testifies the applicability
of our theory to a relatively wide range of effects.
Example 1. Let X be a set: the following are examples of ωCPPO.
• The flat lifting X⊥ of X, defined as X + {⊥}, ordered as follows: x ⊑ y iff x = ⊥ or x = y.
• The set (X + E)⊥ (think to E as a set of exceptions), ordered as in the previous example.
We can consider the signature Σ = {raisee | e ∈ E}, where each operation symbol raisee is
interpreted as the constant inl (inr (e)).
• The powerset PX, ordered by inclusion. The least upper bound of a chain of sets is their union,
whereas the bottom is the empty set. We can consider the signature Σ = {⊕} containing a
binary operation symbol for nondeterministic choice. The latter can be interpreted as (binary)
union, which is indeed continuous.
P
• The set of subdistributions DX = {µ : X → [0, 1] | supp(µ) countable,
x∈X µ(x) ≤ 1} over
X, ordered pointwise: µ ⊑ ν iff ∀x ∈ X. µ(x) ≤ ν(x). P
Note that requiring the support of µ to
be countable is equivalent to requiring the existence of x∈X µ(x). The ωCPPO structure is
pointwise induced by the one of [0, 1] with the natural ordering. The least element is the always
zero distribution x 7→ 0 (note that the latter is a subdistribution, and not a distribution).
We can consider the signature Σ = {⊕p | p ∈ [0, 1]} with a family of probabilistic choice
• The ωCPPO structure on D × Eis given by:
(x, y) ⊑D×E (x′ , y ′ )

⇔

x ⊑D x ′ ∧ y ⊑E y ′ ;

⊥D×E

=

{(xn , yn ) | n < ω}

=

(⊥D , ⊥E );
G
G
( {xn | n < ω}, {yn | n < ω}).

G
D×E

D

E

c

• The ωCPPO structure on D −
→ E is given by:
f ⊑
G

c

D−
→E

⊥

g

c

D−
→E

{fn | n < ω}

⇔

∀x ∈ D. f (x) ⊑E g(x);

=

x 7→ ⊥E ;
G
x 7→ {fn (x) | n < ω}.

=

c

E

D−
→E
2 We

call such ωCPOs discrete

5

operations indexed by real numbers in [0, 1]. We can interpret ⊕p as the binary operation
(x, y) 7→ p · x + (1 − p) · y, which is indeed continuous.
• The set (S × X)S⊥ , or equivalently S ⇀ (X × S) (the set of partial states over X) with extension
order: f ⊑ g iff ∀x ∈ X. f (x) 6= ⊥ ⇒ f (x) = g(x), for a fixed set S (of states). The bottom
element is the totally undefined function x 7→ ⊥, whereas the least upper bound of a chain
(fn )n<ω is computed pointwise. Depending on the choice of S, we can define several continuous
operations on (S × X)S⊥ . For instance, taking S = {true, false}, the set of booleans, we can
consider the signature Σ = {read, writeb | b ∈ S} to be interpreted as the continuous operations
read and write b defined by
write b (f ) = x 7→ f (b);
read (f, g) = x 7→ if x = true then f (x) else g(x).
• The set U ∞ × X⊥ (modelling computations with output streams) with the product order, for
a fixed set U (think of U as a set of characters). The set U ∞ of streams over U is the set
of all finite and infinite strings (or words) over U . Formally, a stream u ∈ U ∞ is a function
u : N → U⊥ (i.e. a partial function from N to U ) such that u(n) = ⊥ implies u(n + c) = ⊥, for
any c ≥ 0. A finite stream is a function u such that there exists an n for which u(n) = ⊥. We
can endow U ∞ with the so-called approximation order, i.e. the extension order on N → U⊥ . A
finite approximation of length n of a stream u is a stream w of length n such that w ⊑ u holds.
Clearly, the set
approximants of a stream u forms an ω-chain, and for any u ∈ U ∞
F of finite
(n)
we have u = n<ω u , where u(n) = (u(0), . . . , u(n − 1), ⊥) denotes the n-th approximant of
u. We can define the concatenation u :: w of a finite stream u = (u(0), . . . , u(n − 1), ⊥) and a
stream w ∈ U ∞ by
(
u(k) if k ≤ n − 1;
(u :: w)(k) =
w(c) if k = n + c, for c ≥ 0.
We can extend concatenation to infinite streams defining u :: w = u, for u infinite stream.
It is easy to prove that concatenation is continuous in its second argument, although even
monotonicity fails for its first argument. For, consider the streams c, cc (which are shorthand
for (c, ⊥), (c, c, ⊥), respectively). We clearly have c ⊑ cc, but c :: b = cb 6⊑ ccb = cc :: b.
Finally, we can consider the signature Σ = {printc | c ∈ U } interpreted as the family of
operations print c defined by print c (u, x) = (c :: u, x). It is easy to see that since concatenation
is continuous in its second argument, then so does print c .

3.2

Monads

The notion of monad is given via the equivalent notion of Kleisli Triple (see [31]). Let C be a
category.
Definition 5. A Kleisli Triple hT, η, (·)† i consists of an endomap T over objects of C, a family
of arrows ηX , for any object X, and an operation (called Kleisli extension or Kleisli star) (·)† :
HomC (X, T Y ) → HomC (T X, T Y ), (for all objects X, Y ) satisfying the equations
f† ◦ η = f;
η † = id;
(g † ◦ f )† = g † ◦ f † ;
where f and g have the appropriate types.
Given the equivalence between the notions of monad and Kleisli Triple, we will be terminologically sloppy, using the terms ‘monads’ and ‘Kleisli Triples’ interchangeably. In particular, for a
monad/Kleisli Triple hT, η, (·)† i we will implicitly assume functoriality of the endomap T . Finally,
we will often denote a Kleisli Triple hT, η, (·)† i simply as T .
To any Kleisli Triple hT, η, (·)† i on a category C we can associate the so-called Kleisli category
Kℓ(T ) over C.
6

Definition 6. Given a Kleisli triple as above, we define the Kleisli category Kℓ(T ) (over C) as
follows:
• Objects of Kℓ(T ) are those of C.
• To any arrow f : X → T Y in C we associate an arrow f¯ : X → Y in Kℓ(T ).
• The identity arrow idX : X → X in Kℓ(T ) is ηX .
• Given arrows f¯ : X → Y, ḡ : Y → Z (which correspond to arrows f : X → T Y and g : Y → T Z
in C), define their composition to be g † ◦ f .
From now on we fix the base category C to be the category SET of sets and functions.
Remark 3. Since we work in SET, we will extensively use the so called bind operator »= in place
of Kleisli extensions. Such operator takes as arguments an element u of T X, together with a
function f : X → T Y and returns an element u»=f in T Y . Concretely, we can define u»=f as
f † (u). Vice versa, we can define the Kleisli extension f † of f as x 7→ (x»=f ).
Example 2. All the constructions introduced in Example 1 carry the structure of a monad.
• The functor T X = X⊥ is (part of ) a monad, with left injection as unit and bind operator
defined by
(
f (x)
if u = inl (x), for some x ∈ X;
u»=f =
inr (⊥) otherwise.
• S
The powerset functor P is a monad with unit x 7→ {x} and bind operator defined by u»=f =
x∈u f (x).
• The subdistribution functor D is a monad with unit given via the Dirac distribution δ and bind
operator defined by
X
µ»=f = y 7→
µ(x) · f (x)(y).
x∈X

• The partiality and exception functor T X = (X + E)⊥ for a given set E of exceptions is a
monad with the function x 7→ inl (inl (x)) as unit. The bind operator is defined by
(
u
if u = inr (⊥) or u = inl (inr (e));
u»=f =
f (x) if u = inl (inl (x)).
• The partiality and global state functor T X = S → (X × S)⊥ for a given set S of states, is a
monad with unit x 7→ (s 7→ (x, s)) and the bind operator defined by
(
inr (⊥)
if σ(s) = inr (⊥);
(σ»=f )(s) =
f (y)(t) if σ(s) = inr (y, t).
• The output functor T X = U ∞ × X⊥ is a monad with unit x 7→ (ε, inl (x)) where, to avoid
confusion, we use denote the empty stream by ε, and bind operator defined by
(u, inr (⊥))»=f = (u, inr (⊥));
(u, inl (x))»=f = (u :: w, y)
where (w, y) = f (x).
For a given signature Σ, we are interested in monads on SET that carry a continuous Σ-algebra
structure.
Definition 7. An ωCPPO order ⊑ on a monad T is a map that assigns to each set X a relation
⊑X ⊆ T X × T X and an element ⊥X ∈ T X such that
• The structure (T X, ⊑X , ⊥X ) is an ωCPPO.

7

• The bind operator is continuous in both arguments. That is,
G
G
(
un )»=f =
(un »=f );
n<ω

u»=(

G

n<ω

fn ) =

n<ω

G

(u»=fn ).

n<ω

We say that ⊑ is strict in its first argument if we additionally have ⊥»=f = ⊥ (and similarly for
its second argument). We say that T carries a continuous Σ-algebra structure if T has an ωCPPO
order such that T X is a continuous Σ-algebra with respect to the order ⊑X , for any set X.
Most of the time we will work with a fixed set X. As a consequence, we will omit subscripts,
just writing ⊑ in place of ⊑X . Similarly, for an operation σ in Σ, we will write σ T in place of σ T X
(the interpretation of σ as an operation on T X).
Remark 4. The last definition is essentially regarding the bind operator as a continuous function
(in both arguments) from T X × (X → T Y ) to T Y . This makes sense since T X × (X → T Y ) is
c
an ωCPPO: regarding the set X as the discrete ωCPO, we have X → T Y = X −
→ T Y , so that
T X × (X → T Y ) is an ωCPPO,
of two ωCPPOs. Because »= is continuous
F being the
F product F
in both its arguments, we have ( n un )»=( n fn ) = n (un »=fn ).
The bind operation will be useful when giving an operational semantics to the sequential
(monadic) composition of programs. As a consequence, although we did not explicitly require the
bind operator to be strict (especially in its first argument), such condition will be often desired
(especially when giving semantics to call-by-value languages).

Example 3. Example 1 shows that all monads in Example 2 have an ωCPPO order. It is easy
to check that all bind operations, with the exception of the one for the output monad, are strict
in their first argument. In fact, even monotonicity of the bind operator for output monad fails,
due to the failure of monotonicity for concatenation (see 1). The reason why this property does
not hold for the output monad relies on non-monotonicity of the concatenation operator on its
first argument. Nonetheless, we can endow U ∞ × X⊥ with a different order, obtaining the desired
result:
(u, x) ⊑ (w, y) iff (x = inr (⊥) ∧ u ⊑ w) ∨ (x 6= inr (⊥) ∧ x = y ∧ u = w).
It is not hard to see that we obtain an ωCPPO with continuous bind operator.
Definition 7 requires the bind operator to be continuous. This condition is a special case of
the more general notion of order-enrichment [23] for a monad.
Definition 8. We say that a category C is ωCPPO-enriched if
• Each hom-set HomC (X, Y ) carries a partial order ⊑ with an ωCPPO structure.
• Composition is continuous. That is, the following equations hold:
G
G
g◦(
fn ) =
(g ◦ fn );
G

(

n<ω

n<ω

fn ) ◦ g =

n<ω

G

(fn ◦ g).

n<ω

Definition 9. A monad T on C is ωCPPO-enriched if Kℓ(T ) is ωCPPO-enriched. That is, for
every pair of objects X, Y , the set HomC (X, T Y ) carries an ωCPPO-structure such that composition is continuous and Kleisli star is locally continuous. Concretely, that means that the following
equations hold (cf. [16]):
G
G
(
fn ) ◦ h =
(fn ◦ h);
n<ω
†

u ◦

G

n<ω

fn =

n<ω

(

G

G

(u† ◦ fn );

n<ω
†

fn ) =

n<ω

G

n<ω

8

fn† .

Our notion of ωCPPO order on a monad T on SET is nothing but a special case of ωCPPOenrichment. Since we are in SET, and we have the terminal object 1 (say 1 = {∗}), any element u
of T X directly corresponds to the arrow ū : 1 → T X, defined by ū(∗) = u. In particular, we have
c
TX ∼
→ T X (since 1 is discrete). For a function f : X → Y and an element u ∈ X
= 1 → TX = 1 −
we can simulate function application f (u) as ū ◦ f (meaning that ū ◦ f = f (u)). As a consequence,
we have that u»=f corresponds to f † ◦ ū. Finally, observe that the equation
G
G
{un | n < ω} =
{un | n < ω}
1→T X

TX

holds. We show thatF if T is ωCPPO-enriched, then the bind operator is continuous in both
arguments. In fact, ( n<ω un )»=f corresponds to the function
G
G
G
f† ◦
un = f † ◦
ūn =
(f † ◦ ūn )
n<ω

which itself corresponds to

n<ω

F
Similarly, u»= n<ω fn corresponds to
G
G
G
(
fn )† ◦ ū =
fn† ◦ ū =
(fn† ◦ ū)
n<ω (un »=f ).

n<ω

F

n<ω

F

n<ω

n<ω

which corresponds to n<ω (u»=fn ).
Most of the monads commonly used e.g. in functional programming to model side-effects
are not order enriched. This follows from the requirement of having a bottom element. The
reason behind that condition relies on the fact that our operational semantics will be model
non-termination explicitly. That is, a (purely) divergent program M will be evaluated in the
bottom element of the monad. For instance let us consider pure λ-calculus. Standard operational
semantics employs inductively defined judgments of the form M ⇓ V , meaning that ⇓⊆ Λ × V
(which, in general, can be viewed as ⇓⊆ Λ × T V, for T the identity monad). Such a semantics
does not capture divergence explicitly: for instance, we just have that there exists no value V
such that Ω ⇓ V . The operational semantics we will define in the next chapter associates to each
program a subset of the finite approximations it is evaluated to, and then consider the lub of such
approximations. As a consequence, we need the monad to have bottom element ⊥, so that we
will have that the semantics of Ω to be indeed ⊥. Nevertheless, we recall that any set can always
be lifted to an ωCPPO by adding a bottom element to it and considering the flat ordering. As
a consequence, although most of the monads commonly used in functional programming are not
order-enriched, their flat version is.

4

A Computational Calculus and Its Operational Semantics

In this section we define a computational λ-calculus. Following [32, 27, 30], we syntactically
distinguish between values and computations. We fix a signature Σ of operation symbols (the
sources of side-effects), and a monad T carrying a continuous Σ-algebra structure (which describes
the nature of the wanted effectful computations generated by the operations in Σ).
Definition 10. Given a signature Σ, the sets ΛΣ and VΣ of terms and values are defined by the
following grammars:
M, N
V, W

::=
::=

return V | V W | M to x.N | σ(M, . . . , M );
x | λx.M.

where x ranges over a fixed countably infinite set X of variables and σ ranges over Σ.
The term (M to x.N ) captures monadic binding (which is usually expressed using a “let-in”
notation). A calculus with an explicit separation between terms and values has the advantage
to make proofs simpler, without sacrificing expressiveness. For instance, we can encode terms’
application M N as (M to x.(N to y.xy)) and vice versa (M to x.N ) as (λx.N )M .
9

Example 4. We can model several calculi combining the signatures from Example 1.
• For a given set E of exceptions, we can define a probabilistic λ-calculus with exceptions as ΛΣ ,
for a signature Σ = {⊕p , raisee | p ∈ [0, 1], e ∈ E}. In particular, we will have terms of the form
M ⊕p N and raisee . Replacing the probabilistic choice operator ⊕p with its nondeterministic
counterpart ⊕ we obtain a nondeterministic calculus with exceptions.
• We can define a nondeterministic calculus with global (boolean) states as ΛΣ , for a signature
Σ = {⊕, writeb , read | b ∈ {true, false}}. In particular, we will have terms of the form M ⊕ N ,
writeb .M , and read(M, N ). The intuitive meaning of writeb .M is to store b and then continue
as M , whereas the intuitive meaning of read(M, N ) is to read the value in the store: if such
value is the boolen true then continue as M , otherwise as N . A formal semantics for these two
functions is given in Example 1.
• We can define a nondeterministic calculus with output using the signature Σ = {⊕, printc | c ∈
U }, where U is a given alphabet. The intuitive meaning of print c.M is to output c and then
continue as M . A formal semantics for this function is given in Example 1.
In what follows, we work with a fixed arbitrary signature Σ. As a consequence, we often
denote the sets of terms and values as Λ and V, respectively, thus omitting subscripts. Moreover,
we consider terms and values modulo α-equivalence and assume Barendregt Convention [4]. We
let F V (M ) denote the set of free variables of the term M . A term M is closed if F V (M ) = ∅.
We denote finite sets of variables, terms and values using “bar notation”: for instance, we write x̄
and V̄ for a finite set of variables and values, respectively. For a finite set x̄ of variables define
Λ(x̄) = {M | F V (M ) ⊆ x̄};
V(x̄) = {V | F V (V ) ⊆ x̄};
to be the sets of terms and values with free variables in x̄, respectively. The set of closed terms
and values are then defined as Λ(∅) and V(∅), and denoted by Λ0 and V0 , respectively.
Definition 11. Define for all values V, W and any term M , the value V [W/y] obtained by (simultaneous) substitution of W for y in V , and the term M [y := V ] obtained by (simultaneous)
substitution of V for y in M as follows (recall we are assuming Barendregt’s convention):
x[W/x]
x[W/y]
(λx.M )[W/y]

= W
= x
= λx.M [y := W ]

(return V )[y := W ] = return V [W/y]
(V V ′ )[y := W ] = V [W/y]V ′ [W/y]
(M to x.N )[y := W ] = M [y := W ] to x.N [y := W ]
Big-step semantics associates to each closed term M an element JM K in T V0 . Such a semantics
is defined by means of an approximation relation ⇓n , indexed by a natural number n, whose
definition is given in Figure 3. Judgments are of the form M ⇓n X, where M ∈ Λ0 , X ∈ T V0
and n ≥ 0. Intuitively, a judgment M ⇓n X states that X is the n-th approximation of the
computation obtained by call-by-value evaluating M . (By the way, all the results in this paper
would remain valid also if evaluating terms in call-by-name order, which is however less natural
in presence of effects.)
The system in Figure 3 is ‘syntax directed’, meaning that given a judgment M ⇓n X, the solely
syntactic form of M and the number n uniquely determine the last rule used to derive M ⇓n X.
As a consequence, each judgment has a unique derivation.
Lemma 3 (Determinacy). For any term M , if M ⇓n X and M ⇓n Y , then X = Y .
Proof. By induction on n. If n = 0, then both M ⇓n X and M ⇓n Y must be the conclusion of
an instance of rule (bot) (all other rules requires n to be positive). As a consequence, we have
10

M ⇓0 ⊥

(bot)

return V ⇓n+1 η(V )

(ret)

M ⇓n X
N [x := V ] ⇓n YV
(seq)
M to x.N ⇓n+1 X»=(V 7→ YV )
M [x := V ] ⇓n X
(app)
(λx.M )V ⇓n+1 X
M 1 ⇓n X1
...
M k ⇓n Xk
(op)
T
σ(M1 , . . . , Mk ) ⇓n+1 σ (X1 , . . . , Xk )
Figure 3: Big-step Semantics.
X = ⊥ = Y . Suppose now n = m + 1, for some m ≥ 0. We proceed by case analysis on the last
rule used to derive M ⇓n X.
Case (bot). This case is not possible, since n > 0.
Case (ret). Then M is of the form return V , for some value V , X is η(V ), and M ⇓m+1 Y is
return V ⇓m+1 Y . The latter judgment must follow from an instance of rule (ret) as well, and
thus Y = η(V ).
Case (app). Then M is of the form (λx.N )V and we have N [x := V ] ⇓m X, for some term N .
Therefore, the judgment M ⇓m+1 Y is of the form (λx.N )V ⇓m+1 Y implying it can only be
the conclusion of an instance of the rule (app). Therefore, N [x := V ] ⇓m Y holds as well. We
can apply the induction hypothesis on the latter and N [x := V ] ⇓m X thus inferring X = Y .
Case (seq). Then M is of the form N to x.N ′ , X is of the form X ′ »=(V 7→ XV′ ), and both
N ⇓m X ′ and N ′ [x := V ] ⇓m XV′ hold, for some terms N, N ′ and elements X ′ , XV′ in T V0 . As
a consequence, the judgment M ⇓m+1 Y has the form N to x.N ′ ⇓m+1 Y , implying it must
be the conclusion of an instance of the rule (seq) as well. Therefore, we have N ⇓m Y ′ and
N ′ [x := V ] ⇓m YV′ , and Y = Y ′ »=(V 7→ YV′ ), for some elements Y ′ , YV′ . We can then apply
the induction hypothesis on N ⇓m X ′ , N ⇓m Y ′ and N ′ [x := V ] ⇓m XV′ , N ′ [x := V ] ⇓m YV′ ,
obtaining X ′ = Y ′ , XV′ = YV′ and thus X ′ »=(V 7→ XV′ ) = Y ′ »=(V 7→ YV′ ).
Case (op). Then M is of the form σ(M1 , . . . , Mk ), X is of the form σ T (X1 , . . . , Xk ), and the judgment M1 ⇓m X1 , . . . , Mk ⇓m Xk hold, for some terms M1 , . . . , Mk and elements X1 , . . . , Xk in
T V0 . As a consequence, the judgment M ⇓m+1 Y has the form σ T (M1 , . . . , Mk ) ⇓m+1 Y . The
latter must be the conclusion of an instance of the rule (op), meaning that we have judgments
M1 ⇓m Y1 , . . . , Mk ⇓m Ym and Y = σ T (Y1 , . . . , Ym ). We can apply the induction hypothesis on
the pair of judgments Mi ⇓m Xi , Mi ⇓m Yi , for i ∈ {1, . . . , k}, inferring Xi = Yi . We conclude
σ T (X1 , . . . , Xk ) = σ T (Y1 , . . . , Yk ).
Lemma 4. For any term M if M ⇓n X and M ⇓n+N Y , then X ⊑ Y .
Proof. The proof follows the same pattern of the previous one, where in the inductive case we use
monotonicity of both the bind operator and the operations σ T .
Corollary 1. Let M be a a term and Xn be the (unique) element in T V0 such that M ⇓n X.
Then, the sequence (Xn )n<ω forms an ω-chain in T V0 .
A direct consequence of the above corollary is that we can define the evaluation JM K of a term
M as
G
JM K =
X.
M⇓n X

This allows us to explicitly capture non-termination (which is usually defined coinductively). For
instance, it is easy to show that for the purely (i.e. having no side-effects) divergent program
11

Ω, defined as (λx.xx)(λx.xx), we have JΩK = ⊥. This style of operational semantics [11, 10] is
precisely the reason we require the monad T to carry an ωCPPO structure. Modelling divergence
in this way turned out to be fundamental in e.g. probabilistic calculi [11].
Definition 12. Let M be a term. Define the n-th approximation M (n) ∈ T V0 of M as follows:
M (0) = ⊥
(return V )(n+1) = η(V )
((λx.M )V )(n+1) = (M [x := V ])(n)
(M to x.N )(n+1) = M (n) »=(V 7→ (N [x := V ])(n) )
(n)

(n)

(σ(M1 , . . . , Mk ))(n+1) = σ T (M1 , . . . , Mk )
Lemma 5. For any term M we have M ⇓n M (n) .
Proof. The proof is by induction on n. If n = 0, then we trivially have M ⇓0 ⊥. If n = m + 1, for
some m ≥ 0, we proceed by case analysis on the last rule used to derive the judgment M ⇓m+1
M (m+1) . As a paradigmatic example, we show the case for rule (seq). Suppose M ⇓m+1 M (m+1)
is of the form (N to x.N ′ ) ⇓m+1 Y »=(V 7→ YV′ ) and the judgments N ⇓m Y , N ′ [x := V ] ⇓m YV′
hold, for some terms N, N ′ and elements Y, YV′ in T V0 . We can apply the induction hypothesis
on m, obtaining N ⇓m N (m) and N ′ [x := V ] ⇓m (N ′ [x := V ])(m) . By Lemma 3 we thus have
N (m) = Y and (N ′ [x := V ])(m) = YV′ . We can conclude
Y »=(V 7→ YV′ ) = N (m) »=(V 7→ (N ′ [x := V ])(m) ) = (N to x.N ′ )(m+1) .

Corollary 1 and Lemma 5 together imply that for any term M we have the ω-chain
(M (n) )n<ω
F
of finite approximations of M . That means, in particular, that JM K is equal to n<ω M (n) . For
instance, by previous lemma we have Ω(0) = ⊥ and Ω(n+1) = ((xx)[x := λx.xx])(n) = Ω(n) . As a
consequence, we have for any n, Ω(n) = ⊥, and thus JΩK = ⊥.
Since both »= and σ T are continuous, we can characterise operational semantics equationally.
Lemma 6. The following equations hold:
Jreturn V K = η(V );
J(λx.M )V K = JM [x := V ]K;
JM to x.N K = JM K»=(V 7→ JN [x := V ]K);
Jσ(M1 , . . . , Mn )K = σ T (JM1 K, . . . , JMn K).
F
Proof. By Lemma 1 we have JM K = n<ω M (n+1) , meaning that we can freely ignore M (0) (which
is ⊥). We prove each equation separately.
Case 1. We have:
G
G
Jreturn V K =
(return V )(n+1) =
η(V ) = η(V ).
n<ω

n<ω

Case 2. We have:

J(λx.M )V K =

G

((λx.M )V )(n+1) =

n<ω

G

n<ω

12

(M [x := V ])(n) = JM [x := V ]K.

Case 3. We have:
JM to x.N K =

G

(M to x.N )(n+1)

n<ω

=

G

(M (n) »=(V 7→ (N [x := V ])(n) ))

n<ω

=

G

M (n) »=

n<ω

=

G

G

(V 7→ (N [x := V ])(n) )

n<ω

M (n) »=(V 7→

n<ω

G

(N [x := V ])(n) )

(Continuouity of »=)
(Lub of functions)

n<ω

= JM K»=(V 7→ JN [x := V ]K).
Case 4. We have:
Jσ(M1 , . . . , Mk )K =

G

(σ(M1 , . . . , Mk ))(n+1)

n<ω

=

G

(n)

n<ω

= σT (

G

(n)

M1 , . . . ,

n<ω
T

(n)

σ T (M1 , . . . , Mk )
G

(n)

Mk )

(Continuouity of σ T )

n<ω

= σ (JM1 K, . . . , JMk K)

It is actually not hard to see that the function J·K is the least solution to the equations in
Lemma 6.

5

On Relational Reasoning

In this section we introduce the main machinery behind our soundness results. The aim is to
generalise notions and results from e.g. [27, 17, 28] to take into account generic effects. We will
use results from the theory of coalgebras [39] to come up with a general notion of applicative
(bi)similarity parametric over a notion of observation, given through the concept of relator.

5.1

Relators

The concept of relator [41, 29] is an abstraction meant to capture the possible ways a relation
on a set X can be turned into a relation on T X. Recall that for an endofunctor F : C → C, an
F -coalgebra [39] consists of an object X of C together with a morphism γX : X → F X. As usual,
we are just concerned with the case in which C is SET.
Definition 13. Let F be an endofunctor on SET, and X, Y be sets. A relator Γ for F is a map
that associates to each relation R ⊆ X × Y a relation ΓR ⊆ F X × F Y such that
=F X ⊆ Γ(=X )
ΓS ◦ ΓR ⊆ Γ(S ◦ R)
Γ((f × g)−1 R) = (F f × F g)−1 ΓR
R ⊆ S =⇒ ΓR ⊆ ΓS

(Rel-1)
(Rel-2)
(Rel-3)
(Rel-4)

where for f : Z → X, g : W → Y we have (f × g)−1 R = {(z, w) | f (z) R g(w)}, and =X denotes
the identity relation on X. A relator Γ is conversive if Γ(Rc ) = (ΓR)c , where Rc denotes the
converse of R.

13

Example 5. For each of the monads introduced in previous sections, we give some examples of
relators. Most of these relators coincide with the relation lifting of their associated functor. It is
in fact well known that for any weak-pullback preserving functor, its relation lifting is a relator
[25]. We use the notation Γ for a relator aimed to capture the structure of a simulation relation,
and ∆ for a relator aimed to capture the structure of a bisimulation relation. This distinction is
not formal, and only makes sense in the context of concrete examples: its purpose is to stress that
from formal view point, both concrete notions of similarity and bisimilarity are modeled as forms
of Γ-similarity (for a suitable relator Γ). Let R ⊆ X × Y :
• For the partiality monad T X = X⊥ define the relators Γ⊥ , ∆⊥ by
u Γ⊥ R v iff u = inl (x) =⇒ v = inl (y) ∧ x R y;
u ∆⊥ R v iff u = inl (x) =⇒ v = inl (y) ∧ x R y,
v = inl (y) =⇒ u = inl (x) ∧ x R y.
Note that u = inl (x) means, in particular, u 6= inr (⊥). Thus, for instance, u and v are Γ⊥ R
related if whenever u converges, so does v and the values to which u, v converge are R-related.
The relator ∆⊥ is conversive.
• For the nondeterministic powerset monad P define relators ΓP and ∆P by
u ΓP R v iff ∀x ∈ u. ∃y ∈ v. x R y;
u ∆P R v iff ∀x ∈ u. ∃y ∈ v. x R y,
∀y ∈ v. ∃x ∈ u. x R y.
The relator ∆P is conversive.
• For the probabilistic subdistributions monad D define relators ΓD and ∆D by
µ ΓD R ν iff ∀U ⊆ X. µ(U ) ≤ ν(R(U ));
µ ∆D R ν iff µ ΓD R ν ∧ ν ΓD Rc µ;
P
where R(U ) = {y ∈ Y | ∃x ∈ U. x R y} and µ(U ) = x∈U µ(x). The relator ∆D is conversive.
• For the exception monad T X = X + E define the relators ΓE and ∆E by (letters e, e′ range
over E)
u ΓE R v iff u = inr (e) =⇒ v = inr (e′ ) ∧ e = e′ ,
u = inl (x) =⇒ v = inl (y) ∧ x R y;
u ∆E R v iff u ΓE R v,
v = inr (e′ ) =⇒ u = inr (e) ∧ e = e′ ,
v = inl (y) =⇒ u = inl (x) ∧ x R y.
The relator ∆E is conversive.
• For the partiality and exception monad (i.e. the exception monad with divergence) T X =
(X +E)⊥ we can define relators simply composing relators for the partiality monad with relators
for the exceptions monads (see Lemma 7). Notably, define ΓE⊥ as Γ⊥ ◦ΓE and ∆E⊥ as ∆⊥ ◦∆E .
The relator ∆E⊥ is conversive.
• For the state monad T X = (X × S)S define the relator ∆S by
f ∆S R g iff ∀s ∈ S. s1 = s2 and x1 R x2 ,
where (x1 , s1 ) = f (s) and (x2 , s2 ) = g(s).
The relator ∆S is conversive.
• For the output monad T X = U ∞ × X⊥ we can define relators based on the order defined in
Example 3.
(u, x) ΓU R (w, y) iff (x = inr (⊥) ∧ u ⊑ w) ∨ (x = inl (x′ ) ∧ y = inl (y ′ ) ∧ x′ R y ′ );
(u, x) ∆U R (w, y) iff (u, x) ΓU R (w, y) ∧ (w, y) ΓU Rc (u, x).
The relator ∆U is conversive.
14

Checking that the above are indeed relators is a tedious but easy exercise. It is useful to know
that the collection of relators is closed under certain operations (see [29] for proofs).
Lemma 7 (Algebra of Relators). Let F, G be endofunctors on SET.
Then
T
T
1. T
Let (Γi )i∈I be a family of relators for F . The intersection i∈I Γi defined by ( i∈I Γi )R =
i∈I Γi (R) is a relator for F .
2. The converse Γc of Γ defined by Γc (R) = (ΓRc )c is a relator for F . We have the equality
(Γc )c = Γ and, additionally, Γc = Γ if Γ is conversive.
3. Let Γ, Γ′ be relators for F, G, respectively. Then Γ′ ◦ Γ is a relator for G ◦ F . Moreover, if both
Γ and Γ′ are conversive, then so is Γ′ ◦ Γ.
4. Given a relator Γ for F , Γ ∩ Γc is the greatest (wrt the pointwise order) conversive relator for
F contained in Γ.
We can now give a general notion of simulation with respect to a given relator.

5.2

Bisimulation, in the Abstract

A relator Γ for a monad T expresses the observable part of the side-effects encoded by T . Its
abstract nature allows to give abstract definitions of simulation and bisimulation parametric in
the notion of observation given by Γ.
Definition 14. Let γX : X → F X, γY : Y → F Y be F -coalgebras:
1. A Γ-simulation is a relation R ⊆ X × Y such that
xRy =⇒ γX (x) ΓR γY (y).
2. Γ-similarity -ΓX,Y is the largest Γ-simulation.
Example 6. It is immediate to see that the corresponding notions of Γ-similarity for the (bi)simulation
relators of Example 5 coincide with widely used notions of (bi)similarity.
As usual, the notion of similiarity can be characterised coinductively as the greatest fixed point
of a suitable functional.
Definition 15. Let γX : X → F X, γY : Y → F Y be F -coalgebras. Define the functional
Γ
FX,Y
: 2X×Y → 2X×Y by
Γ
FX,Y
(R) = (γX × γY )−1 (ΓR).
Γ
When clear from the context, we will write FΓ and -Γ in place of FX,Y
and -ΓX,Y .

Lemma 8. The following hold:
1. The functional FΓ is monotone, and thus has a greatest fixed point νFΓ .
2. A relation R is a Γ-simulation iff it is a post fixed-point of FΓ . Therefore, Γ-similarity coincides
with νFΓ .
Proof. Monotonicity of FΓ directly follows from monotonicity of Γ, and thus it has greatest fixed
point by Knaster-Tarski Theorem (recall that the set 2X×Y carries a complete lattice structure
under the inclusion order). A straightforward calculation shows that a relation R is a Γ-simulation
iff it is a post fixed-point of FΓ . Together with point 1, the latter implies νFΓ =-Γ .
Proposition 1. Let γX : X → F X be an F -coalgebra.
1. Γ-similarity is a preorder.
2. If Γ is conversive, then Γ-similarity is an equivalence relation.
Proof. Let γX : X → F X be an F -coalgebra.

15

1. We prove that -Γ is reflexive by coinduction, showing that the identity relation =X on X is
a Γ-simulation. In fact, from x =X x we obtain γX (x) =F X γX (x), and thus we can conclude
γX (x) Γ(=X ) γX (x), by (Rel-1).
We now show that -Γ is transitive. Suppose to have x -Γ y -Γ z. By very definition of -Γ
there exist Γ-simulations R, S such that x R y and y S z, and thus γX (x) (ΓS ◦ ΓR) γX (z).
Thanks to (Rel-4) we can conclude that S ◦ R is a Γ-simulation as well, meaning, in particular,
that x -Γ z
2. We simply observe that if R is a Γ-simulation, then so is Rc , for a conversive relator Γ.
Since T is a monad we consider relators that properly interact with the monadic structure of
T , which are also known as lax extensions for T [5].
Definition 16. Let T be a monad, X, X ′ , Y, Y ′ be sets, f : X → T X ′ , g : Y → T Y ′ be functions,
and R ⊆ X × Y, S ⊆ X ′ × Y ′ be relations. We say that Γ is a relator for T if it is a relator for T
regarded as a functor, and
• x R y =⇒ ηX (x) ΓR ηY (y);
• u ΓR v =⇒ (u»=f ) ΓS (v»=g), whenever x R y =⇒ f (x) ΓS g(y).
Remark 5. Definition 16 can be more compactly expressed using Kleisli star, thus requiring that
R ⊆ (ηX × ηY )−1 (ΓS)
−1

R ⊆ (f, g)

(Lax-Unit)
†

† −1

(ΓS) =⇒ ΓR ⊆ (f × g )

(ΓS)

(Lax-Bind)

or diagramatically
R

X

/

/Y

/


/ TY

ηX

ηY


TX
X

R
/

/Y

/


/ TY ′

TX
g

f


T X′

ΓS

ΓR

=⇒

ΓR
/

/ TY
g†

f†


TX

/

ΓS


/ TY

where we write R : X 9 Y for R ⊆ X × Y .
Example 7. All relators of the form ΓT in Example 5 are relators for T . Proving that is quite
standard, with the exception of the probabilistic case where the proof essentially relies on the Max
Flow Min Cut Theorem [40].
Definition 17. Let T come with an ωCPPO order ⊑. We say that ΓR is inductive if for any
ω-chain (un )n<ω in T X, we have:
⊥ ΓR u
(∀n. un ΓR v) =⇒

G

(ω-comp 1)
un ΓR v.

(ω-comp 2)

n

We say that Γ respects Σ if
(∀k. uk ΓR vk ) =⇒ σ(u1 , . . . , un ) ΓR σ(v1 , . . . , vn )
for any σ ∈ Σ, where k ∈ {1, . . . , α(σ)}.

16

(Σ-comp)

Remark 6. For a monad T carrying a continuous Σ-algebra structure and a function f : X → T Y ,
we required f † : T X → T Y to be continuous, T X being an ωCPPO. Since T X is also a Σ-algebra,
it seems natural to require f † to be also a Σ-algebra homomorphism. In fact, such requirement
implies condition (Σ-comp) and has the advantage of being more general than the latter, not
depending from the specific relator considered. Let T be a monad on SET. Following [38] we
say that an n-ary algebraic operation (where n is some set) associates to each set X a function
σX : (T X)n → T X in such a way for every function f : X → T Y , the Kleisli extension f † is a
homomorphism. Recall that an n-ary generic effect is an element of T n. As shown in [38], there
is a bijection from generic effects to algebraic operations as follows. Every n-ary generic effect p
gives rise to an n-ary algebraic operation p̂, where p̂X sends u to u† (p). Conversely, each n-ary
algebraic operation σ is p̂ for a unique n-ary generic effect p, viz. σn (ηn ).
We can now generalise our condition on T by requiring it to be equipped with an n-ary algebraic
operation for each σ ∈ Σ of arity n. This is the equivalent to extending our definitions by requiring
the additional axiom that Kleisli extensions are homomorphisms. Moreover, requiring the bind
operator to be strict in its first argument means that ⊥ is an algebraic constant. Let us now prove
that this condition implies condition (Σ-comp). For, suppose σ has arity n, and ∀k. uk ΓR vk
holds, meaning that we have the square
n

=n
/

/n

/


/ TY

v

u


TX

ΓR

As a consequence, we also have the square
Tn

Γ(=n )
/

/ Tn

/


/ TY

u†


TX

v†
ΓR

and therefore
Tn

=T n
/

/ Tn

/


/ TY

u†


TX

v†
ΓR

Writing the algebraic operation associated with σ as p̂, we have p =T n p, and so u† (p) ΓR v † (p),
which essentially means
σX (u1 , ..., un ) ΓR σY (v1 , ..., vn ).
To the ends of this paper, condition (Σ-comp) is sufficient and thus we will use that throughout.
Following Abramsky [1] we introduce Applicative Transition System (ATSs) over a monad
(taking into account effectful computations) and define the notion of applicative simulation. Let
T be a monad.
Definition 18. An applicative transition system (over T ) consists of the following:
• A state space made of a pair of sets (X, Y ) modelling closed terms and values, respectively.
• An evaluation function ε : X → T Y .
• An application function · : Y → Y → X.
The notion of ATS distinguishes between terms and values. As a consequence, we often deal
with pairs of relations (RX , RY ), where RX , RY are relations over X and Y , respectively. We
refer to such pairs as XY -relations. XY -relations belongs to 2X×X × 2Y ×Y . The latter, being the
product of complete lattices, is itself a complete lattice.
17

Definition 19. Let Γ be a relator for T . An applicative Γ-simulation is an XY -relation R =
(RX , RY ) such that:
x RX x′ =⇒ ε(x) ΓRY ε(x′ )
′

(Sim-1)
′

y RY y =⇒ ∀w ∈ Y. y · w RX y · w.

(Sim-2)

The above definition induces an operator BΓ on 2X×X × 2Y ×Y defined for R = (RX , RY ) as
(BΓ (RX ), BΓ (RY )), where
BΓ (RX ) = {(x, x′ ) | ε(x) ΓRY ε(x′ )}
BΓ (RY ) = {(y, y ′ ) | ∀w ∈ Y. y · w RX y ′ · w}.
It is easy to prove that since Γ is monotone, then so is BΓ . As a consequence, we can define
applicative Γ-similarity as the greatest fixed point νBΓ of BΓ .
Proposition 2. The following hold:
1. Applicative Γ-similarity -Γ is a preorder.
2. If Γ is conversive, then -Γ is an equivalence relation.
Proof. The proof strictly follows the proof of Proposition ?? (proving the desired properties with
respect to clause (Sim-2) is straightforward). As an example, we show by coinduction that -Γ is
reflexive by proving that the XY -identity relation (=X , =Y ) is an applicative Γ-simulation. From
x =X x we infer ε(x) =T Y ε(x), and thus ε(x) Γ(=Y ) ε(x), by (Rel-1). Moreover, we trivially
have that y =Y y implies y · w =X y · w.

6

Contextual Preorder and Applicative Similarity

In the previous section, the axioms needed to generalise applicative bisimilarity to our setting have
been given. What remains to be done is to appropriately instantiate all this to ΛΣ . We introduce
the notions of contextual preorder and applicative similarity (which will be then extended to
contextual equivalence and applicative bisimilarity). From now we assume to have a monad T
carrying a continuous Σ-algebra structure. Moreover, we assume any relator for T to be inductive
and to respect Σ. It is convenient to work with generalisations of relations on closed terms (resp.
values) called λ-term relations.
Definition 20. An open relation over terms is a set RΛ of triples (x̄, M, N ) where M, N ∈ Λ(x̄).
Similarly, an open relation over values is a set RV of triples (x̄, V, W ) where V, W ∈ V(x̄). A
λ-term relation is a pair R = (RΛ , RV ) made of an open relation RΛ over terms and an open
relation RV over values. A closed λ-term relation is a pair R = (RΛ , RV ) where RΛ ⊆ Λ0 × Λ0
and similarly for RV .
Remark 7. Formally, we can see an
Q open relation over terms (and similarly over values) as
an element of the cartesian product x̄ 2Λ(x̄)×Λ(x̄) . That is, an open relation is a function that
associates to each finite set x̄ of variables a (binary) relation between open terms
Q in Λ(x̄). Since,
2Λ(x̄)×Λ(x̄) is a complete lattice, for any finite set of variables x̄, then so is x̄ 2Λ(x̄)×Λ(x̄) . That
is, the set of open relations over terms (and over values) forms a complete lattice (the order is
given pointwise). As a consequence, the set of λ-term relations is a complete lattice as well. These
algebraic properties allow us to define open relations both inductively and coinductively, and, in
particular, to extend notions and results developed in the relational calculus of [27, 26, 17, 28].
We will use infix notation and write x̄ ⊢ M RΛ N to indicate that (x̄, M, N ) ∈ RΛ . The same
convention applies to values and open relations over values. For a λ-term relation R = (RΛ , RV ),
we often write x̄ ⊢ M R N (i.e. (x̄, M, N ) ∈ R) for x̄ ⊢ M RΛ N (i.e. (x̄, M, N ) ∈ RΛ ). The
same convention holds for values and RV . Finally, we will use the notations ∅ ⊢ M R N and
M R N interchangeably (and similarly for values).
There is a canonical way to extend a closed relation to an open one.
18

∀x̄. ∀x ∈ x̄. x̄ ⊢ x RV x
∀x̄. ∀x ∈
6 x̄. ∀M, N. x̄ ∪ {x} ⊢ M RΛ N =⇒ x̄ ⊢ λx.M RV λx.N

(Comp1)
(Comp2)

∀x̄. ∀V, W x̄ ⊢ V RV W =⇒ x̄ ⊢ return V RΛ return W
∀x̄. ∀V, V ′ , W, W ′ . x̄ ⊢ V RV V ′ ∧ x̄ ⊢ W RV W ′ =⇒ x̄ ⊢ V W RΛ V ′ W ′

(Comp3)
(Comp4)

∀x̄. ∀x 6∈ x̄. ∀M, M ′ , N, N ′ .
x̄ ⊢ M RΛ M ′ ∧ x̄ ∪ {x} ⊢ N RΛ N ′ =⇒ x̄ ⊢ (M to x.N ) RΛ (M ′ to x.N ′ )
∀x̄. ∀σ ∈ Σ. ∀M1 , N1 , . . . , Mn , Nn .

(Comp5)

(∀i ∈ {1, . . . , n}. x̄ ⊢ Mi RΛ Ni ) =⇒ x̄ ⊢ σ(M1 , . . . , Mn ) RΛ σ(N1 , . . . , Nn )

(Comp6)

Figure 4: Compatibility Clauses.
Definition 21. Define the open extension operator mapping a closed relation over terms R to
the open relation R◦ (over terms) as follows: (x̄, M, N ) ∈ R◦ iff M, N ∈ Λ(x̄), and for all V̄ ,
M [x̄ := V̄ ] R N [x̄ := V̄ ] holds.
The notion of open extension for a closed relation over values can be defined in a similar way
(using the appropriate notion of substitution).
The notion of reflexivity, symmetry and transitivity straightforwardly extends to open λ-term
relation (see e.g. [35]).
Definition 22. Let R = (RΛ , RV ) be a λ-term relation. We say that R is compatible if the
clauses in Figure 4 hold. We say that R is a precongruence if it is a compatible preorder. We say
that R is a congruence if it is a compatible equivalence.
The following lemma will be useful.
Lemma 9. Let R = (RΛ , RV ) be a λ-term relation. If R is a preorder, then properties (Comp4),
(Comp5), (Comp6) are equivalent to their ‘unidirectional’ versions:
∀x̄. ∀V, V ′ , W. x̄ ⊢ V RV V ′ =⇒ x̄ ⊢ V W RΛ V ′ W
∀x̄. ∀V, W, W ′ . x̄ ⊢ W RV W ′ =⇒ x̄ ⊢ V W RΛ V W ′

(Comp4L)
(Comp4R)

∀x̄. ∀x 6∈ x̄. ∀M, M ′ , N. x̄ ⊢ M RΛ M ′ =⇒ x̄ ⊢ (M to x.N ) RΛ (M ′ to x.N )
(Comp5L)
∀x̄. ∀x ∈
6 x̄. ∀M, N, N ′ . x̄ ∪ {x} ⊢ N RΛ N ′ =⇒ x̄ ⊢ (M to x.N ) RΛ (M to x.N ′ ) (Comp5R)
∀x̄. ∀σ ∈ Σ. ∀M, N, M̄ , N̄ . x̄ ⊢ M RΛ N =⇒ x̄ ⊢ σ(M̄ , M, N̄ ) RΛ σ(M̄ , N, N̄ )

(Comp6C)

where in (Comp6C) M̄ , N̄ are possibly empty finite tuples of terms such that the sum of their
lengths is equal to the ariety of σ minus one.
Proof. The proof is straightforward. As a paradigmatic example, we show that clause (Comp5) is
equivalent to the conjunction of clauses (Comp5L) and (Comp5R). For the left to right implication,
we assume that both (Comp5) and x̄ ⊢ M RΛ M ′ hold, and show that x̄ ⊢ M to x.N RΛ M ′ to x.N
holds as well, thus proving that (Comp5) implies (Comp5L) (the proof that (Comp5) implies
(Comp5R) is morally the same). To prove the thesis, we observe that since R is reflexive, we
have x̄ ∪ {x} ⊢ N RΛ N . Applying (Comp5) to the latter and x̄ ⊢ M RΛ M ′ , we conclude
x̄ ⊢ M to x.N RΛ M ′ to x.N .
Now for the right to left direction. Assume (Comp5L) and (Comp5R) to be valid, and suppose both
x̄ ⊢ M RΛ M ′ and x̄ ∪ {x} ⊢ N RΛ N ′ to hold. We can apply (Comp5L) to the former, obtaining
x̄ ⊢ M to x.N RΛ M ′ to x.N , and (Comp5R) to the latter, obtaining x̄ ⊢ M ′ to x.N RΛ M ′ to x.N ′ .
The thesis now follows by transitivity of R.
It is useful to characterise compatible relations via the notion of compatible refinement.

19

bV x
x̄ ⊢ x R

x̄ ∪ {x} ⊢ M RΛ N
x 6∈ x̄
b V λx.N
x̄ ⊢ λx.M R

x ∈ x̄

x̄ ⊢ V RV V ′

x̄ ⊢ V RV W
x̄ ⊢ return V RΛ return W
x̄ ⊢ M RΛ M ′

x̄ ∪ {x} ⊢ N RΛ N ′
x 6∈ x̄
b Λ M ′ to x.N ′
x̄ ⊢ M to x.N R

x̄ ⊢ W RV W ′

bΛ V ′W ′
x̄ ⊢ V W R

x̄ ⊢ M1 RΛ N1

x̄ ⊢ Mn RΛ Nn
b
x̄ ⊢ σ(M1 , . . . , Mn ) RΛ σ(N1 , . . . , Nn )
...

Figure 5: Compatible Refinement Rules.

b of
Definition 23. Let R = (RΛ , RV ) be a λ-term relation. Define the compatible refinement R
bΛ, R
b V ), where RΛ and RV are inductively defined by rules in Figure 5.
R as the pair (R
b ⊆ R holds.
Proposition 3. A λ-term relation R is compatible iff R

The above notion of precongruence can be justified by observing that when a relation R is a
preorder, being a precongruence does exactly mean to be closed under the term constructors of
the language. That could be formally expressed by saying that R is a precongruence if and only if
x̄ ⊢ M R N implies x̄ ⊢ C[M ] R C[N ], for any term context C[·]. Defining term contexts requires
some care. In particular, when dealing with the contextual preorder it is not possible to reason
modulo α-conversion, thus making definition syntactically involved (see [27, 26, 35] for details). As
remarked in [35], it is possible to avoid those difficulties by giving a coinductive characterisation of
the contextual preorder in the style of [27, 17]. Essentially, the contextual preorder (and, similarly
the contextual equivalence) is defined as the largest compatible and preadequate (see Definition
24) λ-term relation. It is then easy to provide a more syntactic definition of contextual preorder
and to prove that the two given definitions are equivalent [17, 27, 35].
The notion of adequacy defines the available observation on values. Being in an untyped
setting, it is customary not to observe them.

Definition 24. Let U denote V0 × V0 seen as a closed relation, i.e. the trivial relation relating
all values. We say that a relation R on terms is preadequate if
∅ ⊢ M R N =⇒ JM K ΓU JN K
where M, N ∈ Λ0 . That is, a relation R on terms is preadequate if whenever R relates two closed
terms, evaluating these programs produces the same side-effects. A λ-term relation R = (RΛ , RV )
is preadequate iff RΛ is.
Example 8. It is easy to check that the above notion of adequacy (together with the relators in
Example 5) captures standard notions of adequacy used for untyped λ-calculi.
• Consider a calculus without operation symbols and with operational semantics over (V0 )⊥ . A
relation is preadequate if whenever ∅ ⊢ M R N , then if M converges, then so does N .
• Consider a nondeterministic calculus with operational semantics over PV0 . A relation is preadequate if whenever ∅ ⊢ M R N , then if there exists a value V to which M may converge (i.e.
V ∈ JM K), then there exists a value W to which N may converge (i.e. W ∈ JN K).
• Consider a probabilistic calculus with operational semantics over DV0 . A relation is preadequate
if whenever ∅ ⊢ M R N , then the probability of convergence of M is smaller or equal than the
probability of convergence of N .
Following [27], we shall define the Γ-contextual preorder as the largest λ-term relation that is
both compatible and preadequate.

20

Definition 25. LetSCA be the set of relations on terms that are both compatible and preadequate.
Then define ≤Γ as CA.
Proposition 4. The Γ-contextual preorder ≤Γ is a compatible and preadequate preorder.

Proof. We prove that ≤Γ ∈ CA. First of all note that CA contains the open identity relation. In
fact, the latter is clearly compatible. To see it is also preadequate suppose ∅ ⊢ M =Λ0 M so that
JM K =T V0 JM K. By (Rel-1), we have =T V0 ⊆ Γ(=V0 ). Moreover, by very definition of U, we also
have =V0 ⊆ U so that we can conclude JM K ΓU JM K, by monotonicity of Γ. As a consequence,
≤ Γ satisfies (Comp1). Observe also that (Comp1) implies, in particular, reflexivity of ≤Γ .
We now show that ≤Γ satisfies (Comp2). Suppose (x̄ ∪ {x}, M, N ) ∈≤Γ . That means there exists
a λ-term relation R = (RΛ , RV ) ∈ CA such that (x̄ ∪ {x}, M, N ) ∈ RΛ . Since R is compatible it
satisfies (Comp2), and thus we have (x̄, λx.M, λy.N ) ∈ RV . It then follows (x̄, λx.M, λx.N ) ∈≤Γ
(i.e. in its value component). Similarly, we can prove that ≤Γ satisfies (Comp3).
This approach does not work neither for (Comp4), (Comp5) nor for (Comp6). The reason
is that all these clauses are multiple premises implications (and that badly interacts with the
existential information obtained from being in ≤Γ ). Nonetheless, we can appeal to Lemma 9 to
replace clauses (Comp4)-(Comp6) to single premiss implications (for which the proof works as
for previous compatibility conditions). In order to use Lemma 9, we need to prove that ≤Γ is
transitive, and thus a preorder. For, it is sufficient to prove that CA is closed under relation
composition. The proof is rather standard and we just prove a couple of cases as examples.
We first show that if R = (RΛ , RΛ ) and S = (SΛ , SV ) are preadequate, then so is S ◦ R =
(SΛ ◦ RΛ , SV ◦ RV ). Suppose ∅ ⊢ M RΛ L and ∅ ⊢ L SΛ N . Since both R and S are preadequate,
we have JM K ΓU JLK and JLK ΓU JN K. By very definition of relator we have ΓU ◦ ΓU ⊆ Γ(U ◦ U).
The latter is contained in ΓU, since Γ is monotone and we trivially have U ◦ U.
Proving that the composition of compatible relations is compatible is a straightforward exercise.
For instance, we show that if relations R = (RΛ , RV ), S = (SΛ , SV ) satisfy (Comp5), then so does
S ◦ R. For, suppose x̄ ⊢ M (SΛ ◦ RΛ ) M ′ and x̄ ∪ {x} ⊢ N (SΛ ◦ RΛ ) N ′ . As a consequence, we
have
x̄ ⊢ M RΛ M ′′
x̄ ⊢ M ′′ SΛ M ′

(1)
(2)

x̄ ∪ {x} ⊢ N RΛ N ′′
x̄ ∪ {x} ⊢ N ′′ SΛ N ′ .

(3)
(4)

From (1) and (3) we infer x̄ ⊢ M to x.N RΛ M ′′ to x.N ′′ , since R satisfies (Comp5). Similarly,
from (2) and (4) we infer x̄ ⊢ M ′′ to x.N ′′ SΛ M ′ to x.N ′ . We can conclude x̄ ⊢ M to x.N (SΛ ◦
RΛ ) M ′ to x.N ′ .
Finally, we define the notion of an applicative Γ-simulation observing that the collection of
closed terms and values, together with the operational semantics defined in previous section,
carries an ATS structure.
Definition 26. A closed relation R = (RΛ , RV ) respects values if for all closed values V, W ,
V RV W implies V U RΛ W U , for any closed value U .
Definition 27. Define the ATS of closed λ-terms as follows:
• The state space is given by the pair (Λ0 , V0 );
• The evaluation function is J·K : Λ0 → T V0 ;
• The application function · : V0 → V0 → Λ0 is defined as term application: V · W = V W .
As a consequence, we can apply the general definition of applicative Γ-simulation to the ATS
of λ-terms. Instantiating the general definition of applicative Γ-simulation we obtain:
Definition 28. Let Γ be a relator for the monad T . A closed relation R = (RΛ , RV ) is an
applicative Γ-simulation if:
21

• M RΛ N =⇒ JM K ΓRV JN K;
• R respects values.
We can then define applicative Γ-similarity -Γ as the largest applicative Γ-simulation, which
we know to be a preorder by Proposition 2. Most of the time the relator Γ will be fixed; in those
cases we will often write - in place of -Γ .
Example 9. It is immediate to see that using the relators in Example 5 we recover well-known
notions of simulation and bisimulation.
We want to prove that applicative similarity is a sound proof technique for contextual preorder. That is, we want to prove that -Γ ⊆ ≤Γ holds. The relation ≤Γ being defined as the
largest preadequate compatible relation, the above inclusion is established by proving that -Γ is
a precongruence.

7

Howe’s Method and Its Soundness

In this section we generalise Howe’s technique to show that applicative similarity is a precongruence, thus a sound proof technique for the contextual preorder. Our generalisation shows how
Howe’s method crucially (but only!) depends on the structure of the monad modelling side-effects
and the relators encoding their associated notion of observation.
Definition 29. Let R be a closed λ-term relation. The Howe extension RH of R is defined as
b
the least relation S such that S = R◦ ◦ S.
It was observed in [28] that the above equation actually defines a unique relation.

Lemma 10. Let R be a closed λ-term relation. Then there is a unique relation S such that
b
S = R◦ ◦ S.

As a consequence, RH can be characterised both inductively and coinductively. Here we give
two (well-known) equivalent inductive characterisations of RH .

Lemma 11. The following are equivalent and all define the relation RH .
H
1. The Howe extension RH = (RH
Λ , RV ) of R is defined as the least relation closed under the
following rules:
d
H L
x̄ ⊢ M R
Λ

d
H U
x̄ ⊢ V R
V

x̄ ⊢ L R◦Λ N

x̄ ⊢ M RH
Λ N

x̄ ⊢ U R◦V W

x̄ ⊢ V RH
V W

2. The Howe extension RH of R is the relation inductively defined by rules in Figure 6.
Proof. It is easy to see that the functional F on λ-term relations associated to Definition 29 (i.e.
b is also the functional induced by rules in point 1. We can prove by
defined by F (S) = R◦ ◦ S)
induction the equivalence between the relations defined in point 1 and point 2 (in fact, these are
both defined inductively). This is tedious but easy, and thus the proof is omitted.
The following lemma states some nice properties of Howe’s lifting of preorder relations. The
proof is standard and can be found in, e.g., [10].
Lemma 12. Let R be a preorder. The following hold:
1. R ◦ RH ⊆ RH .
2. RH is compatible, and thus reflexive.
3. R ⊆ RH .
Remark 8. To prove properties 2 and 3 it is actually sufficient to require R to be reflexive,
whereas property 1, which we refer to transitivity of RH wrt R, requires R to be transitive. It is
easy to see that a compatible relation is also reflexive.
22

x̄ ⊢ x R◦V V
x̄ ⊢ x RH
V V
x̄ ∪ {x} ⊢ M RH
Λ L

(How1)

x̄ ⊢ λx.L R◦V V

(How2)

x̄ ⊢ λx.M RH
V V
x̄ ⊢ V RH
V W

x̄ ⊢ return W R◦Λ N

x̄ ⊢ return V RH
Λ N
′
x̄ ⊢ W RH
V W

′
x̄ ⊢ V RH
V V

(How3)

x̄ ⊢ V ′ W ′ R◦Λ N

x̄ ⊢ V W RH
Λ N
x̄ ⊢ M RH
Λ L

′
x̄ ∪ {x} ⊢ M ′ RH
Λ L

(How4)

x̄ ⊢ L to x.L′ R◦Λ N

x̄ ⊢ M to x.M ′ RH
Λ N
x̄ ⊢ Mk RH
Λ Nk (∀k ≥ n)

x̄ ⊢ σ(N1 , . . . , Nn ) R◦Λ N

x̄ ⊢ σ(M1 , . . . , Mn ) RH
Λ N

(How5)

(How6)

Figure 6: Howe’s Extension Rules.
We now consider the Howe extension -H
Γ of applicative Γ-similarity. Since -Γ is a preorder
(Proposition 2), -H
is
a
compatible
relation
containing -Γ .
Γ
Definition 30. A λ-term relation R = (RΛ , RV ) is value-substitutive if x ⊢ M RΛ N and
∅ ⊢ V RV W imply ∅ ⊢ M [x := V ] RΛ N [x := W ].
Lemma 13. The relation -H
Γ is value-substitutive.
Proof. The proof is standard, see e.g. [10].
Summing up, we have defined a compatible relation -H
Γ which is value-substitutive and contains
-Γ . As a consequence, to prove that the latter is compatible it is sufficient to prove -H
Γ ⊆-Γ . We
can proceed coinductively, showing that -H
is
an
applicative
Γ-simulation.
This
is
proved
via the
Γ
so-called Key Lemma. Before proving the Key Lemma it is useful to spell out basic facts on the
Howe extension of applicative similarity that we will extensively use. In the following we assume
to have fixed a relator Γ, thus omitting subscripts. Let Γ be a relator.
Lemma 14. The following hold:
1. - ◦ -H ⊆ -H .
2. (Γ -) ◦ (Γ -H ) ⊆ Γ -H .
H
Lemma 15 (Key Lemma). Let -H = (-H
Λ , -V ) be the Howe extension of applicative similarity.
H
H
If ∅ ⊢ M -Λ N and M ⇓n X, then X Γ -V JN K.

Proof. We proceed by induction on the derivation of the judgment M ⇓n X.
Case (bot). Suppose to have M ⇓0 ⊥. We are done since Γ is inductive, and thus ⊥ Γ -H
V JN K
trivially holds (see property (ω-comp 2)).
Case (ret). Suppose to have return V ⇓n+1 η(V ). By hypothesis we have ∅ ⊢ return V -H
Λ N,
so that the latter must have been obtained as the conclusion of an instance of rule (How3).
As a consequence, we have ∅ ⊢ V -H
V W and return W -Λ N , for some value W . We
η(W ) from ∅ ⊢ V -H
can now appeal to (Lax-Unit), thus inferring η(V ) Γ -H
V W . By
V
very definition of applicative similarity, return W -Λ N implies Jreturn W K Γ -V JN K, i.e.
23

η(W ) Γ -V JN K. Therefore, we have η(V ) (Γ -V ) ◦ (Γ -H
V ) JN K, from which the thesis
follows by Lemma 14.
Case (app). Suppose the judgment (λx.M )V ⇓n+1 X has been obtained from the judgment
M [x := V ] ⇓n X. By hypothesis we have ∅ ⊢ (λx.M )V -H
Λ N , meaning that the latter
must have been obtained as the conclusion of an instance of (How4). We thus obtain ∅ ⊢
H
λx.M -H
V W , ∅ ⊢ V -V U and W U -Λ N , for values W, U . Looking at the first of
these three judgments, we see that it must be the conclusion of an instance of rule (How2).
H
Therefore, we have {x} ⊢ M -H
is value-substitutive, from
Λ L and λx.L -V W . Since H
H
{x} ⊢ M -Λ L and ∅ ⊢ V -V U we conclude ∅ ⊢ M [x := V ] -H
Λ L[x := U ]. We
can now apply the induction hypothesis on the latter and M [x := V ] ⇓n X, obtaining
X Γ(-H
V ) JL[x := U ]K. Since - respects values, from λx.L -V W we infer (λx.L)U -Λ W U ,
which gives, by very definition of applicative similarity, J(λx.L)U K Γ(-V ) JW U K. By Lemma
6, J(λx.L)U K = JL[x := U ]K, and thus, X Γ(-H
V ) JW U K, by Lemma 14. Finally, from
W U -V N we obtain JW U K Γ(-V ) JN K, which allows us to conclude X Γ(-V ) JN K by
Lemma 14.
Case (seq). Suppose the judgment (M to x.M ′ ) ⇓n+1 X»=(V 7→ YV ) has been obtained from
M ⇓n X and M ′ [x := V ] ⇓n YV . By hypothesis we have ∅ ⊢ M to x.M ′ -H
Λ N , which must
′
H
′
have been obtained via an instance of rule (How5) thus giving ∅ ⊢ M -H
Λ L, {x} ⊢ M -Λ L
′
and ∅ ⊢ L to x.L -Λ N . We can apply the induction hypothesis on M ⇓n X and
H
∅ ⊢ M -H
Λ L obtaining X Γ(-V ) JLK. We now claim to have
′
X»=(V 7→ YV ) Γ(-H
V ) JLK»=(V 7→ JL [x := V ]K).

The latter is equal to JL to x.L′ K, by Lemma 6. Besides, ∅ ⊢ L to x.L′ -Λ N entails
JL to x.L′ K Γ(-V ) JN K: we conclude X»=(V 7→ YV ) Γ(-H
V ) JN K, by Lemma 14.
The above claim directly follows from (Lax-Bind). In fact, since X Γ(-H
V ) JLK holds, by
H
′
(Lax-Bind) it is sufficient to prove that V -H
W
implies
Y
Γ()
JL
[x
:= W ]K. Assume
V
V
V
H
′
H
′
V -H
W
,
i.e.
∅
⊢
V
W
.
The
latter,
together
with
{x}
⊢
M
L
,
implies
∅ ⊢ M ′ [x :=
V
V
Λ
H
′
H
V ] -Λ L [x := W ], since - is value-substitutive. We can finally apply the inductive
hypothesis on the latter and M ′ [x := V ] ⇓n YV , thus concluding the wanted thesis.
Case (op). Suppose the judgment σ(M1 , . . . , Mk ) ⇓n+1 σ T (X1 , . . . , Xk ) has been obtained from
M1 ⇓n X1 , . . . , Mk ⇓n Xk . By hypothesis we have ∅ ⊢ σ(M1 , . . . , Mk ) -H
Λ N , which must
be the conclusion of an instance of rule (How6). As a consequence, judgments ∅ ⊢ M1 -H
Λ
N1 , . . . , ∅ ⊢ M k - H
Λ Nk and ∅ ⊢ σ(N1 , . . . , Nk ) -Λ N hold, for some terms N1 , . . . , Nk . We
can repeatedly apply the induction hypothesis on Mi ⇓n Xi and ∅ ⊢ Mi -H
Λ Ni , inferring
T
Xi Γ - H
JN
K,
for
all
i
∈
{1,
.
.
.
,
k}.
(Σ-comp)
allows
to
conclude
σ
(X
,
. . . , Xk ) Γ - H
i
1
V
V
T
σ (JN1 K, . . . , JNk K). By Lemma 6 the latter is equal to Jσ(N1 , . . . , Nk )K. Finally, from
∅ ⊢ σ(N1 , . . . , Nk ) -Λ N we infer Jσ(N1 , . . . , Nk )K Γ -V JN K from which the thesis follows
by Lemma 14.

Corollary 2. The relation -H
Γ is an applicative Γ-simulation.

F
H
H
Proof. Suppose M -H
Λ N . We have to prove JM K Γ -V JN K, i.e.
M⇓n X X Γ(-V ) JN K. The
H
latter follows from (ω-comp 1) by the Key Lemma. Finally, since - is compatible, it clearly
respects values.

Theorem 1. Similarity is a precongruence. Moreover, it is sound for contextual preorder ≤Γ .
Proof. We already know -Γ is a preorder. By previous corollary it follows that -Γ coincides with
-H
Γ , so that -Γ is also compatible, and thus a precongruence. Now for soundness. We have to
prove -Γ ⊆ ≤Γ . Since ≤Γ is defined as the largest preadequate compatible relation, it is sufficient
to prove that -Γ is preadequate (we have already showed it is compatible), which directly follows
from Sim-1, since -V ⊆ U.
24

8

Bisimilarity, Two-similarity and Contextual Equivalence

In this section we extend previous definitions and results to come up with sound proof techniques
for contextual equivalence. In particular, by observing that contextual equivalence always coincides with the intersection between the contextual preorder and its converse, Theorem ?? implies
that two-way similarity (i.e. the intersection between applicative similarity and its converse) is
contained in contextual equivalence. Applicative bisimilarity being finer than two-way similarity,
we can also conclude the former to be a sound proof technique for contextual equivalence.
Given a relator Γ, we can extract a canonical notion of Γ-bisimulation from the one of Γsimulation following the idea that a bisimulation is a relation R such that both R and Rc are
simulations. Recall that given a relator Γ we can define a converse operation Γc as Γc (R) =
(Γ(Rc ))c . Γc is indeed a relator. Similarly, we have proved that the intersection of relators is
again a relator.
Definition 31 (Γ-bisimulation). Given a relator Γ, we say that a relation R is a Γ-bisimulation
if it is a (Γ ∩ Γc )-simulation.
Proposition 5. Let Γ be a relator. A relation R is a Γ-bisimulation if and only if both R and
Rc are Γ-simulation.
Since, by Lemma 7, Γ ∩ Γc is a relator, we can define Γ-bisimilarity ∼Γ as (Γ ∩ Γc )-similarity.
Lemma 16. Let Γ be a relator. Γ-bisimilarity is an equivalence relation.
Proof. From Lemma 2 we know that ∼Γ is a preorder, whereas Lemma 7 shows that Γ ∩ Γc is
conversive. We conclude ∼Γ to be an equivalence relation.
Definition 32. Let Γ be a relator. Define Γ-cosimilarity %Γ as (-Γ )c . Define Γ two-way similarity
≃Γ as -Γ ∩ %Γ .
As usual, bisimilarity is finer than two-way similarity, meaning that ∼Γ ⊆ ≃Γ . Moreover,
taking Γ to be the simulation relator for the powerset monad (see Example 5), we have that ∼Γ
and ≃Γ do not coincide. See e.g. [27, 35].
Proposition 6. Let Γ be a relator. Then, ∼Γ ⊆ ≃Γ , and the inclusion is, in general, strict.
Recall that we have defined the Γ-contextual preorder ≤Γ as the largest relation that is both
compatible and Γ-preadequate. In analogy with what we did for simulation and bisimulation we
can give the following:
Definition 33. Let Γ be a relator. Define Γ-contextual equivalence ≡Γ as the largest relation that
is both compatible and (Γ ∩ Γc )-preadequate. That is, define ≡Γ as ≤Γ∩Γc .
Lemma 17. Let Γ be a relator. The cocontextual preorder ≥Γ is the largest relation that is both
Γc -preadequate and compatible.
Proof. First of all observe that if a relation R is Γ-preadequate, then Rc is Γc -preadequate. For,
suppose N Rc M , so that M R N . Since R is Γ-preadequate, we have JM K ΓU JN K, and thus
JN K (ΓU)c JM K. From U c = U we can conclude JN K Γc (U) JM K.
As a consequence, since ≤Γ is Γ-preadequate, we have that ≥Γ is Γc -preadequate. Moreover,
compatibility of ≤Γ implies compatibility of ≥Γ . It remains to prove that ≥Γ is the largest Γc preadequate and compatible relation. Let R be a Γc -preadequate and compatible relation. We
show R ⊆ ≥Γ by showing Rc ⊆ (≥Γ )c , i.e. Rc ⊆ ≤Γ . We proceed by coinduction showing
that Rc is Γ-preadequate and compatible. Compatibility of Rc directly follows from that of R.
Moreover, since R is Γc -preadequate, Rc is (Γc )c -preadequate. A simple calculation shows that
(Γc )c = Γ, so that we are done.
Although bisimilarity is finer than two-way similarity, this is not the case for contextual equivalence and the associated contextual preorders.
25

Proposition 7. Let Γ be a relator. Then, ≡Γ = ≤Γ ∩ ≥Γ .
Proof. First of all observe that since U = U c , a relation R is (Γ ∩ Γc )-preadequate if M RΛ N
implies that both JM K ΓU JN K and JN K ΓU JM K hold. Since ≡Γ is defined coinductively, to
prove that it contains ≤Γ ∩ ≥Γ it is sufficient to prove that ≤Γ ∩ ≥Γ is compatible and (Γ ∩ Γc )preadequate. Standard calculations show that the set of compatible relations is closed under
converse and intersection. Since ≤Γ is compatible, then so is ≥Γ and thus ≤Γ ∩ ≥Γ . We show
that ≤Γ ∩ ≥Γ is (Γ ∩ Γc )-preadequate. Suppose M (≤Γ ∩ ≥Γ ) N , so that both M ≤Γ N and
M ≥Γ N hold. From the former it follows JM K ΓU JN K, whereas from the latter we infer N ≤Γ M
and thus JN K ΓU JM K.
We now show that ≡Γ is contained in ≤Γ ∩ ≥Γ . Since ≤Γ is defined coinductively, to prove
≡Γ ⊆ ≤Γ it is sufficient to prove that ≡Γ is compatible and Γ-preadequate, which is indeed the
case. Thanks to Lemma 17 we can proceed coinductively to prove ≡Γ ⊆ ≥Γ as well. In fact, it is
sufficient to prove that ≡Γ is Γc -preadequate, which is trivially the case.
We can finally prove our soundness result.
Theorem 2 (Soundness). Let Γ be a relator. Two-way similarity ≃Γ is a congruence, and thus
sound for contextual equivalence ≡Γ . Since bisimilarity ∼Γ is finer than ≃Γ , it is sound for ≡Γ
as well.
Proof. From Theorem 1 we know that -Γ is a precongruence and that -Γ ⊆ ≤Γ . It follows %Γ
is a precongruence as well, and that %Γ ⊆ ≥Γ holds. We can conclude ≃Γ is a congruence and
≃Γ ⊆ ≡Γ . Since ∼Γ ⊆ ≃Γ , we also have ∼Γ ⊆ ≡Γ .
Noticeably, Theorem 2 can be seen as a proof of soundness for applicative bisimilarity in any
calculus ΛΣ which respects our requirements (see Definition 16, 17), and in particular for those
described in Example 5. The case of probabilistic calculi is illuminating: the apparent complexity
of all proofs of congruence from the literature [10, 9] has been confined to the proof that the relator
for subdistributions satisfies our axioms.
We can rely on Theorem 2 to prove that the terms W raise and Z raise , our example programs
from Section 2, being bisimilar, are indeed contextually equivalent. This only requires checking
that the map ΓD ◦ ΓE (see Example 5) is an inductive relator for the monad T X = D(X + E)
(which trivially carries a continuous Σ-algebra structure) respecting operations in Σ. This is an
easy exercise, and does not require any probabilistic reasoning.
Let (D, δ, (·)D ) denote the subdistributions monad, where we write f D for the Kleisli lifting of
f and δX for the Dirac distribution on the set X. Similarly, let (E, ǫ, (·)E ) denote the exception
monad, where we write f E for the Kleisli lifting of f , and ǫ for unit of E (see Example 2 for formal
definitions). Moreover, recall that we have relators ΓD and ΓE for D and E, respectively (see
Example 5). A standard calculation shows that we have the following:
Proposition 8. The functor D ◦ E induces a Kleisli triple (D ◦ E, η, (·)† ), where the unit η is
defined, for any set X, by ηX = δE(X) ◦ ǫX , whereas for a function f : X → DE(Y ) the Kleisli
extension f † of f is defined as (f∗ )D , where f∗ : E(X) → DE(Y ) is defined by
(
f (x)
if u = inl (x);
f∗ (u) =
δE(Y ) (u) otherwise.
Being defined as composition of relators, the map ΓD ◦ ΓE (also written ΓD ΓE ) is a relator for
the functor D ◦ E. We show that it also satisfies conditions (Lax-Unit) and (Lax-Bind), meaning
that it is a relator for D ◦ E, regarded as a monad. In order to have a more readable proof we use
a couple of simple auxiliary lemmas. In the following, let f : X → DEZ and g : Y → DEW be
maps, and R ⊆ X × Y , S ⊆ Z × W be relations.
Lemma 18. The following implication holds
R ⊆ (f × g)−1 (ΓD ΓE S) =⇒ ΓE R ⊆ (f∗ × g∗ )−1 (ΓD ΓE S)
26

Proof. Suppose R ⊆ (f × g)−1 (ΓD ΓE S) and let u ΓE R v. We prove f∗ (u) ΓD ΓE S g∗ (v). By very
definition of f∗ we have two possible cases.
Case 1. Suppose f∗ (u) = δ(u) and u = inr (e), for some e ∈ E (we will omit subscripts in the
Dirac’s functions). Since u ΓE R v we have v = inr (e) as well, meaning that g∗ (v) = δ(v).
The thesis can now be rewritten as δ(u) ΓD ΓE R δ(v). Since ΓD satisfies property (Lax-Unit),
we have ΓE S ⊆ (δE(X) × δE(Y ) )−1 (ΓD ΓE S), meaning that the thesis follows from u ΓE S v.
The latter indeed holds (since both u = inr (e) = v), by very definition of ΓE .
Case 2. Suppose now f∗ (u) = f (x) and u = inl (x), for some x ∈ X. The latter, together with
u ΓE R v implies v = inl (y), for some y ∈ Y such x R y. In particular, v = inl (y) implies
g∗ (v) = g(y). By hypothesis, x R y implies f (x) ΓD ΓE S g(y), i.e. f∗ (v) ΓD ΓE S g∗ (v).

Lemma 19. The following holds
R ⊆ (ηX × ηY )−1 (ΓD ΓE R).
Proof. Suppose x R y and recall that ηZ = δE(Z) ◦ ǫZ . Since ΓE satisfies property (Lax-Unit) (wrt
E), from x R y, we infer ǫX (x) ΓE R ǫY (y). We conclude that δE(X) (ǫX (x)) ΓD ΓE R δE(Y ) (ǫY (y))
holds, since ΓD satisfies (Lax-Bind) as well (wrt D).
Corollary 3. The map ΓD ◦ ΓE is a relator for the monad D ◦ E.
Proof. By previous lemma it is sufficient to prove that given R ⊆ (f × g)−1 (ΓD ΓE S) we have
ΓD ΓE R ⊆ (f † × g † )−1 (ΓD ΓE S), i.e. ΓD ΓE R ⊆ (f∗D × g∗D )−1 (ΓD ΓE S). Since ΓD is a relator
for the monad D, the latter is implied by ΓE R ⊆ (f∗ × g∗ )−1 (ΓD ΓE S), which itself follows from
R ⊆ (f × g)−1 (ΓD ΓE S) and Lemma 18.
To conclude, we have to show that the monad D ◦ E and the relator ΓD ◦ ΓE have the required
order-theoretic properties. First of all note that the monad D ◦ E carries a continuous Σ-algebra
structure, with the ωCPPO order given by the functor D. Moreover, trivial calculations show that
the monad is ωCPPO-enriched (this
F essentiallyFfollows from the order-enrichment of D, together
with the validity of the equation ( n<ω fn )∗ = n<ω fn∗ ), and thus the associated bind operator
is continuous. Finally, it is immediate to observe that ΓD ◦ ΓE is inductive, since ΓD is.

9

Related Work

As mentioned in the Introduction, this is certainly not the first paper about program equivalence
for higher-order effectful calculi. Denotational semantics of calculi having this nature, has been
studied since Moggi’s seminal work [32], thus implicitly providing a notion of equivalence. All this
has been given a more operational flavour starting with Plotkin and Power account on adequacy
for algebraic effects [36], from which the operational semantics presented in this paper is greatly
inspired. The literature also offers abstract accounts on logical relations for effectful calculi. The
first of them is due to Goubault-Larrecq, Lasota and Nowak [18], which is noticeably able to deal
with nondeterministic and probabilistic effects, but also with dynamic name creation, for which
applicative bisimilarity is known to be unsound. Another piece of work which is related to ours is
due to Johann, Simpson, and Voigtländer [20], who focused on algebraic effects and observational
equivalence, and their characterisation via CIU theorems and a form of logical relation based ⊤⊤lifting. In both cases, the target language is typed. Similar in spirit to our approach (which is
based on the notion of relator), the work of Katsumata and Sato [22] analyses monadic lifting of
relations in the context of ⊤⊤-lifting.
Although no abstract account exists on applicative coinductive techniques for calculi with
algebraic effects, some work definitely exists in some specific cases. As a noticeable example,
the works by Ong [34] and Lassen [27] deal with nondeterminism, and establish soundness in all
27

relevant cases, although full abstraction fails. The first author, together with Alberti, Crubillé and
Sangiorgi [10, 9] have studied the probabilistic case, where full abstraction can indeed be obtained
if call-by-value evaluation is employed.

10

Conclusion

This is the first abstract account on applicative bisimilarity for calculi with effects. The main
result is an abstract soundness theorem for a notion of applicative similarity which can be naturally
defined as soon as a monad and an associated relator are given which on the one hand serve to
give an operational semantics to the algebraic operations, and on the other need to satisfy some
mild conditions in order for similarity to be a precongruence. Soundness of bisimilarity is then
obtained as a corollary. Many concrete examples are shown to fit into the introduced axiomatics.
A notable example is the output monad, for which a definition of applicative similarity based
on labeled transition systems as in e.g. [8] is unsound, a fact that the authors discovered after
noticing the anomaly, and not vice versa. Nevertheless, we defined a different notion of applicative
similarity that fits into our framework and whose associated notion of bisimilarity (Definition 31)
coincide with the usual notion of bisimilarity.
A question that we have not addressed in this work, but which is quite natural, is whether
an abstract full-abstraction result could exist, analogously to what, e.g., Johann, Simpson, and
Voigtländer obtained for their notion of logical relation. This is a very interesting topic for future
work. It is however impossible to get such a theorem without imposing some further, severe,
constraints on the class of effects (i.e. monads and relators) of interest, e.g., applicative bisimilarity
is well-known not to be fully-abstract in calculi with nondeterministic effects, which perfectly fit
in the picture we have drawn in this paper. A promising route towards this challenge would be
to understand which class of tests (if any) characterise applicative bisimilarity, depending on the
underlying monad and relator, this way generalising results by van Breugel, Mislove, Ouaknine
and Worrell [42] or Ong [9].
Finally, environmental bisimilarity is known [24] to overcome the limits of applicative bisimilarity in presence of information hiding. Studying the applicability of the methodology developed
in this work to environmental bisimilarity is yet another interesting topic for future researches.

Acknowledgment
The authors would like to thank Raphaëlle Crubillé and the anonymous reviewers for the many
useful comments, some of which led to a substantial improvement of our work. Special thanks go
to Davide Sangiorgi, Ryo Tanaka, and Valeria Vignudelli for many insightful discussions about
the topics of this work.

References
[1] Samson Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in
Functional Programming, pages 65–117. Addison Wesley, 1990.
[2] Samson Abramsky and Achim Jung. Domain theory. In Handbook of Logic in Computer
Science, pages 1–168. Clarendon Press, 1994.
[3] Andrew W. Appel and David A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657–683, 2001.
[4] Hendrik P. Barendregt. The lambda calculus: its syntax and semantics. Studies in logic and
the foundations of mathematics. North-Holland, 1984.
[5] M. Barr. Relational algebras. Lect. Notes Math., 137:39–55, 1970.

28

[6] Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann. Relational semantics
for effect-based program transformations: higher-order store. In Proc. of PPDP 2009, pages
301–312, 2009.
[7] Ales Bizjak and Lars Birkedal. Step-indexed logical relations for probability. In Proc. of
FOSSACS 2015, pages 279–294, 2015.
[8] Roy L. Crole and Andrew D. Gordon. Relating operational and denotational semantics for
input/output effects. Mathematical Structures in Computer Science, 9(2):125–158, 1999.
[9] Raphaëlle Crubillé and Ugo Dal Lago. On probabilistic applicative bisimulation and callby-value λ-calculi. In Proc. of ESOP 2014, volume 8410 of LNCS, pages 209–228. Springer,
2014.
[10] Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On coinductive equivalences for higherorder probabilistic functional programs. In Proc. of POPL 2014, pages 297–308, 2014.
[11] Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda
calculus. RAIRO - Theor. Inf. and Applic., 46(3):413–450, 2012.
[12] Vincent Danos and Russell Harmer. Probabilistic game semantics. ACM Transactions on
Computational Logic, 3(3):359–382, 2002.
[13] Brian A. Davey and Hilary A. Priestley. Introduction to lattices and order. Cambridge
University Press, 1990.
[14] Ugo de’Liguoro and Adolfo Piperno. Non deterministic extensions of untyped lambdacalculus. Inf. Comput., 122(2):149–177, 1995.
[15] Joseph A. Goguen, James W. Thatcher, Eric G. Wagner, and Jesse B. Wright. Initial algebra
semantics and continuous algebras. J. ACM, 24(1):68–95, 1977.
[16] Sergey Goncharov and Lutz Schröder. A relatively complete generic hoare logic for orderenriched effects. In Proc. of LICS 2013, pages 273–282. IEEE Computer Society, 2013.
[17] Andrew D. Gordon. A tutorial on co-induction and functional programming. In Workshops
in Computing, pages 78–95. Springer London, September 1994.
[18] Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic
types. Mathematical Structures in Computer Science, 18(6):1169–1217, 2008.
[19] Douglas J. Howe. Proving congruence of bisimulation in functional programming languages.
Inf. Comput., 124(2):103–112, 1996.
[20] Patricia Johann, Alex Simpson, and Janis Voigtländer. A generic operational metatheory for
algebraic effects. In Proc. of LICS 2010, pages 209–218. IEEE Computer Society, 2010.
[21] Claire Jones. Probabilistic Non-determinism. PhD thesis, University of Edinburgh, 1990.
Available as Technical Report CST-63–90.
[22] Shin-ya Katsumata and Tetsuya Sato. Preorders on Monads and Coalgebraic Simulations,
pages 145–160. Springer, 2013.
[23] Gregory M. Kelly. Basic concepts of enriched category theory. Reprints in Theory and
Applications of Categories, (10):1–136, 2005.
[24] Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. From applicative to environmental
bisimulation. Electr. Notes Theor. Comput. Sci., 276:215–235, 2011.
[25] Alexander Kurz and Jiri Velebil. Relation lifting, a survey. J. Log. Algebr. Meth. Program.,
85(4):475–499, 2016.
29

[26] Søren B. Lassen. Relational reasoning about contexts. In Andrew D. Gordon and Andrew M.
Pitts, editors, Higher Order Operational Techniques in Semantics, pages 91–136. 1998.
[27] Søren B. Lassen. Relational Reasoning about Functions and Nondeterminism. PhD thesis,
Dept. of Computer Science, University of Aarhus, May 1998.
[28] Paul Blain Levy. Infinitary Howe’s method. Electr. Notes Theor. Comput. Sci., 164(1):85–104,
2006.
[29] Paul Blain Levy. Similarity quotients as final coalgebras. In Proc. of FOSSACS 2011, volume
6604 of LNCS, pages 27–41, 2011.
[30] Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value
programming languages. Inf. Comput., 185(2):182–210, 2003.
[31] Saunders MacLane. Categories for the Working Mathematician. Springer-Verlag, 1971.
[32] Eugenio Moggi. Computational lambda-calculus and monads. In Proc. of (LICS 1989, pages
14–23. IEEE Computer Society, 1989.
[33] J. Morris. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, 1969.
[34] C.-H. Luke Ong. Non-determinism in a functional setting. In Proc. of LICS 1993, pages
275–286. IEEE Computer Society, 1993.
[35] Andrew M. Pitts. Howe’s method for higher-order languages. In D. Sangiorgi and J. Rutten,
editors, Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge Tracts
in Theoretical Computer Science, chapter 5, pages 197–232. Cambridge University Press,
November 2011.
[36] Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In Proc. of FOSSACS
2001, pages 1–24, 2001.
[37] Gordon D. Plotkin and John Power. Notions of computation determine monads. In Proc. of
FOSSACS 2002, pages 342–356, 2002.
[38] Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69–94, 2003.
[39] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci.,
249(1):3–80, 2000.
[40] Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley & Sons, Inc.,
New York, NY, USA, 1986.
[41] Albert Marchienus Thijs et al. Simulation and fixpoint semantics. Rijksuniversiteit Groningen,
1996.
[42] Franck van Breugel, Michael W. Mislove, Joël Ouaknine, and James Worrell. Domain theory,
testing and simulation for labelled markov processes. Theor. Comput. Sci., 333(1-2):171–197,
2005.

30

