Logical Methods in Computer Science
Vol. 5 (3:8) 2009, pp. 1–69
www.lmcs-online.org

Submitted
Published

Jan. 2, 2008
Sep. 11, 2009

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES
NIKOS TZEVELEKOS
Oxford University Computing Laboratory
e-mail address: nikt@comlab.ox.ac.uk
Abstract. Game semantics has been used with considerable success in formulating fully
abstract semantics for languages with higher-order procedures and a wide range of computational effects. Recently, nominal games have been proposed for modelling functional
languages with names. These are ordinary, stateful games cast in the theory of nominal
sets developed by Pitts and Gabbay. Here we take nominal games one step further, by
developing a fully abstract semantics for a language with nominal general references.

5.5. Observationality
5.6. Definability and full-abstraction
5.7. An equivalence established
semantically
6. Conclusion
Appendix A. Deferred proofs
References

Contents
List of Figures
1. Introduction
2. Theory of nominal sets
2.1. Nominal sets
2.2. Strong support
3. The language
3.1. Definitions
3.2. Categorical semantics
4. Nominal games
4.1. The basic category G
4.2. Arena and strategy orders in G
4.3. Innocence: the category V
4.4. Totality: the category Vt
4.5. A monad, and some comonads
4.6. Nominal games à la Laird
5. The nominal games model
5.1. Solving the Store Equation
5.2. Obtaining the νρ-model
5.3. Adequacy
5.4. Tidy strategies

1
2
4
5
7
8
9
12
21
21
29
30
33
38
40
41
42
45
48
50

53
56
61
61
62
67

List of Figures
1

Typing rules.

2
3

Reduction rules.
The semantic translation.

10
18

4

The store arena and the type
translation.

44

5
6

9

The store monad.
Strategies for update, dereferencing
and fresh-name creation.

45
47

7

A dialogue in innocent store.

47

8

Store-H’s -Q’s -A’s in arena T 1.

50

1998 ACM Subject Classification: F.3.2.
Key words and phrases: game semantics, denotational semantics, monads and comonads, ν-calculus, ML.
Research financially supported by the Engineering and Physical Sciences Research Council, the Eugenides
Foundation, the A. G. Leventis Foundation and Brasenose College.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-5 (3:8) 2009

CC

N. Tzevelekos
Creative Commons

2

N. TZEVELEKOS

1. Introduction
Functional languages constitute a programming paradigm built around the intuitive notion
of a computational function, that is, an effectively specified entity assigning values from a
codomain to elements of a domain in a pure manner : a pure function is not allowed to carry
any notion of state or side-effect. This simple notion reveals great computational power if
the domains considered are higher-order, i.e sets of functions: with the addition of recursive
constructs, higher-order functional computation becomes Turing complete (PCF [42, 37]).
In practice, though, functional programming languages usually contain impure features that
make programming simpler (computational effects), like references, exceptions, etc. While
not adding necessarily to its computational power, these effects affect the expressivity of a
language: two functions which seem to accomplish the same task may have different innerworkings which can be detected by use of effects (e.g. exceptions can distinguish constant
functions that do or do not evaluate their inputs). The study of denotational models for
effects allows us to better understand their expressive power and to categorise languages
with respect to their expressivity.
A computational effect present in most functional programming languages is that of
general references. General references are references which can store not only values of
ground type (integers, booleans, etc.) but also of higher-order type (procedures, higherorder functions) or references themselves. They constitute a very powerful and useful programming construct, allowing us not only the encoding of recursion (see example 3.4) but
also the simulation of a wide range of computational effects and programming paradigms
(e.g. object-oriented programming [3, section 2.3] or aspect-oriented programming [40]).
The denotational modelling of general references is quite demanding since, on top of phenomena of dynamic update and interference, one has to cope with the inherent cyclicity
of higher-order storage. In this paper we provide a fully abstract semantics for a language
with general references called the νρ-calculus.
The νρ-calculus is a functional language with dynamically allocated general references,
reference-equality tests and “good variables”, which faithfully reflects the practice of real
programming languages such as ML [27]. In particular, it extends the basic nominal language of Pitts and Stark [36], the ν-calculus, by using names for general references. That
is, names in νρ are atomic entities which can be (cf. [36]):
created with local scope, updated and dereferenced, tested for equality and
passed around via function application, but that is all.
The fully abstract model of νρ is the first such for a language with general references and
good variables.1
Fully abstract models for general references were given via game semantics in [3] and
via abstract categorical semantics (and games) in [20]. Neither approach used names. The
model of [3] is based on the idea of relaxing strategy conditions in order to model computational effects. In particular, it models references as variables of a read/write product type
and it uses strategies which violate visibility in order to use values assigned to references
previously in a play. The synchronisation of references is managed by cell strategies which
model fresh-reference creation. Because references are modelled by products, and in order
to produce a fully abstract semantics, the examined language needs to include bad variables,
which in turn yield unwanted behaviours affecting severely the expressivity of the language
1In fact, the νρ-calculus and its fully abstract model were first presented in [46], of which the present

paper is an extended and updated version.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

3

and prohibit the use of equality tests for references.2 On the other hand, the approach
in [20] bypasses the bad-variables problem by not including types for references (variables
and references of the same type coincide). This contributes new intuitions on sequential
categorical behaviour (sequoidal category), but we think that it is somehow distanced from
the common notion of reference in functional programming.
The full-abstraction problem has also been tackled via trace semantics in [23]. The
language examined is a version of that in [3] without bad variables. The latter are not needed
since the modelling of references is achieved by names pointing to a store (which is analogous
to our approach). Of relevance is also the fully abstract trace model for a language with
nominal threads and nominal objects presented in [17]. An important difference between
trace models and game models is that the former are defined operationally (i.e. traces are
computed by using the operational semantics), whereas game models are defined in a purely
compositional manner. Nonetheless, trace models and game models have many similarities,
deriving mainly from their sequential-interactive representation of computation, and in
particular there are connections between [23] and the work herein that should be further
examined.
The approach. We model nominal computation in nominal games. These were introduced
independently in [2, 21] for producing fully abstract models of the ν-calculus and its extension with pointers respectively. Here we follow the formulation of [2] with rectifications
pertaining to the issue of unordered state (see remark 4.20).3 Thus, our nominal games
constitute a stateful (cf. Ong [34]) version of Honda-Yoshida call-by-value games [15] built
inside the universe of nominal sets of Gabbay and Pitts [12, 35].
A particularly elegant approach to the modelling of names is by use of nominal
sets [12, 35]. These are sets whose elements involve a finite number of atoms, and
which can be acted upon by finite atom-permutations. The expressivity thus obtained
is remarkable: in the realm (the category) of nominal sets, notions like atom-permutation,
atom-freshness and atom-abstraction are built inside the underlying structure. We therefore use nominal sets, with atoms playing the role of names, as a general foundation for
reasoning about names.
The essential feature of nominal games is the appearance of names explicitly in plays
as constants (i.e. as atoms), which allows us to directly model names and express namerelated notions (name-equality, name-privacy, scope-extrusion, etc.) in the games setting.
Thus nominal games can capture the essential features of nominal computation and, in
particular, they model the ν-calculus. From that model we can move to a model of νρ by
an appropriate effect-encapsulation procedure, that is, by use of a store-monad. A fully
abstract model is then achieved by enforcing appropriate store-discipline conditions on the
games.
2

By “bad variables” we mean read/write constructs of reference type which are not references. They are
necessary for obtaining definability and full-abstraction in [3] since read/write-product semantical objects
may not necessarily denote references.
3The nominal games of [2] use moves attached with finite sets of names. It turns out, however, that
this yields discrepancies, as unordered name-creation is incompatible with the deterministic behaviour of
strategies and, in fact, nominal games in [2] do not form a category. Here (and also in [46]), we recast
nominal games using moves attached with name-lists instead of name-sets. This allows us to restrict our
attention to strong nominal sets (v. definition 2.6), a restriction necessary for overcoming the complications
with determinacy.

4

N. TZEVELEKOS

The paper is structured as follows. In section 2 we briefly present nominal sets and
some of their basic properties. We finally introduce strong nominal sets, that is, nominal
sets with “ordered involvement” of names, and prove the strong support lemma. In section 3
we introduce the νρ-calculus and its operational semantics. We then introduce the notion
of a νρ-model, which provides abstract categorical conditions for modelling νρ in a setting
involving local-state comonads and a store-monad. We finally show definability and, by use
of a quotienting procedure, full-abstraction in a special class of νρ-models. In section 4
we introduce nominal games and show a series of results with the aim of constructing a
category Vt of total, innocent nominal strategies. In the end of the section we attempt a
comparison with the nominal games presented by Laird in [21, 24]. In section 5 we proceed
to construct a specific fully abstract νρ-model in the category Vt . The basic ingredients
for such a construction have already been obtained in the previous section, except for the
construction of the store-monad, which involves solving a recursive domain equation in Vt .
Once this has been achieved and the νρ-model has been obtained, we further restrict legal
strategies to tidy ones, i.e. to those that obey a specific store-related discipline; for these
strategies we show definability and full-abstraction. We conclude in section 6 with some
further directions.
The contributions of this paper are: a) the identification of strong nominal sets as the
adequate setting for nominal language semantics; b) the abstract categorical presentation
in a monadic-comonadic setting of models of a language with nominal general references;
c) the rectification of nominal games of [2] and their use in constructing a specific such
model; d) the introduction of a game-discipline (tidiness) to capture computation with
names-as-references, leading to a definable and hence fully abstract game model.
2. Theory of nominal sets
We give a short overview of nominal sets, which form the basis of all constructions presented
in this paper; our presentation generally follows [35]. Nominal sets are an inspiring paradigm
of the universality (and reusability) of good mathematics: invented in the 1920’s and 1930’s
by Fraenkel and Mostowski as a model of set theory with atoms (ZFA) for showing its
independence from the Axiom of Choice, they were reused in the late 1990’s by Gabbay
and Pitts [12] as the foundation of a general theory of syntax with binding constructs. The
central notion of nominal sets is that of atoms, which are to be seen as basic ‘particles’
present in elements of nominal sets, and of atom-permutations which can act upon those
elements. Moreover, there is an infinite supply of atoms, yet each element of a nominal
set ‘involves’ finitely many of them, that is, it has finite support with regard to atompermutations.
We will be expressing the intuitive notion of names by use of atoms, both in the abstract
syntax of the language and in its denotational semantics. Perhaps it is not clear to the reader
why nominal sets should be used — couldn’t we simply model names by natural numbers?
Indeed, numerals could be used for such semantical purposes (see e.g. [24]), but they would
constitute an overspecification: numerals carry a linear order and a bottom element, which
would need to be carefully nullified in the semantical definitions. Nominal sets factor out
this burden by providing the minimal solution to specifying names; in this sense, nominal
sets are the intended model for names.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

5

2.1. Nominal sets. Let us fix a countably infinite family (Ai )i∈ω of pairwise disjoint,
countably infinite sets of atoms, and let us denote by PERM(Ai ) the group of finite permutations of Ai . Atoms are denoted by a, b, c and variants; permutations are denoted by π
and variants; id is the identity permutation and (a b) is the permutation swapping a and
b (and fixing all other atoms). We write A for the union of all the Ai ’s. We take
M
PERM(A) ,
PERM(Ai )
(2.1)
i∈I

to be the direct sum of the groups PERM(Ai ), so PERM(A) is a group of finite permutations
of A which act separately on each constituent
Ai . In particular, each π ∈ PERM(A) is
Q
an ω-indexed list of permutations, π ∈ i∈ω PERM(Ai ), such that (π)i 6= idAi holds for
finitely many indices i. In fact, we will write (non-uniquely) each permutation π as a finite
composition
π = π1 ◦ · · · ◦ πn
such that each πi belongs to some PERM(Aji ) — note that ji ’s need not be distinct.
Definition 2.1. A nominal set X is a set |X| (usually denoted X) equipped with an
: PERM(A) × X → X such that, for any
action of PERM(A), that is, a function ◦
π, π ′ ∈ PERM(A) and x ∈ X,
π ◦ (π ′ ◦ x) = (π ◦ π ′ ) ◦ x ,

id ◦ x = x .

Moreover, for any x ∈ X there exists a finite set S such that, for all permutations π,
(∀a ∈ S. π(a) = a) =⇒ π ◦ x = x .

N

For example, A with the action of permutations being simply permutation-application is
a nominal set. Moreover, any set can be trivially rendered into a nominal set of elements
with empty support.
Finite support is closed under intersection and hence there is a least finite support for
each element x of a nominal set; this we call the support of x and denote by S(x).
Proposition and Definition 2.2 ([12]). Let X be a nominal set and x ∈ X. For any
finite S ⊆ A, S supports x iff ∀a, a′ ∈ (A \ S). (a a′ ) ◦ x = x .
Moreover, if finite S, S ′ ⊆ A support x then S ∩ S ′ also supports x. Hence, we can
define
\
S(x) ,
{ S ⊆fin A | S supports x } ,
which can be expressed also as:

S(x) = { a ∈ A | for infinitely many b. (a b) ◦ x 6= x } .



For example, for each a ∈ A, S(a) = {a}. We say that a is fresh for x, written a # x, if
a∈
/ S(x). x is called equivariant if it has empty support. It follows from the definition
that
a # x ⇐⇒ for cofinitely many b. (a b) ◦ x = x .
(2.2)
There are several ways to obtain new nominal sets from given nominal sets X and Y :
• The disjoint union X ⊎Y with permutation-action inherited from X and Y is a nominal
set. This extends to infinite disjoint unions.
• The cartesian product X × Y with permutations acting componentwise is a nominal
set; if (x, y) ∈ X ×Y then S(x, y) = S(x) ∪ S(y).

6

N. TZEVELEKOS

• The fs-powerset Pfs (X), that is, the set of subsets of X which have finite support, with
permutations acting on subsets of X elementwise. In particular, X ′ ⊆ X is a nominal
subset of X if it has empty support, i.e. if for all x ∈ X ′ and permutation π, π ◦ x ∈ X ′ .
Apart from A, some standard nominal sets are the following.
• Using products and infinite unions we obtain the nominal set
[
A# ,
{ a1 . . . an | ∀i, j ∈ 1..n. ai ∈ A ∧ (j 6= i =⇒ aj 6= ai ) } ,
(2.3)
n

that is, the set of finite lists of distinct atoms. Such lists we denote by ā, b̄, c̄ and
variants.
• The fs-powerset Pfs (A) is the set of finite and cofinite sets of atoms, and has Pfin (A) as
a nominal subset (the set of finite sets of atoms).
For X and Y nominal sets, a relation R ⊆ X ×Y is a nominal relation if it is a nominal
subset of X×Y . Concretely, R is a nominal relation iff, for any permutation π and (x, y) ∈
X ×Y ,
xRy ⇐⇒ (π ◦ x)R(π ◦ y) .
For example, it is easy to show that # ⊆ A × X is a nominal relation. Extending this
reasoning to functions we obtain the notion of nominal functions.
Definition 2.3 (The category Nom). We let Nom be the category of nominal sets
and nominal functions, where a function f : X → Y between nominal sets is nominal if
f (π ◦ x) = π ◦ f (x) for any π ∈ PERM(A) and x ∈ X.
N
For example, the support function, S( ) : X → Pfin (A) , is a nominal function since
S(π ◦ x) = π ◦ S(x) .
Nom inherits rich structure from Set and is in particular a topos. More importantly, it
contains atom-abstraction mechanisms; we will concentrate on the following.
Definition 2.4 (Nominal abstraction). Let X be a nominal set and x ∈ X. For any
finite S ⊆ A, we can abstract x to S, by forming
[x]S , { y ∈ X | ∃π. (∀a ∈ S ∩ S(x). π(a) = a) ∧ y = π ◦ x } .

N

The abstraction restricts the support of x to S ∩ S(x) by appropriate orbiting of x (note
that [x]S ∈ Pfs (X)). In particular, we can show the following.
Lemma 2.5 ([48]). For any x ∈ X, S ⊆fin A and π ∈ PERM(A),
π ◦ [x]S = [π ◦ x]π ◦ S ∧ S([x]S ) = S(x) ∩ S .



Two particular subcases of nominal abstraction are of interest. Firstly, in case S ⊆ S(x)
the abstraction becomes
[x]S = { y ∈ X | ∃π. (∀a ∈ S. π(a) = a) ∧ y = π ◦ x } .

(∗)

This is the mechanism used in [46]. Note that if S * S(x) ∧ S(x) * S then (∗) does not yield
S([x]S ) = S ∩ S(x). The other case is the simplest possible, that is, of S being empty; it
turns out that this last constructor is all we need from nominal abstractions in this paper.
We define:
[x] , { y ∈ X | ∃π. y = π ◦ x } .
(2.4)

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

7

2.2. Strong support. Modelling local state in sets of atoms yields a notion of unordered
state, which is inadequate for our intended semantics. Nominal game semantics is defined
by means of nominal strategies for games that model computation. These strategies, however, are deterministic up to choice of fresh names, a feature which is in direct conflict to
unordered state. For example, in unordered state the consecutive creation of two atoms
a, b is modelled by adding the set {a, b} to the local state; on the other hand, by allowing
strategies to play such moves we lose determinism in strategies.4
Ordered state is therefore more appropriate for our semantical purposes and so we
restrict our attention to nominal sets with ordered presence of atoms in their elements.
This notion is described as strong support.5
Definition 2.6. For any nominal set X, any x ∈ X and any S ⊆ A, S strongly supports
x if, for any permutation π,
(∀a ∈ S. π(a) = a) ⇐⇒ π ◦ x = x .
We say that X is a strong nominal set if it is a nominal set with all its elements having
strong support.
N
Compare the last assertion above with that of definition 2.1, which employs only the leftto-right implication. In fact, strong support coincides with weak support when the former
exists.
Proposition 2.7. If X is a nominal set and x ∈ X has strong support S then S = S(x).
Proof: By definition, S supports x, so S(x) ⊆ S. Now suppose there exists a ∈ S \ S(x).
For any fresh b, (a b) fixes S(x) but not S, so it doesn’t fix x, .
Thus, for example, the set {a, b} ⊆ Ai of the previous paragraph does not have strong
support, since the permutation (a b) does not fix the atoms in its support (the set {a, b})
but still (a b) ◦ {a, b} = {a, b}. On the other hand, {a, b} strongly supports the list ab. In
fact, all lists of (distinct) atoms have strong support and therefore A# is a strong nominal
set (but Pfin (A) is not).
The main reason for introducing strong nominal sets is the following result, which is a
specialised version of the Strong Support Lemma of [48] (with S = ∅).
Lemma 2.8 (Strong Support Lemma). Let X be a strong nominal set and let
x1 , x2 , y1 , y2 , z1 , z2 ∈ X. Suppose also that S(yi ) ∩ S(zi ) ⊆ S(xi ) , for i = 1, 2, and that
there exist πy , πz such that
πy ◦ x1 = πz ◦ x1 = x2 ,

πy ◦ y 1 = y 2 ,

πz ◦ z1 = z2 .

Then, there exists some π such that π ◦ x1 = x2 , π ◦ y1 = y2 and π ◦ z1 = z2 .
Proof: Let ∆i , S(zi ) \ S(xi ) , i = 1, 2 , so ∆2 = πz ◦ ∆1 , and let π ′ , πy−1 ◦ πz . By
assumption, π ′ ◦ x1 = x1 , and therefore by strong support π ′ (a) = a for all a ∈ S(x1 ).
Take any b ∈ ∆1 . Then π ′ (b) # π ′ ◦ x1 = x1 and πz (b) ∈ πz ◦ ∆1 = ∆2 , ∴ πz (b) # y2 ,
∴ π ′ (b) # πy−1 ◦ y2 = y1 . Hence,
b ∈ ∆1 =⇒ b, π ′ (b) # x1 , y1 .
4The problematic behaviour of nominal games in weak support is discussed again in remark 4.20.
5An even stricter notion of support is linear support, introduced in [31]: a nominal set X is called linear

if for each x ∈ X there is a linear order <x of S(x) such that a <x b =⇒ π(a) <π ◦

x

π(b).

8

N. TZEVELEKOS

Now assume ∆1 = {b1 , ..., bN } and define π1 , ..., πN by recursion:
π0 , id ,

πi+1 , (bi+1 πi ◦ π ′ ◦ bi+1 ) ◦ πi .

We claim that, for each 0 ≤ i ≤ N and 1 ≤ j ≤ i, we have
π i ◦ π ′ ◦ bj = bj ,

πi ◦ x1 = x1 ,

πi ◦ y 1 = y 1 .

We do induction on i; the case of i = 0 is trivial. For the inductive step, if πi ◦ π ′ ◦ bi+1 = bi+1
then πi+1 = πi , and πi+1 ◦ π ′ ◦ bi+1 = πi ◦ π ′ ◦ bi+1 = bi+1 . Moreover, by IH, πi+1 ◦ π ′ ◦ bj =
bj for all 1 ≤ j ≤ i, and πi+1 ◦ x1 = x1 and πi+1 ◦ y1 = y1 . If πi ◦ π ′ ◦ bi+1 = b′i+1 6= bi+1 then,
by construction, πi+1 ◦ π ′ ◦ bi+1 = bi+1 . Moreover, for each 1 ≤ j ≤ i, by IH, πi+1 ◦ π ′ ◦ bj =
(bi+1 b′i+1 ) ◦ bj , and the latter equals bj since bi+1 6= bj implies b′i+1 6= πi ◦ π ′ ◦ bj = bj .
Finally, for any a ∈ S(x1 ) ∪ S(y1 ), πi+1 ◦ a = (bi+1 b′i+1 ) ◦ πi ◦ a = (bi+1 b′i+1 ) ◦ a, by IH,
with a 6= bi+1 . But the latter equals a since π ′ (bi+1 ) 6= a implies that b′i+1 6= πi ◦ a = a, as
required.
Hence, for each 1 ≤ j ≤ N ,
π N ◦ π ′ ◦ bj = bj ,

πN ◦ x1 = x1 ,

πN ◦ y 1 = y 1 .

Moreover, πN ◦ π ′ ◦ z1 = z1 , as we also have
b ∈ S(z1 ) ∩ S(x1 ) =⇒ πN ◦ π ′ ◦ b = πN ◦ b = b
−1
we have:
(again by strong support). Thus, considering π , πy ◦ πN
−1 ◦
x1 = πy ◦ x1 = x2 ,
πy ◦ πN

−1 ◦
y 1 = πy ◦ y 1 = y 2 ,
πy ◦ πN

−1 ◦
−1 ◦
πN ◦ π ′ ◦ z1 = πy ◦ π ′ ◦ z1 = πy ◦ πy−1 ◦ πz ◦ z1 = z2 ,
z1 = πy ◦ πN
πy ◦ πN

as required.
A more enlightening formulation of the lemma can be given in terms of abstractions, as in
the following table. In the context of nominal games later on, the strong support lemma
will guarantee us that composition of abstractions of plays can be reduced to composition
of plays.
Strong Support Lemma.
Let X be a strong nominal set and x1 , x2 , y1 , y2 , z1 , z2 ∈ X. Suppose also that
S(yi ) ∩ S(zi ) ⊆ S(xi ) , for i = 1, 2, and moreover that
[x1 , y1 ] = [x2 , y2 ] ,

[x1 , z1 ] = [x2 , z2 ] .

Then, [x1 , y1 , z1 ] = [x2 , y2 , z2 ].
3. The language
The language we examine, the νρ-calculus, is a call-by-value λ-calculus with nominal general
references. It constitutes an extension of the ν-calculus [36] and Reduced ML [44, chapter
5] in which names are used for general references. It is essentially the same calculus of [23],
that is, the mkvar-free fragment of the language of [3] extended with reference-equality tests
and names.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

ā | Γ |− n : N

ā | Γ |− skip : 1

ā | Γ, x : A |− x : A

ā | Γ |− M : A × B

ā | Γ |− M : A × B

ā | Γ |− fst M : A

ā | Γ |− snd M : B

ā | Γ |− M : N

ā | Γ |− M : N

ā | Γ |− pred M : N

ā | Γ |− succ M : N

ā | Γ, x : A |− M : B

ā | Γ |− M : A

ā | Γ |− a : [A]

ā | Γ |− M : [A]

āa | Γ |− M : B

ā | Γ |− N : B

ā | Γ |− hM, N i : A × B
ā | Γ |− M : N

ā | Γ |− Ni : A

(i=1,2)

ā | Γ |− if0 M then N1 else N2 : A
ā | Γ |− M : A → B

ā | Γ |− λx.M : A → B
a ∈ AA
∧a ∈ ā

9

ā | Γ |− N : A

ā | Γ |− M N : B
ā | Γ |− M : [A]

ā | Γ |− νa.M : B
ā | Γ |− N : A

ā | Γ |− M := N : 1

ā | Γ |− N : [A]

ā | Γ |− [M = N ] : N
ā | Γ |− M : [A]
ā | Γ |− ! M : A

Figure 1: Typing rules.

3.1. Definitions. The syntax of the language is built inside Nom. In particular, we assume
there is a set of names (atoms) AA ∈ (Ai )i∈ω for each type A in the language. Types include
types for commands, naturals and references, product types and arrow types.
Definition 3.1. The νρ-calculus is a typed functional language of nominal references. Its
types, terms and values are given as follows.
TY ∋ A, B ::= 1 | N | [A] | A → B | A × B
TE ∋ M, N ::= x | λx.M | M N hM, N i | fst M | snd N

λ-calculus

| n | pred M | succ N

arithmetic

| skip | if0 M then N1 else N2

return / if then else

|a

reference to type A (a ∈ AA )

| [M = N ]

name-equality test

| νa.M

ν-abstraction

| M := N

update

| !M

dereferencing

VA ∋ V, W ::= n | skip | a | x | λx.M | hV, W i
The typing system involves terms in environments ā | Γ, where ā a list of (distinct) names
and Γ a finite set of variable-type pairs. Typing rules are given in figure 1.
N
The ν-constructor is a name-binder : an occurrence of a name a inside a term M is bound

10

N. TZEVELEKOS

if it is in the scope of some νa . We follow the standard convention of equating terms up to
α-equivalence, the latter defined with respect to both variable- and name-binding.
Note that TE and VA are strong nominal sets: each name a of type A is taken from
AA and all terms contain finitely many atoms — be they free or bound — which form their
support. Note also the notion of ordered state that is imposed by use of name-lists (instead
of name-sets) in type-environments. In fact, we could have used unordered state at the level
of syntax (and operational semantics) of νρ, and ordered state at the level of denotational
semantics. This already happens with contexts: a context Γ is a set of premises, but JΓK is
an (ordered) product of type-translations. Nevertheless, we think that ordered state does
not add much complication while it saves us from some informality.
The operational semantics of the calculus involves computation in some store environment where created names have their values stored. Formally, we define store environments
S to be lists of the form:
S ::= ǫ | a, S | a :: V, S .
(3.1)
Observe that the store may include names that have been created but remain as yet unassigned a value. For each store environment S we define its domain to be the name-list given
by:
dom(ǫ) , ǫ , dom(a, S) , a, dom(S) , dom(a :: V, S) , a, dom(S) .
(3.2)
We only consider environments whose domains are lists of distinct names. We write
S |=Γ,A M , or simply S |= M , only if dom(S) | Γ |− M : A is valid (i.e., derivable).
Definition 3.2. The operational semantics is given in terms of a small-step reduction, the
rules of which are given in figure 2. Evaluation contexts E[ ] are of the form:
[ = N ] , [a =
(λx.N )

,

], !

,

N , fst

:= N , a :=
, snd

, pred

, if0

then N1 else N2 ,

, succ

, h , N i , hV, i

N

We can see that νρ is not strongly normalising with the following example. Recall the
NEW

EQ

IF0

a#S

n=0 if a=b

PRD

S |= [a = b] −→ S |= n n=1 if a6=b

S |= if0 n then N1 else N2 −→ S |= Nj

UPD

SUC

S |= νa.M −→ S, a |= M

j=1 if n=0
j=2 if n>0

S, a :: V, S ′ |= ! a −→ S, a :: V, S ′ |= V

LAM

S |= pred (n+1) −→ S |= n

PRD

FST

S, a(:: W ), S ′ |= a := V −→ S, a :: V, S ′ |= skip
DRF

S |= succ n −→ S |= n+1

SND

S |= (λx.M ) V −→ S |= M {V /x}

Figure 2: Reduction rules.

CTX

S |= pred 0 −→ S |= 0

S |= fst hV, W i −→ S |= V
S |= snd hV, W i −→ S |= W
S |= M −→ S ′ |= M ′
S |= E[M ] −→ S ′ |= E[M ′ ]

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

11

standard CBV encoding of sequencing:
M ; N , (λz.N )M

(3.3)

with z not free in N .
Example 3.3. For each type A, take
stopA , νb.(b := λx.(! b)skip) ;(! b)skip
with b ∈ A1→A . We can see that stopA diverges, since:
|= stopA −→
→ b :: λx.(! b)skip |= (! b)skip −→ b :: λx.(! b)skip |= (λx.(! b)skip)skip
−→ b :: λx.(! b)skip |= (! b)skip .



The great expressive power of general references is seen in the fact that we can encode the
Y combinator. The following example is adapted from [3].
Example 3.4. Taking a ∈ AA→A , define:
YA , λf.νa.(a := λx.f (! a)x) ; ! a .
YA has type ((A → A) → A → A) → A → A and, for any relevant term M and value V ,
we have
|= (YA (λy.M ))V −→
→ a :: λx.(λy.M )(! a)x |= (! a)V
−→ a :: λx.(λy.M )(! a)x |= (λx.(λy.M )(! a)x)V
−→ a :: λx.(λy.M )(! a)x |= (λy.M )(! a)V ,
and also |= (λy.M )(YA (λy.M ))V −→
→ a :: λx.(λy.M )(! a)x |= (λy.M )(! a)V .
For example, setting
addrecx , λx. if0 snd x then x else xhsucc fst x, pred snd xi ,
add , Y(λh.addrech ) ,
S , a :: λx.(λh.addrech )(! a)x ,
where x is a metavariable of relevant type, we have that, for any n, m ∈ N,
|= addhn, mi −→
→ S |= (λh.addrech )(! a)hn, mi −→
→ S |= addrecS(a) hn, mi
−→
→ S |= if0 m then hn, mi else S(a)hsucc fst hn, mi, pred snd hn, mii
−→
→ S |= S(a)hn+1, m−1i −→ S |= (λh.addrech )(! a)hn+1, m−1i
· · · −→
→ S |= (λh.addrech )(! a)hn+m, 0i −→
→ S |= hn+m, 0i .



The notions of observational approximation and observational equivalence are built
around the observable type N. Two terms are equivalent if, whenever they are put inside
a variable- and name-closing context of resulting type N, called a program context, they
reduce to the same natural number. The formal definition follows; note that we usually
omit ā and Γ and write simply M / N .
Definition 3.5. For typed terms ā | Γ |− M : A and ā | Γ |− N : A , define
ā | Γ |− M / N ⇐⇒ ∀C. (∃S ′ . |= C[M ] −→
→ S ′ |= 0) =⇒ (∃S ′′ . |= C[N ] −→
→ S ′′ |= 0)
where C is a program context. Moreover, ≅ , / ∩ ' .

N

12

N. TZEVELEKOS

3.2. Categorical semantics. We now examine sufficient conditions for a fully abstract
semantics of νρ in an abstract categorical setting. Our aim is to construct fully abstract
models in an appropriate categorical setting, pinpointing the parts of structure needed for
such a task. In section 5 we will apply this knowledge in constructing a concrete such model
in nominal games.
Translating each term M into a semantical entity JM K and assuming a preorder “.”
in the semantics, full-abstraction amounts to the assertion:
M / N ⇐⇒ JM K . JN K

(FA)

Note that this formulation is weaker than equational full abstraction, which is given by:
M ≅ N ⇐⇒ JM K = JN K .

(EFA)

Nevertheless, once we achieve (FA) we can construct an extensional model, via a quotienting construction, for which EFA holds. Being a quotiented structure, the extensional
model does not have an explicit, simple description, and for this reason we prefer working
with the intensional model (i.e., the unquotiented one). Of course, an intensional model
satisfying (EFA) would be preferred but this cannot be achieved in our nominal games.
Therefore, our categorical models will be guided by the (FA) formulation.
3.2.1. Monads and comonads. The abstract categorical semantics we put forward is based
on the notions of monads and comonads. These are standard categorical notions (v. [25],
and [8, Triples]) which have been used extensively in denotational semantics of programming
languages. We present here some basic definitions and properties.
Monads. Monads were introduced in denotational semantics through the work of Moggi [29,
30] as a generic tool for encapsulating computational effects. Wadler [49] popularised monads in programming as a means of simulating effects in functional programs, and nowadays
monads form part and parcel of the Haskell programming language [18].
Definition 3.6. A strong monad over a category C with finite products is a quadruple
(T, η, µ, τ ), where T is an endofunctor in C and η : IdC → T , µ : T 2 → T and τ : × T →
T ( × ) are natural transformations such that the following diagrams commute.
µT A

T 3A

/ T 2A
µA

T µA



T 2A



µA

(A × B) × T C

/ TA

ηT A

/ T 2A

JJ
JJ
JJ
µA
T ηA
J
 idT A JJ% 
/ TA
T 2A
µA

A × (B × T C)id

1 × T AO

τA,B

τ

A,T B
/ T ((A × B) × C)
/ T (A × T B)
A × T 2 BP
RRR
P
P
PPP
RRR
RRRT ∼
idA ×µB PPPP
RR=R
PPP
R(
(
/ A × T (B × C)
/ T (A × (B × C))
A × TB

A ×τB,C

τ1,A

/ T (1 × A)
OOO
OOO
OO
OOO η
∼
idA ×ηB
T∼
OOA×B
=
= OOOO
OO'
OOO

' 
/ T (A × B)
A × TB
TA

A × BO

τA×B,C

∼
=



TA J

τA,B×C

T τA,B

/ T 2 (A × B)
µA×B

τA,B


/ T (A × B)

We say that C has T -exponentials if, for every pair B, C of objects, there exists an object
T C B such that for any object A there exists a bijection
∼
=

ΛTA,B,C : C(A × B, T C) −
→ C(A, T C B )
natural in A.

N

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

13

Given a strong monad (T, η, µ, τ ), we can define the following transformations.
∼
=

∼
=

τA,B

′
→ T (A × B) ,
→ B × T A −−−→ T (B × A) −
τA,B
, TA × B −
′
τA,T
B

T τA,B

µA×B

τT A,B

′
T τA,B

µA×B

ψA,B , T A × T B −−−−→ T (A × T B) −−−−→ T 2 (A × B) −−−−→ T (A × B) ,

(3.4)

′
ψA,B
, T A × T B −−−−→ T (T A × B) −−−−→ T 2 (A × B) −−−−→ T (A × B) .

Moreover, T -exponentials supply us with T -evaluation arrows, that is,
evTB,C : T C B × B → T C , ΛT

−1

(idT C B )

(3.5)

so that, for each f : A × B → T C,
f = ΛT (f ) ×B ; evTB,C .
In fact, T -exponentiation upgrades to a functor (T )− : C op × C → C which takes each
f : A′ → A and g : B ′ → B to
′

evT

id×f

Tg

−→ T B) .
T g f : T B ′ A → T B A , ΛT (T B ′ A × A′ −−−→ T B ′ A × A −−→ T B ′ −

(3.6)

Naturality of ΛTA,B,C in A implies its naturality in B, C too, by use of the above construct.
Comonads. Comonads are the dual notion of monads. They were first used in denotational semantics by Brookes and Geva [9] for modelling programs intensionally, that is, as
mechanisms which receive external computation data and decide on an output. Monadiccomonadic approaches were examined by Brookes and van Stone [10].
Definition 3.7. A comonad on a category C is a triple (Q, ε, δ), where Q is an endofunctor
in C and ε : Q → IdC , δ : Q → Q2 are natural transformations such that the following
diagrams commute.
Q3O A o

δQA

QδA

Q2A o

Q2O A
δA

δA

QA oeL

εQA

Q2A

O
LLL
LLL
δ
L A
idQA LLL

QA

QA

QεA

/ QA
r9
r
r
r
rridr
r
r
QA
rr

Now assume C has binary products. We define a transformation ζ̄ : Q( × ) →
hQπ1 ,Qπ2 i

× Q( ),

εA ×idQB

ζ̄ A,B , Q(A × B) −−−−−−→ QA × QB −−−−−−→ A × QB .
Q is called a product comonad if ζ̄ is a natural isomorphism, and is written (Q, ε, δ, ζ)
where ζ is the inverse of ζ̄.
N
It is easy to see that the transformation ζ̄ makes the relevant (dualised) diagrams of definition 3.6 commute, even without stipulating the existence of the inverse ζ. Note that we
write ζ ′ , ζ̄ ′ for the symmetric counterparts of ζ, ζ̄.
Product comonads are a stronger version of “strong comonads” of [10]. A product
comonad Q can be written as:
Q ∼
= Q1 ×
6
hence the name. We say that Q1 is the basis of the comonad .
6Note this is an isomorphism between comonads, not merely between functors.

14

N. TZEVELEKOS

Monadic-comonadic setting. In the presence of both a strong monad (T, η, µ, τ ) and a product comonad (Q, ε, δ, ζ) in a cartesian category C, one may want to solely consider arrows
from some initial computation data (i.e., some initial state) of type A to some computation
of type B, that is, arrows of type:
QA → T B
T
This amounts to applying the biKleisli construction on C, that is, defining the category CQ
with the same objects as C, and arrows
T
CQ
(A, B) , C(QA, T B) .

For arrow composition to work in the biKleisli category, we need a distributive law between
Q and T , that is, a natural transformation ℓ : QT → T Q making the following diagrams
commute.
QηA

εT A

/ TA
/ QT A
QA M
q8
MMM
q
q
MMM
qq
ℓ
qqTq εA
ηQA MMMM A
q
q
&  q
T QA

QT 2 A

QµA

ℓT A ; T ℓA

/ QT A

δT A

/ Q2 T A
QℓA ; ℓQA

ℓA



T 2 QA





µQA

/ T QA

T δA

/ T Q2 A

In this case, composition of f : QA → T B and g : QB → T C is performed as:
δ

Qf

Tg

ℓ

µC

B
QA −
→ Q2A −−→ QT B −→
T QB −−
→ T 2 C −−→ T C

Since we are examining a monadic-comonadic setting for strong monad T and product
comonad Q, a distributive law amounts to a natural transformation
ℓ : Q1 × T

→ T (Q1 × ) ,

which is therefore given for free: take ℓ , τQ1, . The distributivity equations follow
straightforwardly from the monadic equations.
Exponentials and the intrinsic preorder. The notion of T -exponentials can be generalised to
the monadic-comonadic setting as follows.
Definition 3.8. Let C be a category with finite products and let (T, η, µ, τ ), (Q, ε, δ) be a
strong monad and comonad, respectively, on C. We say that C has (Q, T )-exponentials
if, for each pair B, C of in C there exists an object (Q, T )C B such that, for each object A,
there exists a bijection
∼
=

→ C(QA, (Q, T )C B )
φA,B,C : C(Q(A × B), T C) −
N

natural in A.

Assume now we are in a monadic-comonadic setting (C, Q, T ) with T a strong monad with
T -exponentials and Q a product comonad. (Q, T )-exponentials then come for free.
Proposition 3.9. In the setting of the previous definition, if T is a strong monad with
exponentials and Q is a product comonad then C has (Q, T )-exponentials defined by:
(Q, T )C B , T C B ,
ζ′

f

φ(f ) , ΛT (QA × B −
→ Q(A × B) −
→ T C) .

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

15

φ is a bijection with its inverse sending each g : QA → T C B to the arrow:
ζ̄ ′

evT

g×id

Q(A × B) −
→ QA × B −−−→ T C B × B −−→ T C .



In the same setting, we can define a notion of intrinsic preorder . Assuming an object
O of observables and a collection O ⊆ C(1, T O) of observable arrows, we can have the
following.
Definition 3.10. Let C, Q, T, O, O be as above. We define . to be the union, over all
objects A, B, of relations . A,B ⊆ C(QA, T B)2 defined by:
f . A,B g ⇐⇒ ∀ρ ∈ C(Q(T B A ), T O). ΛQ,T (f ); ρ ∈ O =⇒ ΛQ,T (g); ρ ∈ O ,
δ

QΛT (ζ ′ ; f )

where ΛQ,T (f ) , Q1 −
→ Q21 −−−−−−−→ Q(T B A ) .

N

We have the following enrichment properties.
Proposition 3.11. Let C, Q, T, O, O and . be as above. Then, for any f, g : QA → T B
and any arrow h, if f . g then:
• if h : QB → T B ′ then δ ; Qf ; ℓ ; T h ; µ . δ ; Qg ; ℓ ; T h ; µ ,
• if h : QA′ → T A then δ ; Qh ; ℓ ; T f ; µ . δ ; Qh ; ℓ ; T g ; µ ,
• if h : QA → T C then hf, hi ; ψ . hg, hi ; ψ
• if A = A1 × A2 then

ΛTQA1 ,A2 ,B (ζ ′ ; f ) ; η

.

and

hh, f i ; ψ . hh, gi ; ψ ,

ΛTQA1 ,A2 ,B (ζ ′ ; g) ; η .

3.2.2. Soundness. We proceed to present categorical models of the νρ-calculus. The approach we take is a monadic and comonadic one, over a computational monad T and
a family of local-state comonads Q = (Qā )ā∈A# , so that the morphism related to each
ā | Γ |− M : A be of the form JM K : Qā JΓK → T JAK. Computation in νρ is store-update and
fresh-name creation, so T is a store monad, while initial state is given by product comonads.
Definition 3.12. A νρ-model M is a structure (M, T, Q) such that:
I. M is a category with finite products, with 1 being the terminal object and A × B the
product of A and B.
II. T is a strong monad (T, η, µ, τ ) with exponentials.
III. M contains an appropriate natural numbers object N equipped with successor and
predecessor arrows and ñ : 1 → N, each n ∈ N. Moreover, for each object A, there is
an arrow cndA : N × T A × T A → T A for zero-equality tests.
IV. Q is a family of product comonads (Qā , ε, δ, ζ)ā∈A# on M such that:
′
(a) the basis of Qǫ is 1, and Qā = Qā whenever [ā] = [ā′ ] (i.e., whenever π ◦ ā = ā′ ),
′
(b) if S(ā′ ) ⊆ S(ā) then there exists a comonad morphism āā′ : Qā → Qā such that
ā
ā
′
′′
ǫ = ε, ā = id and, whenever S(ā ) ⊆ S(ā ) ⊆ S(ā),
ā ā′′
ā
;
= ′
ā′′ ā′
ā

16

N. TZEVELEKOS

(c) for each āa ∈ A# there exists a natural transformation nuāa : Qā → T Qāa such
that, for each A, B ∈ Ob(M) and āa, ā′a with S(āa) ⊆ S(ā′a), the following diagrams commute.
ā′

Q A

ā′
ā

hid,nuāa i

/ Qā A

′

τ

nuāa

nuāa



′

T Qā a A

ā′a
T āa

/ T Qāa A

/ Qā (A × B)




A × T Qāa B

/ T (Qā A × Qāa A)

āa
T h ā ,idi

(N2)

nuA×B

id×nuB





ζ

A × Qā B

/ Qā A × T Qāa A

/ T Qāa (A × B)

τ ;Tζ

V. Setting AA , Qa 1, for each a ∈ AA , there is a name-equality arrow eqA : AA × AA → N
such that, for any distinct a, b ∈ AA , the following diagram commutes.
∆

Qa 1

/

ab ab
ha, b i

AA × AA o

Qab 1

eqA

!



0̃

1

/

(N1)

!





1̃

No

1

VI. Setting J1K , 1, JNK , N, J[A]K , AA , JA → BK , T JBK JAK , JA × BK , JAK × JBK,
M contains, for each A ∈ TY, arrows
drfA : AA → T JAK

and

updA : AA × JAK → T 1

such that the following diagrams commute,

AA × JAK

hid,updA i ; τ ; ∼
=

/ T (AA × JAK)

T (π1 ; drfA ) ; µ

-

1 T JAK

T π2
hid×π1 ;updA ,id×π2 ;updA i

AA × JAK × JAK
Qab 1 ×

ψ ;∼
=

+

/ T1 × T1
π2

JAK × JBK

ab
ab
h a ×π1 ;updA , b ×π2 ;updB i
/

3 T1

(NR)

ψ;∼
=

T1 × T1
ψ′ ; ∼
=

+
3 T1

and, moreover,

āa
′
(nuāa
A × updB ) ; ψ = (nuA × updB ) ; ψ ,
i.e., updates and fresh names are independent effects.

(SNR)
N

The second subcondition of (N2) above essentially states that, for each object A, nuA can
be expressed as:
∼
=

∼
=

τ′

nu ×id

Qā A −
→ Qā 1 × A −−1−−→ T Qāa 1 × A −
→ T (Qāa 1 × A) −
→ T Qāa A
It is evident that the role reserved for nu in our semantics is that of fresh name creation.
Accordingly, nu gives rise to a categorical name-abstraction operation: for any arrow f :
Qāa A → T B in M, we define
nu

Tf

µ

A
^ a _ f , Qā A −−→
T Qāa A −−→ T 2 B −
→ TB .

(3.7)

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

17

The (NR) diagrams give the basic equations for dereferencings and updates (cf. [38, definition 1] and [44, section 5.8]). The first diagram stipulates that by dereferencing an updated
reference we get the value of the update. The second diagram ensures that the value of a
reference is that of the last update: doing two consecutive updates to the same reference
is the same as doing only the last one. The last diagram states that updates of distinct
references are independent effects.
Let us now proceed with the semantics of νρ in νρ-models.
Definition 3.13. Let (M, T, Q) be a νρ-model. Recall the type-translation:
J 1K , 1 ,

JNK , N ,

J[A]K , AA ,

JA → BK , T JBK JAK ,

JA × BK , JAK × JBK .

A typing judgement ā | Γ |− M : A is translated to an arrow JM Kā|Γ : Qā JΓK → T JAK in
M, which we write simply as JM K : Qā Γ → T A, as in figure 3.
N
We note that the translation of values follows a common pattern: for any ā | Γ |− V : B,
we have JV K = |V | ; η , where
|x| , Qā π ; āǫ
|a| , Qā ! ; āa

|ñ| , Qā ! ; āǫ ; ñ
|skip| , Qā ! ; āǫ

|λx.M | , ΛT (ζ ′ ; JM K)

(3.8)

|hV, W i| , h|V |, |W |i .

We can show the following lemmas, which will be used in the proof of Correctness.
′

Lemma 3.14. For any ā | Γ |− M : A and S(ā) ⊆ S(ā′ ), JM Kā′ |Γ = āā ; JM Kā|Γ .
Moreover, if Γ = x1 : B1 , ..., xn : Bn , and ā | Γ |− M : A and ā | Γ |− Vi : Bi are derivable,
ζ ′ ; Qā π2

hid,|V1 |,...,|Vn|i

JM K

~ /~x}K = Qā Γ −−−−−−−−−→ Qā Γ × Γ −−−−−→ Qā Γ −−→ T A .
JM {V



Lemma 3.15. For any relevant f, g,
āa


hf, ā ; gi
h^ a _ f,gi
ψ
ψ
āa
→ T (B × C) ,
^ a _ Q A −−−−−→ T B × T C −
→ T (B × C) = Qā A −−−−−→ T B × T C −


^a_f
f
Tg
µ
Tg
µ
→ T B −−
→ T 2C −
→ T C = Qā A −−−→ T B −−
^ a _ Qāa A −
→ T 2C −
→ TC .

Lemma 3.16. Let ā | Γ |− M : A and ā | Γ |− E[M ] : B be derivable, with E[ ] being an
evaluation context. Then JE[M ]K is equal to:
hid,JM Ki

T ζ′

τ

T JE[x]K

µ

Qā Γ −−−−−→ Qā Γ × T A −
→ T (Qā Γ × A) −−→ T Qā (Γ × A) −−−−−
→ T 2B −
→ TB .



r

We write S |= M −
→ S ′ |= M ′ with r ∈ {NEW,SUC,EQ,...,LAM′ } if the last non-CTX rule
in the related derivation is r. Also, to any store S, we relate the term S̄ of type 1 as:
ǭ , skip ,

a, S , S̄ ,

a :: V, S , (a := V ; S̄)

(3.9)

Proposition 3.17 (Correctness). For any typed term ā | Γ |− M : A, and S with
dom(S) = ā, and r as above,
r

1. if r ∈
/ {NEW, UPD, DRF} then S |= M −
→ S |= M ′ =⇒ JM K = JM ′ K ,
r
2. if r ∈ {UPD, DRF} then S |= M −
→ S ′ |= M ′ =⇒ JS̄ ; M K = JS̄ ′ ; M ′ K ,
NEW

3. S |= M −−−→ S, a |= M ′ =⇒ JS̄ ; M K = ^ a _ JS̄ ; M ′ K .
Therefore, S |= M −
→ S ′ |= M ′ =⇒ JS̄ ; M K = ^ ā′ _ JS̄ ′ ; M ′ K , with dom(S ′ ) = āā′ .

18

N. TZEVELEKOS

Qā !

ā
ǫ

ā

ā
ǫ

Qā π

η

JxK , Qā Γ −−−→ Qā A −→ A −
→ TA
ā

Qā !

η

a
→ T AA
JaK , Qā Γ −−→ Qā 1 −→
AA −
ā

Qā !

JM K : Qā Γ −
→ TN

η

ñ

→N−
JñK , Q Γ −−→ Q 1 −→ 1 −
→ TN
ā

JMK
/ TN
Qā Γ S
S S
S S
T succ
Jsucc MK S S S 
)
TN

η

JM K : Qā Γ −
→ T AA

ǫ
1−
→ T1
JskipK , Qā Γ −−→ Qā 1 −→

JN K : Qā Γ −
→ T AA

JM K : Qāa Γ −
→ TA
^ a _ JMK

Jνa.M K : Qā Γ −−−−−→ T A

Qā Γ K

hJMK,JN Ki

K

K

ā

K

JM K : Q (Γ × A) −
→ TB

/ T AA × T AA
ψ

K

K

J[M=N ]K

K


T (AA × AA )
K

′

T

Λ (ζ ; JMK)

/ TBA
Qā Γ T T
T T
T T
η
Jλx.MK T T*

T (T B A )

K

K

T eq

K% 
TN

JM K : Qā Γ −
→ T AA
JN K : Qā Γ −
→ TA

ā

A

JM K : Q Γ −
→ T (T B )
JN K : Qā Γ −
→ TA
hJMK,JN Ki

ā

Q ΓL

L

LL

hJMK,JN Ki

K

LL

L

K

/ T (T B A ) × T A

A
L L T (T B × A)
LL
T evT ; µ
L% 
TB

JM K : Qā Γ −
→ T (A × B)
JMK
/ T (A × B)
Qā Γ U U
U U
U U
T π1
U U
Jfst MK
U* 
TA

JM K : Qā Γ −
→ TA
JN K : Q Γ −
→ TB
hJMK,JN Ki

/ TA × TB

Q ΓT T
T T
T T
JhM,N iK T T*

ψ


T (A × B)

K

K



K

T (AA × A)
K

K

K

T updA ; µ

K% 
T1

JM K : Qā Γ −
→ T AA
JMK
/ T AA
Qā Γ T T
T T
T
T drfA ; µ
J!MK T T T 
)
TA

JM K : Qā Γ −
→ TN
JNi K : Qā Γ −
→ TA
Qā Γ K

ā

/ T AA × T A
ψ

K

JM:=N K

ψ

JM N K

ā

Qā Γ K

hJMK,JN1 K,JN2 Ki

K

K

K

Jif0 M then N1 else

/ T N × T A2
τ′


K
T
(
N
×
T A2 )
K
N2 K
K
K
cndA ; µ
K
K% 
TA

K

Figure 3: The semantic translation.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

19

Proof: The last assertion follows easily from 1-3. For 1-3 we do induction on the size of the
reduction’s derivation. The base case follows from the specifications of definition 3.12 and
lemma 3.14. For the inductive step we have that, for any S, M, E, the following diagram
commutes.
′

2

′

hid,JS̄Ki
τ ;Tζ
/ T QāΓ T hid,JMKi ; T τ / T 2 (Qā Γ × A) T (ζ ; JE[x]K) / T 3 B
/ Qā Γ × T 1
Qā Γ XXXXX
XXXXX
XXXXX
XXXXX
µ
µ
Tµ
XXXXX
hid,JS̄ ; MKi
XXX+

′


τ
/ T (Qā Γ × A) T (ζ ; JE[x]K) / T 2 B
Qā Γ × T AT
TTTT
TTTT
µ
T (ΛT (ζ ′ ; JE[x]K)×id)
ΛT (ζ ′ ; JE[x]K)×id ; τ TTTTT
hΛT (ζ ′ ; JE[x]K) ; η,JS̄ ; MKi ; ψ ′
T)


/ TB
/ T ((A −−⊗ T B) × A)
T
T ev

;µ

By the previous lemma, the upper path is equal to hid, JS̄Ki ; τ ; T ζ ′ ; T JE[M ]K ; µ and therefore to JS̄ ; E[M ]K. Hence, we can immediately show the inductive steps of 1-2. For 3,
NEW

assuming S |= E[M ] −−−→ S, a |= E[M ′ ] and JS̄ ; M K = ^ a _ JS̄ ; M ′ K , we have, using also
lemmas 3.14 and 3.15,

^ a _ JS̄ ; E[M ′ ]K = ^ a _ (hΛT (ζ ′ ; JE[x]K) ; η, JS̄ ; M ′ Ki ; ψ′ ; T evT ; µ)
= ^ a _ (hΛT (ζ ′ ; JE[x]K) ; η, JS̄ ; M ′ Ki ; ψ ′ ) ; T evT ; µ
= hΛT (ζ ′ ; JE[x]K) ; η, ^ a _ JS̄ ; M ′ Ki ; ψ ′ ; T evT ; µ
= hΛT (ζ ′ ; JE[x]K) ; η, JS̄ ; M Ki ; ψ ′ ; T evT ; µ = JS̄ ; E[M ]K .



In order for the model to be sound, we need computational adequacy. This is added explicitly as a specification.
Definition 3.18. Let M be a νρ-model and J K the respective translation of νρ. M is
adequate if
→ S ′ |= 0̃ ,
∃S, b̄. JM K = ^ b̄ _ JS̄ ; 0̃K =⇒ ∃S ′ . ā |= M −→
for any typed term ā | ∅ |− M : N.
N
Proposition 3.19 (Equational Soundness). If M is an adequate νρ-model,
JM K = JN K =⇒ M / N .



3.2.3. Completeness. We equip the semantics with a preorder to match the observational
preorder of the syntax as in (FA). The chosen preorder is the intrinsic preorder with regard
to a collection of observable arrows in the biKleisli monadic-comonadic setting (cf. definition 3.10). In particular, since we have a collection of monad-comonad pairs, we also need
a collection of sets of observable arrows.
Definition 3.20. An adequate νρ-model M = (M, T, Q) is observational if, for all ā:
• There exists Oā ⊆ M(Qā 1, T N) such that, for all ā | ∅ |− M : N,
JM K ∈ Oā ⇐⇒ ∃S, b̄. JM K = ^ b̄ _ JS̄ ; 0̃K .

20

N. TZEVELEKOS

• The induced intrinsic preorder on arrows in M(Qā A, T B) defined by
f .ā g ⇐⇒ ∀ρ : Qā (T B A ) → T N. (Λā (f ) ; ρ ∈ Oā =⇒ Λā (g) ; ρ ∈ Oā )
with Λā (f ) , ΛQ

ā ,T

(f ), satisfies, for all relevant a, ā′ , f, f ′ ,

f .āa f ′ =⇒ ^ a _ f .ā ^ a _ f ′

∧

f .ā f ′ =⇒

ā′
ā

′

; f .a

ā′
ā

; f′ .
N

We write M as (M, T, Q, O).
Recurring to ΛQ

ā ,T

of definition 3.10, we have that Λā (f ) is the arrow:
δ

Qā ΛT (ζ ′ ; f )

Qā 1 −
→ Qā Qā 1 −−−−−−−→ Qā (T B A ) .

(3.10)

Hence, Oā contains those arrows that have a specific observable behaviour in the model, and
the semantic preorder is built over this notion. In particular, terms that yield a number
have observable behaviour.
In order to make good use of the semantic preorder we need it to be a congruence with
regard to the semantic translation. Congruences for νρ, along with typed contexts, are
defined properly in [48]. For now, we state the following.
Lemma 3.21. Let (M, T, Q, O) be an observational νρ-model. Then, for any pair ā | Γ |−
M, N : A of typed terms and any context C such that ā′ | Γ′ |− C[M ], C[N ] : B are valid,
′

JM K .ā JN K =⇒ JC[M ]K .ā JC[N ]K .



Assuming that we translate νρ into an observational νρ-model, we can now show one direction of (FA).
Proposition 3.22 (Inequational Soundness). For typed terms ā | Γ |− M, N : A,
JM K . JN K =⇒ M / N .
Proof: Assume JM K .ā JN K and |= C[M ] −→
→ S ′ |= 0̃ , so JC[M ]K = ^ ā′ _ JS̄ ′ ; 0̃K with
′
′
ā
ā = dom(S ). JM K . JN K implies JC[M ]K . JC[N ]K , and hence JC[N ]K ∈ Oǫ . Thus, by
adequacy, there exists S ′′ such that |= C[N ] −→
→ S ′′ |= 0̃ .
In order to achieve completeness, and hence full-abstraction, we need our semantic translation to satisfy some definability requirement with regard to the intrinsic preorder.
Definition 3.23. Let (M, T, Q, O) be an observational νρ-model and let J K be the semantic translation of νρ to M. M satisfies ip-definability if, for any ā, A, B, there exists
ā
⊆ M(Qā JAK, T JBK) such that:
DA,B
ā
• For each f ∈ DA,B
there exists a term M such that JM K = f .
• For each f, g ∈ M(Qā A, T B),
ā
f .ā g ⇐⇒ ∀ρ ∈ DA→B,N
. (Λā (f ) ; ρ ∈ Oā =⇒ Λā (g) ; ρ ∈ Oā ) .

We write M as (M, T, Q, O, D).
For such a model M we achieve full abstraction.
Theorem 3.24 (FA). For typed terms ā | Γ |− M, N : A,
JM K . JN K ⇐⇒ M / N .

N

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

21

Proof: Soundness is by previous proposition. For completeness (“⇐=”), we do induction
on the size of Γ.
For the base case suppose ā | ∅ |− M / N and take any ρ ∈ D 1→A,N such that
Λā (JM K) ; ρ ∈ Oā . Let ρ = Jā | y : 1 → A |− L : NK , some term L, so Λā (JM K) ; ρ is
Λā (JM K) ; JLK = δ ; Qā |λz.M | ; JLK = J(λy.L)(λz.M )K
for some z : 1. The latter being in Oā implies that it equals ^ b̄ _ JS̄ ; 0̃K, some S. Now,
M / N implies (λy.L)(λz.M ) / (λy.L)(λz.N ) , hence ν b̄.(S̄ ; 0̃) / (λy.L)(λz.N ) , by soundness. But this implies that ā |= (λy.L)(λz.N ) −→
→ S ′ |= 0̃ , so J(λy.L)(λz.N )K ∈ Oā , by
ā
ā
ā
correctness. Hence, Λ (JN K) ; ρ ∈ O , so JM K . JN K, by ip-definability.
For the inductive step, if Γ = x : B, Γ′ then
IH

ā | Γ |− M / N =⇒ ā | Γ′ |− λx.M / λx.N =⇒ Jλx.M K .ā Jλx.N K
=⇒ JM K = J(λx.M )xK .ā J(λx.N )xK = JN K
where the last approximation follows from lemma 3.21.

4. Nominal games
In this section we introduce nominal games and strategies, and construct the basic structure
from which a fully abstract model of νρ will be obtained in the next section. We first
introduce nominal arenas and strategies, which form the category G. We afterwards refine
G by restricting to innocent, total strategies, obtaining thus the category Vt .
Vt is essentially a semantical basis for call-by-value nominal computation in general. In
fact, from it we can obtain not only fully abstract models of νρ, but also of the ν-calculus [2],
the νερ-calculus [47] (νρ+exceptions), etc.
4.1. The basic category G. The basis for all constructions to follow is the category Nom
of nominal sets. We proceed to arenas.
Definition 4.1. A nominal arena A , (MA , IA , ⊢A , λA ) is given by:
• a strong nominal set MA of moves,
• a nominal subset IA ⊆ MA of initial moves,
• a nominal justification relation ⊢A ⊆ MA × (MA \ IA ),
• a nominal labelling function λA : MA → {O, P } × {A, Q}, which labels moves as
Opponent or Player moves, and as Answers or Questions.
An arena A is subject to the following conditions.
(f) For each m ∈ MA , there exists unique k ≥ 0 such that IA ∋ m1 ⊢A · · · ⊢A mk ⊢A m ,
for some ml ’s in MA . k is called the level of m, so initial moves have level 0.
(l1) Initial moves are P-Answers.
(l2) If m1 , m2 ∈ MA are at consecutive levels then they have complementary OP-labels.
(l3) Answers may only justify Questions.
N
We let level-1 moves form the set JA ; since ⊢A is a nominal relation, JA is a nominal subset
of MA . Moves in MA are denoted by mA and variants, initial moves by iA and variants, and
level-1 moves by jA and variants. By I¯A we denote MA \ IA , and by J¯A the set MA \ JA .

22

N. TZEVELEKOS

Note that, although the nominal arenas of [2] are defined by use of a set of weaker
conditions than those above, the actual arenas used there fall within the above definition.
We move on to prearenas, which are the ‘boards’ on which nominal games are played.
Definition 4.2. A prearena is defined exactly as an arena, with the only exception of
condition (l1): in a prearena initial moves are O-Questions.
Given arenas A and B, construct the prearena A → B as:
MA→B , MA + MB
IA→B , IA
λA→B , [ (iA 7→ OQ , mA 7→ λ̄A (mA )) , λB ]
⊢A→B , {(iA , iB )} ∪ { (m, n) | m ⊢A,B n }
N

where λ̄A is the OP -complement of λA .

It is useful to think of the (pre)arena A as a vertex-labelled directed graph with vertex-set
MA and edge-set ⊢A such that the labels on vertices are given by λA (and satisfying (l1-3)).
It follows from (f) that the graph so defined is levelled: its vertices can be partitioned into
disjoint sets L0, L1, L2,. . . such that the edges may only travel from level i to level i + 1
and only level-0 vertices have no incoming edges (and therefore (pre)arenas are directed
acyclic). Accordingly, we will be depicting arenas by levelled graphs or triangles.
The simplest arena is 0 , (∅, ∅, ∅, ∅). Other (flat) arenas are 1 (unit arena), N (arena
of naturals) and Aā (arena of ā-names), for any ā ∈ A# , which we define as
(4.1)
MAā = IAā , Aā ,
where Aā , { π ◦ ā | π ∈ PERM(A) }. Note that for ā empty we get Aǫ = 1, and that we
write Ai for Aa with a being of type i.
More involved are the following constructions. For arenas A, B, define the arenas A⊗B,
A⊥ , A −−⊗ B and A ⇒ B as follows.
MA⊗B , IA ×IB + I¯A + I¯B
M1 = I1 , {∗} ,

MN = IN , N ,

IA⊗B , IA ×IB
λA⊗B , [ ((iA , iB ) 7→ P A) , λA ↾ I¯A , λB ↾ I¯B ]
2

2

⊢A⊗B , { ((iA , iB ), m) | iA ⊢A m ∨ iB ⊢B m } ∪ (⊢A ↾ I¯A ) ∪ (⊢B ↾ I¯B )
B

, IB + IA ×JB + I¯A + I¯B ∩ J¯B

B

, IB

B

, [ (iB 7→ P A) , ((iA , jB ) 7→ OQ) , λ̄A ↾ I¯A , λB ↾ (I¯B ∩ J¯B ) ]

B

, { (iB , (iA , jB )) | iB ⊢B jB } ∪ { ((iA , jB ), m) | iA ⊢A m }

MA

−−⊗

IA

−−⊗

λA

−−⊗

⊢A

−−⊗

2
∪ { ((iA , jB ), m) | jB ⊢B m } ∪ (⊢A ↾ I¯A ) ∪ (⊢B ↾ (I¯B ∩ J¯B )2 )

A B
A⊗B

A B
A −−⊗ B

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

MA⊥ , {∗1 } + {∗2 } + MA
IA⊥ , {∗1 }

23

∗
∗

∗

A
A⊥

A B
A⇒B

λA⊥ , [ (∗1 7→ P A) , (∗2 7→ OQ) , λA ]
⊢A⊥ , {(∗1 , ∗2 ), (∗2 , iA )} ∪ (⊢A ↾ MA 2 )

A ⇒ B , A −−⊗ B⊥
In the constructions above it is assumed that all moves which are not hereditarily justified
by initial moves are discarded. Hence, for example, for any A, B
JB = ∅ =⇒ A −−⊗ B = B
Moreover, we usually identify arenas with graph-isomorphic structures; for example,
1 −−⊗ A = A ,

0 ⇒ A = A⊥ .

Using the latter convention, the construction of A⇒B in the previous definition is equivalent
to A ⇒ B of [15, 2] ; concretely, it is given by:
(4.2)
MA⇒B , {∗} + IA + I¯A + MB
IA⇒B , {∗}
λA⇒B , [ (∗ 7→ P A) , (iA 7→ OQ) , λ̄A , λB ]
⊢A⇒B , {(∗, iA )} ∪ { (iA , m) | iA ⊢A m ∨ m ∈ IB } ∪ (⊢A ↾ I¯A 2 ) ∪ (⊢B ↾ MB 2 )
Of the previous constructors all look familiar apart from −−⊗ (which in [46] appears as ⇒).
˜
The latter can be seen as a function-space constructor merging the contravariant part of its
RHS with its LHS. For example, for any A, B, C, we have
A −−⊗ N = N

and A −−⊗ (B ⇒ C) = (A⊗B) ⇒ C

In the first equality we see that N which appears on the RHS of −−⊗ has no contravariant
part, and hence A is redundant. In the second equality B, which is the contravariant part
of B ⇒ C, is merged with A. This construction will be of great use when considering a
monadic semantics for store.
We move on to describe how are nominal games played. Plays of a game consist of
sequences of moves from some prearena. These moves are attached with name-lists to the
effect of capturing name-environments.
Definition 4.3. A move-with-names of a (pre)arena A is a pair, written mā , where m
is a move of A and ā is a finite list of distinct names (name-list).
N
If x is a move-with-names then its name-list is denoted by nlist(x) and its underlying move
by x ; therefore,
x = xnlist(x) .
We introduce some notation for sequences (and lists).
Notation 4.4 (Sequences). A sequence s will be usually denoted by xy . . . , where x, y, ...
are the elements of s. For sequences s, t,
• s ≤ t denotes that s is a prefix of t, and then t = s(t \ s),
• s  t denotes that s is a (not necessarily initial or contiguous) subsequence of t,
• s− denotes s with its last element removed,
• if s = s1 . . . sn then s1 is the first element of s and sn the last. Also,

24

N. TZEVELEKOS

◦ n is the length of s, and is denoted by |s|,
◦ s.i denotes si and s.−i denotes sn+1−i , that is, the i-th element from the end of s
(for example, s.−1 is sn ),
◦ s≤si denotes s1 . . . si , and so does s<si+1 ,
◦ if s is a sequence of moves-with-names then, by extending our previous notation, we
N
have s = snlist(s) , where nlist(s) is a list of length |s| of lists of names.
A justified sequence over a prearena A is a finite sequence s of OP-alternating moves
such that, except for s.1 which is initial, every move s.i has a justification pointer to
some s.j such that j < i and s.j ⊢A s.i ; we say that s.j (explicitly) justifies s.i . A move
in s is an open question if it is a question and there is no answer inside s justified by it.
There are two standard technical conditions that one may want to apply to justified
sequences: well-bracketing and visibility . We say that a justified sequence s is wellbracketed if each answer s.i appearing in s is explicitly justified by the last open question
in s<i (called the pending question). For visibility, we need to introduce the notions of
Player- and Opponent-view . For a justified sequence s, its P-view psq and its O-view
xsy are defined as follows.
pǫq , ǫ
xǫy , ǫ
psxq , psq x
pxq , x

if x a P-move
if x is initial

psxs′ yq , psq xy if y an O-move
expl. justified by x

xsxy , xsyx if x an O-move
′
xsxs yy , xsyxy if y a P-move
expl. justified by x

The visibility condition states that any O-move x in s is justified by a move in xs<xy , and
any P-move y in s is justified by a move in ps<yq. We can now define plays.
Definition 4.5. Let A be a prearena. A legal sequence on A is sequence of moves-withnames s such that s is a justified sequence satisfying Visibility and Well-Bracketing. A
legal sequence s is a play if s.1 has empty name-list and s also satisfies the following Name
Change Conditions (cf. [34]):
(NC1) The name-list of a P-move x in s contains as a prefix the name-list of the move
preceding it. It possibly contains some other names, all of which are fresh for s<x .
(NC2) Any name in the support of a P-move x in s that is fresh for s<x is contained in
the name-list of x.
(NC3) The name-list of a non-initial O-move in s is that of the move justifying it.
The set of plays on a prearena A is denoted by PA .

N

It is important to observe that plays have strong support, due to the tagging of moves with
lists of names (instead of sets of names [2]). Note also that plays are the ǫ-plays of [46].
Now, some further notation.
Notation 4.6 (Name-introduction). A name a is introduced (by Player) in a play s,
written a ∈ L(s), if there exist consecutive moves yx in s such that x is a P-move and
a ∈ S(nlist(x) \ nlist(y)).
N
From plays we move on to strategies. Recall the notion of name-restriction we introduced
in definition 2.4; for any nominal set X and any x ∈ X, [x] = { π ◦ x | π ∈ PERM(A) } .

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

25

Definition 4.7. Let A be a prearena. A strategy σ on A is a set of equivalence classes [s]
of plays in A, satisfying:
• Prefix closure: If [su] ∈ σ then [s] ∈ σ.
• Contingency completeness: If even-length [s] ∈ σ and sx is a play then [sx] ∈ σ.
• Determinacy: If even-length [s1 x1 ], [s2 x2 ] ∈ σ and [s1 ] = [s2 ] then [s1 x1 ] = [s2 x2 ].
We write σ : A whenever σ is a strategy on A.
N
By convention, the empty sequence ǫ is a play and hence, by prefix closure and contingency
completeness, all strategies contain [ǫ] and [iA ]’s. Some basic strategies are the following —
note that we give definitions modulo prefix closure.
Definition 4.8. For any ā′ , ā ∈ A# with S(ā′ ) ⊆ S(ā), n ∈ N and any arena B, define the
following strategies.
• ñ : 1 → N , {[∗ n]}
• !B : B → 1 , {[iB ∗]}
•

ā
ā′

: Aā → Aā , {[ā ā′ ]}
′

• idB : B → B , { [s] | s ∈ PB(1) →B(2) ∧ ∀t ≤even s. t ↾ B(1) = t ↾ B(2) }

N

It is easy to see that the aforedefined are indeed strategies. That definitions are given
modulo prefix closure means that e.g. ñ is in fact:
ñ = { [ǫ], [∗], [∗ n] } .
We proceed to composition of plays and strategies. In ordinary games, plays are composed
by doing “parallel composition plus hiding” (v. [4]); in nominal games we need also take
some extra care for names.
Definition 4.9. Let s ∈ PA→B and t ∈ PB→C . We say that:
• s and t are almost composable, s ` t, if s ↾ B = t ↾ B.
• s and t are composable, s ≍ t, if s ` t and, for any s′ ≤ s, t′ ≤ t with s′ ` t′ :
(C1) If s′ ends in a (Player) move in A introducing some name a then a # t′ .
Dually, if t′ ends in a move in C introducing some name a then a # s′ .
(C2) If both s′ , t′ end in B and s′ ends in a move introducing some name a then a # t′− .
Dually, if t′ ends in a move introducing some name a then a # s′− .
N
The following lemma is taken verbatim from [15], adapted from [7].
Lemma 4.10 (Zipper lemma). If s ∈ PA→B and t ∈ PB→C with s ` t then either
s ↾ B = t = ǫ, or s ends in A and t in B, or s ends in B and t in C, or both s and t end
in B.
Note that in the sequel we will use some standard switching condition results (see e.g. [15, 5])
without further mention. Composable plays are composed as below. Note that we may tag
a move m as m(O) (or m(P ) ) to specify it is an O-move (a P-move).
Definition 4.11. Let s ∈ PA→B and t ∈ PB→C with s ≍ t . Their parallel interaction
s k t and their mix s • t, which returns the final name-list in s k t, are defined by mutual

26

N. TZEVELEKOS

recursion as follows. We set ǫ k ǫ , ǫ , ǫ • ǫ , ǫ , and:
smb̄A • t

smb̄A k t , (s k t)mA

smb̄B • tmc̄B

smb̄B k tmc̄B , (s k t)mB

s • tmc̄C

s k tmc̄C , (s k t)mC

b̄s b̄
smA(P
) • t , (s • t) b̄

b̄s b̄
c̄
smB(P
) • tmB(O) , (s • t) b̄

c̄t c̄
s • tmC(P
) , (s • t) c̄

smb̄A(O) • t , b̄′

c̄t c̄
smb̄B(O) • tmB(P
) , (s • t) c̄

s • tmc̄C(O) , c̄ ′ ,

where b̄s is the name-list of the last move in s, and b̄′ is the name-list of mA(O) ’s justifier
inside s k t ; similarly for c̄t and c̄ ′ .
The composite of s and t is:
s ; t , (s k t) ↾ AC .
The set of interaction sequences of A, B, C is defined as:
ISeq(A, B, C) , { s k t | s ∈ PA→B ∧ t ∈ PB→C ∧ s ≍ t } .

N

When composing compatible plays s and t, although their parts appearing in the common
component (B) are hidden, the names appearing in (the support of) s and t are not lost
but rather propagated to the output components (A and C). This is shown in the following
lemma (the proof of which is tedious but not difficult, see [48]).
Lemma 4.12. Let s ≍ t with s ∈ PA→B and t ∈ PB→C .
(a) If s k t ends in a generalised P-move mb̄ then b̄ contains as a prefix the name-list of
(s k t).−2 . It possibly contains some other names, all of which are fresh for (s k t)− .
(b) If s ; t ends in a P-move mb̄ then b̄ contains as a prefix the name-list of (s ; t).−2 . It
possibly contains some other names, all of which are fresh for (s ; t)− .
(c) If s k t ends in a move mb̄ then b̄ contains as a prefix the name-list of the move explicitly
justifying mb̄ .
(d) If s = s′ mb̄ ends in A and t in B then b̄  s • t,
if s = s′ mb̄ and t = t′ mc̄ end in B then b̄  s • t and c̄  s • t,
if s ends in B and t = t′ mc̄ in C then c̄  s • t.
(e) S(s) ∪ S(t) = S(s k t) = S(s ; t) ∪ S(s • t) .
Proposition 4.13 (Plays compose). If s ∈ PA→B and t ∈ PB→C with s ≍ t, then
s ; t ∈ PA→C .
Proof: We skip visibility and well-bracketing, as these follow from ordinary CBV game
analysis. It remains to show that the name change conditions hold for s ; t. (NC3) clearly
does by definition, while (NC1) is part (b) of previous lemma.
For (NC2), let s ; t end in some P-move ms • t and suppose a ∈ S(ms • t ) and a # (s ; t)− .
Suppose wlog that s = s′ mb̄ , and so (s ; t)− = s′ ; t. Now, if a # s′ • t then, by part (e) of
previous lemma, a # s′ , t and therefore a ∈ b̄ , by (NC2) of s. By part (d) then, a ∈ S(s • t).
Otherwise, a ∈ S(s′ • t) and hence, by part (a), a ∈ S(s • t).
We now proceed to composition of strategies. Recall that we write σ : A → B if σ is a
strategy on the prearena A → B.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

27

Definition 4.14. For strategies σ : A → B and τ : B → C, their composition is defined as
σ ; τ , { [s ; t] | [s] ∈ σ ∧ [t] ∈ τ ∧ s ≍ t } ,
N

and is a candidate strategy on A → C.

Note that, for any sequence u, if [u] ∈ σ ; τ then u = π ◦ (s ; t) = (π ◦ s) ;(π ◦ t) for some
[s] ∈ σ, [t] ∈ τ, s ≍ t and π. Therefore, we can always assume u = s ; t with [s] ∈ σ, [t] ∈ τ
and s ≍ t. Our next aim is to show that composites of strategies are indeed strategies.
Again, the proofs of the following technical lemmata are omitted for economy (but see [48]).
Lemma 4.15. For plays s1 ≍ t1 and s2 ≍ t2 , if s1 k t1 = s2 k t2 then s1 = s2 and t1 = t2 .
Hence, if s1 k t1 ≤ s2 k t2 then s1 ≤ s2 and t1 ≤ t2 .
Lemma 4.16. Let σ : A → B and τ : B → C be strategies with [s1 ], [s2 ] ∈ σ and [t1 ], [t2 ] ∈
τ . If |s1 k t1 | ≤ |s2 k t2 | and [s1 ; t1 ] = [s2 ; t2 ] then there exists some π such that π ◦ (s1 k t1 ) ≤
s 2 k t2 .
Proposition 4.17 (Strategies compose). If σ : A → B and τ : B → C are strategies
then so is σ ; τ .
Proof: By definition and proposition 4.13, σ ; τ contains equivalence classes of plays. We
need also check prefix closure, contingency completeness and determinacy. The former two
are rather straightforward, so we concentrate on the latter.
Assume even-length [u1 x1 ], [u2 x2 ] ∈ σ ; τ with [u1 ] = [u2 ], say ui xi = si ; ti , [si ] ∈ σ and
[ti ] ∈ τ , i = 1, 2 . By prefix-closure of σ, τ we may assume that si , ti don’t both end in B,
for i = 1, 2.
b̄′
If si end in A then si = s′i nb̄i i and si ; ti = (s′i ; ti )ni i , i = 1, 2 . Now, [s′1 ; t1 ] = [u1 ] =
[u2 ] = [s′2 ; t2 ], so, by lemma 4.16 and assuming wlog that |s′1 k t1 | ≤ |s′2 k t2 |, we have
′′
′
′′′
π ◦ (s′1 k t1 ) ≤ (s′2 k t2 ), ∴ π ◦ s′1 ≤ s′2 , say s′2 = s′′2 s′′′
2 with s2 = π ◦ s1 and s2 in B. Then
b̄
b̄
′
′
′′′
′
1
2
[s′′2 ] = [s′1 ], ∴ [s′′2 (s′′′
2 n2 ).1] = [s1 n1 ], by determinacy of σ, and hence |s2 | = 0, s2 = π ◦ s1
b̄
b̄
and t2 = π ◦ t1 . Moreover, π ′ ◦ s′1 n11 = s′2 n22 , some permutation π ′ . Now we can apply the
Strong Support Lemma, as (C1) implies (S(nb̄i i ) \ S(s′i )) ∩ S(ti ) = ∅. Hence, there exists a
permutation π ′′ such that π ′′ ◦ s1 = s2 and π ′′ ◦ t1 = t2 , ∴ [s1 ; t1 ] = [s2 ; t2 ] , as required.
If si end in B and ti in C, then work similarly as above. These are, in fact, the only cases we
need to check. Because if, say, s2 , t1 end in B, s1 in A and t2 in C then t1 , s2 end in P-moves
−
− −
−
−
and [s−
1 ; t1 ] = [s2 ; t2 ] implies that s1 , t2 end in O-moves in B. If, say, |s1 k t1 | ≤ |s2 k t2 |
−
′
then we have, by lemma 4.16, π ◦ s−
1 ≤ s2 , some permutation π. So if π ◦ s1 = s2 and
′′
′′
′
s2 = s2 s2 , determinacy of σ dictates that s2 .1 be in A, to |s1 ; t1 | = |s2 ; t2 | and s2 ; t2
ending in C.
In order to obtain a category of nominal games, we still need to show that strategy composition is associative. We omit the (rather long) proof and refer the interested reader
to [48].
Proposition 4.18. For any σ : A → B, σ1 : A′ → A and σ3 : B → B ′ ,
idA ; σ = σ = σ ; idB

∧

(σ1 ; σ) ; σ3 = σ1 ;(σ ; σ3 ) .



Definition 4.19. The category G of nominal games contains nominal arenas as objects
and nominal strategies as arrows.
N

28

N. TZEVELEKOS

In the rest of this section let us examine closer the proof of proposition 4.17 in order identify
where exactly is strong support needed, and for which reasons is the nominal games model
of [2] flawed.
Remark 4.20 (The need for strong support). The nominal games presented here
differ from those of [2] crucially in one aspect; namely, the modelling of local state. In [2]
local state is modelled by finite sets of names, so a move-with-names is a move attached
with a finite set of names, and other definitions differ accordingly. The problem is that
thus determinacy is not preserved by strategy composition: information separating freshly
created names may be hidden by composition and hence a composite strategy may break
determinacy by distinguishing between composite plays that are equivalent.
In particular, in the proof of determinacy above we first derived from [s′1 ; t1 ] = [s′2 ; t2 ]
that there exists some π so that π ◦ s′1 = s2 and π ◦ t1 = t2 , by appealing to lemma 4.16;
in the (omitted) proof of that lemma, the Strong Support Lemma needs to be used several
times. In fact, the statement
|s′1 k t1 | = |s′2 k t2 | ∧ [s′1 ; t1 ] = [s′2 ; t2 ] =⇒ ∃π. π ◦ s′1 = s′2 ∧ π ◦ t1 = t2
does not hold in a weak support setting such that of [2]. For take some i ∈ ω and consider
the following AGMOS-strategies (i.e. strategies of [2]).
σ : 1 → Ai , { [∗ a{a,b} ] | a, b ∈ Ai ∧ a 6= b } ,

(4.20:A)

τ : Ai → Ai ⇒ Ai , { [a ∗ c a] | a, c ∈ Ai } .
Then,

[∗ a{a,b} ; a ∗ b] = [∗ ∗{a,b} b{a,b} ] = [∗ ∗{a,b} a{a,b} ] = [∗ a{a,b} ; a ∗ a] ,
yet for no π do we have π ◦ (∗ a{a,b} ) = ∗ a{a,b} and π ◦ (a∗b) = a∗a. As a result, determinacy
fails for σ ; τ since both [∗ ∗{a,b} b{a,b} a{a,b} ], [∗ ∗{a,b} a{a,b} a{a,b} ] ∈ σ ; τ .
Another point where we used the Strong Support Lemma in the proof of determinacy
was in showing (the dual of):
∃π, π ′ . π ◦ (s1 , t′1 ) = (s2 , t′2 ) ∧ π ′ ◦ t′1 nb̄11 = t′2 nb̄22 =⇒ ∃π ′′ . π ′′ ◦ (s1 , t′1 nb̄11 ) = (s2 , t′2 nb̄22 )
i.e.

[s1 , t′1 ] = [s2 , t′2 ] ∧ [t′1 nb̄11 ] = [t′2 nb̄22 ] =⇒ [s1 , t′1 nb̄11 ] = [s2 , t′2 nb̄22 ] .

The above statement does not hold for AGMOS-games. To show this, we need to introduce7
the flat arena Ai ⊙ Ai with MAi ⊙Ai , P2 (Ai ) (the set of 2-element subsets of Ai ). This is
not a legal arena in our setting, since its moves are not strongly supported, but it is in the
AGMOS setting. Consider the following strategies.
σ : Ai ⊗ Ai → Ai ⊙ Ai , { [ (a, b) {a, b}] | a, b ∈ Ai ∧ a 6= b }
τ : Ai ⊙ Ai → Ai , { [{a, b} a] | a, b ∈ Ai ∧ a 6= b }

(4.20:B)

We have that [ (a, b) {a, b}, {a, b}] = [ (a, b) {a, b}, {a, b}] and [{a, b} a] = [{a, b} b] , yet
[ (a, b) {a, b}, {a, b} a] 6= [ (a, b) {a, b}, {a, b} b] .
N

In fact, determinacy is broken since [ (a, b) a], [ (a, b) b] ∈ σ ; τ .

7This is because our presentation of nominal games does not include plays and strategies with non-empty

initial local state. In the AGMOS setting we could have used to the same effect the {a, b}-strategies:
σ : Ai ⊗ Ai → 1 , { [ (a, b){a,b} ∗{a,b} ]{a,b} } ,

τ : 1 → Ai , { [∗{a,b} a

{a,b}

]{a,b} } .

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

29

4.2. Arena and strategy orders in G. G is the raw material from which several subcategories of nominal games will emerge. Still, though, there is structure in G which will be
inherited to the refined subcategories we will consider later on. In particular, we consider
(subset) orderings for arenas and strategies, the latter enriching G over Cpo.8 These will
prove useful for solving domain equations in categories of nominal games.
Definition 4.21. For any arenas A, B and each σ, τ ∈ G(A, B) define σ ⊑ τ ⇐⇒ σ ⊆ τ .
F
S
For each ⊑-increasing sequence (σi )i∈ω take i σi , i σi .
N
F
It is straightforward to see that each such i σi is indeed a strategy: prefix closure, contingency completeness and determinacy easily follow from the fact that the sequences we
consider are ⊑-increasing. Hence, each G(A, B) is a cpo with least element the empty
strategy (i.e. the one containing only [ǫ]). More than that, these cpo’s enrich G.
Proposition 4.22. G is Cpo-enriched wrt ⊑.
Proof: Enrichment amounts to showing the following straightforward assertions.
σ ⊑ σ ′ ∧ τ ⊑ τ ′ =⇒ σ ; τ ⊑ σ ′ ; τ ′
G
G
(σi ; τ )
(σi )i∈ω an ω-chain =⇒ ( σi ) ; τ ⊑
i∈ω

i∈ω

(τi )i∈ω an ω-chain =⇒ σ ;(

G

τi ) ⊑

i∈ω

G

(σ ; τi )

i∈ω



On the other hand, arenas are structured sets and hence also ordered by a ‘subset relation’.
Definition 4.23. For any A, B ∈ Ob(G) define
A E B ⇐⇒ MA ⊆ MB ∧ IA ⊆ IB ∧ λA ⊆ λB ∧ ⊢A ⊆ ⊢B ,
and for any E-increasing sequence (Ai )i∈ω define
[
G
Ai .
Ai ,
i∈ω

i∈ω

If A E B then we can define an embedding-projection pair of arrows by setting:
inclA,B : A → B , { [s] ∈ [PA→B ] | [s] ∈ idA ∨ (odd(|s|) ∧ [s− ] ∈ idA ) } ,
projB,A : B → A , { [s] ∈ [PB→A ] | [s] ∈ idA ∨ (odd(|s|) ∧ [s− ] ∈ idA ) } .

There is also an indexed version of E, for any k ∈ N,
A Ek B ⇐⇒ A E B ∧ { m ∈ MB | level(m) < k } ⊆ MA .

N

F

It is straightforward to see that i∈ω Ai is well-defined, and that E forms a cpo on Ob(G)
with least element the empty arena 0. By inclA,B and projB,A being an embeddingprojection pair we mean that:
inclA,B ; projB,A = idA

∧

projB,A ; inclA,B ⊑ idB

(4.3)

8By cpo we mean a partially ordered set with least element and least upper bounds for increasing ωsequences. Cpo is the category of cpos and continuous functions.

30

N. TZEVELEKOS

Note that in essence both inclA,B and projB,A are equal to idA , the latter seen as a
partially defined strategy on prearenas A → B and B → A. Finally, it is easy to show the
following.
A E B E C =⇒ inclA,B ; inclB,C = inclA,C
(TRN)
4.3. Innocence: the category V. In game semantics for pure functional languages (e.g.
PCF [16]), the absence of computational effects corresponds to innocence of the strategies.
Here, although our aim is to model a language with effects,
our model will use innocent strategies: the effects will still
be achieved, by using monads.
Innocence is the condition stipulating that the strategies
be completely determined by their behaviour on P-views.
In our current setting the manipulation of P-views presents
some difficulties, since P-views of plays need not be plays
themselves. For example, the P-view of the play on the
side (where curved lines represent justification pointers) is
∗ (∗, ∗) ∗ a and violates (NC2). Consequently, we need to
explicitly impose innocence on plays.

1

/ 1⊥ ⊗ A
i

∗

OQ

(∗, ∗)

PA

∗

OQ

∗a

PA

∗

OQ

a

PA

Definition 4.24. A legal sequence s is an innocent play if s.1 has empty name-list and
s also satisfies the following Name Change Conditions:
(NC1) The name-list of a P-move x in s contains as a prefix the name-list of the move
preceding it. It possibly contains some other names, all of which are fresh for s<x .
(NC2′ ) Any name in the support of a P-move x in s that is fresh for ps<xq is contained
in the name-list of x.
(NC3) The name-list of a non-initial O-move in s is that of the P-move justifying it.
The set of innocent plays of A is denoted by PAi .

N

It is not difficult to show now that a play s is innocent iff, for any t ≤ s, ptq is a play. We
can obtain the following characterisation of name-introduction in innocent plays.
Proposition 4.25 (Name-introduction). Let s be an innocent play. A name a is introduced by Player in s iff there exists a P-move x in s such that a ∈ S(x) and a # ps<xq.
Proof: If a is introduced by a P-move x in s then a ∈ nlist(x) and a # nlist(s<x .−1), hence,
by (NC1), a # s<x so a # ps<xq. Conversely, if a ∈ S(x) and a # ps<xq then, by (NC2′ ),
a ∈ nlist(x), while a # ps<xq implies a # nlist(s<x .−1).
Innocent plays are closed under composition (proof omitted, v. [48]).
Proposition 4.26. If s ∈ PA→B , t ∈ PB→C are innocent and s ≍ t then s ; t is innocent.
We now move on to innocent strategies and show some basic properties.
Definition 4.27. A strategy σ is an innocent strategy if [s] ∈ σ implies that s is innocent,
and if even-length [s1 x1 ] ∈ σ and odd-length [s2 ] ∈ σ have [ps1q] = [ps2q] then there exists
x2 such that [s2 x2 ] ∈ σ and [ps1 x1q] = [ps2 x2q].
N
Lemma 4.28. Let σ be an innocent strategy.
(1) If [s] ∈ σ then [psq] ∈ σ.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

31

(2) If sy is an even-length innocent play and [s], [psyq] ∈ σ then [sy] ∈ σ.
(3) If psyq is even-length with nlist(y) = nlist(s.−1) and [s], [psyq] ∈ σ then [sy] ∈ σ.
(4) If s is an even-length innocent play and, for any s′ ≤even s, [ps′q] ∈ σ then [s] ∈ σ.
Proof: For (1) we do induction on |s|. The base case is trivial. Now, if s = s′ y with y a
P-move then psq = ps′q y and [ps′q] ∈ σ by prefix closure and IH. By innocence, there exists
y ′ such that [ps′q y ′ ] ∈ σ and [ps′q y ′ ] = [psyq], so done. If s = s1 ys2 x and x an O-move
justified by y then [ps1 yq] ∈ σ by prefix closure and IH, hence [ps1 yq x] ∈ σ by contingency
completeness.
For (2) note that by innocence we have [sy ′ ] ∈ σ for some y ′ such that [psyq] = [psy ′q].
Then,
[psq, y] = [psq, y ′ ] ∧ [psq, s] = [psq, s] ∧ (S(y) \ S(psq)) ∩ S(s) = (S(y ′ ) \ S(psq)) ∩ S(s) = ∅ .
Thus we can apply the strong support lemma and get [sy] = [sy ′ ], as required.
For (3) it suffices to show that sy is an innocent play. As s, psq y are plays, it suffices
to show that sy satisfies the name conditions at y. (NC3) and (NC2′ ) hold because psyq a
play. (NC1) also holds, as y is non-introducing.
For (4) we do induction on |s|. The base case is encompassed in psq = s, which is trivial.
For the inductive step, let s = s− x with psq 6= s. By IH and contingency completeness we
have [s− ] ∈ σ, and since [psq] ∈ σ, by (2), [s] ∈ σ.
We can now show that innocent strategies are closed under composition (details in [48]).
Proposition 4.29. If σ : A → B, τ : B → C are innocent strategies then so is σ ; τ .
Definition 4.30. V is the lluf subcategory of G of innocent strategies.

N

Henceforth, when we consider plays and strategies we presuppose them being innocent.
Viewfunctions. We argued previously that innocent strategies are specified by their behaviour on P-views. We formalise this argument by representing innocent strategies by
viewfunctions.
Definition 4.31. Let A be a prearena. A viewfunction f on A is a set of equivalence
classes of innocent plays of A which are even-length P-views, satisfying:
• Even-prefix closure: If [s] ∈ f and t is an even-length prefix of s then [t] ∈ f .
• Single-valuedness: If [s1 x1 ], [s2 x2 ] ∈ f and [s1 ] = [s2 ] then [s1 x1 ] = [s2 x2 ].
Let σ be an innocent strategy and let f be a viewfunction. Then, we can define a corresponding viewfunction and a strategy by:
viewf(σ) , { [s] ∈ σ | |s| even ∧ psq = s } ,
[
strat(f ) ,
stratn (f ) ,
n

where strat0 (f ) , {[ǫ]} and:

strat2n+1 (f ) , { [sx] | sx ∈ PAi ∧ [s] ∈ strat2n (f ) } ,
strat2n+2 (f ) , { [sy] | sy ∈ PAi ∧ [s] ∈ strat2n+1 (f ) ∧ [psyq] ∈ f } .

N

Note in the above definition that, for any even-length s, [s] ∈ strat(f ) implies [psq] ∈ f .
We can show that the conversion functions are well-defined inverses.

32

N. TZEVELEKOS

Proposition 4.32. For any innocent strategy σ, viewf(σ) is a viewfunction. Conversely,
for any viewfunction f , strat(f ) is an innocent strategy. Moreover,
f = viewf(strat(f )) ∧ σ = strat(viewf(σ)) .



Recall the subset ordering ⊑ of strategies given in definition 4.21. It is easy to see that
the ordering induces a cpo on innocent strategies and that V is Cpo-enriched. We can also
show the following.
Corollary 4.33. For all viewfunctions f, g and innocent strategies σ, τ ,
(1) f ⊆ strat(f ) ,
(2) σ ⊆ τ ⇐⇒ viewf(σ) ⊆ viewf(τ ) , f ⊆ g ⇐⇒ strat(f ) ⊆ strat(g) ,
(3) viewf(σ) ⊆ τ ∧ viewf(τ ) ⊆ σ =⇒ σ = τ .
Moreover, ⊑ yields a cpo on viewfunctions, and viewf and strat are continuous with
respect to ⊑.
Notation 4.34 (Diagrams of viewfunctions). We saw previously that innocent strategies can be represented by their viewfunctions. A viewfunction is a set of (equivalence
classes of) plays, so the formal way to express such a construction is explicitly as a set. For
example, we have that
viewf(idA ) = { [sm(1) m(2) ] | [s] ∈ viewf(idA ) ∧ (m ∈ IA ∨ (s.−1 ⊢A m(1) ∧ s.−2 ⊢A m(2) )) } .
The above behaviour is called copycat (v. [4]) and is perhaps the most focal notion in game
semantics.
A more convenient way to express viewfunctions is by means of diagrams. For example,
for idA we can have the following depiction.
idA : A
iA

/A
OQ

iA

PA

The polygonal line in the above depiction stands for a copycat link , meaning that the
strategy copycats between the two iA ’s. A more advanced example of this notation is the
strategy in the middle below.
A⇒B
∗
iA

hA,B : (A ⇒ B)⊗A
PA

(∗, iA )

OQ

A−

OQ

∗
∗
iA

hA,B : (A ⇒ B)⊗A

/ B⊥

(∗, iA )

PA

OQ

∗
∗

OQ
PQ

/ B⊥

iA

PA
OQ
PQ

B
jA

OQ

jA

PQ

iB

OA

iB

PA

Note first that curved lines (and also the line connecting the two ∗’s) stand for justification
pointers. Moreover, recall that the arena A ⇒ B has the form given on the left above, so
the leftmost iA (l-iA ) in the diagram of hA,B has two child components, A− and B. Then,

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

33

the copycat links starting from the l-iA have the following meaning. hA,B copycats between
the A− -component of l-iA and the other iA , and copycats also between the B-component
of l-iA and the lower ∗. That is (modulo prefix-closure),
hA,B , strat{ [ (∗, iA ) ∗ ∗ iA s ] | [ iA iA s ] ∈ viewf(idA ) ∨ [s] ∈ viewf(idB ) } .
Another way to depict hA,B is by cases with regard to Opponent’s next move after l-iA , as
seen on the right diagram above.
Finally, we will sometimes label copycat links by strategies (e.g. in the proof of proposition 4.42). Labelling a copycat link by a strategy σ means that the specified strategy plays
like σ between the linked moves, instead of doing copycat. In this sense, ordinary copycat
links can be seen as links labelled with identities.
4.4. Totality: the category Vt . We introduce the notion of total strategies, specifying
those strategies which immediately answer initial questions without introducing fresh names.
We extend this type of reasoning level-1 moves, yielding several subclasses of innocent
strategies. Note that an arena A is pointed if IA is singleton.
Definition 4.35. An innocent strategy σ : A → B is total if for any [iA ] ∈ σ there exists
[iA iB ] ∈ σ. A total strategy σ : A → B is:
• l4 if whenever [s] ∈ σ and s.−1 ∈ JA then | psq | = 4,
b̄ ] ∈ σ,
• t4 if for any [iA iB jB ] ∈ σ there exists [iA iB jB jA
• tl4 if it is both t4 and l4,
• ttotal if it is tl4 and for any [iA iB jB ] ∈ σ there exists [iA iB jB jA ] ∈ σ.
A total strategy τ : C ⊗A → B is:
• l4* if whenever [s] ∈ τ and s.−1 ∈ JA then | psq | = 4,
b̄ ] ∈ τ ,
• t4* if for any [ (iC , iA )iB jB ] ∈ τ there exists [ (iC , iA )iB jB jA
• tl4* if it is both t4* and l4*.
We let Vt be the lluf subcategory of V of total strategies, and Vtt its lluf subcategory of
ttotal strategies. Vt∗ and Vtt∗ are the full subcategories of Vt and Vtt respectively containing
pointed arenas.
N
The above subclasses of strategies will be demystified in the sequel. For now, we show a
technical lemma. Let us define, for each arena A, the diagonal strategy ∆A as follows.
∆A : A → A⊗A , strat{ [ iA (iA , iA ) s ] | [ iA iA s ] ∈ viewf(idA ) }

(4.4)

Lemma 4.36 (Separation of Head Occurrence). Let A be a pointed arena and let
f : A → B be a t4 strategy. There exists a tl4* strategy f˜ : A⊗A → B such that f = ∆ ; f˜.
Proof: Let us tag the two copies of A in A ⊗ A as A(1) and A(2) , and take
b̄
b̄
˜ viewf(f ) ∧ ∀i. s.i ∈
/ JA(2) } ,
f˜ , strat{ [ (iA , iA )iB jB jA
s ] | [ iA iB jB jA
s]∈
(2)
(2)

˜ is the composition of de-indexing from MA(1) and MA(2) to MA with ∈. Intuitively,
where ∈
f˜ plays the first JA -move of f in A(2) , and then mimics f until the next JA -move of f ,
which is played in A(1) . All subsequent JA -moves are also played in A(1) . Clearly, f˜ is tl4*
and f = ∆ ; f˜.

34

N. TZEVELEKOS

We proceed to examine Vt . Eventually, we will see that it contains finite products and that
it contains some exponentials, and that lifting promotes to a functor.
Lifting and product. We first promote the lifting and tensor arena-constructions to functors.
In the following definition recall L from notation 4.6 and note that we write L(m) # m′ for
L(m) ∩ S(m′ ) = ∅.
Definition 4.37. Let f : A → A′ , g : B → B ′ in Vt . Define the arrows
f ⊗g , strat{ [ (iA , iB ) (iA′ , iB ′ ) s ] |
( [ iA iA′ s ] ∈ viewf(f ) ∧ [iB iB ′ ] ∈ g ∧ L(iA iA′ s) # iB )
∨ ( [ iB iB ′ s ] ∈ viewf(g) ∧ [iA iA′ ] ∈ f ∧ L(iB iB ′ s) # iA ) } ,
f⊥ , strat{ [∗ ∗′ ∗′ ∗ s] | [s] ∈ viewf(f ) } ,
of types f ⊗g : A⊗B → A′ ⊗B ′ and f⊥ : A⊥ → A′⊥ .

N

Let us give an informal description of the above constructions:
• f⊥ : A⊥ → A′⊥ initially plays a sequence of asterisks [∗ ∗′ ∗′ ∗] and then continues playing
like f .
• f ⊗g : A⊗B → A′ ⊗B ′ answers initial moves [ (iA , iB ) ] with f ’s answer to [iA ] and g’s
answer to [iB ]. Then, according to whether Opponent plays in JA′ or in JB ′ , Player
plays like f or like g respectively.
Note that f⊥ is always ttotal. We can show the following.
Proposition 4.38.

⊗

: Vt × Vt → Vt and ( )⊥ : Vt → Vtt∗ are functors.

Moreover, ⊗ yields products and hence Vt is cartesian.
Proposition 4.39. Vt is cartesian: 1 is a terminal object and ⊗ is a product constructor.
Proof: Terminality of 1 is clear. Moreover, it is straightforward to see that ⊗ yields
a symmetric monoidal structure on Vt , with its unit being 1 and its associativity, leftunit, right-unit and symmetry isomorphisms being the canonical ones. Hence, it suffices
to show that there exists a natural coherent diagonal, that is, a natural transformation
∆ : IdVt → ⊗ ◦ hIdVt , IdVt i (where hIdVt , IdVt i is the diagonal functor on Vt ) such that the
following diagrams commute for any A, B in Vt .
∆A ⊗∆B

/ (A⊗A)⊗(B ⊗B)
A⊗B TT
TTTT
TTTT
∼
TTT
=
∆A⊗ B TTTT)

(A⊗B)⊗(A⊗B)

A
qq MMMMM ∼
MM=
MMM
∆A
MM&

/ A⊗1
A⊗A

q
∼
=qqqq

qq
xqqq
1⊗A o

!A ⊗idA

idA ⊗!A

But it is easy to see that the diagonal of (4.4) makes the above diagrams commute. Naturality follows from the single-threaded nature of strategies (v. [14]).

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

π

35

π

1
2
Products are concretely given by triples A ←−
A⊗B −→
B, where

π1 = strat{ [ (iA , iB ) iA s ] | [iA iA s] ∈ viewf(idA ) }
f

g

and π2 similarly, while for each A ←
−C−
→ B we have
hf, gi : C → A⊗B = strat{ [ iC (iA , iB ) s ] |
( [iC iA s] ∈ viewf(f ) ∧ [iC iB ] ∈ viewf(g) )
∨ ( [iC iA ] ∈ viewf(f ) ∧ [iC iB s] ∈ viewf(g) ) } .
Finally, we want to generalise the tensor product to a version applicable to countably many
arguments. In arenas, the construction comprises of gluing countably many arenas together
at their initial moves. The problem that arises then is that the product of infinitely many
(initial) moves need not have finite support, breaking the arena specifications. Nevertheless,
in case we are interested only in pointed arenas, this is easily bypassed: a pointed arena has
a unique initial move, which is therefore equivariant, and the product of equivariant moves
is of course also equivariant.
N
Proposition and Definition 4.40. For pointed arenas {Ai }i∈ω define i Ai by:
]
MNi Ai , {∗} +
λNi Ai , [ (∗ 7→ P A), [λAi i∈ω ]] ,
I¯Ai ,
i
[
⊢Ni Ai , {(†, ∗)} ∪ { (∗, jAi ) | i ∈ ω } ∪
INi Ai , {∗} ,
(⊢Ai ↾ I¯Ai 2 ) .
i

For {fi : Ai → Bi }i∈ω with Ai ’s and Bi ’s pointed define:
O
fi , strat{ [∗ ∗ s] | ∃k. [iAk iBk s] ∈ viewf(fk ) } .
i
N Q
: Vt∗ → Vt∗ is a functor.
Then,

In fact, we could proceed and show that the aforedefined tensor yields general products of
pointed objects, but this will not be of use here.
Partial exponentials. We saw that Vt has products, given by the tensor functor ⊗. We
now show that the arrow constructor yields appropriate partial exponentials, which will be
sufficient for our modelling tasks.
Let us introduce the following transformations on strategies.
Definition 4.41. For all arenas A, B, C with C pointed, define a bijection
∼
=

→ Vt (A, B −−⊗ C)
ΛB
A,C : Vt (A⊗B, C) −
by taking, for each h : A⊗B → C and g : A → B −−⊗ C ,9
−−⊗ C , strat{ [i
ΛB
A iC (iB , jC ) s] | [ (iA , iB ) iC jC s ] ∈ viewf(h) } ,
A,C (h) : A → B

−1
ΛB
A,C (g) : A⊗B → C , strat{ [ (iA , iB ) iC jC s ] | [iA iC (iB , jC ) s] ∈ viewf(g) } .

For each (f, g) : (A, B) → (A′ , B ′ ), define the arrows
A
evA,B : (A −−⊗ B)⊗A → B , ΛA

f

−−⊗

−1
B,B (idA−−⊗B ) ,

−−⊗

g : A′ −−⊗ B → A −−⊗ B ′ , ΛA
A

′

B,A′ −−⊗B ′ (id⊗f

−−⊗

; ev ; g) .

N

9Note the reassignment of pointers that takes place implicitly in the definitions of Λ, Λ−1 , in order e.g. for

(iA , iB ) iC jC s to be a play of viewf(h).

36

N. TZEVELEKOS

It is not difficult to see that Λ and Λ−1 are well-defined and mutual inverses. What is more,
they supply us with exponentials.
Proposition 4.42. Vt has partial exponentials wrt to ⊗, in the following sense. For any
object B, the functor ⊗B : Vt → Vt has a partial right adjoint B −−⊗ : Vt∗ → Vt , that
is, for any object A and any pointed object C the bijection ΛB
A,C is natural in A.
Proof: It suffices to show that, for any
f : A⊗B → C and g : A → B −−⊗ C,
Λ(f )⊗id ; ev = f ,

Λ(f ) ⊗id

A⊗B

A consequence of partial exponentiation is that
: (Vt )

Now, in case g is ttotal, the strategy f
strat(φ), where

−−⊗

/C

(iC , iB )

These equalities are straightforward. For example, the viewfunction of Λ(f )⊗id ; ev is given by
the diagram on the side, which also gives the
viewfunction of f .

−−⊗

ev

(iA , iB )

g ⊗id ; ev = Λ−1 (g) .

op

/ (B −−⊗ C)⊗B

iC
jC
(iB , jC )
f
−−⊗

naturally upgrades to a functor:

× Vt∗ → Vt .

g : A′

−−⊗

B → A −−⊗ B ′ is given concretely by

φ = { [iB iB ′ (iA , jB ′ ) (iA′ , jB ) s] |
([iA iA′ s] ∈ viewf(f ) ∧ [iB iB ′ jB ′ jB ] ∈ g ∧ L(iA iA′ s)#iB , jB ′ )
∨ ([iB iB ′ jB ′ jB s] ∈ viewf(g) ∧ [iA iA′ ] ∈ f ∧ L(iB iB ′ jB ′ jB s)#iA ) }.
That is, f −−⊗ g answers initial moves [iB ] like g and then responds to [iB iB ′ (iA , jB ′ ) ] with
f ’s answer to [iA ] and g’s response to [iB iB ′ jB ′ ] (recall g ttotal). It then plays like f or
like g, according to Opponent’s next move. Note that φ is a viewfunction even if B, B ′ are
not pointed.
A special case of ttotality in the second argument arises in the defined functor:
⇒

: (Vt )op × Vt → Vtt∗ ,

−−⊗

( )⊥ .

(4.5)

Remark 4.43. In the work on CBV games of Honda & Yoshida [15] the following version
of partial exponentiation is shown.
V(A⊗B, C) ∼
(4.6)
= Vt (A, B ⇒ C)
Interestingly, that version can be derived from ours (using also another bijection shown
in [15]),
V(A⊗B, C) ∼
= Vt (A⊗B, C⊥ ) ∼
= Vt (A, B −−⊗ C⊥ ) = Vt (A, B ⇒ C) .

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

37

But also vice versa, if C is pointed then C ∼
= C2 ⇒ C1 , for some arenas C1 , C2 ,10 and
(4.6)

(4.6)

Vt (A⊗B, C2 ⇒C1 ) ∼
= Vt (A, (B ⊗ C2 )⇒C1 ) = Vt (A, B −−⊗(C2 ⇒C1 )) .
= V(A⊗B ⊗C2 , C1 ) ∼
Strategy and arena orders. Recall the orders defined for strategies (⊑) and arenas (E) in
section 4.2. These being subset orderings are automatically inherited by Vt . Moreover,
by use of corollary 4.33 we can easily show that the aforedefined functors are continuous.
Note that, although the strategy order ⊑ is inherited from V, the least element (the empty
strategy) is lost, as it is not total.
Proposition 4.44. Vt and Vtt are PreCpo-enriched wrt ⊑.11 Moreover,
O
Y
( )⊥ : Vt → Vtt∗ ,
( ⊗ ) : Vt × Vt → Vt ,
(
):
Vt∗ → Vt∗ ,
(

−−⊗

) : Vtop × Vtt∗ → Vtt∗ , ( ⇒ ) : Vtop × Vt → Vtt∗

are locally continuous functors.
The order of arenas in Vt is the same as in G, and therefore Ob(Vt ) is a cpo with least
element 0. Note that A E B does not imply that the corresponding projection is a total
strategy — but A E1 B does imply it. In fact,
A E1 B =⇒ projB,A ∈ Vtt (B, A)

∧

A E2 B =⇒ inclA,B ∈ Vtt (A, B) .

Moreover, we have the following.
Proposition 4.45. All of the functors of proposition 4.44 are continuous wrt E . Moreover,
A E A′ ∧ B E B ′ =⇒ inclA,A′ ⊗inclB,B ′ = inclA⊗B,A′ ⊗B ′
A E1 A′ ∧ B E1 B ′ =⇒ projA′ ,A ⊗projB ′ ,B = projA′ ⊗B ′ ,A⊗B
O
∀i ∈ ω. Ai E A′i =⇒
inclAi ,A′i = inclNi Ai ,Ni A′i
i
O
∀i ∈ ω. Ai E A′i =⇒
projA′ ,Ai = projNi A′ ,Ni Ai
i

i

i

A E1 A′ ∧ B E B ′ =⇒ projA′ ,A ⇒ inclB,B ′ = inclA⇒B,A′ ⇒B ′
A E A′ ∧ B E1 B ′ =⇒ inclA,A′ ⇒ projB ′ ,B = projA′ ⇒B ′ ,A⇒B

A E1 A′ ∧ B E2 B ′ =⇒ projA′ ,A −−⊗ inclB,B ′ = inclA
′

′

A E A ∧ B E1 B =⇒ inclA,A′

−−⊗

B,A′ −−⊗B ′

−−⊗

projB ′ ,B = projA′

B ′ ,A−−⊗B

−−⊗

.

Proof: All the clauses are in effect functoriality statements, since the underlying sets of
inclusions and projections correspond to identity strategies.
10 In fact, for C to be expressed as C ⇒ C we need a stronger version of condition (f), namely:
2
1

(f’)

For each m ∈ MA , there exists unique k ≥ 0 and a unique sequence x1 . . . xn ∈ {Q, A}∗ such that
IA ∋ m1 ⊢A · · · ⊢A mk ⊢A m , for some ml ’s in MA with λQA
C (ml ) = xl .

A
In such a case, C1 and C2 are given by taking KC
, { m ∈ MC | ∃jC . jC ⊢C m ∧ λC (m) = P A } and
A
A
A
⊢C1 , ⊢C ↾ (MC1 × I¯C1 ) λC1 , λC ↾ MC1
MC1 , KC + { m ∈ MC | ∃k ∈ KC . k ⊢C · · · ⊢C m } IC1 , KC

MC2 , I¯C \ MC1

λC2 , [iC2 7→ P A, m 7→ λ̄C (m) ] IC2 , JC

⊢C2 , ⊢C ↾ (MC2 × I¯C2 ) .

11 By precpo we mean a cpo which may not have a least element. PreCpo is the category of precpos and
continuous functions.

38

N. TZEVELEKOS

4.5. A monad, and some comonads. We now proceed to construct a monad and a
family of comonads on Vt that will be of use in later sections. Specifically, we will upgrade
lifting to a monad and introduce a family of product comonads for initial state.
Lifting monad. It is a more-or-less standard result that the lifting functor induces a monad.
Definition 4.46. Define the natural transformations up, dn, st as follows.
upA : A → A⊥ = strat{ [iA ∗1 ∗2 iA s] | [iA iA s] ∈ viewf(idA ) }
dnA : A⊥⊥ → A⊥ , strat{ [∗1 ∗′1 ∗′2 ∗2 ∗3 ∗4 s] | [s] ∈ viewf(idA ) }
stA,B : A⊗B⊥ → (A⊗B)⊥ , strat{ [ (iA , ∗1 ) ∗′1 ∗′2 ∗2 iB (iA , iB ) s]
| [ (iA , iB ) (iA , iB ) s] ∈ viewf(idA⊗B ) }
N

(primed asterisks are used for arenas on the RHS, where necessary).

Proposition 4.47. The quadruple (( )⊥ , up, dn, st) is a strong monad on Vt . Moreover,
it yields monadic exponentials by taking (C⊥ )B to be B ⇒ C, for each B, C.
Proof: It is not difficult to see that (( )⊥ , up, dn, st) is a strong monad. Moreover, for
each B, C we have that B ⇒ C = B −−⊗ C⊥ is a ( )⊥ -exponential, because of exponentiation
properties of −−⊗.
Although finding a canonical arrow from A to A⊥ is elementary (upA ), finding a canonical
arrow in the inverse direction is not always possible. In some cases, e.g. A = Ai , there is no
such arrow at all, let alone canonical. An exception occurs when A is pointed, by setting:
puA : A⊥ → A , strat{ [∗ iA jA ∗ iA jA s] | [iA iA jA jA s] ∈ viewf(idA ) } .

(4.7)

Lemma 4.48. puA yields a natural transformation pu : ( )⊥(Vtt∗ ) → IdVtt∗ . Moreover, for
any arenas A, B with B pointed, upA ; puA = idA , puA⊥ = dnA and


puB
st′
ev⊥
puA B = Λ (A −−⊗ B)⊥ ⊗A −−→ ((A −−⊗ B)⊗A)⊥ −−→
B⊥ −−→
B .

−−⊗

Initial-state comonads. Our way of modelling terms-in-local-state will be by using initial
state comonads, in the spirit of intensional program modelling of Brookes & Geva [9]. In
our setting, the initial state can be any list ā of distinct names; we define a comonad for
each one of those lists.
Definition 4.49 (Initial-state comonads). For each ā ∈ A# define the triple (Qā , ε, δ)
and
by taking Qā : Vt → Vt , Aā ⊗
π

2
ε : Qā → IdVt , { εA : Aā ⊗A −→
A},

∆⊗id

δ : Qā → (Qā )2 , { δA : Aā ⊗A −−−−→ Aā ⊗ Aā ⊗A } .
For each S(ā′ ) ⊆ S(ā) define the natural transformation

ā
ā′

′

: Qā → Qā by taking

′

( āā′ )A : Aā ⊗A → Aā ⊗A , ( āā′ )1 ⊗idA ,
where ( āā′ )1 is

ā
ā′

of definition 4.8, that is, ( āā′ )1 , { [ (ā, ∗) (ā′ , ∗) ] } .

N

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

39

Note that Qǫ , the comonad for empty initial state, is the identity comonad. Note also that
we have suppressed indices ā from transformations ε, δ for notational economy.
Clearly, each triple (Qā , ε, δ) forms a product comonad on Vt . Moreover, it is straightforward to show the following.
Proposition 4.50 (Chain rule). For each S(ā′ ) ⊆ S(ā) ∈ A# , the transformation āā′ is
a comonad morphism. Moreover, āǫ = ε : Qā → IdVt , āā = id : Qā → Qā and, for each
′′
S(ā′ ) ⊆ S(ā′′ ) ⊆ S(ā), āā′′ ; āā′ = āā′ .
Finally, for each name-type i, we can define a name-test arrow:
eqi : Ai ⊗ Ai → N , { [ (a, a) 0] } ∪ { [ (a, b) 1] | a 6= b } ,

(4.8)

which clearly makes the (N1) diagram (definition 3.12) commute.
Fresh-name constructors. Combining the monad and comonads defined previously we can
obtain a monadic-comonadic setting (Vt , ( )⊥ , Q), where Q denotes the family (Qā )ā∈A# .
This setting, which in fact yields a sound model of the ν-calculus [2, 48], will be used as
the basis of our semantics of nominal computation in the sequel. Nominal computation of
type A, in name-environment ā and variable-environment Γ, will be translated into the set
of strategies
{ σ : Qā JΓK → JAK ⊥ } .
The lifting functor, representing the monadic part of our semantical setting, will therefore
incorporate the computational effect of fresh-name creation.
We describe in this section the semantical expression of fresh-name creation. Fresh
names are created by means of natural transformations which transform a comonad Qā ,
say, to a monad-comonad composite (Qāa )⊥ .
Definition 4.51. Consider the setting (Vt , ( )⊥ , Q). We define natural transformations
newāa : Qā → (Qāa )⊥ by
newāa ⊗idA

st′

1
ā
āa
−→ (Aāa ⊗A)⊥ ,
newāa
A , A ⊗A −−−−−−−→ (A )⊥ ⊗A −

ā
āa
a
newāa
1 : A ⊗1 → (A ⊗1)⊥ , strat{ [ (ā, ∗) ∗ ∗ (āa, ∗) ] } ,

for each āa ∈ A# .

N

That new is a natural transformation is straightforward: for any f : A → B we can form
the following commutative diagram.

Aā ⊗A

new1 ⊗id

/ (Aāa )⊥ ⊗A

st′

/ (Aāa ⊗A)⊥

id ⊗f

id ⊗f

Aā ⊗B

(id ⊗f )⊥







new1 ⊗id

/ (Aāa )⊥ ⊗B

st′

/ (Aāa ⊗B)⊥

Moreover, we can show the following.
Proposition 4.52. In the setting (Vt , ( )⊥ , Q) with new defined as above, the (N2) diagrams (definition 3.12) commute.

40

N. TZEVELEKOS

The fresh-name constructor allows us to define name-abstraction on strategies by taking:
newāa

pu

σ

C
⊥
^ a _ σ , Qā B −−−B→ (Qāa B)⊥ −→
C⊥ −−→
C.

(4.9)

Name-abstraction can be given an explicit description as follows. For any sequence of
moves-with-names s and any name a # nlist(a), let sa be s with a in the head of all of its
name-lists. Then, for σ as above, we can show that:
viewf(^ a _ σ) = { [ (ā, iB ) iC jC mab̄ sa ] | [ (āa, iB ) iC jC mb̄ s] ∈ viewf(σ) ∧ a # iB , jC }
(4.10)
We end our discussion on fresh-name constructors with a technical lemma stating that
name-abstraction and currying commute.
Lemma 4.53. Let f : Qāa (A⊗B) → C with C a pointed arena. Then,

^ a _ Λ(ζ ′ ; f ) = Λ(ζ ′ ; ^ a _ f ) : Qā A → B −−⊗ C .
Proof: As follows.
′
^ a _ Λ(ζ ′ ; f ) = newāa
A ;(Λ(ζ ; f ))⊥ ; puB

C

−−⊗

′
′
= newāa
A ;(Λ(ζ ; f ))⊥ ; Λ(st ; ev ⊥ ; puC )

′
′
= Λ(newāa
A ⊗idB ;(Λ(ζ ; f ))⊥ ⊗idB ; st ; ev ⊥ ; puC )
′
′
= Λ(newāa
A ⊗idB ; st ;(Λ(ζ ; f )⊗idB )⊥ ; ev ⊥ ; puC )
(N2)

′
′
′
āa
= Λ(newāa
A ⊗idB ; st ;(ζ ; f )⊥ ; puC ) = Λ(ζ ; newA⊗B ; f⊥ ; puC )

and the latter equals Λ(ζ ′ ; ^ a _ f ).
Note that the above result does not imply that ν- and λ-abstractions commute in our
semantics of nominal languages, i.e. that we obtain identifications of the form Jνa.λx.M K =
Jλx.νa.M K. As we will see in the sequel, λ-abstraction is not simply currying, because of
the use of monads.
4.6. Nominal games à la Laird. As aforementioned, there have been two independent
original presentations of nominal games, one due to Abramsky, Ghica, Murawski, Ong and
Stark (AGMOS) [2] and another one due to Laird [21, 24]. Although Laird’s constructions
are are not explicitly based on nominal sets (natural numbers are used instead of atoms),
they constitute nominal constructions nonetheless. In this section we highlight the main
differences between our nominal games, which follow AGMOS, and those of [21, 24].
Laird’s presentation concerns the ν-calculus with pointers, i.e. with references to names.
The main difference in his presentation is in the treatment of name-introduction. In particular, a name does not appear in a play at the point of evaluation of its ν-constructor, but
rather at the point of its first use; let us refer to this condition as name-frugality (cf. [31]).
An immediate result is that strategies are no longer innocent, as otherwise e.g. νa.λx.a
and λx.νa.a would have the same denotation.12 More importantly, name-frugality implies
that strategies capture the examined nominal language more accurately: Opponent is not
expected to guess names he is not supposed to know and thus, for example, the denotations of νa.skip and skip are identical. In our setting, Player is not frugal with his names
12Non-innocence can be seen as beneficial in terms of simplicity of the model, since strategies then
have one condition less. On the other hand, though, innocent strategies are specified by means of their
viewfunctions, which makes their presentation simpler. Moreover, non-innocence diminishes the power of
definability results, as finitary behaviours are less expressive in absence of innocence.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

41

and therefore the two terms above are identified only at the extensional level (i.e. after
quotienting).13
The major difference between [21] and [24] lies in the modelling of (ground-type, namestoring) store. In [21] the store is modelled by attaching to strategies a global, top-level
(non-monadic), store arena. Then, a good-store-discipline is imposed on strategies via
extra conditions on strategy composition which enforce that hidden store-moves follow the
standard read/write pattern. As a result (and in contrast to our model), the model relies
heavily on quotienting by the intrinsic preorder in order for the store to work properly.
The added accuracy obtained by using frugality conditions is fully exploited in [24],
where a carefully formulated setting of moves-with-store14 allows for an explicit characterisation result, that is, a semantic characterisation of operational equality at the intensional
level. The contribution of using moves-with-store in that result is that thus the semantics is relieved from the (too revealing) internal workings of store: for example, terms like
(a := b) ; λx. ! a ; 0 and (a := b) ; λx.0 are equated semantically at the intensional level, in
contrast to what happens in our model.15 Note, though, that in a setting with higher-order
store such that of νρ, moves-with-store would not be as simple since stores would need to
store higher-order values, that is, strategies.
Laird’s approach is therefore advantageous in its use of name-frugality conditions, which
allow for more accurate models. At the same time, though, frugality conditions are an extra
burden in constructing a model: apart from the fact that they need to be dynamically preserved in play-composition by garbage collection, they presuppose an appropriately defined
notion of name-use. In [21, 24], a name is considered as used in a play if it is accessible
through the store (in a reflexive transitive manner) from a name that has been explicitly
played. This definition, however, does not directly apply to languages with different nominal effects (e.g. higher-order store). Moreover, frugality alone is not enough for languages
like Reduced ML or the ν-calculus: a name may have been used in a play but may still
be inaccessible to some participant (that is, if it is outside his view [31]). On the other
hand, our approach is advantageous in its simplicity and its applicability on a wide rage of
nominal effects (see [48]), but suffers from the accuracy issues discussed above.
5. The nominal games model
We embark on the adventure of modelling νρ in a category of nominal arenas and strategies.
Our starting point is the category Vt of nominal arenas and total strategies. Recall that Vt
is constructed within the category Nom of nominal sets so, for each type A, we have an
arena AA for references to type A.
13Note here, though, that the semantics being too explicit about the created names can prove beneficial:

here we are able to give a particularly concise proof adequacy for νρ (see section 5.3 and compare e.g. with
respective proof in [3]) by exploiting precisely this extra information!
14
Inter alia, frugality of names implies that sequences of moves-with-store have strong support even if
stores are represented by sets!
15In our model they correspond to the strategies (see also section 5):
σ1 , { [ (a, b) ∗ ⊛(∗, ⊛)(n, ⊛) a c 0] } ,

σ2 , { [ (a, b) ∗ ⊛(∗, ⊛)(n, ⊛) 0] } .

Thus, the inner-workings of the store revealled by σ1 (i.e. the moves a c) differentiate it from σ2 . In fact, in our
attempts to obtain an explicit characterisation result from our model, we found store-related innaccuracies
to be the most stubborn ones.

42

N. TZEVELEKOS

The semantics is monadic in a store monad built around a store arena ξ, and comonadic in an initial state comonad. The store monad is defined on top of the lifting monad
(see definition 4.46) by use of a side-effect monad constructor, that is,
T A , ξ −−⊗ (A ⊗ ξ)⊥

i.e. T A = ξ ⇒ A ⊗ ξ .

Now, ξ contains the values assigned to each name (reference), and thus it is of the form
O
(AA ⇒ JAK)
A∈TY

where JAK is the translation of each type A. Thus, a recursive (wrt type-structure) definition
of the type-translation is not possible because of the following cyclicity.
JA → BK = JAK −−⊗ (ξ ⇒ JBK ⊗ ξ)
O
(SE)
ξ=
(AA ⇒ JAK)
A

Rather, both ξ and the type-translation have to be computed as the least solution to the
above domain equation. By the way, observe that JA → BK = JAK ⊗ ξ ⇒ JBK ⊗ ξ .
5.1. Solving the Store Equation. The full form of the store equation (SE) is:
J1K = 1 ,

JNK = N ,

J[A]K = AA ,

JA → BK = JAK ⊗JBK ,
N
ξ = A(AA ⇒ JAK) .

JA → BK = JAK −−⊗ (ξ ⇒ JBK ⊗ ξ) ,

This can be solved either as a fixpoint equation in the cpo of nominal arenas or as a domain
equation in the PreCpo-enriched category Vt . We follow the latter approach, which provides
the most general notion of canonical solution (and which incorporates the solution in the
cpo of nominal arenas, analogously to [26]). It uses the categorical constructions of [43, 11]
for solving recursive domain equations, as adapted to games in [26].
Definition 5.1. Define the category
C , Vt ×

Y

Vt

A∈TY

with objects D of the form (Dξ , DA A∈TY ) and arrows f of the form (fξ , fA A∈TY ).
Now take F : (C)op ×C → C to be defined on objects by F (D, E) , (ξD,E , JAK D,E A∈TY ),
where:
JA × BK D,E , JAK D,E ⊗JBK D,E
J[A]K D,E , AA
J1K D,E , 1
N
JNK D,E , N
JA → BK D,E , DA −−⊗ (ξE,D ⇒ EB ⊗ξD,E )
ξD,E ,
A∈TY(AA ⇒ EA )
and similarly for arrows, with F (f, g) , (ξf,g , JAK f,g A∈TY ) .

N

Now (SE) has been reduced to:
D = F (D, D)
(SE∗ )
where F is a locally continuous functor wrt the strategy ordering (proposition 4.44), and
continuous wrt the arena ordering (proposition 4.45). The solution to (SE∗ ) is given via a
local bilimit construction to the following ω-chain in C.16
16Recall that we call an arrow e : A → B an embedding if there exists eR : B → A such that

e ; eR = idA ∧ eR ; e ⊑ idB .

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

43

Definition 5.2. In C form the sequence (Di )i∈ω taking D0 as below and Di+1 , F (Di , Di ).
D0,N , N

D0,1 , 1
D0,A→B , 1

D0,A×B , D0,A ⊗D0,B

Moreover, define arrows ei : Di → Di+1 and
e0 , inclD0 ,D1

D0,[A] , AA
O
D0,ξ ,
(AA ⇒ 0)

eR
0

eR
i

A

: Di+1 → Di as:

ei+1 , F (eR
i , ei )

, projD1 ,D0

R
eR
i+1 , F (ei , ei ) .

N

The above inclusion and projection arrows are defined componentwise. In fact, there is a
hidden lemma here which allows us to define the projection arrow, namely that D0 E1 D1
(which means D0,ξ E1 D1,ξ and D0,A E1 D1,A for all A).
(∆)

e0

D0

/ D1

e1

/ D2

e2

/ D3

e3

/ ···

Thus, we have formed the ω-chain ∆. We show that ∆ is a E-increasing sequence of objects
and embeddings, and proceed to the main result.
Lemma 5.3. For (ei , eR
i )i∈ω as above and any i ∈ ω,
ei = inclDi ,Di+1

∧

eR
i = projDi+1 ,Di .

Proof: It is easy to see that Di E1 Di+1 , all i ∈ ω, so the above are well-defined. We now
do induction on i; the base case is true by definition. The inductive step follows easily from
proposition 4.45.
Theorem 5.4. We obtain a local bilimit (D∗ , ηi i∈ω ) for ∆ by taking:
G
D∗ ,
Di ,
ηi , inclDi ,D∗ (each i ∈ ω).
i

Hence, idD∗ : F (D ∗ , D∗ ) → D ∗ is a minimal invariant for F .

Proof: First, note that D0 E1 Di , for all i ∈ ω, implies that all Di ’s share the same initial
moves, and hence Di E1 D ∗ . Thus, for each i ∈ ω, we can define ηiR , projD∗ ,Di , and
hence each ηi is an embedding. We now need to show the following.
(1) (D∗ , ηi i∈ω ) is a cone for ∆,
R ;η
(2) for all i ∈ ω, ηiR ; ηi ⊑ ηi+1
i+1 ,
F
R
∗
(3) i∈ω (ηi ; ηi ) = idD .
∗ , which follows from
For 1, we nts that, for any i, inclD1 ,D∗ = inclDi ,Di+1 ; inclDi+1 ,DS
(TRN). For 2 we essentially nts that idDi ⊆ idDi+1 , and for 3 that i idDi = idD∗ ; these
are both straightforward.
From the local bilimit (D∗ , ηi i∈ω ) we obtain a minimal invariant α : F (D∗ , D∗ ) → D∗
by taking (see e.g. [1]):
G
prop. 4.45
α ,
αi , αi , F (ηi , ηiR ) ; ηi+1
=
projF (D∗ ,D∗ ),Di+1 ; inclDi+1 ,D∗ .
i

D∗

R ;η
Moreover,
= F (D∗ , D∗ ) by the Tarski-Knaster theorem, and therefore αi = ηi+1
i+1 ,
which implies α = idD∗ .

Given an ω-chain ∆ = (Di , ei )i∈ω of objects and embeddings, a cone for ∆ is an object D together with a
family (ηi : Di → D)i∈ω of embeddings such that, for all i ∈ ω, ηi = ei ; ηi+1 . Such a cone is a local bilimit
for ∆ if, for all i ∈ ω,
G
R
(ηiR ; ηi ) = idD .
ηiR ; ηi ⊑ ηi+1
; ηi+1 ∧
i∈ω

44

N. TZEVELEKOS

Thus, D ∗ is the canonical solution to D = F (D, D), and in particular it solves:
O
DA→B = DA −−⊗ (Dξ ⇒ DB ⊗Dξ ) , Dξ =
(AA ⇒ DA ) .
A

Definition 5.5. Taking

D∗

as in the previous theorem define, for each type A,
ξ , Dξ∗ ,

∗
JAK , DA
.

N

The arena ξ and the translation of compound types
N are given explicitly in the following
figure. ξ is depicted by means of unfolding it to A(AA ⇒ JAK) : it consists of an initial
move ⊛ which justifies each name-question a ∈ AA , all types A, with the answer to the
latter being the denotation of A (and modelling the stored value of a). Note that we reserve
the symbol “⊛” for the initial move of ξ. ⊛-moves in type-translations can be seen as
opening a new store.
ξ
⊛
a

PA

JA × BK
(iJAK , iJBK )

PA

OQ

(a ∈ AA )

JAK
JAK

−

JBK

JA → BK
∗
(iJAK , ⊛)
(iJBK , ⊛)

−

JAK

−

PA
OQ
PA

ξ−
JBK

−

ξ−

Figure 4: The store arena and the type translation.
The store monad T . There is a standard construction (v. [28]) for defining a monad of Aside-effects (any object A) starting from a given strong monad with exponentials. Here we
define a store monad, i.e. a ξ-side-effects monad, from the lifting monad as follows.
T : C → C , ξ ⇒ ( ⊗ ξ)


up
ηA : A → T A , Λ A ⊗ ξ −→ (A ⊗ ξ)⊥


(5.1)
ev⊥
ev
dn
µA : T 2 A → T A , Λ T 2 A ⊗ ξ −→ (T A ⊗ ξ)⊥ −−→
(A ⊗ ξ)⊥⊥ −→ (A ⊗ ξ)⊥


id⊗ev
st
τA,B : A ⊗ T B → T (A ⊗ B) , Λ A ⊗ T B ⊗ ξ −−−−→ A ⊗ (B ⊗ ξ)⊥ −→ (A ⊗ B ⊗ ξ)⊥

A concrete description of the store monad is given in figure 5 (the diagrams of strategies
depict their viewfunctions, as described in notation 4.34). For the particular case of ⊛moves which appear as second moves in T A’s, let us recall the convention we are following.
Looking at the diagram for T A (figure 5), we see that ⊛ justifies a copy of ξ − (left) and
a copy of A⊗ξ (right). Thus, a copycat link connecting to the lower-left of a ⊛ expresses
a copycat concerning the ξ − justified by ⊛ (e.g. the link between the first two ⊛-moves in
the diagram for µA ), and similarly for copycat links connecting to the lower-right of a ⊛.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

ηA : A
iA

TA
∗
⊛

∗

⊛

OQ

(iA , ⊛)

PA

OQ

∗

PA

⊛

OQ

(iA , ⊛)

ξ

OQ

PA

/ TB

Tf : TA
∗

/ TA

PQ

(iA , ⊛)

OA

(iB , ⊛)

f

A

ξ−

µA : T 2 A
∗

τA,B : A⊗T B

/ TA
OQ

∗

(iA , ∗)

(∗, ⊛)
⊛

OQ

∗
⊛

OQ

⊛

PA

/ T (A⊗B)

PA

⊛

PA
OQ

⊛

PA

−

−

45

PA
OQ

PQ

⊛

PQ

OA

(iB , ⊛)

OA

PQ

(iA , iB , ⊛)

PA

Figure 5: The store monad.

Thus, for example, µA is given by:
µA = strat( { [∗ ∗ ⊛ ⊛ s] | [⊛ ⊛ s] ∈ viewf(idξ ) }
∪ { [∗ ∗ ⊛ ⊛ (∗, ⊛′ ) ⊛′ s] | [⊛′ ⊛′ s] ∈ viewf(idξ ) ∨ [s] ∈ viewf(idA⊗ξ ) } ) .
A consequence of lifting being a strong monad with exponentials is that the store monad is
also a strong monad with exponentials. T -exponentials are given by:
T B A , A −−⊗ T B ,

ΛT (f : A⊗B → T C) , Λ(f ) .

(5.2)

Moreover, for each arena A we can define an arrow:
(ηA )⊥

pu

TA
αA , A⊥ −−−−→ (T A)⊥ −−−
→ TA.

(5.3)

The transformation pu was introduced in (4.7). Using lemma 4.48 we obtain αA = Λ(st′A,ξ ).
Moreover, we can show that α : ( )⊥ → T is a monad morphism.
5.2. Obtaining the νρ-model. Let us recapitulate the structure that we have constructed
thus far to the effect of obtaining a νρ-model in Vt . Our numbering below follows that of
definition 3.12.
I. Vt is a category with finite products (proposition 4.39).
II. The store monad T is a strong monad with exponentials.
III. Vt contains adequate structure for numerals.
IV. There is a family (Qā , ε, δ, ζ)ā∈A# of product comonads, with each Qā having basis Aā
(see section 4.5), which fulfils specifications (a,b). There are also fresh-name constructors, newāa : Qā → (Qāa )⊥ , which satisfy (N2).

46

N. TZEVELEKOS

V. There are name-equality arrows, eqA for each type A, making the (N1) diagram commute (section 4.5).
From new we can obtain a fresh-name transformation for the store monad.
Definition 5.6. For each āa ∈ A# , define a natural transformation nuāa : Qā → T Qāa by:
new

αQāa A

A
ā
nuāa
−−→
(Qāa A)⊥ −−−−→ T Qāa A .
A , Q A−

nu

Tf

µ

B
A
T Qāa A −−→ T 2 B −−→
TB . N
Moreover, for each f : Qāa A → T B, take ^ a _ f , Qā A −−→

Each arrow nuāa
A is explicitly given by (note we use the same conventions as in (4.10)):
a a
nuāa
A = strat{ [(ā, iA ) ∗ ⊛ (āa, iA , ⊛) s ] |

a # iA ∧ ([iA iA s] ∈ viewf(idA ) ∨ [⊛ ⊛ s] ∈ viewf(idξ )) }
and diagrammatically as in figure 6. Moreover, using the fact that α is a monad morphism
and lemma 4.48 we can show that, in fact, ^ a _ f is given exactly as in (4.9), that is,

^ a _ f = newA ; f⊥ ; puT B .
Finally, α being is a monad morphism implies also the following.
Proposition 5.7. The nu transformation satisfies the (N2) diagrams of definition 3.12.
What we are only missing for a νρ-model is update and dereferencing maps.
Definition 5.8. For any type A we define the following arrows in Vt ,
drfA , strat{ [ a ∗ ⊛ a iJAK (iJAK , ⊛) s ] |
[⊛ ⊛ s] ∈ viewf(idξ ) ∨ [iJAK iJAK s] ∈ viewf(idJAK ) } ,
updA , strat { [ (a, iJAK ) ∗ ⊛ b b s ] | [⊛ ⊛ b b s] ∈ viewf(idξ ) ∧ b#a }
depicted also in figure 6.


∪ { [ (a, iJAK ) ∗ ⊛ a iJAK s ] | [iJAK iJAK s] ∈ viewf(idJAK ) } ,

N

These strategies work as follows. updA responds with the answer (∗, ⊛) to the initial sequence (a, iJAK ) ∗ ⊛ and then:
• for any name b # a that is asked by O to (∗, ⊛) (which is a store-opening move), it copies
b under the store ⊛ (opened by O) and establishes a copycat link between the two b’s;
• if O asks a to (∗, ⊛), it answers iJAK and establishes a copycat link between the two iJAK ’s.
On the other hand, drfA does not immediately answer to the initial sequence a ∗ ⊛ but
rather asks (the value of) a to ⊛. Upon receiving O’s answer iJAK , it answers (iJAK , ⊛) and
establishes two copycat links. We can show by direct computation the following.
Proposition 5.9. The (NR) and (SNR) diagrams of definition 3.12 commute.
We have therefore established the following.
Theorem 5.10. (Vt , T, Q) is a νρ-model.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

drfA : AA

updA : AA ⊗JAK

/ T1

47

/ T JAK

a

(a, iJAK )

OQ

∗

OQ

∗

⊛

PA

⊛
(∗, ⊛)

PA
OQ

OQ

a

PQ

PA

iJAK

OA

(iJAK , ⊛)
b

PA

OQ

b

PQ

ā
nuāa
A : Q A

/ T Qāa A

(ā, iA )
a

OQ

iJAK

PA

OQ

∗

PA

⊛

OQ

(āa, iA , ⊛)

a

PA

Figure 6: Strategies for update, dereferencing and fresh-name creation.

We close this section with a discussion on how the store-effect is achieved in our innocent
setting, and with some examples of translations of νρ-terms in Vt .
Remark 5.11 (Innocent store). The approach to the modelling of store which we
have presented differs fundamentally from previous such approaches in game semantics.
Those approaches, be they for basic or higher-order store [6, 3], are based on the following
methodology. References are modelled by read/write product types, and fresh-reference
creation is modelled by a “cell” strategy which creates the fresh cell and imposes a good
read/write discipline on it. In order for a cell to be able to return the last stored value,
innocence has to be broken since each read-request hides previous write-requests from the
P-view. Higher-order cells have to also break visibility in order to establish copycat links
between read- and write-requests.
Here instead we have only P – What’s the value of a?
used innocent strategies and a
O – I don’t know, you tell me: what’s the value of a?
monad on a store ξ. Because of
P – I don’t know, you tell me: what’s the value of a?
..
the monad, an arena JAK con.
tains several copies of ξ, thereO – I don’t know, you tell me: what’s the value of a?
fore several stores are opened
P – I know it, it is v.
inside a play. The read/ write
..
.
discipline is then kept in an inO – I know it, it is v.
teractive way: when a particiP – I know it, it is v.
pant asks (the value of) a name
O
–
I know it, it is v.
a at the last (relevant) store,17
Figure 7: A dialogue in innocent store.
17i.e. at the last store-opening move played by the other participant.

48

N. TZEVELEKOS

the other participant either answers with a value or asks himself a at the penultimate store,
and so on until one of the participants answers or the first store in the play is reached. At
each step, a participant answers the question a only if he updated the value of a before
opening the current store (of that step, i.e. the last store in the participant’s view) — note
that this behaviour does not break innocence. If no such update was made by the participant then he simply passes a to the previous store and establishes a copycat link between
the two a’s. These links ensure that when an answer is eventually obtained then it will
be copycatted all the way to answer the original question a. Thus, we innocently obtain a
read/write discipline: at each question a, the last update of a is returned.
Example 5.12. Consider the typed terms:
ǫ | ∅ |− νa.a := hfst ! a, snd ! ai ,

b | ∅ |− b := λx.(! b)skip ,

b | ∅ |− (! b)skip

with a ∈ AN×N and b ∈ A1→B . Their translations in Vt are as follows.

A1→B

/ T1

1
∗

OQ

∗

b

OQ

∗

PA

⊛

OQ

aa
(n, n )

(∗, ⊛)
c

PQ

PA

OQ

c

a

(l, l′ )

(∗, ⊛)

b

PA

OQ

∗
b

a

(∗, ⊛)

OQ

ba

PQ

aa

OQ
a

(n, l′ )

OQ

∗
⊛

PA
OQ

b

PQ

∗

OA

(∗, ⊛)

PQ

PQ

OA
a

b

OQ

OA

aa

/ T JBK

PA

⊛

PQ
′ a

A1→B

/ T1

b

PA

(iB , ⊛)
(iB , ⊛)

OA
PA

OQ
PQ

∗

OA

(∗, ⊛)

PQ

PA

In the first example we see that, although the strategy is looking up the fresh (and therefore
uninitialised) reference a, the play does not deadlock: if Opponent answered the question
aa then the play would proceed as depicted. In practice, however, Opponent will never
be able to answer that question and the play will halt indeed (this is because Opponent
must play tidily, see section 5.4). Moreover, from the latter two examples we can compute
JstopB K : 1 → T JBK = { [∗ ∗ ⊛] } .

5.3. Adequacy. We proceed to show that Vt is adequate (v. definition 3.18). First we
characterise non-reducing terms as follows.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

49

Lemma 5.13. Let ā | ∅ |− M : A be a typed term. M is a value iff there exists a store S
such that S |= M has no reducts and [(ā, ∗) ∗ ⊛ (iA , ⊛)b̄ ] ∈ JS̄ ; M K , for some iA , b̄.
Proof: The “only if”-part is straightforward. For the “if”-part assume that M is a non-value
and take any S such that S |= M has no reducts. We show by induction on M that there
exist no iA , b̄ such that [(ā, ∗) ∗ ⊛ (iA , ⊛)b̄ ] ∈ JS̄ ; M K. The base case follows trivially from
M not being a value. Now, for the inductive step, the specifications of S |= M (and M )
imply that either M ≡ ! a with a not having a value in S, or M ≡ E[K] with E an evaluation
context and K a non-value typed as ā | ∅ |− K : B and such that S |= K non-reducing.
In case of M ≡ ! a, we have that [(ā, ∗) ∗ ⊛ a] ∈ JS̄ ; M K, which proves the claim because
of determinacy. On the other hand, if M ≡ E[K] then, as in proof of proposition 3.17, we
have:
JS̄ ; M K = hΛ(ζ ′ ; JE[x]K), JS̄ ; KKi ; τ ; T ev ; µ = hid, JS̄ ; KKi ; τ ; T (ζ ′ ; JE[x]K) ; µ
By IH, there are no iB , c̄ such that [(ā, ∗) ∗ ⊛ (iB , ⊛)c̄ ] ∈ JS̄ ; KK, which implies that there
are no iA , b̄ such that [(ā, ∗) ∗ ⊛ (iA , ⊛)b̄ ] ∈ JS̄ ; M K.
Because of the previous result, in order to show adequacy it suffices to show that, whenever
JM K = ^ b̄ _ JS̄ ; 0̃K, there is no infinite reduction sequence starting from ā |= M . We will
carry out the following reasoning.
• Firstly, since the calculus without DRF reductions is strongly normalising — this is inherited from strong normalisation of the ν-calculus — it suffices to show there is no reduction
sequence starting from ā |= M and containing infinitely many DRF reduction steps.
• In fact, the problem can be further reduced to showing that, whenever [(ā, ∗)∗⊛ (0, ⊛)b̄ ] ∈
JM K, there is no reduction sequence starting from ā |= M and containing infinitely many
NEW reduction steps. The latter clearly holds, since M cannot create more than |b̄| fresh
names in that case, because of correctness.
The reduction to this simpler problem is achieved as follows. For each term M , we
construct a term M ′ by adding immediately before each dereferencing in M a freshname construction. The result is that, whenever there is a sequence with infinitely many
DRF’s starting from S |= M , there is a sequence with infinitely many NEW’s starting
from S |= M ′ . The reduction is completed by finally showing that, whenever we have
′
[(ā, ∗) ∗ ⊛ (0, ⊛)b̄ ] ∈ JM K, we also have [(ā, ∗) ∗ ⊛ (0, ⊛)b̄ ] ∈ JM ′ K.
The crucial step in the proof is the reduction to “the simpler problem”, and particularly
showing the connection between JM K and JM ′ K described above. The latter is carried out
by using the observational equivalence relation on strategies, defined later in this section.
Note, though, that a direct proof can also be given (see [48]).
Proposition 5.14 (Adequacy). (Vt , T, Q) is adequate.
Proof: This follows from O-adequacy (lemma 5.28), which is proved independently.
Hence, (Vt , T, Q) is a sound model for νρ and thus, for all terms M, N ,
JM K = JN K =⇒ M / N .

50

N. TZEVELEKOS

5.4. Tidy strategies. Leaving adequacy behind, the route for obtaining a fully abstract
model of νρ proceeds to definability. That is, we aim for a model in which elements with
finite descriptions correspond to translations of νρ-terms.
However, Vt does not satisfy such a requirement: it includes (finitary) store-related
behaviours that are disallowed in the operational semantics of νρ. In fact, our strategies
treat the store ξ like any other arena, while in νρ the treatment of store follows some basic
guidelines. For example, if a store S is updated to S ′ then the original store S is not
accessible any more (irreversibility). In strategies we do not have such a condition: in
a play there may be several ξ’s opened, yet there is no discipline on which of these are
accessible to Player whenever he makes a move. Another condition involves the fact that
a store either ‘knows’ the value of a name or it doesn’t know it. Hence, when a name is
asked, the store either returns its value or it deadlocks: there is no third option. In a play,
however, when Opponent asks the value of some name, Player is free to evade answering
and play somewhere else!
To disallow such behaviours we will constrain total strategies with further conditions,
defining thus what we call tidy strategies. But first, let us specify store-related moves inside
type-translating nominal arenas.
Definition 5.15. Consider Vνρ , the full subcategory of Vt with objects given by:
Ob(Vνρ ) ∋ A, B ::= 1 | N | Aā | A⊗B | A −−⊗ T B
For each such arena A we define its set of store-Handles, HA , as follows.
H1 = HN = HAā , ∅ ,

HA⊗B , HA ∪ HB ,

[
, {(iA , ⊛A ), (iB , ⊛B )} ∪ HA ∪ HB ∪ HξA ∪ HξB with Hξ ,
HJCK ,
C
N
where we write A −−⊗ T B as A −−⊗ (ξA ⇒ B ⊗ξB ), and ξ as C(AC ⇒ JCK).
In an arena A ∈ Ob(Vνρ ), a store-Handle justifies (all) questions of the form a, which
we call store-Questions. Answers to store-Questions are called store-Answers.
N
HA

TB

−−⊗

Note in particular that, for each type A, we have JAK, Qā JAK, T JAK ∈ Ob(Vνρ ), assuming
that T JAK is equated with 1 −−⊗ T JAK. Note also there is a circularity in HA T B in the
S
i and,
above definition. In fact, it is a definition by induction: we take HA , i∈ω HA
−−⊗

0
, ∅,
H1i = HNi = HAi ā = HA

i
i
i
HA⊗B
, HA
∪ HB
,

i+1
i
i
i+1
i+1
HA
T B , {(iA , ⊛A ), (iB , ⊛B )} ∪ HA ∪ HB ∪ HξA ∪ HξB
−−⊗

Intuitively, store-H’s are store-opening
moves, while store-Q’s and store-A’s are
obtained from unfolding the store structure. On the side we give examples of
store-related moves in a simple arena.
From now on we work in Vνρ , unless stated otherwise. A first property
we can show is that a move is exclusively either initial or an element of the
aforedefined move-classes.

with Hξi+1 ,

[

C

i
HJCK
.

T 1 = ξ ⇒ 1⊗ξ
∗
⊛
store-Q’s

(∗, ⊛)

a
iA

store-A’s

store-H’s
b
iB

Figure 8: Store-H’s -Q’s -A’s in arena T 1.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

51

Proposition 5.16. For any A ∈ Ob(Vνρ ),
MA = IA ⊎ HA ⊎ { m ∈ MA | m a store-Q} ⊎ {m ∈ MA | m a store-A } .
Proof: We show that any m ∈ MA belongs to exactly one of the above sets. We do
induction on the level of m, l(m), inside A and on the size of A, |A|, specified by the
inductive definition of Ob(Vνρ ). If m is initial then, by definition, it can’t be a store-H.
Neither can it be a store-Q or store-A, as these moves presuppose non-initiality.
Assume l(m) > 0. If A is base then trivial, while if A = A1 ⊗A2 then use the IH on
(l(m), |A|). Now, if A = A1 −−⊗ T A2 then let us write A as A1 −−⊗ (ξ1 ⇒ A2 ⊗ξ2 ); we have the
following cases.
• If m = (iA1 , ⊛1 ) ∈ HA then m a question and not a store-Q, as store-Q’s are names.
• If m = (iA2 , ⊛2 ) ∈ HA then m an answer and not a store-A as its justifier is (iA1 , ⊛1 ).
• If m is in A1 or in A2 then use the IH.
• If m is in ξ1 then it is either some store-Q a to (iA1 , ⊛1 ) (and hence not a store-H or
store-A), or it is in some JCK. In the latter case, if m initial in JCK then a store-A in
JAK and therefore not a store-H, as m not a store-H in JCK by IH (on l(m)). If m is
non-initial in JCK then use the IH and the fact that store-H’s -Q’s -A’s of JCK are the
same in JAK.
• Similarly if m is in ξ2 .
The notion of store-handles can be straightforwardly extended to prearenas.
Definition 5.17. Let A, B ∈ Ob(Vνρ ). The set HA→B of store-handles in prearena A → B
is HA ∪ HB . Store-Q’s and store-A’s are defined accordingly.
N
Using the previous proposition, we can see that, for any A and B, the set MA→B can be
decomposed as:
IA ⊎ IB ⊎ HA→B ⊎ { m ∈ MA→B | m a store-Q } ⊎ { m ∈ MA→B | m a store-A }

(5.4)

We proceed to define tidy strategies. We endorse the following notational convention. Since
stores ξ may occur in several places inside a (pre)arena we may use parenthesised indices
to distinguish identical moves from different stores. For example, the same store-question q
may be occasionally denoted q(O) or q(P ) , the particular notation denoting the OP-polarity
of the move. Moreover, by O-store-H’s we mean store-H’s played by Opponent, etc.
Definition 5.18 (Tidy strategies). A total strategy σ is tidy if whenever odd-length
[s] ∈ σ then:
(TD1) If s ends in a store-Q q then [sx] ∈ σ , with x being either a store-A to q introducing
no new names, or a copy of q. In particular, if q = aā with a # psq− then the latter
case holds.
(TD2) If [sq(P ) ] ∈ σ with q a store-Q then q(P ) is justified by last O-store-H in psq.
(TD3) If psq = s′ q(O) q(P ) t y(O) with q a store-Q then [sy(P ) ] ∈ σ, where y(P ) is justified by
psq .−3 .
N
(TD1) states that, whenever Opponent asks the value of a name, Player either immediately
answers with its value or it copycats the question to the previous store-H. The former case
corresponds to Player having updated the given name lastly (i.e. between the previous Ostore-H and the last one). The latter case corresponds to Player not having done so and
hence asking its value to the previous store configuration, starting thus a copycat between
the last and the previous store-H. Hence, the store is, in fact, composed by layers of stores

52

N. TZEVELEKOS

— one on top of the other — and only when a name has not been updated in the top layer
is Player allowed to search for it in layers underneath. We can say that this is the nominal
games equivalent of a memory cell (cf. remark 5.11). (TD3) further guarantees the abovedescribed behaviour. It states that when Player starts a store-copycat then he must copycat
the store-A and all following moves he receives, unless Opponent chooses to play elsewhere.
(TD2) guarantees the multi-layer discipline in the store: Player can see one store at each
time, namely the last played by Opponent in the P-view.
The following straightforward result shows that (TD3), as stated, provides the intended
copycat behaviour.
Proposition 5.19. Let σ be a tidy strategy. If [s′ q(O) q(P ) t] ∈ σ is an even-length P-view
and q is a store-Q then q(O) q(P ) t is a copycat.
Proof: We do induction on |t|. The base case is straightforward. For the inductive step, let
t = t′ xz. Then, by prefix closure, [s′ q(O) q(P ) t′ x] ∈ σ, this latter a P-view. By IH, q(O)q(P ) t′ is
a copycat. Moreover, by (TD3), [s′ q(O) q(P ) t′ xx] ∈ σ with last x justified by (q(O) q(P ) t′ x).−3,
thus s′ q(O) q(P ) t′ xx a copycat. Now, by determinacy, [s′ q(O) q(P ) t′ xx] = [s′ q(O) q(P ) t′ xz], so
there exists π such that π ◦ x = x ∧ π ◦ x = z, ∴ x = z, as required.
A good store discipline would guarantee that store-Handles OP-alternate in a play. This
indeed happens in P-views played by tidy strategies. In fact, such P-views have canonical
decompositions, as we show below.
Proposition 5.20 (Tidy Discipline). Let σ : A → B be a tidy strategy and [s] ∈ σ with
psq = s. Then, s is decomposed as in the following diagram.
@ABC
GFED
iA

HIJK
ONML
@ABC
GFED
CC o

GFED
/ @ABC
iB

S-H
HIJK
/ ONML
X
e XXXXXXXXXX
mm6 OQ
m
m
M
XXXXX
m
m
XXXXX
mmm
XXXXXX
m
m
%
mm
XXXX,
m
S-H
S-A
S-H
S-Q
HIJK
ONML
HIJK
ONML
HIJK
ONML
HIJK
ONML
lXRXXXXX
PQ hRR
hRRR
P
PA hR
l6 P
l
X
RRR XXlXlXlX M
RRR
l
l
RRR
L
RRlRll XXXXXX
R ll
RRR
XXXXlXlXllRlRRRR
l RRR
l
RRR

l
RR
R
vlll
lll XXXXXXRXR S-A
S-Q
S-H
HIJK
ONML
HIJK
ONML
HIJK
ONML
O

OA

O

(by CC we mean the state that, when reached by a sequence s = psq, the rest of s is copycat.)

Proof: The first two transitions are clear. After them neither P nor O can play initial
moves, so all remaining moves in s are store-H -Q -A’s. Assume now O has just played a
question x0 which is a store-H and the play continues with moves x1 x2 x3 ... .
x1 cannot be a store-A, as this would not be justified by x0 , breaching well-bracketing.
If x1 is a store-Q then x2 must be a store-A, by P-view. If x1 is an answer-store-H then x2
is an OQ, while if x1 a question-store-H then x2 is either a store-Q or a store-H.
If x2 is a store-Q then, by (TD1), x3 either a store-A or a store-Q, the latter case
meaning transition to the CC state. If x2 is not a store-Q then x3 can’t be a store-A: if
x3 were a store-A justified by q 6= x2 then, as q wouldn’t have been immediately answered,
s≥q would be a copycat and therefore we would be in the CC state right after playing q.
Finally, if x3 is a store-A then x4 must be justified by it, so it must be a Q-store-H.
Corollary 5.21 (Good Store Discipline). Let [s] ∈ σ with σ tidy and psq = s. Then:
• The subsequence of s containing its store-H’s is OP-alternating and O-starting.
• If s.−1 = q is a P-store-Q then either q is justified by last store-H in s, or s is in copycat
mode at q.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

53

Observe that strategies that mostly do copycats are tidy; in particular, identities are tidy.
Moreover, tidy strategies are closed under composition (proof delegated to the appendix).
Proposition 5.22. If σ : A → B and τ : B → C are tidy strategies then so is σ ; τ .
N

Definition 5.23. T is the lluf subcategory of Vνρ of tidy strategies.

Finally, we need to check that all structure required for a sound νρ-model pass from Vt to
T . It is not difficult to see that all such structure which does not handle the store remains
safely within the tidy universe. On the other hand, strategies for update and dereferencing
are tidy by construction. (A fully formal proof is given in [48].)
Proposition 5.24. T forms an adequate νρ-model by inheriting all the necessary structure
from Vt .
Henceforth, by strategies we shall mean tidy strategies, unless stated otherwise.
5.5. Observationality. Strategy equality is too fine grained to capture contextual equivalence in a complete manner. For example, even simple contextual equivalences like
skip ≅ νa.skip
are not preserved by the semantical translation, since strategies include in their name-lists
all introduced names, even useless ones. For similar reasons, equivalences like
νa.νb.M ≅ νb.νa.M
are not valid semantically. In fact, it is not only because of the treatment of name-creation
that the semantics is not complete. Terms like
a := 1 ; λx. ! a ; 2 ≅ a := 1 ; λx.2
are distinguished because of the ‘explicit’ way in which the store works.
So there are many ways in which our semantics is too expressive for our language.
We therefore proceed to a quotienting by the intrinsic preorder and prove full-abstraction
in the extensional model. Following the steps described in section 3.2, in this section we
introduce the intrinsic preorder on T and show that the resulting model is observational.
Full-abstraction is then shown in the following section.
Definition 5.25. Expand T to (T , T, Q, O) by setting, for each ā ∈ A# ,
Oā , { f ∈ T (Qā 1, T N) | ∃b̄. [(ā, ∗) ∗ ⊛ (0, ⊛)b̄ ] ∈ f } .
Then, for each f, g ∈ T (Qā A, T B), f .ā g if
∀ρ : Qā (A −−⊗ T B) → T N. (Λā (f ) ; ρ ∈ Oā =⇒ Λā (g) ; ρ ∈ Oā ) .
Thus, the observability predicate O is a family (Oā )ā∈A# , and the intrinsic
ā
family (.ā )ā∈A# . Recall that by Λā (f ) we mean ΛQ ,T (f ), that is,
δ

N

preorder . is a

Qā Λ(ζ ′ ; f )

Λā (f ) = Qā 1 −
→ Qā Qā 1 −
−−−−−−
→ Qā (A −−⊗ T B) .
Note in particular that f ⊑ g implies Λā (f ) ; ρ ⊑ Λā (g) ; ρ, for any relevant ρ, and therefore:
f ⊑ g =⇒ f .ā g

(5.5)

The intrinsic preorder is defined by use of test arrows ρ, which stand for possible program
contexts. As the following result shows, not all such tests are necessary.

54

N. TZEVELEKOS

Lemma 5.26 (tl4 tests suffice). Let f, g ∈ T (Qā 1, B) with B pointed. The following are
equivalent (recall definition 4.35).
I.
∀ρ : Qā B → T N. δ ; Qā f ; ρ ∈ Oā =⇒ δ ; Qā g ; ρ ∈ Oā
II. ∀ρ : Qā B → T N. ρ is tl4 =⇒ (δ ; Qā f ; ρ ∈ Oā =⇒ δ ; Qā g ; ρ ∈ Oā )
Hence, for each ā and f, g ∈ T (Qā A, T B), f .ā g iff
∀ρ : Qā (A −−⊗ T B) → T N. ρ is tl4 =⇒ (Λā (f ) ; ρ ∈ Oā =⇒ Λā (g) ; ρ ∈ Oā ) .
Proof: I ⇒ II is trivial. Now assume II holds and let ρ : Qā B → T N be any strategy such
that δ ; Qā f ; ρ ∈ Oā . Then, there exist [s] ∈ δ ; Qā f and [t] ∈ ρ such that [s ; t] = [(ā, ∗) ∗
⊛ (0, ⊛)b̄ ] ∈ (δ ; Qā f ) ; ρ. We show by induction on the number of JB -moves appearing in
s k t that δ ; Qā g ; ρ ∈ Oā .
If no such moves appear then t = (ā, iB ) ∗ ⊛ (0, ⊛)b̄ , so done. If n + 1 such moves
appear then ρ is necessarily t4, as B is pointed, so by lemma 4.36 there exists tl4* strategy ρ̃ such that ρ = ∆ ; ρ̃. It is not difficult to see that ρ being tidy implies that ρ̃ is
tidy. Moreover, δ ; Qā f ; ρ = δ ; Qā f ; ∆ ; ρ̃ = δ ; Qā f ;hid, Qā ! ; δ ; Qā f i ; ρ̃ = δ ; Qā f ; ρ′ ,
with ρ′ being hid, Qā ! ; δ ; Qā f i ; ρ̃. Now, by definition of ρ̃, [(ā, ∗) ∗ ⊛ (0, ⊛)b̄ ] = [s′ ; t′ ] ∈
δ ; Qā f ; ρ′ with s′ k t′ containing n JB -moves so, by IH, δ ; Qā g ; ρ′ ∈ Oā . But δ ; Qā g ; ρ′ =
δ ; Qā g ;hid, Qā ! ; δ ; Qā f i ; ρ̃ = δ ; Qā f ;hQā ! ; δ ; Qā g, idi ; ρ̃ = δ ; Qā f ; ρ′′ , where ρ′′ is given
by hQā ! ; δ ; Qā g, idi ; ρ̃. But ρ′′ is tl4, thus, by hypothesis, Oā ∋ δ ; Qā g ; ρ′′ = δ ; Qā g ; ρ , as
required.
We can now prove the second half of observationality.
Lemma 5.27. For any morphism f : Qāa 1 → B, with B pointed, and any tl4 morphism
ρ : Qā B → T N,
āa
δ ; Qā ^ a _ f ; ρ ∈ Oā ⇐⇒ δ ; Qāa f ; āa
ā ; ρ ∈ O
Moreover, for each ā and relevant a, ā′ , f, g,
f .āa g =⇒ ^ a _ f .ā ^ a _ g ,

f .ā g =⇒

ā′
ā

′

; f .ā

ā′
ā

;g.

Proof: For the first part, ρ being tl4 and B being pointed imply that there exists some
b̄ # ā and a ttotal strategy ρ′ such that ρ = ^ b̄ _ ρ′ . Now let δ ; Qā ^ a _ f ; ρ ∈ Oā , so there
¯
exists [s ; t] = [(ā, ∗) ∗ ⊛ (0, ⊛)b̄ac̄ ] ∈ (δ ; Qā ^ a _ f ) ; ρ, and let s = (ā, ∗) (ā, iB ) jB mad s′ and
¯
b̄ t′ . Letting sra be snlist(s)ra , we can see that [(āa, ∗) i j md s′ra ] ∈ f and
t = (ā, iB ) ∗ ⊛ jB
B B
¯ ′ra
āa
′′
′′
d
āa
thus [s ] , [(āa, ∗) (ā, iB ) jB m s ] ∈ δ ; Q f ; ā . Hence, [s ; t] = [(āa, ∗) ∗ ⊛ (0, ⊛)b̄c̄ ] ∈
δ ; Qāa f ; āa
ā ; ρ, as required. The converse is shown similarly.
For the second part, suppose f .āa g : Qāa A → T B and take any tl4 morphism
ρ : Qā (A −−⊗ T B) → T N. Then,
lem 4.53

Λā (^ a _ f ) ; ρ ∈ Oā ⇐⇒ δ ; Qā Λ(ζ ′ ; ^ a _ f ) ; ρ ∈ Oā ⇐⇒ δ ; Qā ^ a _ (Λ(ζ ′ ; f )) ; ρ ∈ Oā
āa
⇐⇒ δ ; Qāa Λ(ζ ′ ; f ) ; āa
ā ; ρ ∈ O
f .āa g

āa
⇐⇒ Λā (^ a _ g) ; ρ ∈ Oā .
=⇒ δ ; Qāa Λ(ζ ′ ; g) ; āa
ā ; ρ ∈ O

For the other claim, let us generalise the fresh-name constructors new to:
 
ā
′
′
: Aā → (Aā )⊥ , { [ (ā, ∗) ∗ ∗ (ā′ , ∗)ā r ā ] }
ā′

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

55

′

for any S(ā) ⊆ S(ā′ ). The above yields a natural transformation of type Qā → Qā⊥ . It is

′
′
easy to see that, for any h : Qā 1 → T N, h ∈ Oā iff āā′ ; h⊥ ; pu ∈ Oā and, moreover, that
the diagram on the right below commutes. Hence, if f .ā g then
′

′

′

δ ; Qā Λ(ζ ′ ; āā ; f ) ; ρ ∈ Oā
⇐⇒
⇐⇒
⇐⇒
f .ā g

′
′
′ ′
δ ; Qā āā ; Qā Λ(ζ ′ ; f ) ; ρ ∈ Oā
ā 
ā′ ā′
′
ā′
ā′ ;(δ ; Q ā ; Q Λ(ζ ; f ) ; ρ)⊥ ; pu

δ ; Qā Λ(ζ ′ ; f ) ; āā′ ; ρ⊥ ; pu ∈ Oā

ā

′

=⇒ δ ; Q Λ(ζ ; g) ;
ā′

⇐⇒ δ ; Q Λ(ζ ′ ;

ā′
ā

ā 
ā′ ; ρ⊥

; pu ∈ O

∈ Oā

ā

Aā
ā
ā′



ā 
h ā′ ,idi

/ (Aā′ ) ⊗ Aā
⊥
st′



′
(Aā )⊥

ā′

; g) ; ρ ∈ O ,

ā′
hid, ā i⊥


/ (Aā′ ⊗ Aā )
⊥

as required.
In order to prove that T is observational, we are only left to show that
JM K ∈ Oā ⇐⇒ ∃b̄, S. JM K = ^ b̄ _ JS̄ ; 0K
for any ā | ∅ |− M : N. The “⇐=” direction is trivial. For the converse, because of
correctness, it suffices to show the following generalisation of adequacy.
Lemma 5.28 (O-Adequacy). Let ā | ∅ |− M : N be a typed term. If JM K ∈ Oǫ then
there exists some S such that ā |= M −→
→ S |= 0.
Proof: The idea behind the proof is given above proposition 5.14. It suffices to show that,
for any such M , there is a non-reducing sequent S |= N such that ā |= M −→
→ S |= N ;
therefore, because of Strong Normalisation in the ν-calculus, it suffices to show that there
is no infinite reduction sequence starting from ā |= M and containing infinitely many DRF
reduction steps.
To show the latter we will use an operation on terms adding new-name constructors just
before dereferencings. The operation yields, for each term M , a term (M )◦ the semantics of
which is equivalent to that of M . On the other hand, ā |= (M )◦ cannot perform infinitely
many DRF reduction steps without creating infinitely many new names. For each term M ,
define (M )◦ by induction as:
(a)◦ , a ,
(! N )◦

(x)◦ , x ,

... (λx.M )◦ , λx.(M )◦ ,

(M N )◦ , (M )◦ (N )◦ ,

...

νa. !(N )◦

,
, some a # N .
We show that J(M )◦ K ⋍ JM K, by induction on M ; the base cases are trivial. The
induction step follows immediately from the IH and the fact that ⋍ is a congruence, in all
◦
cases except for M being ! N . In the latter case we have that J(M )◦ K = ^ a _ ( āa
ā ; J!(N ) K) ,
◦
ā
while the IH implies that JM K ⋍ J!(N ) K. Hence, it sts that for each f : Q A → T B we
have f ⋍ ^ a _ ( āa
ā ; f ) . Indeed, for any relevant ρ which is tl4,
and

lem 5.27

ā
āa
āa
⇐⇒ δ ; Qāa Λ(ζ ′ ; āa
Λā (^ a _ ( āa
ā ; f )) ; ρ ∈ O
ā ; f ) ; ā ; ρ ∈ O
ā
′
āa
āa
⇐⇒ δ ; Qāa āa
ā ; ā ; Q Λ(ζ ; f ) ; ρ ∈ O

⇐⇒

āa
ā

; Λā (f ) ; ρ ∈ Oāa ⇐⇒ Λā (f ) ; ρ ∈ Oā .

Now, take any ā | ∅ |− M : N and assume JM K ∈ Oā , and that ā |= M diverges using
infinitely many DRF reduction steps. Then, ā |= (M )◦ diverges using infinitely many
NEW reduction steps. However, since J(M )◦ K ⋍ JM K, we have J(M )◦ K ∈ Oā and therefore

56

N. TZEVELEKOS

[(ā, ∗) ∗ ⊛ (0̃, ⊛)b̄ ] ∈ J(M )◦ K for some b̄. However, ā |= (M )◦ reduces to some S |= M ′ using
|b̄|+ 1 NEW reduction steps, so J(M )◦ K = ^ c̄ _ JS̄ ; M ′ K with |c̄| = |b̄|+ 1, to determinacy.
We have therefore shown observationality.
Proposition 5.29 (Observationality). (T , T, Q, O) is observational.
5.6. Definability and full-abstraction. We now proceed to show definability for T , and
through it ip-definability. According to the results of section 3.2.3, this will suffice for full
abstraction.
We first make precise the notion of finitary strategy, that is, of (tidy) strategy with
finite description, by introducing truncation functions that remove inessential branches
from a strategy’s description.
Definition 5.30. Let σ : A → B in T and let [s] ∈ viewf(σ) be of even length. Define
trunc(s) and trunc′ (s) by induction as follows.
trunc(ǫ) = trunc′ (ǫ) , ǫ
(
ǫ
, if x = y are store-Q’s
trunc(x(O) y(P ) s′ ) ,
′
xy trunc(s ) , o.w.

ǫ
, if x = y are store-Q’s



ǫ
, if x store-Q , y a store-A and s′ = ǫ
trunc′ (x(O) y(P ) s′ ) ,

ǫ
, if x ∈ IA , y ∈ IB and s′ = ǫ



xy trunc′ (s′ ) , o.w.

Moreover, say σ is finitary if trunc(σ) is finite, where

trunc(σ) , { [trunc(s)] | [s] ∈ viewf(σ) ∧ |s| > 3 } .
Finally, for any [t] ∈ σ define:
σ≤t , strat{ [s] ∈ viewf(σ) | ∃ t′ ≤ t. trunc′ (s) = pt′q } .

N

Hence, finitary are those strategies whose viewfunctions become finite if we delete all the
store-copycats and all default initial answers — the latter dictated by totality. Moreover,
the strategy σ≤t is the strategy we are left with if we truncate viewf(σ) by removing all
its branches of size greater than 3 that are not contained in t, except for the store-copycats
which are left intact and for the store-A’s branches which are truncated to the point of
leaving solely the store-A, so that we retain tidiness. Note that, in general, trunc′ (s) ≤
trunc(s) ≤ s. We can then show the following (proof in [48]).
Proposition 5.31. If σ is a strategy and [t] ∈ σ is even-length then σ≤t is a finitary strategy
with [t] ∈ σ≤t and σ≤t ⊑ σ.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

57

We proceed to show definability. The proof is facilitated by the following lemma, the proof
of which is delegated to the appendix. Note that for economy we define strategies by means
of their viewfunctions modulo totality and even-prefix closure. Moreover, we write σ ↾ i
for the (total) restriction of a strategy σ to an initial move i, and srb̄ for s with b̄ removed
from all of its name-lists.
Lemma 5.32 (Decomposition Lemma). Let σ : Qā JAK → T JBK be a strategy. We can
decompose σ as follows.
1. If there exists an iA(0) such that ∃x0 . [(ā, iA(0) ) ∗ ⊛x0 ] ∈ σ then
Qā JAK

MMM
ā
′
Mh[x
MMM=iA(0) ],hσ0 ,σ ii
MMM
&

T JBK o
N ⊗(T JBK)2
σ

cnd

where:
ā

[x = iA(0) ] : Qā JAK → N

, { [(ā, iA(0) ) 0 ]} ∪ { [ (ā, iA ) 1 ] | [ (ā, iA ) ] 6= [ (ā, iA(0) ) ] } ,

ā

σ0 : Q JAK → T JBK , strat{ [ (ā, iA(0) ) s ] ∈ viewf(σ) } ,
σ ′ : Qā JAK → T JBK , strat{ [ (ā, iA ) s ] ∈ viewf(σ) | [ (ā, iA ) ] 6= [ (ā, iA(0) ) ] } .
2. If there exists iA(0) such that ∀iA . (∃x0 . [(ā, iA ) ∗ ⊛ x0 ] ∈ σ) ⇐⇒ [(ā, iA )] = [(ā, iA(0) )] ,
then σ = ^ b̄ _ σb̄ where:
σb̄ : Qāb̄ JAK → T JBK , strat{ [ (āb̄, iA(0) ) ∗ ⊛ m0 srb̄ ] |
[ (ā, iA(0) ) ∗ ⊛ mb̄0 s ] ∈ viewf(σ) } .
3. If there exist iA(0) , m0 such that ∀iA , x. [(ā, iA ) ∗ ⊛ x] ∈ σ ⇐⇒ [(ā, iA ) x] = [(ā, iA(0) ) m0 ] ,
then one of the following is the case.
(a) m0 = a, a store-Q of type C under ⊛, in which case σ = σ ′ ↾ (ā, iA(0) ) where
σ ′ : Qā JAK → T JBK , hid, φi; τ ; T ζ ′ ; T σa ; µ
σa : Qā (JAK ⊗JCK) → T JBK , strat{ [ (ā, iA(0) , iC ) ∗ ⊛ s] |
[ (ā, iA(0) ) ∗ ⊛ a iC s ] ∈ viewf(σ) } ,
(
, if a ∈ S(ā)
Qā ! ; aā ; drfC
φ : Qā JAK → T JCK ,
ā
ā
Q πj ; ǫ ; drfC , if a # ā .
(b) m0 = jA ∨ m0 = (iB , ⊛) , a store-H, in which case if [ (ā, iA(0) ) ∗ ⊛ m0 a iC ] ∈ σ,
for some store-Q a and store-A iC , then
Qā JAK

h∆,σa i

/ Qā JAK ⊗Qā JAK ⊗T JCK
τ ;T (id⊗φ;τ );µ

σ





T JBK o
where:

T σ′ ; µ

T Qā JAK

58

N. TZEVELEKOS

σa : Qā JAK → T JCK , strat{ [ (ā, iA(0) ) ∗ ⊛ (iC , ⊛) s ] |
[ (ā, iA(0) ) ∗ ⊛ m0 a iC s ] ∈ viewf(σ)
∨ [ ⊛ ⊛ s ] ∈ viewf(idξ ) } ,
′

ā

σ : Q JAK → T JBK , strat( { [ (ā, iA(0) ) ∗ ⊛ m0 y s ] ∈ viewf(σ) | y 6= a }
∪ { [ (ā, iA(0) ) ∗ ⊛ m0 a s ] |
[ ⊛ ⊛ a s ] ∈ viewf(idξ )} ) ,
φ : Qā JAK ⊗JCK → T 1 ,

(

(Qā ! ; aā )⊗idJCK ; updC
(Qā πj ; āǫ )⊗idJCK ; updC

, if a ∈ S(ā)
, if a # ā .

In both cases above, we take j = min{ j | (iA(0) )j = a }.
The proof of definability is a nominal version of standard definability results in game semantics. In fact, using the Decomposition Lemma we reduce the problem of definability of
a finitary strategy σ to that of definability of a finitary strategy σ0 of equal length, with
σ0 having no initial effects (i.e. fresh-name creation, name-update or name-dereferencing).
On σ0 we then apply almost verbatim the methodology of [15] — itself based on previous
proofs of definability.
Theorem 5.33 (Definability). Let A, B be types and σ : Qā JAK → T JBK be finitary.
Then σ is definable.
Proof: We do induction on (|trunc(σ)|, kσk), where we let kσk , max{ |L(s)| | [s] ∈
viewf(σ) }, i.e. the maximum number of names introduced in any play of trunc(σ). If
|trunc(σ)| = 0 then σ = JstopB K ; otherwise, there exist x0 , iA(0) such that [(ā, iA(0) ) ∗
⊛ x0 ] ∈ σ . By Decomposition Lemma,
ā

σ = h[x = iA(0) ], hσ0 , σ ′ ii; cnd
with |trunc(σ ′ )| < |trunc(σ)| and (0, 0) < (|trunc(σ0 )|, kσ0 k) ≤ (|trunc(σ)|, kσk) , so by
IH there exists term M ′ such that JM ′ K = σ ′ . Hence, if there exist terms M0 , N0 with
ā
JM0 K ↾ (ā, iA(0) ) = σ0 and JN0 K = [x = iA(0) ]; η , then we can see that
σ = Jif0 N0 then M0 else M ′ K .
We first construct N0 . Assume that A = A1 × A2 × · · · × An with Ai ’s non-products,
and similarly B = B1 × · · · × Bm . Moreover, assume without loss of generality that A is
segmented in four parts: each of A1 , ..., Ak is N; each of Ak+1 , ..., Ak+i , ..., Ak+k′ is [A′′′
i ]; each
of Ak+k′ +1 , ..., Ak+k′ +i , ..., Ak+k′ +k′′ is A′i → A′′i ; and the rest are all 1. Take z̄, z̄ ′ , z̄ ′′ , z̄ ′′′ to
be variable-lists of respective types. Define φ0 , φ′0 by:
φ0 , κ1 , ..., κk , with (κ1 , ..., κk ) being the initial N-segment of iA(0) ,

(iA(0) )k+i , if (iA(0) )k+i ∈ S(ā)



z ′
, if (iA(0) )k+i # ā
j
φ′0 , κ′1 , ..., κ′k′ , with each κ′i ,

∧ j = min{ j < i | (iA(0) )k+i = (iA(0) )k+j }



fresh(i) , otherwise .

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

59

fresh(i) is a meta-constant denoting that Opponent has played a fresh name in Ak+i . If
the same fresh name is played in several places inside iA(0) then we regard its leftmost
occurrence as introducing it — this explains the second item in the cases-definition above.
Now, define
N0 , [hz̄, z̄ ′ i = hφ0 , φ′0 i] where:
[hz̄, z̄ ′ i = h~κ, ~κ′ i] , [z1 = κ1 ] ∧ · · · ∧ [zk = κk ] ∧ [z1′ = κ′1 ] ∧ · · · ∧ [zk′ ′ = κ′k′ ] ,
′
[z ′ = fresh(i)] , [z ′ 6= a1 ] ∧ · · · ∧ [z ′ 6= a|ā| ] ∧ [z ′ 6= z1′ ] ∧ · · · ∧ [z ′ 6= zi−1
],

with the logical connectives ∧ and ¬ defined using if0’s, and [zi = κi ] using pred ’s, in the
ā
standard way. It is not difficult to show that indeed JN0 K = [x = iA(0) ]; η .
We proceed to find M0 . By second part of Decomposition Lemma, σ0 = ^ b̄ _ σb̄ with
b̄ = nlist(x0 ), |trunc(σb̄ )| = |trunc(σ0 )| and kσb̄ k = kσ0 k − |b̄| . If |b̄| > 0 then, by IH, there
exists term Mb̄ such that JMb̄ K = σb̄ , so taking
M0 , ν b̄.Mb̄
we have σ0 = JM0 K .
Assume now |b̄| = 0, so x0 = m0 . σ0 satisfies the hypotheses of the third part of the
Decomposition Lemma. Hence, if m0 = a, a store-Q of type C under ⊛, then
σ0 = (hid, φi ; τ ; T ζ ′ ; T σa ; µ) ↾ (ā, iA(0) )
with trunc(σa ) < trunc(σ0 ) . Then, by IH, there exists ā | Γ, y : C |− Ma : B such that
σa = JMa K , and taking
(
(λy.Ma )(! a) , if a ∈ S(ā)
M0 ,
(λy.Ma )(! zj′ ) , if a # ā ∧ j = min{ j | a = (iA(0) )k+j }
we have σ0 = JM0 K ↾ (ā, iA(0) ).
Otherwise, m0 = jA ∨ m0 = (iB , ⊛), a store-H. If there exists an a ∈ AC such that σ0
answers to [iA(0) ∗ ⊛ m0 a] then, by Decomposition Lemma,
σ0 = h∆, σa i ; τ ; T (id⊗φ ; τ ) ; µ ; T σ ′ ; µ
with |trunc(σa )| , |trunc(σ ′ )| < |trunc(σ0 )| . By IH, there exist ā | Γ |− Ma : C and
ā | Γ |− M ′ : B such that σa = JMa K and σ ′ = JM ′ K. Taking
(
(a := Ma ); M ′
, if a ∈ S(ā)
M0 ,
′
′
(zj := Ma ); M
, if a # ā ∧ j = min{ j | a = (iA(0) )k+j }
we obtain σ0 = JM0 K . Note here that σa blocks initial moves [ā, iA ] 6= [ā, iA(0) ] and hence
we do not need the restriction.
We are left with the case of m0 being as above and σ0 not answering to any store-Q,
which corresponds to the case of Player not updating any names before playing m0 .
If m0 = (iB , ⊛) then we need to derive a value term hV1 , ..., Vm i (as B = B1 × · · · × Bm ).
For each p, if Bp is a base or reference type then we can choose a Vp canonically so that
its denotation be iBp (the only interesting such case is this of iBp being a name a # ā,
where we take Vp to be zj′ , for j = min{ j | a = (iA(0) )k+j }). Otherwise, Bp = Bp′ → Bp′′
and from σ0 we obtain the (tidy) viewfunction f : Qā (JAK ⊗JBp′ K) → T JBp′′ K by:
f , { [ (ā, iA(0) , iBp′ ) ∗ ⊛ s ] | [ (ā, iA(0) ) ∗ ⊛ (iB , ⊛) (iBp′ , ⊛) s ] ∈ viewf(σ0 ) }.

60

N. TZEVELEKOS

Note that, for any [(ā, iA ) ∗ ⊛ (iB , ⊛) (iBp′ , ⊛) s] ∈ viewf(σ0 ), s cannot contain store-Q’s
justified by ⊛ , as these would break (TD2). Hence, f fully describes σ0 after (iBp′ , ⊛) . By
IH, there exists ā | Γ, y : Bp′ |− N : Bp′′ such that JN K = strat(f ) ; take then Vp , λy.N .
Hence, taking
M0 , hV1 , ..., Vm i
we obtain σ0 = JM0 K ↾ (ā, iA(0) ).
If m0 = jA , played in some Ak+k′ +i = A′i → A′′i , then m0 = (iA′i , ⊛) . Assume that A′i =
A′i,1 × · · · × A′i,ni with A′i,p ’s being non-products. Now, O can either ask some name a
(which would lead to a store-CC), or answer at A′′i , or play at some A′i,p of arrow type,
′ . Hence,
say A′i,p = Ci,p → Ci,p
[ni
viewf(σ0 ) = fA ∪
fp where:
p=1

fA , f0 ∪ { [ (ā, iA(0) ) ∗ ⊛ (iA′i , ⊛) (iA′′i , ⊛) s ] ∈ viewf(σ0 ) }

fp , f0 ∪ { [ (ā, iA(0) ) ∗ ⊛ (iA′i , ⊛) (iCi,p , ⊛) s ] ∈ viewf(σ0 ) }
f0 , { [ (ā, iA(0) ) ∗ ⊛ (iA′i , ⊛) s] | [⊛ ⊛ s ] ∈ viewf(idξ ) }
and where we assume fp , f0 if A′i,p is not an arrow type. It is not difficult to see that
fA , fp are viewfunctions. Now, from fA we obtain:
fA′ : Qā (JAK ⊗JA′′i K) → T JBK , { [ (ā, iA(0) , iA′′i ) ∗ ⊛ s ] |
[(ā, iA(0) ) ∗ ⊛ (iA′i , ⊛) (iA′′i , ⊛) s ] ∈ fA } .
It is not difficult to see that fA′ is indeed a viewfunction (note that P cannot play a storeQ under ⊛ on the RHS once (iA′′i , ⊛) is played, by tidiness). By IH, there exists some
ā | Γ, y : A′′i |− MA : B such that JMA K = strat(fA′ ).
′ K by:
From each fp 6= f0 we obtain a viewfunction fp′ : Qā (JAK ⊗JCi,pK) → T JCi,p
fp′ , { [ (ā, iA(0) , iCi,p ) ∗ ⊛ s ] | [ (ā, iA(0) ) ∗ ⊛ (iA′i , ⊛) (iCi,p , ⊛) s ] ∈ fp } .
′ such that JM K = strat(f ′ ) , so
By IH, there exists some ā | Γ, y ′ : Ci,p |− Mp : Ci,p
p
p
take Vp , λy ′ .Mp . For each A′i,p of non-arrow type, the behaviour of σ0 at A′i,p is fully
described by (iA′i )p , so we choose Vp canonically as previously. hV1 , ..., Vni i is now of type
A′i and describes σ0 ’s behaviour in A′i .
Now, taking
M0 , (λy.MA )(zi′′ hV1 , ..., Vni i)
we obtain σ0 = JM0 K ↾ (ā, iA(0) ).

Finally, using the definability result and proposition 5.31 we can now show the following.
Corollary 5.34. T = (T , T, Q, O) satisfies ip-definability.
ā
Proof: For each ā, A, B, define DA,B
, { f : Qā JAK → T JBK | f is finitary } . By definabilā
ity, every f ∈ DA,B
is definable. We need also show:
ā
. Λā (f ) ; ρ ∈ Oā =⇒ Λā (g) ; ρ ∈ Oā ) =⇒ f .ā g .
(∀ρ ∈ DA→B,N

Assume the LHS assertion holds and let Λā (f ) ; ρ ∈ Oā , some ρ : Qā (JAK −−⊗ T JBK) → T N.
Then, let [s ; t] = [(ā, ∗) ∗ ⊛ (0, ⊛)b̄ ] ∈ Λā (f ) ; ρ , [s] ∈ Λā (f ) and [t] ∈ ρ. By proposition 5.31,

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

61

ā
[t] ∈ ρ≤t , so Λā (f ) ; ρ≤t ∈ Oā . Moreover, ρ≤t ∈ DA→B,N
, so Λā (g) ; ρ≤t ∈ Oā , by hypothesis.
Finally, ρ≤t ⊑ ρ implies Λā (g) ; ρ≤t ⊑ Λā (g) ; ρ , hence the latter observable, so f .ā g.

Hence, we have shown full abstraction.
Theorem 5.35. T = (T , T, Q, O) is a fully abstract model of νρ.
5.7. An equivalence established semantically. In this last section we prove that the
following terms M and N are equivalent. The particular equivalence exemplifies the fact
that exceptional behaviour cannot be simulated in general by use of references, even of
higher-order.
M , λf. stop : (1 → 1) → 1 ,

N , λf. f skip ; stop : (1 → 1) → 1 .

By full-abstraction, it suffices to show JM K ⋍ JN K, where the latter are given as follows.
1

JM K

/ T ((1 −−⊗ T 1) −−⊗ T 1)

∗

1
OQ

∗

OQ

(∗, ⊛)(1)
⊥

/ T ((1 −−⊗ T 1) −−⊗ T 1)

∗

PA

⊛

JN K

OQ

∗

PA

⊛

OQ

(∗, ⊛)(1)

PA

(∗, ⊛)(2)
(∗, ⊛)(3)
⊥

PA
OQ
PQ

Bottom links stand for deadlocks: if Opponent plays a move (∗, ⊛)(2) under the last ∗ in JM K
(thus providing the function f ) then Player must play JstopK, i.e. remain idle. Similarly
for JN K: if Opponent gives an answer to (∗, ⊛)(3) (providing thus the outcome of f skip)
then Player deadlocks the play.
We have that JM K ⊑ JN K and therefore, by (5.5), JM K . JN K . Conversely, let ρ :
T ((1 −−⊗ T 1) −−⊗ T 1) → T N be a tl4 tidy strategy such that [∗ ∗ ⊛ (0, ⊛)ā ] ∈ JN K ; ρ for
some ā. Then, because of the form of JN K, ρ can only play initial moves up to (∗, ⊛)(1) ,
then possibly ask some names to (∗, ⊛)(1) , and finally play (0, ⊛)ā . Crucially, ρ cannot play
(∗, ⊛)(2) under ∗: this would introduce a question that could never be answered by JN K,
and therefore ρ would not be able to play (0, ⊛)ā without breaking well-bracketing. Hence,
JM K and ρ can simulate the whole interaction and therefore [∗ ∗ ⊛ (0, ⊛)ā ] ∈ JM K ; ρ.
6. Conclusion
Until recently, names used to be bypassed in Denotational Semantics: most approaches focussed on the effect achieved by use of names rather than names themselves. Characteristic
of this attitude was the ‘object-oriented’ modelling of references [6, 3] and exceptions [19]
as products of their effect-related methods (in the spirit of [39]). These approaches were
unsatisfactory to some extent, due to the need for ‘bad’ syntactic constructors in the examined languages. Moreover, they could not apply to the simplest nominal language, the

62

N. TZEVELEKOS

ν-calculus [36], since there the achieved effect could not be given an extensional, name-free
description. These issues revealed the need that names be treated as a proper computational
effect [44], and led to the advent of nominal games [2, 21].
In this paper we have taken some further steps in the semantics of nominal computation
by examining the effect of (nominal) general references. We have shown that nominal games
provide a framework expressive enough that, by use of appropriate monadic (and comonadic)
constructions, one can model general references without moving too far from the model of
the ν-calculus [2]. This approach can be extended to other nominal effects too; e.g. in [47]
it is applied to exceptions (with and without references). Moreover, we have examined
abstract categorical models for nominal computation, and references in particular (in the
spirit of [45, 44]).
There are many threads in the semantics of nominal computation which need to be
pursued further. Firstly, there are many nominal games models to build yet: research in
this direction has already been undertaken in [24, 22, 47, 31]. By constructing models for
more nominal languages we better understand the essential features of nominal computation (e.g. name-availability [31]) and build stronger intuitions on nominal games. Another
direction for further research is that of characterising the nominal effect — i.e. the computational effect that rises from the use of names — in abstract categorical terms. Here we
have pursued this task to some extent by introducing the monadic-comonadic description
of nominal computation, but it is evident that the description needs further investigation.
We see that there are more monad-comonad connections to be revealed, which will simplify
and further substantiate the presentation. The work of Schöpp which examines categories
with names [41] seems to be particularly helpful in this direction.
A direction which has not been pursued here is that of decidability of observational
equivalence in nominal languages. The use of denotational methods, and game semantics
in particular, for attacking the problem has been extremely successful in the ‘non-nominal’
case, having characterised decidability of (fragments of) Idealized Algol [13, 34, 32]. It
would therefore be useful to ‘nominalise’ that body of work and apply it to nominal calculi.
Already from [32] we can deduce that nominal languages with ground store are undecidable,
and from [36] we know that equivalence is decidable for programs of first-order type in the
ν-calculus, but otherwise the problem remains open.
Acknowledgements. I would like to thank Samson Abramsky for his constant encouragement,
support and guidance. I would also like to thank Andy Pitts, Andrzej Murawski, Dan
Ghica, Ian Stark, Luke Ong, Guy McCusker, Jim Laird, Paul Levy, Sam Sanjabi and the
anonymous reviewers for fruitful discussions, suggestions and criticisms.
Appendix A. Deferred proofs
I. Proof of closure of tidiness under composition.
Lemma A.1. Let σ : A → B and τ : B → C be tidy strategies, and let [s ; t] ∈ σ ; τ , [s] ∈ σ
and [t] ∈ τ , with ps k tq = s k t ending in a generalised O-move in AB and x, an O-move,
being the last store-H in psq. Let x appear in s k t as x̃. Then, x̃ is the last store-H in s k t
and if x is in A then all moves after x̃ in s k t are in A. Similarly for BC and t.
Proof: We show the (AB, s) case, the other case being entirely dual. Let s = s1 xs2 and let
x appear in s k t as some x̃. If x is in A then we claim that s2 is in A. Suppose otherwise,

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

63

so s = s1 xs21 ys22 with s21 in A and y a P-move in B. Since x appears in psq, the whole
of s21 y appears in it, as it is in P-view mode already. Since x is last store-H in psq, s21 y is
store-H-less. If y a store-Q then it should be justified by last O-store-H in ps<yq, that is x,
which is not possible as x is in A. Thus, y must be a store-A, say to some O-store-Q q in
B. Now, since q wasn’t immediately answered by P, tidiness dictates that psq be a copycat
from move q and on. But then the move following x in s must be a copy of x in B, .
Hence, s2 is in A and therefore it appears in psq, which implies that it is store-H-less. Thus,
x̃ is last store-H in s k t.
If x is in B then we do induction on |s k t|. The base case is encompassed in the case of
s2 being empty, which is trivial. So let s2 = s21 ys22 z with y justifying z (since x appears
in psq, z has to be justified in s2 ). z is not a store-H and neither is it a store-Q, as then
y would be a store-H after x in psq. Thus z a store-A and y a store-Q, the latter justified
by last O-store-H in ps<yq = psq<y , that is x, so y, z in B. Now, s = s1 xs21 ys22 z and
t = t1 x′ t21 y ′ t22 z ′ ; we claim that s21 and t21 are store-H-less. Indeed, s<y k t<y′ ends in a
generalised O-move in AB and x is still the last store-H in ps<yq , from which we have, by
IH, that x̃ is the last store-H in s<y k t<y′ .
Thus, s k t = (s1 k t1 )x̃v ỹuz̃ with v store-H-less. It suffices to show that u is also storeH-less. In fact, u = ỹ . . . ỹ z̃ . . . z̃ for some n ≥ 0. Indeed, by tidiness of τ , (t22 z ′ ).1 is either
| {z } | {z }
n

n

an answer to y ′ , whence t22 = u = ǫ, or a copy of it under the last O-store-H in pt≤y′q. If
the latter is in B then σ reacts analogously, and so on, so there is initially a sequence ỹ . . . ỹ
in u, played in B. As u finite, at some point σ (or τ ) either answers y (y ′ ) or copycats it
in A (in C). In the latter case, O immediately answers, as s (t) is in P-view mode in A (in
C). Hence, in either cases there is an answer that is copycatted to all open ỹ in u, yielding
thus the required pattern. Therefore, u is store-H-less.

Lemma A.2. Let σ : A → B and τ : B → C be tidy strategies, and let [s ; t] ∈ σ ; τ ,
[s] ∈ σ and [t] ∈ τ , with ps k tq = s k t ending in a generalised O-move. If there exists i ≥ 1
and store-Q’s q̃1 , ..., q̃i with q̃ = q̃j , all 1 ≤ j ≤ i, and q̃1 , ..., q̃i−1 in B and q̃i in AC and
[(s k t)q̃1 ...q̃i ] ∈ σ k τ , then q̃i is justified by the last O-store-H in s ; t.
Proof: By induction on |s k t|. The base case is encompassed in the case of s ; t containing
at most one O-store-H, which is trivial. Now let without loss of generality (s k t)q̃1 ...q̃i =
′ ) with [sq ...q ] ∈ σ and [tq ′ ...q ′ ] ∈ τ , and let each q be justified by
(sq1 ...qi ) k(tq1′ ...qi−1
1
i
j
1
i−1
xj and each qj′ by x′j . Moreover, by hypothesis, xj = x′j , for 1 ≤ j ≤ i − 1, and therefore
each such pair xj , x′j appears in s k t as some x̃j , the latter justifying q̃j in s k t.
Now, assume without loss of generality that s k t ends in AB. Then, by tidiness of σ
and τ we have that, for each j ≥ 1,
q2j+1 = q2j

,

′
′
q2j
= q2j−1

,

qj = qj′

For each j ≥ 1, q2j+1 is a P-move of σ justified by some store-H, say x2j+1 . By tidiness of
σ, x2j+1 is the last O-store-H in ps<q2j+1q = ps≤q2jq, and therefore x2j+1 is the last store-H
in ps<x2jq. Then, by previous lemma, x̃2j+1 is the last store-H in s<x2j k t<x′2j = (s k t)<x̃2j .
Similarly, x̃2j is the last store-H in (s k t)<x̃2j−1 . Hence, the store-H subsequence of (s k t)≤x̃1
ends in x̃i ...x̃1 .
Now, by tidiness of σ, x1 is the last O-store-H in psq. If x1 is also the last store-H in
psq then, by previous lemma, x̃1 is the last store-H in s k t, hence x̃i is the last store-H in
s ; t. Otherwise, by corollary 5.21, q1 is a copy of s.−1 = q0 . If q0 is in A then its justifier is

64

N. TZEVELEKOS

s.−2 = x0 and, because of CC-mode, the store-H subsequence of s k t ends in x̃i ...x̃1 x̃0 , so x̃i
is the last O-store-H in s ; t. If q0 is in B then we can use the IH on s− k t− and q̃0 , q̃1 , ..., q̃i ,
and obtain that x̃i is the last O-store-H in s− ; t− = s ; t.
Proposition A.3. If σ : A → B and τ : B → C are tidy strategies then so is σ ; τ .
Proof: Take odd-length [s ; t] ∈ σ ; τ with not both s and t ending in B, ps k tq = s k t and
|s ; t| odd. We need to show that s ; t satisfies (TD1-3). As (TD2) is a direct consequence
of the previous lemma, we need only show the other two conditions. Assume without loss
of generality that s ; t ends in A.
For (TD1), assume s ; t ends in a store-Q q̃. Then s ends in some q, which is justified
by the P-store-H s.−2 = x (also in A). q is either answered or copied by σ ; in particular,
if q̃ = aā with a # ps ; tq− = s− ; t then a # s− , t , so σ copies q. If σ answers q with z then
z doesn’t introduce new names, so [(s ; t)z̃] ∈ σ ; τ with nlist(z̃) = nlist(q̃) and z̃ = z , as
required.
Otherwise, let σ copy q as q1 , say, under last O-store-H in psq, say x1 . If x1 is in B
then sq1 ≍ tq1′ , with q1 , q1′ in B and q1′ being q1 with name-list that of its justifier, say x′1 ,
where x1 = x′1 . Now [tq1′ ] ∈ τ and it ends in a store-Q, so τ either answers it or copies it
under last O-store-H in ptq1′q. In particular, if q = aā with a # ps ; tq then, as above, a # t
and τ copies q1′ . This same reasoning can be applied consecutively, with copycats attaching
store-Q’s to store-H’s appearing each time earlier in s and t. As the latter are finite and
initial store-H’s are third moves in s and t, at some point either σ plays qi in A or answers it
in B, or τ plays qi′ in C or answers it in B. If an answer occurs then it doesn’t introduce new
names (by tidiness), so it is copycatted back to q closing all open qj ’s and qj′ ’s. Otherwise,
we need only show that, for each j, q̃j = q̃, which we do by induction on j: q̃1 = q s • t,ǫ and
(s≤q ) •(t

′

),ǫ

IH

≤q
j
j
q̃j+1 = q
= q̃j = q̃. This proves (TD1).
For (TD3), assume s ; t = uq̃(O) q̃(P ) v ỹ with q̃(O)q̃(P ) v a copycat. Then, either both
q̃(O) , q̃(P ) are in A, or one is in A and the other in C. Let’s assume q̃(O) in A and q̃(P ) in C
— the other cases are shown similarly. Then, q̃(O) her(editarily)-justifies ỹ, and let s.−1 = y
be justified by some x in s. Now, as above, q̃(O) q̃(P ) is witnessed by some q̃(O)q̃1 . . . q̃i q̃(P ) in
s k t, with odd i ≥ 1 and all q̃j ’s in B. We show by induction on 1 ≤ k ≤ i that there exist
x1 , ..., xk , x′1 , ..., x′k , y1 , ..., yk , y1′ , ..., yk′ in B such that (sy1 . . . yk k ty1′ . . . yk′ ) ∈ σ k τ and, for
each relevant j ≥ 1,

yj = yj′ = y

,

y1 = y

,

y2j = y2j+1

,

′
′
y2j−1
= y2j

,

xj = x′j

with qj her-justifying xj in s and xj justifying yj (and qj′ her-justifying x′j in t and x′j
justifying yj′ ), and x̃j+1 , x̃j consecutive in s k t, and x̃1 , x̃ also consecutive.
For k = 1, let s = s1 q(O) q1 s2 y. Now, q̃(O) her-justifying ỹ implies that q(O) her-justifies
y, hence it appears in psq. Thus psq = s′1 q(O) q1 s′2 y, so, by (original definition of) tidiness,
[sy1 ] ∈ σ with y1 = y justified by x1 = psq .−3 = s.−3. Then, [ty1′ ] ∈ τ with y1′ = y1 .
By proposition 5.19, q(O) q1 s′2 is a copycat, so q1 her-justifies x1 and therefore x1 , y1 in B.
Finally, x = psq .−2 = s.−2 is a P-move so x̃1 , x̃ are consecutive in s k t.
′ ) ∈ σ k τ with y ′
For even k > 1 we have, by IH, that (sy1 . . . yk−1 k ty1′ . . . yk−1
k−1 an O′ q, so pty ′ ...y ′ q =
′
′
move her-justified by qk−1 , an O-move. Then, qk−1 appears in pty1′ ...yk−1
1
k−1
′
′ q ′ t y ′ , thus (by tidiness) [ty ′ ...y ′ y ′ ] ∈ τ with y ′ = y ′
t1 qk−1
1
k−1 justified by xk =
k
k−1 k
k 2 k−1
′
′
′
′
′
′
′
′
pty1 ...yk−1q .−3. Now, qk−1 qk t2 is a copycat so qk her-justifies xk . Moreover, xk , xk−1 are
consecutive in ptq, so, as x′k−1 a P-move, they are consecutive in t, and therefore x̃k , x̃k−1

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

65

consecutive in s k t. Finally, [sy1 . . . yk−1 yk ] ∈ σ with yk = yk′ . The case of k odd is entirely
dual.
′ ]∈
′
Now, just as above, we can show that there exist x′i+1 , yi+1
in C such that [ty1′ ...yi′ yi+1
′
′
′
τ and yi+1 justified by xi+1 , xi+1 her. justified by q(P ) , etc. Then [(s ; t)ỹi+1 ] ∈ σ ; τ with
x̃i+1 , x̃i , ..., x̃1 , x̃ consecutive in s k t, so x̃i+1 = (s ; t).−3. Finally, as above, ỹi+1 = ỹj = ỹ,
all j, as required.


II. Proof of Decomposition Lemma 5.32: 1 is straightforward: we just partition σ into σ0
ā
and σ ′ and recover it by use of [x = iA(0) ] and cnd. For 2, we just use the definition of
name-abstraction for strategies and the condition on σ.
For 3, it is clear that m0 is either a store-Q a under ⊛, or a store-H jA , or a store-H
(iB , ⊛).
In case m0 = a with a ∈ AC , we define σa : Qā (JAK ⊗JCK) → T JBK , strat(fa ) ,
where
fa , { [ (ā, iA(0) , iC ) ∗ ⊛ s ] | [ (ā, iA(0) ) ∗ ⊛ a iC s ] ∈ viewf(σ) } .
To see that fa is a viewfunction it suffices to show that its elements are plays, and for
that it suffices to show that they are legal. Now, for any [(ā, iA(0) , iC ) ∗ ⊛ s] ∈ fa with
[(ā, iA(0) ) ∗ ⊛ a iC s] ∈ viewf(σ), (ā, iA(0) , iC ) ∗ ⊛ s is a justified sequence and satisfies wellbracketing, as its open Q’s outside s are the same as those in (ā, iA(0) ) ∗ ⊛ a iC s , i.e. ⊛.
Moreover, visibility is obvious. Hence, fa is a viewfunction, and it inherits tidiness from σ.
Moreover, we have the following diagram.
Qā JAK

hid,φi ; τ ; T ζ ′

/ T Qā (JAK ⊗JCK)

T σa

/ T 2 JBK

µ

/ T JBK

(ā, iA(0) )
∗
∗
∗
⊛
⊛
⊛
a
a
a
iC
iC
iC
(ā, iA(0) , iC , ⊛)
(∗, ⊛)
⊛

66

N. TZEVELEKOS

Because of the copycat links, we see that
viewf(hid, φi ; τ ; T ζ ′ ; T σa ; µ) ↾ (ā, iA(0) )
= {[(ā, iA(0) ) ∗ ⊛ a iC s] | [(ā, iA(0) , iC ) ∗ ⊛ s] ∈ viewf(σa )} = viewf(σ) ,
as required. Note that the restriction to initial moves [ā, iA(0) ] taken above is necessary in
case φ contains a projection (in which case it may also answer other initial moves).
In case m0 = jA (so m0 a store-H) and [(ā, iA(0) ) ∗ ⊛ m0 a iC ] ∈ σ, we have that
σ = strat(fa ∪ (f ′ \ fa′ )) ,
where fa , f ′ are viewfunctions of type Qā JAK → T JBK, so that fa determines σ’s behaviour
if O plays a at the given point, and f ′ \ fa′ determines σ’s behaviour if O plays something
else. That is,
fa , { [ (ā, iA(0) ) ∗ ⊛ jA a iC s ] ∈ viewf(σ) }
fa′ , { [ (ā, iA(0) ) ∗ ⊛ jA a s ] | [⊛ ⊛ a s] ∈ viewf(idξ ) }
f ′ , fa′ ∪ { [ (ā, iA(0) ) ∗ ⊛ jA y s ] ∈ viewf(σ) | y 6= a } .
f ′ differs from viewf(σ) solely in the fact that it doesn’t answer a but copycats it instead;
it is a version of viewf(σ) which has forgotten the name-update of a. On the other hand,
fa contains exactly the information for this update. It is not difficult to see that f ′ , fa are
indeed viewfunctions. We now define
fa′′ : Qā JAK → T JCK , { [ (ā, iA(0) ) ∗ ⊛(iC , ⊛) s ] |
[ (ā, iA(0) ) ∗ ⊛jA a iC s ] ∈ fa ∨ [⊛ ⊛ s] ∈ viewf(idξ ) }
σa : Qā JAK → T JCK , strat(fa′′ )
σ ′ : Qā JAK → T JBK , strat(f ′ )
σ ′′ : Qā JAK → T JBK , h∆, σa i ; τ ; T (id⊗φ ; τ ) ; µ ; ∼
= ; T σ′ ; µ .
We can see that σ ′ is a tidy strategy. For σa , it suffices to show that fa′′ is a viewfunction,
since tidiness is straightforward. For that, we note that even-prefix closure and singlevaluedness are clear, so it suffices to show that the elements of fa′′ are plays.
So let [(ā, iA(0) ) ∗ ⊛ (iC , ⊛) s] ∈ fa′′ with [(ā, iA(0) ) ∗ ⊛ jA a iC s] ∈ viewf(σ). We have
that (ā, iA(0) ) ∗ ⊛ (iC , ⊛) s is a justified sequence, because s does not contain any moves
justified by jA or a. In the former case this holds because we have a P-view, and in the
latter because a is a closed (answered) Q. Note also that there is no move in s justified by
⊛: such a move (iB , ⊛) would be an A ruining well-bracketing as jA is an open Q, while a
store-Q under ⊛ is disallowed by tidiness as s.1 is an O-store-H. Finally, well-bracketing,
visibility and NC’s are straightforward.
We now proceed to show that σ = σ ′′ . By the previous analysis on fa′′ we have that
σa = σa′ ; η (modulo totality) where σa′ is the possibly non-total strategy
σa′ : Qā JAK → JCK , strat{ [ (ā, iA(0) ) iC s ] | [ (ā, iA(0) ) ∗ ⊛ jA a iC ] ∈ fa } ,
∼ ; T σ ′ ; µ . Analysing the behaviour of the
and hence σ ′′ ↾ (ā, iA(0) ) = h∆, σa′ i ; id⊗φ ; τ ; =
latter composite strategy and observing that the response of σ ′′ to inputs different than

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

67

[ā, iA(0) ] is merely the initial answer ∗ imposed by totality, we obtain:
viewf(σ ′′ ) = { [ (ā, iA(0) ) ∗ ⊛ jA a s ], [(ā, iA(0) ) ∗ ⊛ jA y s] ∈ viewf(σ ′′ ) | y 6= a }
= { [ (ā, iA(0) ) ∗ ⊛ jA a iC s ] | [ (ā, iA(0) ) ∗ ⊛ (iC , ⊛) s] ∈ fa′′ ∧ s.1 ∈ JJCK }
∪ { [ (ā, iA(0) ) ∗ ⊛ jA y s ] ∈ f ′ | y 6= a }
= fa ∪ (f ′ \ fa′ ) = viewf(σ)
as required.
In case x = (iB , ⊛) we work similarly as above.
References
[1] Abramsky, S. Domain theory. Lecture Notes, Oxford University Computing Laboratory, 2007.
[2] Abramsky, S., Ghica, D., Murawski, A., Ong, L., and Stark, I. Nominal games and full abstraction for the nu-calculus. In LICS ’04: Proceedings of the 19th Annual IEEE Symposium on Logic in
Computer Science (Turku, 2004), IEEE Computer Society Press, pp. 150–159.
[3] Abramsky, S., Honda, K., and McCusker, G. A fully abstract game semantics for general references. In LICS ’98: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science
(Indianapolis, 1998), IEEE Computer Society Press, pp. 334–344.
[4] Abramsky, S., and Jagadeesan, R. Games and full completeness for multiplicative linear logic.
Journal of Symbolic Logic 59, 2 (1994), 543–574.
[5] Abramsky, S., Jagadeesan, R., and Malacaria, P. Full abstraction for PCF. Information and
Computation 163, 2 (2000), 409–470.
[6] Abramsky, S., and McCusker, G. Linearity, Sharing and State: a fully abstract game semantics for
Idealized Algol. In O’Hearn and Tennent [33], pp. 297–329. Vol. 2, 1997.
[7] Baillot, P., Danos, V., and Ehrhard, T. Believe it or not, AJM’s games model is a model of classical
linear logic. In LICS ’97: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer
Science (Warsaw, 1997), IEEE Computer Society Press, pp. 68–75.
[8] Barr, M., and Wells, C. Category theory for computing science, third ed. Les Publications CRM,
Montreal, 1999.
[9] Brookes, S., and Geva, S. Computational comonads and intensional semantics. In Applications of
Categories in Computer Science: Proceedings LMS Symposium (Durham, 1991), vol. 177, Cambridge
University Press, pp. 1–44.
[10] Brookes, S., and van Stone, K. Monads and comonads in intensional semantics. Tech. Rep. CMUCS-93-140, Carnegie Mellon University, 1993.
[11] Freyd, P. J. Recursive types reduced to inductive types. In LICS’90: Proceedings of the 5th Annual
IEEE Symposium on Logic in Computer Science (Philadelphia, 1990), IEEE CS Press, pp. 498–507.
[12] Gabbay, M. J., and Pitts, A. M. A new approach to abstract syntax with variable binding. Formal
Aspects of Computing 13 (2002), 341–363.
[13] Ghica, D. R., and McCusker, G. Reasoning about Idealized Algol using regular languages. In
ICALP ’00: Proceedings of 27th International Colloquium on Automata, Languages and Programming
(Geneva, 2000), vol. 1853 of LNCS, Springer-Verlag, pp. 103–116.
[14] Harmer, R. Games and full abstraction for nondeterministic languages. DPhil thesis, University of
London, 1999.
[15] Honda, K., and Yoshida, N. Game-theoretic analysis of call-by-value computation. Theoretical Computer Science 221, 1–2 (1999), 393–456.
[16] Hyland, J. M. E., and Ong, C.-H. L. On full abstraction for PCF: I, II, III. Information and
Computation 163, 2 (2000), 285–408.
[17] Jeffrey, A., and Rathke, J. A fully abstract may testing semantics for concurrent objects. In
LICS ’02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (Copenhagen, 2002), IEEE Computer Society Press, pp. 101–112.
[18] Jones, S. P. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press,
May 2003.

68

N. TZEVELEKOS

[19] Laird, J. A fully abstract game semantics of local exceptions. In LICS ’01: Proceedings of the 16th
Annual IEEE Symposium on Logic in Computer Science (Boston, 2001), IEEE CS Press, p. 105.
[20] Laird, J. A categorical semantics of higher order store. In CTCS ’02: Category Theory and Computer
Science (Ottawa, 2002), vol. 69 of Electronic Notes in Theoretical Computer Science, pp. 209–226.
[21] Laird, J. A game semantics of local names and good variables. In FoSSaCS ’04: Proceedings of the 7th
International Conference on Foundations of Software Science and Computation Structures (Barcelona,
2004), vol. 2987 of Lecture Notes in Computer Science, Springer, pp. 289–303.
[22] Laird, J. Game semantics for higher-order concurrency. In FSTTCS ’06: Proceedings of the 26th
International Conference on Foundations of Software Technology and Theoretical Computer Science
(Kolkata, 2006), vol. 4337 of Lecture Notes in Computer Science, Springer, pp. 417–428.
[23] Laird, J. A fully abstract trace semantics for general references. In ICALP ’07: Proceedings of the
34th International Colloquium on Automata, Languages and Programming (Wroclaw, 2007), vol. 4596
of Lecture Notes in Computer Science, Springer-Verlag, pp. 667–679.
[24] Laird, J. A game semantics of names and pointers. Annals of Pure and Applied Logic 151 (2008), 151–
169. GaLoP ’05: First Games for Logic and Programming Languages Workshop (post-proceedings).
[25] Mac Lane, S. Categories for the working mathematician, second ed., vol. 5 of Graduate texts in
mathematics. Springer Verlag, 1998.
[26] McCusker, G. Games and Full Abstraction for a Functional Metalanguage with Recursive Types.
Distinguished Dissertations. Springer-Verlag, London, 1998.
[27] Milner, R., Tofte, M., and Macqueen, D. The Definition of Standard ML. MIT Press, 1997.
[28] Moggi, E. Computational lambda calculus and monads. Tech. Rep. ECS-LFCS-88-86, University of
Edinburgh, 1988.
[29] Moggi, E. Computational lambda-calculus and monads. In LICS ’89: Proceedings of 4th Annual IEEE
Symposium on Logic in Computer Science (Pacific Grove, 1989), IEEE CS Press, pp. 14–23.
[30] Moggi, E. Notions of computation and monads. Information and Computation 93, 1 (1991), 55–92.
[31] Murawski, A., and Tzevelekos, N. Full abstraction for Reduced ML. In FoSSaCS ’09: Proceedings
of the 12th International Conference on Foundations of Software Science and Computation Structures
(York, 2009), vol. 5504 of Lecture Notes in Computer Science, Springer, pp. 32–47.
[32] Murawski, A. S. On program equivalence in languages with ground-type references. In LICS ’03:
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (Ottawa, 2003), pp. 108–117.
[33] O’Hearn, P. W., and Tennent, R. D., Eds. ALGOL-like Languages. Birkhäuser, 1997.
[34] Ong, C.-H. L. Observational equivalence of third-order Idealized Algol is decidable. In LICS ’02:
Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (Copenhagen, 2002),
IEEE Computer Society Press, pp. 245–256.
[35] Pitts, A. M. Nominal logic, a first order theory of names and binding. Information and Computation
186 (2003), 165–193.
[36] Pitts, A. M., and Stark, I. D. B. Observable properties of higher order functions that dynamically
create local names, or: What’s new? In MFCS ’93: Proceedings of 18th International Symposium on
Mathematical Foundations of Computer Science (Gdańsk, 1993), vol. 711 of Lecture Notes in Computer
Science, Springer-Verlag, Berlin, pp. 122–141.
[37] Plotkin, G. D. LCF considered as a programming language. Theoretical Computer Science 5 (1977),
223–255.
[38] Plotkin, G. D., and Power, J. Notions of computation determine monads. In FoSSaCS ’02: Proceedings of the 5th International Conference on Foundations of Software Science and Computation
Structures (Grenoble, 2002), Springer-Verlag, pp. 342–356.
[39] Reynolds, J. C. The essence of Algol. In Proceedings of the International Symposium on Algorithmic
Languages (Amsterdam, 1981), North-Holland, pp. 345–372. Reprinted in [33, vol. 1, pages 67–88].
[40] Sanjabi, S. B., and Ong, C.-H. L. Fully abstract semantics of additive aspects by translation. In
AOSD ’07: Proceedings of the 6th international conference on Aspect-oriented software development
(Vancouver, 2007), ACM, pp. 135–148.
[41] Schöpp, U. Names and Binding in Type Theory. DPhil thesis, University of Edinburgh, 2006.
[42] Scott, D. S. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science
121, 1-2 (1993), 411–440. First written in 1969 and circulated privately.
[43] Smyth, M. B., and Plotkin, G. D. The category-theoretic solution of recursive domain equations.
SIAM Journal on Computing 11, 4 (1982), 761–783.

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES

69

[44] Stark, I. D. B. Names and Higher-Order Functions. PhD thesis, University of Cambridge, Dec. 1994.
Also available as Technical Report 363, University of Cambridge Computer Laboratory.
[45] Stark, I. D. B. Categorical models for local names. Lisp and Symbolic Computation 9, 1 (Feb. 1996),
77–107.
[46] Tzevelekos, N. Full abstraction for nominal general references. In LICS ’07: Proceedings of the 22nd
Annual IEEE Symposium on Logic in Computer Science (Wroclaw, 2007), IEEE Computer Society
Press, pp. 399–410.
[47] Tzevelekos, N. Full abstraction for nominal exceptions and general references. In GaLoP ’08: Games
for Logic and Programming Languages (Budapest, 2008). Journal version submitted to APAL.
[48] Tzevelekos, N. Nominal game semantics. DPhil thesis, Oxford University, 2008.
[49] Wadler, P. The essence of functional programming. In POPL ’92: Conference Record of the 19th
ACM Symposium on Principles of Programming Languages (Albuquerque, 1992), pp. 1–14.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http:// reative ommons.org/li enses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany

