On completeness of logical relations for monadic types ⋆
Sławomir Lasota1

⋆⋆

David Nowak2

Yu Zhang3 ⋆ ⋆ ⋆

arXiv:cs/0612106v1 [cs.LO] 21 Dec 2006

1

Institute of Informatics, Warsaw University, Warszawa, Poland
2
Research Center for Information Security,
National Institute of Advanced Industrial Science and Technology, Tokyo, Japan
3
Project Everest, INRIA Sophia-Antipolis, France

Abstract. Software security can be ensured by specifying and verifying security properties of software using formal methods with strong theoretical bases.
In particular, programs can be modeled in the framework of lambda-calculi, and
interesting properties can be expressed formally by contextual equivalence (a.k.a.
observational equivalence). Furthermore, imperative features, which exist in most
real-life software, can be nicely expressed in the so-called computational lambdacalculus. Contextual equivalence is difficult to prove directly, but we can often use
logical relations as a tool to establish it in lambda-calculi. We have already defined logical relations for the computational lambda-calculus in previous work.
We devote this paper to the study of their completeness w.r.t. contextual equivalence in the computational lambda-calculus.

1 Introduction
Contextual equivalence. Two programs are contextually equivalent (a.k.a. observationally equivalent) if they have the same observable behavior, i.e. an outsider cannot
distinguish them. Interesting properties of programs can be expressed using the notion
of contextual equivalence. For example, to prove that a program does not leak a secret,
such as the secret key used by an ATM to communicate with the bank, it is sufficient to
prove that if we change the secret, the observable behavior will not change [18,3,19]:
whatever experiment a customer makes with the ATM, he or she cannot guess information about the secret key by observing the reaction of the ATM. Another example is
to specify functional properties by contextual equivalence. For example, if sorted is a
function which checks that a list is sorted and sort is a function which sorts a list, then,
for all list l, you want the expression sorted(sort(l)) to be contextually equivalent to the
expression true. Finally, in the context of parameterized verification, contextual equivalence allows the verification for all instantiations of the parameter to be reduced to the
⋆

Partially supported by the RNTL project Prouvé, the ACI Sécurité Informatique Rossignol,
the ACI jeunes chercheurs “Sécurité informatique, protocoles cryptographiques et détection
d’intrusions”, and the ACI Cryptologie “PSI-Robuste”.
⋆⋆
Partially supported by the Polish K BN grant No. 4 T11C 042 25 and by the European Community Research Training Network Games. This work was performed in part during the author’s
stay at LSV.
⋆⋆⋆
This work was mainly done when the author was a PhD student under an MENRT grant on
ACI Cryptologie funding, École Doctorale Sciences Pratiques (Cachan).

verification for a finite number of instantiations (See e.g. [6] where logical relations are
one of the essential ingredients).
Logical relations. While contextual equivalence is difficult to prove directly because
of the universal quantification over contexts, logical relations [15,8] are powerful tools
that allow us to deduce contextual equivalence in typed λ-calculi. With the aid of the
so-called Basic Lemma, one can easily prove that logical relations are sound w.r.t. contextual equivalence. However, completeness of logical relations is much more difficult
to achieve: usually we can only show the completeness of logical relations for types up
to first order.
On the other hand, the computational λ-calculus [10] has proved useful to define
various notions of computations on top of the λ-calculus: partial computations, exceptions, state transformers, continuations and non-determinism in particular. Moggi’s
insight is based on categorical semantics: while categorical models of the standard λcalculus are cartesian closed categories (CCCs), the computational λ-calculus requires
CCCs with a strong monad. Logical relations for monadic types, which are particularly
introduced in Moggi’s language, can be derived by the construction defined in [2] where
soundness of logical relations is guaranteed.
However, monadic types introduce new difficulties. In particular, contextual equivalence becomes subtler due to the different semantics of different monads: equivalent
programs in one monad are not necessarily equivalent in another! This accordingly
makes completeness of logical relations more difficult to achieve in the computational
λ-calculus. In particular the usual proofs of completeness up to first order do not go
through.
Contributions. We propose in this paper a notion of contextual equivalence for the
computational λ-calculus. Logical relations for this language are defined according to
the general derivation in [2]. We then explore the completeness and we prove that for the
partial computation monad, the exception monad and the state transformer monad, logical relations are still complete up to first-order types. In the case of the non-determinism
monad, we need to restrict ourselves to a subset of first-order types. As a corollary, we
prove that strong bisimulation is complete w.r.t. contextual equivalence in a λ-calculus
with monadic non-determinism.
Not like previous work on using logical relations to study contextual equivalence
in models with computational effects [16,13,11], most of which focus on computations
with local states, our work in this paper is based on a more general framework for
describing computations, namely the computational λ-calculus. In particular, very different forms of computations like continuations and non-determinism are studied, not
just those for local states.
Plan. The rest of this paper is structured as follows: we devote Section 2 to preliminaries, by introducing basic knowledge of logical relations in a simple version of typed
λ-calculus; then from Section 3 on, we move to the computational λ-calculus and we
rest on a set-theoretical model. In particular, Section 3.4 sketches out the proof scheme

of completeness of logical relations for monadic types and shows the difficulty of getting a general proof; we then switch to case studies and we explore, in Section 4, the
completeness in the computational λ-calculus for a list of common monads: partial
computations, exceptions, state transformers, continuations and the non-determinism;
the last section consists of a discussion on related work and perspectives.

2 Logical relations for the simply typed λ-calculus
2.1 The simply typed λ-calculus λ→
Let λ→ be a simple version of typed λ-calculus:
Types:
Terms:

τ, τ ′ , ... ::= b | τ → τ ′
t, t′ , ... ::= x | c | λx · t | tt′

where b ranges over a set of base types (booleans, integers, etc.), c over a set of constants
and x over a set of variables. We write t[u/x] the result of substituting the term u for free
occurrences of the variable x in the term t. Typing judgments are of the form Γ ⊢ t : τ
where Γ is a typing context, i.e. a finite mapping from variables to types. We say that
x : τ is in Γ whenever Γ (x) = τ . We write Γ, x : τ for the typing context which agrees
with Γ except that it maps x to τ . Typing rules are as standard. We consider the set
theoretical semantics of λ→ . The semantics of any type τ is given by a set Jτ K. Those
sets are such that Jτ → τ ′ K is the set of all functions from Jτ K to Jτ ′ K, for all types τ
and τ ′ . A Γ -environment ρ is a map such that, for every x : τ in Γ , ρ(x) is an element
of Jτ K. We write ρ[x := a] for the environment which agrees with ρ except that it maps
x to a. We write [x := a] for the environment just mapping x to a. Let t be a term such
that Γ ⊢ t : τ is derivable. The denotation of t, w.r.t. a Γ -environment ρ, is given as
usual by an element JtKρ of Jτ K. We write JtK instead of JtKρ when ρ is irrelevant, e.g.,
when t is a closed term. When given a value a ∈ Jτ K, we say that it is definable if and
only if there exists a closed term t such that ⊢ t : τ is derivable and a = JtK.
Let Obs be a subset of base types, called observation types, such as booleans,
integers, etc. A context C is a term such that x : τ ⊢ C : o is derivable, where o
is an observation type. We spell the standard notion of contextual equivalence in a
denotational setting: two elements a1 and a2 of Jτ K, are contextually equivalent (written
as a1 ≈τ a2 ), if and only if for any context C such that x : τ ⊢ C : o (o ∈ Obs) is
derivable, JCK[x := a1 ] = JCK[x := a2 ]. We say that two closed terms t1 and t2 of
the same type τ are contextually equivalent whenever Jt1 K ≈τ Jt2 K. Without making
confusion, we shall use the same notation ≈τ to denote the contextual equivalence
between terms. We also define a relation ∼τ : for every pair of values a1 , a2 ∈ Jτ K,
a1 ∼τ a2 if and only if a1 , a2 are definable and a1 ≈τ a2 .
2.2 Logical relations
Essentially, a (binary) logical relation [8] is a family (Rτ )τ type of relations, one for
each type τ , on Jτ K such that related functions map related arguments to related results. More formally, it is a family (Rτ )τ type of relations such that for every f1 , f2 ∈

Jτ → τ ′ K,

f1 Rτ →τ ′ f2

⇐⇒

∀a1 , a2 ∈ Jτ K . a1 Rτ a2 =⇒ f1 (a1 ) Rτ ′ f2 (a2 )

There is no constraint on relations at base types. In λ→ , once the relations at base types
are fixed, the above condition forces (Rτ )τ type to be uniquely determined by induction
on types. We might have other complex types, e.g., products in variations of λ→ , and
in general, relations of these complex types should be also uniquely determined by
relations of their type components. For instance, pairs are related when their elements
are pairwise related. A unary logical relation is also called a logical predicate.
A so-called Basic Lemma comes along with logical relations since Plotkin’s work
[15]. It states that if Γ ⊢ t : τ is derivable, ρ1 , ρ2 are two related Γ -environments, and
every constant is related to itself, then JtKρ1 Rτ JtKρ2 . Here two Γ -environments ρ1 ,
ρ2 are related by the logical relation, if and only if ρ1 (x) Rτ ρ2 (x) for every x : τ
in Γ . Basic Lemma is crucial for proving various properties using logical relations [8].
In the case of establishing contextual equivalence, it implies that, for every context C
such that x : τ ⊢ C : o is derivable (o ∈ Obs), JCK[x := a1 ] Ro JCK[x := a2 ] for
every pair of related values a1 , a2 in Jτ K. If Ro is the equality, then JCK[x := a1 ] =
JCK[x := a2 ], i.e., a1 ≈τ a2 . Briefly, for every logical relation (Rτ )τ type such that
Ro is the equality for every observation type o, logically related values are necessarily
contextually equivalent, i.e., Rτ ⊆ ≈τ for any type τ .
Completeness states the inverse: a logical relation (Rτ )τ type is complete if every
contextually equivalent values are related by this logical relation, i.e., ≈τ ⊆ Rτ for
every type τ . Completeness for logical relations is hard to achieve, even in a simple
version of λ-calculus like λ→ . Usually we are only able to prove completeness for
types up to first order (the order of types is defined inductively: ord(b) = 0 for any base
type b; ord(τ → τ ′ ) = max(ord(τ ) + 1, ord(τ ′ )) for function types). The following
proposition states the completeness of logical relations in λ→ , for types up to first order:
Proposition 1. There exists a logical relation (Rτ )τ type for λ→ , with partial equality
on observation types, such that if ⊢ t1 : τ and ⊢ t2 : τ are derivable, for any type τ up
to first order, t1 ≈τ t2 =⇒ Jt1 K Rτ Jt2 K.

Proof. Let (Rτ )τ type be the logical relation induced by Rb = ∼b at every base type b
and we show that it is complete for types up to first order.
The proof is by induction over τ . Case τ = b is obvious. Let τ = b → τ ′ . Take two
terms t1 , t2 of type b → τ ′ such that Jt1 K and Jt2 K are related by ≈b→τ ′ . Let f1 = Jt1 K
and f2 = Jt2 K. Assume that a1 , a2 ∈ JbK are related by Rb , therefore a1 ∼b a2 since
Rb = ∼b . Clearly, a1 and a2 are thus definable, say by terms u1 and u2 , respectively.
Then, for any context C such that x : τ ′ ⊢ C : o (o ∈ Obs) is derivable,
JCK[x := f1 (a1 )]
= JC[xu1 /x]K[x := f1 ]
= JC[xu1 /x]K[x := f2 ]
= JCK[x := f2 (a1 )]
= JC[t2 x/x]K[x := a1 ]
= JC[t2 x/x]K[x := a2 ]
= JCK[x := f2 (a2 )].

(since a1 = Ju1 K)
(since f1 ≈b→τ ′ f2 )
(since f2 = Jt2 K)
(since a1 ≈b a2 )

Hence f1 (a1 ) ≈τ ′ f2 (a2 ). Moreover, f1 (a1 ) and f2 (a2 ) are therefore definable by t1 u1
and t2 u2 respectively. By induction hypothesis, f1 (a1 ) Rτ ′ f2 (a2 ). Because a1 and a2
are arbitrary, we conclude that f1 Rb→τ ′ f2 .
⊓
⊔
Note that an equivalent way to state completeness of logical relations is to say that
there exists a logical relation (Rτ )τ type which is partial equality on observation types
and such that, for all first-order types τ , ∼τ ⊆ Rτ .

3 Logical relations for the computational λ-calculus
3.1 The computational λ-calculus λComp
From the section on, our discussion is based on another language — Moggi’s computational λ-calculus. Moggi defines this language so that one can express various forms
of side effects (exceptions, non-determinism, etc.) in this general framework [10]. The
computational λ-calculus, denoted by λComp , extends λ→ :
Types:
Terms:

τ, τ ′ , ... ::= b | τ → τ ′ | Tτ
t, t′ , ... ::= x | c | λx · t | tt′ | val(t) | let x ⇐ t in t′

An extra unary type constructor T is introduced in the computational λ-calculus: intuitively, a type Tτ is the type of computations of type τ . We call Tτ a monadic type in
the sequel. The two extra constructs val(t) and let x ⇐ t in t′ represent respectively
the trivial computation and the sequential computation, with the typing rules:
Γ ⊢t:τ
Γ ⊢ val(t) : Tτ

Γ ⊢ t : Tτ Γ, x : τ ⊢ t′ : Tτ ′
Γ ⊢ let x ⇐ t in t′ : Tτ ′

Note that the let construct here should not be confused with that in PCF: in λComp ,
we bind the result of the term t to the variable x, but they are not of the same type — t
must be a computation.
Moggi also builds a categorical model for the computational λ-calculus, using the
notion of monads [10]. Whereas categorical models of simply typed λ-calculi such as
λ→ are usually cartesian closed categories (CCCs), a model for λComp requires additionally a strong monad (T, η, µ, t) be defined over the CCC. Consequently, a monadic
type is interpreted using the monad T : JTτ K = T Jτ K, and each term in λComp has a
unique interpretation as a morphism in a CCC with the strong monad [10]. Semantics
of the two additional constructs can be given in full generality in a categorical setting
[10]: the denotations of val construct and let construct are defined by the follwoing
composites respectively:
JΓ ⊢ val(t) : Tτ K :

JΓ ⊢t:τ K

ηJτ K

JΓ K −−−−−→ Jτ K −−−→ T Jτ K,

hidJΓ K ,JΓ ⊢t1 :Tτ Ki
tJΓ K,Jτ K
JΓ ⊢ let x ⇐ t1 in t2 : Tτ ′ K : JΓ K −−−−−−−−−−−→ JΓ K × T Jτ K −−−−−→ T JΓ K × Jτ K
µJτ ′ K
T JΓ,x:τ ⊢t2 :Tτ ′ K
−−−−−−−−−−→ T T Jτ ′ K −−−→ T Jτ ′ K.

In particular, the interpretation of terms in the computational λ-calculus must satisfy
the following equations:
Jlet x ⇐ val(t1 ) in t2 Kρ = Jt2 [t1 /x]Kρ,

(1)

Jlet x2 ⇐ (let x1 ⇐ t1 in t2 ) in t3 Kρ = Jlet x1 ⇐ t1 in let x2 ⇐ t2 in t3 Kρ,(2)
Jlet x ⇐ t in val(x)Kρ = JtKρ.

(3)

We shall focus on Moggi’s monads defined over the category Set of sets and functions. Figure 1 lists the definitions of some concrete monads: partial computations, exceptions, state transformers, continuations and non-determinism. We shall write λPESCN
Comp
to refer to λComp where the monad is restricted to be one of these five monads.

Partial computation:

JTτ K = Jτ K ∪ {⊥}
Jval(t)Kρ = JtKρ
Jlet x ⇐ t1 in t2 Kρ =

Exception:

Continuation:

Non-determinism:

Jt2 Kρ[x := Jt1 Kρ], if Jt1 Kρ 6= ⊥
⊥,
if Jt1 Kρ = ⊥



Jt2 Kρ[x := Jt1 Kρ], if Jt1 Kρ 6∈ E
Jt1 Kρ,
if Jt1 Kρ ∈ E

JTτ K = Jτ K ∪ E
Jval(t)Kρ = JtKρ
Jlet x ⇐ t1 in t2 Kρ =

State transformer:



JTτ K = (Jτ K × St )St
Jval(t)Kρ = λ s · (JtKρ, s)
Jlet x ⇐ t1 in t2 Kρ = λ s · (Jt2 Kρ[x := a1 ])s1 ,
where a1 = π1 ((Jt1 Kρ)s), s1 = π2 ((Jt2 Kρ)s)
Jτ K
JTτ K = RR
Jval(t)Kρ = λ kJτ K→R · k(JtKρ)
Jlet x ⇐ t1 in t2 Kρ = λ kJτ2 K→R · (Jt1 Kρ)k′
where k′ is a function: λ v Jτ1 K · (Jt2 Kρ[x := v])k
JTτ K = Pfin (Jτ K)
Jval(t)Kρ = {JtKρ}
S
Jlet x ⇐ t1 in t2 Kρ =
Jt2 Kρ[x := a]
a∈Jt1 Kρ

Fig. 1. Concrete monads defined in Set

The computational λ-calculus is strongly normalizing [1]. The reduction rules in
λComp are called βc-reduction rules in [1], which, apart from standard β-reduction in
the λ-calculus, contains especially the following two rules for computations:
let x ⇐ val(t1 ) in t2 →βc t2 [t1 /x],
(4)
let x2 ⇐ (let x1 ⇐ t1 in t2 ) in t →βc let x1 ⇐ t1 in (let x2 ⇐ t2 in t).(5)
With respect to the βc rules, every term can be reduced to a term in the βc-normal form.
Considering also the following η-equality rule for monadic types [1]:
let x ⇐ t in t′ [val(x)/x′ ] =η t′ [t/x′ ],

(6)

we can write every term of a monadic type in the following βc-normal η-long form
let x1 ⇐ d1 u11 · · · u1k1 in · · · let xn ⇐ dn un1 · · · unkn in val(u),
where n = 0, 1, 2, . . ., every di (1 ≤ i ≤ n) is either a constant or a variable, u and
uij (1 ≤ i ≤ n, 1 ≤ j ≤ kj ) are all βc-normal terms or βc-normal-η-long terms (of
monadic types). In fact, the rules (4-6) just identify the equations (1-3) respectively.
Lemma 1. For every term t of type Tτ in λComp , there exists a βc-normal-η-long
term t′ such that Jt′ Kρ = JtKρ, for every valid interpretation J_Kρ (i.e., interpretations
satisfying the equations (1-3)).
Proof. Because the computational λ-calculus is strongly normalizing, we consider the
βc-normal form of term t and prove it by the structural induction on t.
– If t is either a variable, a constant or an application, according to the equation (3):
JtKρ = Jlet x ⇐ t in val(x)Kρ.

In particular, if t is an application t1 t1 , then t1 must be either a variable or a constant
since t is βc-normal. Therefore, the term let x ⇐ t in val(x) is in the βc-normalη-long form.
– If t is a trivial computation val(t′ ), by induction there is a βc-normal-η-long term
t′′ such that Jt′ Kρ = Jt′′ Kρ, for every valid ρ, then Jval(t′ )Kρ = Jval(t′′ )Kρ as
well.
– If t is a sequential computation let x ⇐ t1 in t2 , since it is βc-normal, t1 should
not be any val or let term — t1 must be of the form du1 · · · un (n = 0, 1, 2, . . .)
with d either a variable or a constant. By induction, there is a βc-normal-η-long
term t′2 such that Jt2 Kρ = Jt2 Kρ, for every valid ρ, then JtKρ = Jlet x ⇐ t′1 in t′2 Kρ
and the latter is in the βc-normal-η-long form.
⊓
⊔
3.2 Contextual equivalence for λComp
As argued in [3], the standard notion of contextual equivalence does not fit in the setting
of the computational λ-calculus. In order to define contextual equivalence for λComp ,
we have to consider contexts C of type To (o is an observation type), not of type o.
Indeed, contexts should be allowed to do some computations: if they were of type o,
they could only return values. In particular, a context C such that x : Tτ ⊢ C : o is
derivable, meant to observe computations of type τ , cannot observe anything, because
the typing rule for the let construct only allows us to use computations to build other
computations, never values. Taking this into account, we get the following definition:
Definition 1 (Contextual equivalence for λComp ). In λComp , two values a1 , a2 ∈ Jτ K
are contextually equivalent, written as a1 ≈τ a2 , if and only if, for all observable types
o ∈ Obs and contexts C such that x : τ ⊢ C : To is derivable, JCK[x := a1 ] =
JCK[x := a2 ]. Two closed terms t1 and t2 of type τ are contextually equivalent if and
only if Jt1 K ≈τ Jt2 K. We use the same notation
≈τ to denote the contextual equivalence for terms.

3.3 Logical relations for λComp
A uniform framework for defining logical relations relies on the categorical notion of
subscones [9], and a natural extension of logical relations able to deal with monadic
types was introduced in [2]. The construction consists in lifting the CCC structure and
the strong monad from the categorical model to the subscone. We reformulate this construction in the category Set. The subscone is the category whose objects are binary
relations (A, B, R ⊆ A × B) where A and B are sets; and a morphism between
two objects (A, B, R ⊆ A × B) and (A′ , B ′ , R′ ⊆ A′ × B ′ ) is a pair of functions
(f : A → A′ , g : B → B ′ ) preserving relations, i.e. a R b ⇒ f (a) R′ g(b).
The lifting of the CCC structure gives rise to the standard logical relations given in
Section 2.2 and the lifting of the strong monad will give rise to relations for monadic
types. We write T̃ for the lifting of the strong monad T . Given a relation R ⊆ A × B
and two computations a ∈ T A and b ∈ T B, (a, b) ∈ T̃ (R) if and only if there exists
a computation c ∈ T (R) (i.e. c computes pairs in R) such that a = T π1 (c) and b =
T π2 (c). The standard definition of logical relation for the simply typed λ-calculus is
then extended with:
(c1 , c2 ) ∈ RTτ

⇐⇒

(c1 , c2 ) ∈ T̃ (Rτ ).

(7)

This construction guarantees that Basic Lemma always holds provided that every constant is related to itself [2]. A list of instantiations of the above definition in concrete
monads is also given in [2]. Figure 2 cites the relations for those monads defined in
Figure 1.

Partial computation:
Exception:
State transformer:
Continuation:
Non-determinism:

c1 RTτ c2 ⇔ c1 Rτ c2 or c1 = c2 = ⊥
c1 RTτ c2 ⇔ c1 Rτ c2 or c1 = c2 ∈ E
where E is the set of exceptions
c1 RTτ c2 ⇔ ∀s ∈ St . π1 (c1 s) Rτ π1 (c2 s) & π2 (c1 s) = π2 (c2 s)
where St is the set of states
c1 RTτ c2 ⇔ c1 (k1 ) = c2 (k2 ) for every k1 , k2 such that
∀a1 , a2 . a1 Rτ a2 =⇒ k1 (a1 ) = k2 (a2 )
c1 RTτ c2 ⇔ (∀a1 ∈ c1 . ∃a2 ∈ c2 . a1 Rτ a2 ) &
(∀a2 ∈ c2 . ∃a1 ∈ c1 . a1 Rτ a2 )

Fig. 2. Logical relations for concrete monads

We restrict our attention to logical relations (Rτ )τ type such that, for any observation type o ∈ Obs, RTo is a partial equality. Such relations are called observational in
the rest of the paper.
Note that we require partial identity on To, not on o. But if we assume that denotation of val(_), i.e., the unit operation η, is injective, then that RTo is a partial equality
implies that Ro is a partial equality as well. Indeed, let a1 Ro a2 , and by Basic Lemma,
Jval(x)K[x := a1 ] RTo Jval(x)K[x := a2 ], that is to say ηJoK (a1 ) = ηJoK (a2 ). By injectivity of η, a1 = a2 .

Theorem 1 (Soundness of logical relations in λComp ). If (Rτ )τ
tional logical relation, then Rτ ⊆ ≈τ for every type τ .

type

is an observa-

It is straightforward from the Basic Lemma.
3.4 Toward a proof on completeness of logical relations for λComp
Completeness of logical relations for λComp is much subtler than in λ→ due to the
introduction of monadic types. We were expecting to find a general proof following the
general construction defined in [2]. However, this turns out extremely difficult although
it might not be impossible with certain restrictions, on types for example. The difficulty
arises mainly from the different semantics for different forms of computations, which
actually do not ensure that equivalent programs in one monad are necessarily equivalent
in another. For instance, consider the following two programs in λComp :
let x ⇐ t1 in let y ⇐ t2 in val(x),
let y ⇐ t2 in let x ⇐ t1 in val(x),
where both t1 and t2 are closed term. We can conclude that they are equivalent in the
non-determinism monad — they return the same set of possible results of t1 , no matter
what results t2 produces, but this is not the case in, e.g., the exception monad when t1
and t2 throw different exceptions.
Being with such an obstacle, we shall switch our effort to case studies in Section 4
and we explore the completeness of logical relations for a list of common monads,
precisely, all the monads listed in Figure 1. But, let us sketch out here a general structure
for proving completeness of logical relations in λComp . In particular, our study is still
restricted to first-order types, which, in λComp , are defined by the following grammar:
τ 1 ::= b | Tτ 1 | b → τ 1 ,
where b ranges over the set of base types.
Similarly as in Proposition 1 in Section 2.2, we investigate completeness in a strong
sense: we aim at finding an observational logical relation (Rτ )τ type such that if ⊢
t1 : τ and ⊢ t2 : τ are derivable and t1 ≈τ t2 , for any type τ up to first order, then
Jt1 K Rτ Jt2 K. Or briefly, ∼τ ⊆ Rτ , where ∼τ is the relation defined in Section 2. As in
the proof of Proposition 1, the logical relation (Rτ )τ type will be induced by Rb = ∼b ,
for any base type b. Then how to prove the completeness for an arbitrary monad T ?
Note that we should also check that the logical relation (Rτ )τ type , induced by
Rb = ∼b , is observational, i.e., a partial equality on To, for any observable type o.
Consider any pair (a, b) ∈ RTo = T̃ (Ro ). By definition of the lifted monad T̃ , there
exists a computation c ∈ T Ro such that a = T π1 (c) and b = T π2 (c). But Ro = ∼o ⊆
idJoK , hence the two projections π1 , π2 : Ro → JoK are the same function, π1 = π2 , and
consequently a = T π1 (c) = T π2 (c) = b. This proves that RTo is a partial equality.
As usual, the proof of completeness would go by induction over τ , to show ∼τ ⊆
Rτ for each first-order type τ . Cases τ = b and τ = b → τ ′ go identically as in λ→ .
The only difficult case is τ = Tτ ′ , i.e., the induction step:
∼τ ⊆ Rτ =⇒ ∼Tτ ⊆ RTτ

(8)

We did not find any general way to show (8) for an arbitrary monad. Instead, in the next
section we prove it by cases, for all the monads in Figure 1 except the non-determinism
monad. The non-determinism monad is an exceptional case where we do not have completeness for all first-order types but a subset of them. This will be studied separately in
Section 4.3.
At the heart of the difficulty of showing (8), we find an issue of definability at
monadic types in the set-theoretical model. We write def τ for the subset of definable
elements in Jτ K, and we eventually show that the relation between def Tτ and def τ can
be shortly spelled-out:
def Tτ ⊆ T def τ
(9)
for all the monads we consider in this paper. This is a crucial argument for proving
completeness of logical relations for monadic types, but to show (9), we need different
proofs for different monads. This is detailed in Section 4.1.

4 Completeness of logical relations for monadic types
4.1 Definability in the set-theoretical model of λPESCN
Comp
As we have seen in λ→ , definability is involved largely in the proof of completeness of
logical relations (for first-order types). This is also the case in λComp and it apparently
needs more concern due to the introduction of monadic types.
Despite we did not find a general proof for (9), it does hold for all the concrete
monads in λPESCN
Comp . To state it formally, let us first define a predicate Pτ on elements
of Jτ K, by induction on types:
– Pb = def b , for every base type b;
– PTτ = T (def τ ∩ Pτ );
– Pτ →τ ′ = {f ∈ Pτ →τ ′ | ∀a ∈ def τ , f (a) ∈ Pτ ′ }.

We say that a constant c (of type τ ) is logical if and only if τ is a base type or JcK ∈ Pτ .
ESCN
We then require that λP
contains only logical constants. Note that this restriction
Comp
is valid because the predicates PT τ and Pτ →τ ′ depend only on definability at type τ .
Some typical logical constants for monads in λPESCN
are as follows:
Comp
– Partial computation: a constant Ωτ of type Tτ , for every τ . Ωτ denotes the nontermination, so JΩτ K = ⊥.
– Exception: a constant raiseeτ of type Tτ for every type τ and every exception
e ∈ E. raiseeτ does nothing but raises the exception e, so Jraiseeτ K = e.
– State transformer: a constant updates of type Tunit for every state s ∈ St, where
unit is the base type which contains only a dummy value ∗. updates simply changes
the current state to s, so for any s′ ∈ St, Jupdates K(s′ ) = (∗, s).
– Continuation: a constant callkτ of type τ → T bool for every τ and every continuation k ∈ RJτ K . callkτ calls directly the continuation k — it behaves somehow likey “goto” command, so for any a ∈ Jτ K and any continuation k ′ ∈ Rbool,
q
callkτ (a)(k ′ ) = k(a).

– Non-determinism: a constant +τ of type τ → τ → Tτ for every non-monadic type
τ . +τ takes two arguments and returns randomly one of them — it introduces the
non-determinism, so for any a1 , a2 ∈ Jτ K, J+τ K(a1 , a2 ) = {a1 , a2 }.

1
We assume in the rest of this paper that the above constants are present in λPESCN
Comp .
Note that Pτ being a predicate on elements of Jτ K is equivalent to say that Pτ can
be seen as subset of Jτ K, but in the case of monadic types, PTτ (i.e., T (def τ ∩ Pτ )) is
not necessary a subset of JTτ K (i.e., T Jτ K). Fortunately, we prove that all the monads in
preserves inclusions, which ensures that the predicate P is well-defined:
λPESCN
Comp

Proposition 2. All the monads in λPESCN
preserve inclusions: A ⊆ B ⇒ T A ⊆ T B.
Comp
Proof. We check it for every monad in λPESCN
Comp :
– Partial computation: according to the monad definition, if A ⊆ B, then for every
c ∈ T A:
c ∈ T A ⇐⇒ c ∈ A or c = ⊥ =⇒ c ∈ B or c = ⊥ ⇐⇒ c ∈ T B.
– Exception: for every element c ∈ T A:
c ∈ T A ⇐⇒ c ∈ A or c ∈ E =⇒ c ∈ B or c ∈ E ⇐⇒ c ∈ T B.
– State transformer: for every a ∈ T A:
c ∈ T A ⇐⇒ ∀s ∈ St . π1 (cs) ∈ A =⇒ ∀s ∈ St . π1 (cs) ∈ B ⇐⇒ c ∈ T B.
A

– Continuation: this is a special case because apparently T A = RR is not a subset of
B
T B = RR , since they contain functions that are defined on different domains, but
we shall consider here the functions coinciding on the smaller set A as equivalent.
We say that two functions f1 and f2 defined on a domain B coincide on A (A ⊆ B),
written as f1 |A = f2 |A , if and only if for every x ∈ A, f1 (x) = f2 (x). Then for
every c ∈ T A:
∀k1 , k2 ∈ RB . k1 = k2 =⇒ k1 |A = k2 |A =⇒ c(k1 ) = c(k2 ),
so c is also function from RB to R, i.e., c ∈ T B.
– Non-determinism: for every c ∈ T A:
c ∈ T A ⇐⇒ ∀a ∈ c . a ∈ A =⇒ ∀a ∈ c . a ∈ B ⇐⇒ c ∈ T B.

⊓
⊔

Introducing such a constraint on constants is mainly for proving (9). Let us figure
out the proof. Take an arbitrary element c in def Tτ . By definition, there exists a closed
term t of type Tτ such that JtK = c. While it is not evident that c ∈ T def τ , we are expecting to show that JtK ∈ T def τ , by considering the βc-normal-η-long form of t, since
1

It is easy to check that each of these constants is related to itself, except callkτ for continuations. However, we still assume the presence of callkτ for the sake of proving completeness,
while we are not able to prove the soundness with it. Note that Theorem 1 and Theorem 2 still
hold, but they are not speaking of the same language.

λComp is strongly normalizing, Take the partial computation monad as an example,
where T def τ = def τ ∪ {⊥}. Consider the βc-normal-η-long form of t:
let x1 ⇐ d1 u11 · · · u1k1 in · · · let xn ⇐ dn un1 · · · unkn in val(u).
We shall make the induction on n. It is clear that JtK ∈ T def τ when n = 0. For
the induction step, we hope that the closed term d1 u11 · · · u1k1 (of type Tτ1 ) would
produce either ⊥ (the non-termination), or a definable result (of type τ1 ) so that we can
substitute x1 in the rest of the normal term with the result of d1 u11 · · · u1k1 and make
use of induction hypothesis. The constraint on constants helps here: to ensure that after
the substitution, the resulted term is still in the proper form so that the induction would
go through.
The following lemma shows that for every computation term t, JtK ∈ T def τ if t is
in a particular form, which is a more general form of βc-normal-η-long form.
Lemma 2. In λPESCN
Comp , JtK ∈ T def τ , for every closed computation term t (of type Tτ )
of the following form:
t ≡ let x1 ⇐ t1 w11 · · · w1k1 in · · · let xn ⇐ tn wn1 · · · wnkn in val(w),
where n = 0, 1, 2, . . . and ti (1 ≤ i ≤ n) is either a variable or a closed term such that
P(Jti K) holds, and w, wij (1 ≤ i ≤ n, 1 ≤ j ≤ ki ) are valid λPESCN
terms.
Comp
Proof. We prove it by induction on n, for every monad:

– Partial computation (T def τ = def τ ∪ {⊥}): if n = 0, it is clear that JtK ∈ T def τ .
When n > 0, because P(Jt1 K) holds (t1 must be closed), Jt1 w11 · · · w1k1 K ∈
T (def τ1 ∩ Pτ1 ). If Jt1 w11 · · · w1k1 K = ⊥, then JtK = ⊥ ∈ T def τ ; otherwise,
assume that Jt′1 K = Jt1 w11 · · · w1k1 K where t′1 is a closed term of type τ1 (assuming
that t1 w11 · · · w1k1 is of type Tτ1 ). According to the definition of P, P(Jt′1 K) holds.
Let t′ be another closed term:
′
′
′
′
in val(w[t′1 /x1 ]),
in · · · let xn ⇐ t′n wn1
· · · wnk
t′ ≡ let x2 ⇐ t′2 w21
· · · w2k
n
2
′
where t′i (2 ≤ i ≤ n) is either t′1 or ti , wij
≡ wij [t′1 /x1 ] (2 ≤ i ≤ n, 1 ≤ j ≤ ki ).
′
By induction, Jt K ∈ T def τ holds. Furthermore,

Jt′ K = Jlet x2 ⇐ t2 w21 · · · w2k2 in · · ·
let xn ⇐ tn wn1 · · · wnkn in val(w)K[x1 := Jt′1 K]
= Jlet x1 ⇐ t1 w11 · · · w1k1 in · · · let xn ⇐ tn wn1 · · · wnkn in val(w)K
= JtK,

hence JtK ∈ T def τ .
– Exception (T def τ = def τ ∪ E): if n = 0, clearly JtK ∈ T def τ . When n > 0,
because P(Jt1 K) holds, Jt1 w11 · · · w1k1 K ∈ T (def τ1 ∩ Pτ1 ). If Jt1 w11 · · · w1k1 K ∈
E, then JtK ∈ E ⊆ T def τ ; otherwise, exactly as in the case of partial computation,
build a term t′ . Similarly, we prove that JtK = Jt′ K ∈ T def τ by induction.

– State transformer (T def τ = (def τ × St)St ): when n = 0, for every s ∈ St,
π 1 (JtKs) = JwK ∈ def τ hence JtK ∈ T def τ . When n > 0, for every s ∈ St,
assume that Jts1 K = π 1 (Jt1 w11 · · · w1k1 Ks) where t′1 is a closed term of type τ1
(assuming that t1 w11 · · · w1k1 is of type Tτ1 ). According to the definition of P,
P(Jts1 K) holds. Let ts be another closed term:

s
s
s
s
in val(w[ts1 /x1 ]),
in · · · let xn ⇐ tsn wn1
· · · wnk
ts ≡ let x2 ⇐ ts2 w21
· · · w2k
n
2
s
where tsi (2 ≤ i ≤ n) is either ts1 or ti , wij
≡ wij [ts1 /x1 ] (2 ≤ i ≤ n, 1 ≤ j ≤ ki ).
s
By induction, Jt K ∈ T def τ holds. Furthermore, for every s ∈ St,

JtKs = Jlet x1 ⇐ t1 w11 · · · w1k1 in · · · let xn ⇐ tn wn1 · · · wnkn in val(w)Ks
= (Jlet x2 ⇐ t2 w21 · · · w2k2 in · · ·
let xn ⇐ tn wn1 · · · wnkn in val(w)K[x1 := Jts1 K])s′
s ′
= Jt Ks ,

where s′ = π2 (Jt1 w11 · · · w1k1 Ks). Since Jts K ∈ T def τ for every s ∈ St, π1 (JtKs) =
π1 (Jts Ks′ ) ∈ def τ , hence JtK ∈ T def τ .
Jτ K
def τ
– Continuation (T def τ = RR ): we say that an element c ∈ JTτ K = RR is in
Jτ K
T def τ if and only if for every pair of continuations k1 , k2 ∈ R ,
k1 |def τ = k2 |def τ =⇒ c(k1 ) = c(k2 ).
If n = 0, JtK = λ k.k(JwK) ∈ T def τ . When n > 0, according to the definition of
the continuation monad: JtK = λ k · Jt1 w11 · · · wnkn K(k ′ ), where

k ′ = λ a·(Jlet x2 ⇐ t2 w21 · · · w2k2 in · · · let xn ⇐ tn wn1 · · · wnkn in val(w)K[x1 := a])k.

For every continuations k1 , k2 ∈ RJτ K such that k1 |def τ = k2 |def τ let
ki′ = λ a·(Jlet x2 ⇐ t2 w21 · · · w2k2 in · · · let xn ⇐ tn wn1 · · · wnkn in val(w)K[x1 := a])ki ,
i = 1, 2. Because Jt1 w11 · · · w1k1 K ∈ T (Pτ1 ∩def τ1 ), if we can prove k1′ |Pτ1 ∩def τ1 =
k2′ |Pτ1 ∩def τ1 , which implies JtK(k1 ) = JtK(k2 ), we can conclude JtK ∈ T def τ . For
every a ∈ Pτ1 ∩def τ1 , let Jta1 K = a where ta1 is a closed term. Define another closed
term ta :
a
a
a
a
in val(w[ta1 /x1 ]),
in · · · let xn ⇐ tan wn1
· · · wnk
ta ≡ let x2 ⇐ ta2 w21
· · · w2k
n
2
a
where tai (2 ≤ i ≤ n) is either ta1 or ti , wij
≡ wij [ta1 /x1 ] (2 ≤ i ≤ n, 1 ≤
a
′
j ≤ ki ). By induction, Jt K ∈ T def τ , so k1 (a) = Jta Kk1 = Jta Kk2 = k2′ (a), i.e.,
k1′ |Pτ1 ∩def τ1 = k2′ |Pτ1 ∩def τ1 .
– Non-determinism (T def τ = Pfin (def τ )): when n = 0, JtK = {JwK} ∈ T def τ .
When n > 0, for every a ∈ Jt1 w11 · · · w1k1 K, assume that Jta1 K = a where t′1 is a
closed term of type τ1 (assuming that t1 w11 · · · w1k1 is of type Tτ1 ). According to
the definition of P, P(Jta1 K) holds. Let ta be another closed term:

a
a
a
a
in val(w[ta1 /x1 ]),
in · · · let xn ⇐ tan wn1
· · · wnk
ta ≡ let x2 ⇐ ta2 w21
· · · w2k
n
2

a
where tai (2 ≤ i ≤ n) is either ta1 or ti , wij
≡ wij [ta1 /x1 ] (2 ≤ i ≤ n, 1 ≤ j ≤ ki ).
a
By induction, Jt K ∈ T def τ holds. Furthermore,

JtK = Jlet
S x1 ⇐ t1 w11 · · · w1k1 in · · · let xn ⇐ tn wn1 · · · wnkn in val(w)K
Jlet x2 ⇐ t2 w21 · · · w2k2 in · · ·
=
a∈Jt1 K
xn ⇐ tn wn1 · · · wnkn in val(w)K[x1 := a]
S let
=
Jta K.
a∈Jt1 K

Because Jta K ∈ T def τ holds for every a ∈ Jt1 w11 · · · w1k1 K, JtK ∈ T def τ .

⊓
⊔

From the above lemma, we conclude immediately that for every closed βc-normalη-long computation term t in λPESCN
with logical constants, JtK ⊆ T def τ .
Comp

Proposition 3. def Tτ ⊆ T def τ holds in the set-theoretical model of λPESCN
with
Comp
logical constants.

Proof. It follows from Lemma 2 by considering the βc-normal-η-long terms that define
elements in JTτ K since λComp is strongly normalizing.
⊓
⊔
4.2 Completeness of logical relations in λPESC
Comp for first-order types
We prove (8) in this section for the partial computation monad, the exception monad,
the state monad and the continuation monad. We write λPESC
Comp for λComp where the
monad is restricted to one of these four monads.
Proofs depend typically on the particular semantics of every form of computation,
but a common technique is used frequently: given two definable but non-related elements of JTτ K, one can find a context to distinguish the programs (of type Tτ ) that
define the two given elements, and such a context is usually built based on another
context that can distinguish programs of type τ .
Lemma 3. Let (Rτ )τ type be a logical relation in λPESC
Comp with only logical constants.
∼τ ⊆ Rτ =⇒ ∼Tτ ⊆ RTτ holds for every type τ .
Proof. Take two arbitrary elements c1 , c2 ∈ JTτ K such that (c1 , c2 ) 6∈ RTτ , we prove
that c1 6∼Tτ c2 for every monad in λPESC
Comp :
– Partial computation: the fact (c1 , c2 ) 6∈ RTτ amounts to the following two cases:
• c1 , c2 ∈ Jτ K but (c1 , c2 ) 6∈ Rτ , then c1 6∼τ c2 . If one of these two values is
not definable at type τ , by Proposition 3, it is not definable at type Tτ either.
If both values are definable at type τ but they are not contextually equivalent,
then there is a context x : τ ⊢ C : To such that JCK[x := c1 ] 6= JCK[x := c2 ].
Thus, the context y : Tτ ⊢ let x ⇐ y in C : To can distinguish c1 and c2 (as
two values of type Tτ ).
• c1 ∈ Jτ K and c2 = ⊥ (or symmetrically, c1 = ⊥ and c2 ∈ Jτ K), then the
context let x ⇐ y in val(true) can be used to distinguish them.
c1 6∼Tτ c2 in both cases.
– Exception: the fact (c1 , c2 ) 6∈ RTτ amounts to three cases:

• c1 , c2 ∈ Jτ K but (c1 , c2 ) 6∈ Rτ , then c1 6∼τ c2 . Suppose both values are definable at type τ , otherwise by Proposition 3, they must not be definable at type
Tτ . Similar as in the case of partial computation we can build a context that
distinguishes c1 and c2 as values of type Tτ , from the context that distinguishes
c1 and c2 as values of type τ .
• c1 ∈ Jτ K, c2 ∈ E. Consider the following context:
y : Tτ ⊢ let x ⇐ y in val(true) : Tbool.

When y is substituted by c1 and c2 , the context evaluates to different values,
namely, a boolean and an exception.
• c1 , c2 ∈ E but c1 6= c2 . Try the same context as in the second case, which will
evaluate to two different exceptions that can be distinguished.
c1 6∼Tτ c2 in all the three cases.
– State transformer: because (c1 , c2 ) 6∈ RTτ , there exists some s0 ∈ St such that
• either (π1 (c1 s0 ), π1 (c2 s0 )) 6∈ Rτ . Then by induction π1 (c1 s0 ) 6∼τ π1 (c2 s0 ).
If π1 (ci s0 ) (i = 1, 2) is not definable, then by Proposition 3, ci is not definable
either. If both π1 (c1 s0 ) and π1 (c2 s0 ) are definable, but π1 (c1 s0 ) 6≈τ π1 (c2 s0 ),
then there is a context x : τ ⊢ C : To such that JCK[x := π1 (c1 s0 )] 6= JCK[x :=
π1 (c2 s0 )], i.e., for some state s′0 ∈ St ,
JCK[x := π1 (c1 s0 )](s′0 ) 6= JCK[x := π1 (c1 s0 )](s′0 ).

Now we can use the following context:

y : Tτ ⊢ let x ⇐ y in let z ⇐ updates′0 in C : T o,
Let fi =
s ∈ St,

r

z
let x ⇐ y in let z ⇐ updates′0 in C [y := ci ], then for every

r
z
fi (s) = let z ⇐ updates′0 in C [x := π1 (ci s)](π2 (ci s))
= JCK[x := π1 (ci s)](s′0 ),

(i = 1, 2).

f1 6= f2 , because when applied to the state s0 , they will return two different
pairs, so the above context can distinguish the two values c1 and c2 ;
• or π2 (c1 s0 ) 6= π2 (c2 s0 ). we use the context
y : Tτ ⊢ let x ⇐ y in val(true) : Tbool,
then Jlet x ⇐ y in val(true)K[y := ci ] = λs.(true, π2 (ci s)) (i = 1, 2).
These two functions are not equal since they return different results when applied to the state s0 .
In both cases, c1 6∼Tτ c2 .
– Continuation: first say that two continuations k1 , k2 ∈ RJτ K are R-related, if and
only if for every a1 , a2 ∈ Jτ K, a1 Rτ a2 =⇒ k1 (a1 ) = k2 (a2 ). The fact (c1 , c2 ) 6∈

RTτ means that there are two R-related continuations k1 , k2 such that c1 (k1 ) 6=
c2 (k2 ). Because ∼τ ⊆ Rτ , for every definable value a ∈ def τ , clearly,
a ∼τ a =⇒ a1 R a2 =⇒ k1 (a1 ) = k2 (a2 ),
so k1 and k2 coincide over def τ . Suppose that both c1 and c2 are definable, then
by Proposition 3, c1 (k1 ) = c1 (k2 ) and c2 (k1 ) = c2 (k2 ), hence c1 (k1 ) 6= c2 (k1 ).
Consider the context
y : Tτ ⊢ let x ⇐ y in callkτ 1 (x) : T bool.
For every k ∈ RJboolK ,
q
y
k1
let x ⇐
q y inkcallyτ (x) [y := ci ](k)
= ci (λ a · ( callτ 1 (x) [x := a])k)
= ci (λ a · k1 (a)) = ci (k1 ).

(i = 1, 2),

Since c1 (k1 ) 6= c2 (k1 ), this context distinguishes the two computations, hence
c1 6∼Tτ c2 .
⊓
⊔
Theorem 2. In λPESC
Comp , if all constants are logical and in particular, if the following
constants are present
– updates for the state transformer monad;
– callkτ for the continuation monad,
then logical relations are complete up to first-order types, in the strong sense that there
exists an observational logical relation (Rτ )τ type such that for any closed terms t1 , t2
of any type τ 1 up to first order, if t1 ≈τ 1 t2 , then Jt1 K Rτ 1 Jt2 K.

Proof. Take the logical relation (Rτ )τ type induced by Rb =∼b , for any base type b.
We prove by induction on types that ∼τ ⊆ Rτ for any first-order type τ . In particular,
the induction step ∼τ ⊆ Rτ =⇒∼Tτ ; ⊆ RTτ is shown by Lemma 3.
⊓
⊔
4.3 Completeness of logical relations for the non-determinism monad
The non-determinism monad is an interesting case: the completeness of logical relations
for this monad does not hold for all first-order types! To state it, consider the following
two programs of a first-order type that break the completeness of logical relations:
⊢ val(λx.(true +bool false)) : T(bool → Tbool),
⊢ λx.val(true) +bool→Tbool λx.(true +bool false) : T(bool → Tbool).
Recall the logical constant +τ of type τ → τ → Tτ : J+τ K(a1 , a2 ) = {a1 , a2 } for
every a1 , a2 ∈ Jτ K. The two programs are contextually equivalent: what contexts can
do is to apply the functions to some arguments and observe the results. But no matter
how many time we apply these two functions, we always get the same set of possible

values ({true, false}), so there is no way to distinguish them with a context. Recall
the logical relation for non-determinism monad in Figure 2:
c1 RTτ c2 ⇔ (∀a1 ∈ c1 . ∃a2 ∈ c2 . a1 Rτ a2 ) & (∀a2 ∈ c2 . ∃a1 ∈ c1 . a1 Rτ a2 ).
Clearly the denotations of the above two programs are not related by that relation because the function Jλx.val(true)K from the second program is not related to the function in the first.
However, if we assume that for every non-observable base type b, there is an equality
test constant testb : b → b → bool (clearly, P(testb ) holds), logical relations for the
non-determinism monad are then complete for a set of weak first-order types:
τw1 ::= b | Tb | b → τw1 .
Compared to all types up to first order, weak first-order types do not contain monadic
types of functions, so it immediately excludes the two programs in the above counterexample.
Theorem 3. Logical relations for the non-determinism monad are complete up to weak
first-order types. in the strong sense that there exists an observational logical relation
(Rτ )τ type such that for any closed terms t1 , t2 of a weak first-order type τw1 , if t1 ≈τw1
t2 , then Jt1 K Rτw1 Jt2 K.

Proof. Take the logical relation R induced by Rb =∼b , for any base type b. We prove
by induction on types that ∼τw1 ⊆ Rτ 1 for any weak first-order type τw1 .
w
Cases b and b → τw1 go identically as in standard typed lambda-calculi. For monadic
types Tb, suppose that (c1 , c2 ) 6∈ RTb , which means either there is a value in c1 such
that no value of c2 is related to it, or there is such a value in c2 . We assume that every
value in c1 and c2 is definable (otherwise it is obvious that c1 6∼Tb c2 because at least
one of them is not definable, according to Proposition 3). Suppose there is a value a ∈ c1
such that no value in c2 is related to it, and a can be defined by a closed term t of type
b. Then the following context can distinguish c1 and c2 :
x : Tτ ⊢ let y ⇐ x in testb (y, t) : Tbool
since every value in c2 is not contextually equivalent to a, hence not equal to a.



Now let state and label be base types such that label is an observation type,
whereas state is not. Using non-determinism monad, we can define labeled transition
systems as elements of Jstate → label → TstateK, with states in JstateK and labels
in JlabelK, as functions mapping states a and labels l to the set of states b such that
l
/ b . The logical relation at type state → label → Tstate is given by [2]:
a
(f1 , f2 ) ∈ Rstate→label→Tstate ⇐⇒
∀a1 , a2 , l1 , l2 · (a1 , a2 ) ∈ Rstate & (l1 , l2 ) ∈ Rlabel =⇒
(∀b1 ∈ f1 (a1 , l1 ) · ∃b2 ∈ f2 (a2 , l2 ) · (b1 , b2 ) ∈ Rstate )
& (∀b2 ∈ f2 (a2 , l2 ) · ∃b1 ∈ f1 (a1 , l1 ) · (b1 , b2 ) ∈ Rstate )

In case Rlabel is equality, f1 and f2 are logically related if and only if Rstate is a strong
bisimulation between the labeled transition systems f1 and f2 .
Sometimes we explicitly specify an initial state for certain labeled transition system.
In this case, the encoding of the labeled transition system in the nondeterminism monad
is a pair (q, f ) of Jstate × (state → label → Tstate)K, where q is the initial state and
f is the transition relation as defined above. Then (q1 , f1 ) and (q2 , f2 ) are logically
related if and only if they are strongly bisimular, i.e., Rstate is a strong bisimulation
between the two labeled transition systems and q1 Rstate q2 .
Corollary 1 (Soundness of strong bisimulation). Let f1 and f2 be transition systems.
If there exists a strong bisimulation between f1 and f2 , then f1 and f2 are contextually
equivalent.
Proof. There exists a strong bisimulation between f1 and f2 , therefore f1 and f2 are
logically related. By Theorem 1, f1 and f2 are thus contextually equivalent.

In order to prove completeness, we need to assume that label has no junk, in the
sense that every value of JlabelK is definable.

Corollary 2 (Completeness of strong bisimulation). Let f1 and f2 be transition systems which are definable. If f1 and f2 are contextually equivalent and label has no
junk, then there exists a strong bisimulation between f1 and f2 .
Proof. Let R be the logical relation given by Theorem 3. f1 and f2 are definable and
contextually equivalent, so f1 Rstate→label→Tstate f2 . Moreover, because label has no
junk, Rlabel is equality. Rstate is thus a strong bisimulation between f1 and f2 .
⊓
⊔

5 Conclusion
The work presented in this paper is a natural continuation of the authors’ previous
work [2,3]. In [2], we extend [9] and derive logical relations for monadic types which
are sound in the sense that the Basic Lemma still holds. In [3], we study contextual
equivalence in a specific version of the computational λ-calculus with cryptographic
primitives and we show that lax logical relations (the categorical generalization of logical relations [14]) derived using the same construction is complete. Then in this paper,
we explore the completeness of logical relations for the computational λ-calculus and
we show that they are complete at first-order types, for a list of common monads: partial computations, exceptions, state transformers and continuations, while in the case
of continuation, the completeness depends on a natural constant call, with which we
cannot show the soundness.
Pitts and Stark have defined operationally based logical relations to characterize the
contextual equivalence in a language with local store [13]. This work can be traced back
to their early work on the nu-calculus [12] which can be translated in a special version of
the computational λ-calculus and be modeled using the dynamic name creation monad
[17]. Logical relations for this monad are derived in [19] using the construction from
[2]. It is also shown in [19] that such derived logical relations are equivalent to Pitts and
Stark’s operational logical relations up to second-order types.

An exceptional case of our completeness result is the non-determinism monad,
where logical relations are not complete for all first-order types, but a subset of them.
We effectively show this by providing a counter-example that breaks the completeness
at first-order types. This is indeed an interesting case. A more comprehensive study on
this monad can be found in [4], where Jeffrey defines a denotational model for the computational λ-calculus specialized in non-determinism and proves that this model is fully
abstract for may-testing. The relation between our notion of contextual equivalence and
the may-testing equivalence remains to be clarified.
Recently, Lindley and Stark introduce the syntactic ⊤⊤-lifting for the computational λ-calculus and prove the strong normalization [7]. Katsumata then instantiates
their liftings in Set [5]. The ⊤⊤-lifting of strong monads is an essentially different
approach from that in [2]. It would be interesting to establish a formal relationship between these two approaches, and to look for a general proof of completeness using the
⊤⊤-lifting.

References
1. P. N. Benton, G. M. Bierman, and V. C. V. de Paiva. Computational types from a logical
perspective. J. Functional Programming, 8(2):177–193, 1998.
2. J. Goubault-Larrecq, S. Lasota, and D. Nowak. Logical relations for monadic types. In
Proceedings of CSL’2002, volume 2471 of LNCS, pages 553–568. Springer, 2002.
3. J. Goubault-Larrecq, S. Lasota, D. Nowak, and Y. Zhang. Complete lax logical relations for
cryptographic lambda-calculi. In Proceedings of CSL’2004, volume 3210 of LNCS, pages
400–414. Springer, 2004.
4. A. Jeffrey. A fully abstract semantics for a higher-order functional language with nondeterministic computation. Theoretical Computer Science, 228(1-2):105–150, 1999.
5. S. Katsumata. A semantic formulation of ⊤⊤-lifting and logical predicates for computational metalanguage. In Proceedings of CSL’2005, volume 3634 of LNCS, pages 87–102.
Springer, 2005.
6. R. Lazić and D. Nowak. A unifying approach to data-independence. In Proceedings of
CONCUR’2000, volume 1877 of LNCS, pages 581–595. Springer, 2000.
7. S. Lindley and I. Stark. Reducibility and ⊤⊤-lifting for computation types. In Proceedings
of TLCA’2005, number 3461 in LNCS, pages 262–277. Springer, 2005.
8. J. C. Mitchell. Foundations of Programming Languages. MIT Press, 1996.
9. J. C. Mitchell and A. Scedrov. Notes on sconing and relators. In Proceedings of CSL’1992,
volume 702 of LNCS, pages 352–378. Springer, 1993.
10. E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92,
1991.
11. P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42(3):658–709,
1995.
12. A. Pitts and I. Stark. Observable properties of higher order functions that dynamically create
local names, or: What’s new? In Proceedings of MFCS’1993, number 711 in LNCS, pages
122–141. Springer, 1993.
13. A. Pitts and I. Stark. Operational reasoning for functions with local state. In Higher Order
Operational Techniques in Semantics, pages 227–273. Cambridge University Press, 1998.
14. G. Plotkin, J. Power, D. Sannella, and R. Tennent. Lax logical relations. In Proceedings of
ICALP’2000, volume 1853 of LNCS, pages 85–102. Springer, 2000.

15. G. D. Plotkin. Lambda-definability in the full type hierarchy. In To H. B. Curry: Essays
on Combinatory Logic, Lambda Calculus and Formalism, pages 363–373. Academic Press,
1980.
16. K. Sieber. Full abstraction for the second order subset of an algol-like language. Theoretical
Computer Science, 168(1):155–212, 1996.
17. I. Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1):77–107,
1996.
18. E. Sumii and B. C. Pierce. Logical relations for encryption. J. Computer Security, 11(4):521–
554, 2003.
19. Y. Zhang. Cryptographic logical relations. Ph. d. dissertation, ENS Cachan, France, 2005.

