Probabilistic game semantics.
A category of HO/N-style games and probabilistic strategies is developed where the possible choices of a strategy are quantified so as to give a measure of the likelihood of seeing a given play. A two-sided die is shown to be universal in this category, in the sense that any strategy breaks down into a composition between some deterministic strategy and that die. The interpretative power of the category is then demonstrated by delineating a Cartesian closed subcategory that provides a fully abstract model of a probabilistic extension of Idealized Algol.
Introduction
Consider the fixpoint expression Y(x:(1 or x)). This can
have two very different meanings attached. If, by or, it is
meant that both sides can happen with, say, equal chances
almost surely, we'll get the result 1. If, on the other
hand, it is meant only that either can happen-but we don't
know which-then the only consistent answer is to say that
we may get 1 but we also may diverge. This latter meaning
was investigated in a recent games model for nondeterminism
by Harmer & McCusker [12]. In this paper, we construct
a games model of the former by developing a suitable
notion of probabilistic strategy.
One motivation for doing this is to give a means of understanding
quantitative aspects of uncertainty that might
arise in the description of a process. Dually, inherently
probabilistic processes-such as randomized optimization
procedures, optimal strategies in classical game theory or
more general adaptive behavior-can be accounted for in
this framework.
Another motivation is purely mathematical. Extending
games semantics to the probabilistic case is a natural step to
take, just as probabilistic strategies are extremely natural in
VonNeumann matrix games. Indeed, our category smoothly
extends the deterministic games world charted out by Hyland
Ong [13] and Nickau [20] and further developed by
McCusker [2] and Laird [15].
The category also fits in very nicely with the basic concepts
of probability theory. The interaction of a strategy and
a counter-strategy on a game gives rise to a Borelian sub-
probability on the infinite plays. The category has a tensor
product which corresponds to the classical product measure
construction, and composition of strategies is defined using
the image measure under the composition function (which
in our case is always measurable). A factorization result is
shown, saying that any probabilistic strategy can be broken
down into the composition of a deterministic one and the 2-
sided die. In that sense, the 2-sided die is shown to be uni-
versal. This is a discrete version of the basic fact that any
probability on [0; 1] can be reconstructed as the law of some
random variable defined on the Lebesgue probability triple.
In short, we give what seems the fundamentals of a higher-order
probability theory in "interactive" form.
A case study We eventually zero in on a Cartesian closed
subcategory which we show provides a fully abstract model
of a probabilistic extension of Idealized Algol. The exact
choice of probabilistic primitive used to extend Algol is not
overly important since, by our factorization result, any probabilistic
process can be programmed using only a fair coin.
The recent shifting of conditions from plays to strategies and
other advances in the field allow, at this point, the use of
a pretty standard machinery: we restrict to single-threaded
strategies-those that are copyable and discardable with respect
to the tensor product-and show that homsets admit
a !-continuous CPO structure of which the basis is easily
seen to be Algol-definable thanks to the factorization theorem
and a previous theorem of Abramsky & McCusker [3].
For general reasons, this suffices to show full abstraction.
Generality Our construction in no way depends on a particular
games model: we give it in sufficient generality so
that it can be adapted to whatever particular language we
already know a deterministic games model of. And that is
already quite a lot since, apart from the purely functional
PCF, there are models for control, ground and general ref-
erences. That games semantics concepts adapt in this way
gives a sense of the homogeneity of this semantic universe,
in due contrast with traditional denotational semantics.
Related work The most obvious precursor to this work is
the study of probabilistic powerdomains and their application
to denotational semantics as in the early work of Saheb-
Djahromi [22, 23] and of Jones & Plotkin [14] amongst oth-
ers. More recent work [7, 8] has investigated bisimulation
in a probabilistic context. It would be interesting to consider
more closely the connection between that work and our own
as this remains rather unclear for now.
Another possible connection is with exact real arithmetic
[9]. Intriguingly, several of the issues raised in our work,
particularly those surrounding the factorization result, have
a similar flavour to those raised in real arithmetic [21]. It
would be interesting to pursue this line of investigation further
and, indeed, to consider using game semantics to model
a language such as Real PCF [10].
Future work One challenging application could be in
probabilistic program analysis. Hankin and Malacaria's
static analysis techniques derived from games semantics
[16, 17, 18] could get on well with probabilities, and give
tools in code optimization for instance. Less an application
maybe, but still sort of practical, is the tempting question of
whether the probabilistic observational equivalence can be
shown to be decidable for our extension of Idealized Algol
since, in that particular case, the so-called intrinsic equivalence
in the intensional model has a simple concrete charac-
terization. If solved to the positive, that could relate to formal
methods in programming.
A more theoretical question is that of relating our model
to Harmer & McCusker's model [12]. There is an obvious
embedding of theirs into ours, based on an equal chances interpretation
of non-determinism, but it isn't fully abstract,
as the opening example clearly shows. Another possibility
is the investigation of a "timeless" version of our model
in the spirit of the Baillot, Danos, Ehrhard & Regnier [6]
construction starting from a symmetrized games model of
Linear Logic and ending in a polarized variant of relational
semantics. The concurrent games of Abramsky & Mel-
lies [1] and their polarized version by Mellies could prove
useful here, since they are an intermediate step between
games and hypercoherences. Current investigation with
Ehrhard shows that there are probabilistic coherence spaces
that could bridge the gap, at least in the intuitionistic case.
Game semantics represents computation with "execution
traces" that describe the interaction between a System and
its Environment. The System and Environment are modelled
as the protagonists, respectively Player and Opponent,
in a game; an execution trace by a sequence of moves played
by the two protagonists.
To make these ideas precise, we need a few bits of nota-
tion. The set of strings over an alphabet \Sigma is written \Sigma ? . If
s; t 2 \Sigma ? , we write s v t if s is a prefix of t, denote the
length of s by jsj and, for 1  i  jsj, denote the ith symbol
of s by s i . The unique string of length 0 is written ". If
for the restriction of s to \Sigma 0 , i.e. the
subsequence obtained by erasing all symbols of s not in \Sigma 0 .
2.1 Arenas & legal plays
The basic ground rules of a game are determined by the
arena in which it is played. We formally define an arena
as a triple hMA ; A ; 'A i where:
ffl MA is a countable set of moves.
Ag \Theta fI; ng is a labelling
function designating each move m as an Opponent or a
Player move, a Question or an Answer and as an Initial
or non-initial move.
We define  OP
A ,  QA
A and  In
A as the first, second and
third projections respectively from A .
ffl 'A is a binary relation, known as enabling, on MA
such
A (m) 6=  OP
A (n) and  In
A (n) 6=
I.
In
These conditions say that the protagonists enable each
other's moves, not their own; that initial moves can't be en-
abled; that only Opponent can have initial moves and, more-
over, they must be Questions; and that Answers must be enabled
by Questions.
Flat arenas If X is a countable set, we define the flat
arena over X by setting MX to be X
making
q 'X x for every x 2 X . We denote by C, B and N respectively
the flat arenas over the one-point set fag, the two-point
set ftt; ffg and the countably infinite set f0;
Legal plays A string s
A can be endowed with a "jus-
tification structure" by equipping each non-initial move in s
with a "pointer" pointing back to an earlier enabling move.
This can be formalized with a function f s
In
then we say that
then we call s i an initial occurrence. If f s
then we say that s i is
hereditarily justified by s jn . A string equipped with such
an f s is called a justified string. A legal play is a justified
string that strictly alternates between Opponent and Player:
A (a) 6=  OP
A (b).
We write LA for the set of all legal plays in the arena A;
even
A and L odd
A denote the obvious subsets so that Player
made the last move in s 2 L even
A , etc.
If s 2 LA , we write ie(s) for the set of all immediate
extensions of s, i.e. those legal plays t such that s v t and
1. The current thread of sa 2 L odd
A , written
dsae, is defined as the subsequence of sa consisting of all
moves hereditarily justified by the hereditary justifier of a.
Product & arrow If A and B are arenas, we define their
product A \Theta B by:
the disjoint union.
the copairing.
This places A and B "side by side" with no chance of any
interaction between them. The empty arena
with sole legal play " is the unit for this constructor.
Our other constructor is the arrow, defined by:
OP
In
-  In
or  In
In
A (n).
In other words, the initial moves of A ) B are the initial
moves of B, the r"oles of Opponent and Player are reversed
in A and the (formerly) initial moves of A are now enabled
by the (still) initial moves of B.
2.2 Strategies
A strategy is a kind of "rule book" saying which moves may
be made by Player and with what probability. First of all, a
prestrategy oe on an arena A is just a function oe : L even
The traces of oe, which we denote by T oe , are those
even-length legal plays assigned non-zero weight by oe, i.e.
The domain of oe, written dom(oe), is those odd-length
plays that are "reachable" by oe, i.e. fsa 2 L odd
g.
Finally, given s 2 dom(oe), we define the range of oe at s,
written rng oe (s), to be those immediate extensions of s that
are in T oe , i.e. this can be empty.
A prestrategy oe for A is a strategy iff
A then oe(s)
t2ie(sa) oe(t).
Note that (p2) implies that oe is order reversing with respect
to the prefix ordering on T oe and the usual ordering on [0; 1].
This means that T oe is even-length prefix-closed. Further-
more, by (p1), we get oe(s)  1 for all s 2 LA .
Basic constraints A strategy oe is deterministic iff for all
Equivalently, oe takes values in f0; 1g.
Note that (p2) asserts only an inequality. If oe is a strategy
for which this is always in fact an equality, we say that it's a
total strategy. This point is further discussed below.
Local probabilities Given sa 2 dom(oe), define the conditional
probability of sab given sa by:
well-defined. By
(p2), this gives a subprobability on rng oe (sa) for each sa 2
dom(oe). Intuitively speaking, oe(sab=sa) is the "die" that oe
rolls for each sa 2 dom(oe).
2.3 Examples of strategies
The fair coin The simplest example of a probabilistic
strategy is probably the "fair coin" coin on the Boolean arena
B. Its trace set is just the set of even-length sequences of
the form qb 1 \Delta \Delta \Delta qb n where each b i is in ftt; ff g and is justified
by the immediately preceding move. We assign a probability
to such an s 2 T coin by e.g.
etc. All local probabilities, such as oe(qffqtt=qffq), are 1=2.
The polydie Another useful probabilistic strategy is
polydie on N ) N. A typical play of polydie is:
and the probability assigned to this play is
1=n. In other words, polydie asks for a number n and then
rolls an n-sided die, returning something between 0 and
1 with uniform probability.
Strategies on flat arenas as probability measures Plays
in B of the form are in a 1-1 correspon-
dence, denoted by B(\Delta), with finite binary strings over
1g. Given such a binary string w, we set
xg. These Vw s are the basic open sets of
the Cantor topology on infinite binary strings.
Given a total strategy oe on B, we define p oe (V
oe(s), which standardly extends to a unique probability measure
on the Borelian oe-algebra B generated by the Vw s. We
can now see that (p1) says that the measure of the whole
space is 1, while (p2) says that p is countably additive (or
subadditive if oe isn't assumed total). Conversely, any probability
measure on B defines a total stategy on B.
Such a probability measure could be any discrete-time
stochastic process with values in f0; 1g and, in particular,
it needn't be a Markov process. An example of this is
the damped deviation die, denoted 3d, a strategy where the
larger the deviation between trues and falses so far, the likelier
it is to return that value which diminishes the deviation.
For any play such as be the difference
between the number of trues and falses in s, suppose
d(s)+2 . Hence, 3d must
be able to look arbitrarily far back in time.
2.4 Composing strategies
Let u be a finite string of moves from arenas A, B
and C equipped with candidate "justification pointers",
i.e. a strictly decreasing function f
1g. We define uB;C to be the subsequence
of u where we delete all moves from A and suitably "renor-
f u to preserve the "pointers". We define u
similarly. We define u  A; C by removing all moves from
and "pointers" to B except in the case where a 2 MA points
to b 2 MB which, in turn, points to c 2 MC , whence we
make a point directly to c in uA; C.
A legal interaction of arenas A, B and C is such a u
satisfying
We write int(A; B; C) for the set of
all legal interactions of A, B and C.
If s 2 L even
A)C , we define its set of witnesses by:
i.e. all legal interactions playing s "on the outside". Given
strategies oe and  for A ) B and B ) C respectively,
we define oe ;  for A ) C by assigning a probability to
with the following composition formula.
We sometimes write oe k (u) for oe(u A; B) \Delta (uB; C).
Note that oe and  are "rolling" independent dice and that the
above sum is always countable just because int(A; B; C) is.
Well-defined composition It's clear that the composite of
two prestrategies is itself a prestrategy (with the convention
that also easy to see that (p1) is preserved.
The lemma below does most of the rest of the work.
Lemma 2.1 (probabilistic flow) If sa 2 L odd
A)C and ua 2
C) such that u 2 wit(s), let W ua be the set of
all
ie(sa), i.e. all legal interactions starting like ua and witnessing
an immediate extension of sa. If oe : A ) B and
Proof We prove by induction that the interactions obtained
by truncating W ua at any depth d, i.e. W ua
dg, satisfy the inequality. Applying
(p2) to a's component gives the base case. Other-
wise, by the inductive hypothesis,
oe k (u). Each u 0 2 W ua =d which hasn't yet reached the
"outside" can have many extensions in W ua =d
(p2) again, their sum cannot exceed the probability of u 0 .
Hence
Proposition 2.2 If oe and  are strategies for A ) B and
respectively then oe ;  is a strategy for A ) C.
Proof We just check (p2). If sa 2 L odd
t2ie(sa) wit(t). For each u 2 wit(s), we have W ua as
defined in lemma 2.1; clearly W ua ' W sa . Moreover, if
W sa . We now apply lemma 2.1 to each witness u and its associated
W ua so that
and, since
the desired
result follows. \Xi
Remark If both strategies are deterministic, i.e. with values
in f0; 1g, then oe ; (s) is an integer which, by (p1) and
(p2), can only be 0 or 1, so there can be at most one witness
of s. In general, a play can have (infinitely) many witnesses.
A category of arenas & strategies The above result tells
us that we have a good notion of composition and it's routine
to verify that this is associative. The usual copycat strategies
are our identities:
even s: sA
where id A
In summary, we have a category where objects are arenas
and an arrow from A to B is a strategy for A ) B. We
also have a subcategory of deterministic strategies since this
class of strategies is closed under composition.
2.5 Examples of composing strategies
Consider composing coin with the "wait for true" strategy
defined as the semantics of
Y(f: x: if x then skip else f(x)):
Some typical interactions are:
a
ff
a
ff
ff
a
The first witness of qa has probability 1=2, the second has
probability 1=4, etc., so the overall probability of qa is 1=2+
If we use a biased coin instead-where the more time
that's passed, the less likely it is to return true-the probability
of becoming "trapped" in the loop can be non-zero.
For instance, set
coin
1+jsj=2
1. The overall probability of qa
is now
which can be anything between 0
and 1. Of course, for coin 0 to satisfy (p2) we must have, for
all
but this is the case since, by
assumption,
We can easily make coin 0 into a total strategy so that the
class of total strategies can't be closed under composition:
pieces of chance can get lost in infinite chatters. This is the
reason why (p2) is an inequality.
Another variation on this example uses the "count for
true" strategy on B ) N defined as the semantics of
Y(f: x: if x then 0 else 1+f(x)):
In the composite with (the usual) coin, we get q0 with probability
1=2, q1 with probability 1=4, q2 with probability 1=8
and so on. In other words, the result is a geometric distribution
on the natural numbers: we output n with probability
Variations on a -scheme Consider the strategy mu 2 defined
as the semantics of
of type (Nat Com. This term takes an input f
and feeds it successive arguments, beginning with 2, until it
gives an output 0, at which point it just terminates.
If we compose polydie with mu 2 , the behaviour is as fol-
lows. Initially, a 2-sided die is rolled. If it turns up a 0, we're
done; otherwise, a 3-sided die is rolled. If a 0 turns up this
time, we're done; otherwise a 4-sided die is rolled, etc. The
trace qa appears in the composite strategy with probability
An interesting variation on this is to stop once a 0 has
been rolled, but only continue with the larger die if a 1 was
rolled; otherwise, we just give up. This can be done by replacing
the 'if0' subterm with
case f(x) of 0 7! skip
If we compose polydie with the strategy rr associated with
this modified -scheme term, the probability of qa in the
composite is 1=2
0:718. This shows that the class of strategies where all probabilities
are rational isn't closed under composition.
2.6 SMCC structure
If oe and  are strategies for A ) C and B ) D respectively
then we define oe \Theta for (A\ThetaB) ) (C \ThetaD) in the following
manner. Given s 2 T oe\Theta , we define its probability simply
as the product of its probabilities in the two components:
(oe \Theta
Note that there is no interaction between oe and  : they each
have their own die. This makes \Theta into a bifunctor on our cat-
egory. In fact, the evident copycat strategies provide us with
a symmetric monoidal structure. In the usual way, a simple
relabelling of moves gives rise to a natural isomorphism between
oe on
we have a symmetric monoidal closed category. The tensor
is the terminal object.
Finally, for an arena A, the unique strategy ! A on A ) 1
and the diagonal strategy \Delta A on A )
A with a cocommutative comonoid structure: for s 2
even
(with probability 1) iff
s: s
means the subsequence of s 0 consisting of all
moves hereditarily justified by an initial occurrence in A '
and s 0 r is defined similarly.
2.7 Ordering strategies
Given strategies oe and  for some arena A, we set oe 6
iff, for all s 2 LA , we have oe(s)  (s). This is clearly a
partial order. It's straightforward to show that composition
is monotone with respect to this.
CPO-enrichment In fact, we can show that each homset
of our category is a CPO and that composition is continuous,
i.e. our category "is" CPO-enriched.
Proposition 2.3 Given a 6-directed set of strategies \Delta, if
we define
F \Delta by
G
\Deltag
then it's the least upper bound (lub) of \Delta.
Proof We show only that
F \Delta is a well-defined strategy;
that it is the lub follows easily. It's clear that
F \Delta is a pre-
strategy satisfying (p1). For (p2), it suffices to consider
F \Delta). If rng F \Delta
any n 2 N and ffl ? 0, we can find strategies
such that  i (sab
the  i s have an upper bound  in \Delta so that
G
G
G
and the result follows. \Xi
An argument with a similar flavour establishes that composition
respects lubs of directed sets, i.e. if oe : A ) B,
and \Delta is a directed set of strategies for
then oe ;
A countable basis For any arena A, the collection of
strategies with finite trace set and where all probabilities are
rational forms a basis for the CPO of all strategies. i.e. for
any oe on A, the set \Delta oe of such strategies approximating oe
is directed and has oe as its least upper bound.
The only tricky point to check is that \Delta oe is indeed di-
rected. Given oe with trace set
the union of T oe 1
and T oe 2
, assigning probabilities as follows.
If s is a maximal trace, we set oe 3 (s)g.
Otherwise, set oe 3 (s) to be the maximum of oe 1 (s), oe 2 (s) and
f
g. Then, by con-
struction, oe 3 is a valid strategy and is an upper bound for oe 1
and oe 2 in \Delta oe .
This basis is always countable so that the set of all strategies
for A is an !-continuous CPO. This contrasts with all
previous HO-games models, including [12], where strategies
form !-algebraic CPOs, the compact strategies being those
with a finite number of traces.
2.8 Deterministic factorization
The technique of factorization has become standard in game
semantics. The underlying idea is similar to that of [12]
where a nondeterministic strategy is reduced to a deterministic
strategy that has access to a nondeterministic "oracle".
In our case, the "oracle" strategy is a die. It suffices to use a
2-sided die but, for convenience, we use the polydie defined
above.
We first present a simplified factorization that works for
basis strategies. Afterwards, we sketch a more general factorization
that allows us to simulate any probabilistic strategy
with a deterministic strategy and the polydie.
Basis factorization Let oe be a basis strategy for arena A
and consider sa 2 dom(oe). Since T oe is finite, we know
that rng oe (sa) must be finite; we'll write it as rng oe
g. Since all probabilities in oe are rational,
the local probability oe(sab i =sa), for each sab i 2 rng oe (sa),
is too.
Theorem 2.4 (deterministic factorization) If oe is a basis
strategy for the arena A then there exists a deterministic
strategy Det(oe) for (N ) N) ) A such that polydie ;
and Det(oe) is compact.
Proof The above remarks imply that we can find a common
denominator d for the local probabilities oe(sab i =sa).
be the numerators such that p i
=sa). The strategy Det(oe) proceeds in the following
fashion.
a
d
so on. In other words,
we "slice up" the interval from 0 to d \Gamma 1 according to the
numerators
This clearly defines a deterministic strategy and it's easy
to check that supplying the polydie as input achieves a correct
simulation of the original strategy so that polydie ;
obvious that, since oe has a finite trace
set, Det(oe) must have too. \Xi
Conversely, a small calculation with the composition formula
shows that any strategy that can be factorized as
polydie ; oe where oe is deterministic and compact must belong
to the basis.
General factorization To extend this idea to the general
case, consider first a strategy oe all of whose probabilities
are rational (but not necessarily having a finite trace set). If
the local probabilities. If oe(sab 1 we roll a
die. If the result is less than n 1 , we play b 1 ; other-
wise, we renormalize the remaining probabilities by dividing
through by then repeat this process for
For example, if the local probabilities of b 1 and b 2 are 2=3
and 1=6 respectively, the following play produces b 2 .
a
We roll a 2-sided die the second time since the renormalized
probability of b 2 is
Finally, if a play in oe has irrational probability p, we can
always find a sequence of rationals whose series of partial
sums converges to p. So, for each point sab i in the range,
we either have a single rational or a sequence of rationals.
Using a standard trick (such as the one used to enumerate
N \Theta N) we can reduce this to the previous case. The essential
point of this is that a play with irrational probability
is not factorized in "one go". In fact, it will have an infinite
number of witnesses: the desired probability gradually
builds up as we progress further and further down its
sequence of rationals.
3 A fully abstract model of PA
3.1 Probabilistic Algol
Our starting point is the language IA as defined in [3]. All we
need to do is add in some probabilistic primitive. But should
we add a coin or should we rather choose the polydie? Well,
the polydie might be more handy to program with-indeed,
the programminglanguageCAML has a "probabilistic func-
tion" Random:int which exactly implements the polydie-
but, for the contextual equivalence, it makes no difference
whatsoever.
In fact, the polydie can even be programmed inside Algol
using only a coin. Informally it goes this way: given an n,
choose a k such that 2 k  n, then roll for a first round the
2-sided die k times. If the answer, which is a binary string
of length k, codes for some integer in
it; if not, go for another round, and so on, until you succeed.
This idea can be programmed in a purely functional style.
We give an example using CAML:
let rec roll
if k=0
then 0
else if coin ()
then (2* roll (k-1))+1
else (2* roll (k-1));;
let rec polydie
if res<n then res
else polydie n;;
where we assume 'findk n' returns dlog 2 ne and `coin ()'
returns true or false with 50-50 odds.
This coin can, in fact, also be written in CAML using
the Random:int primitive mentioned above. The thunking
is just because CAML is call-by-value.
let coin
if Random.int
then true
else false;;
So, for the sake of simplicity, we just add a single term
coin of type Bool. We call this extended language PA for
probabilistic Algol.
To complete the definition of the language, we need to
give its operational interpretation. We do this in the usual
"big step" style except that derivations must be decorated
with probabilities.
We have the obvious rules for the coin:
The other rules follow naturally; we just give a few exam-
ples. (For the sake of readability, we're eliding the use of
stores; adding them poses no problem.)
if M N L
Because of coin, there might be (countably) many evaluations
of M t be the sequence of their respective
probabilities, it is easy to see that
Finally, let M and N be closed terms of the same type.
They are contextually equivalent iff, for all contexts C[\Gamma]
of ground type, we have C[M
. We denote this by M ' N .
As an example, let Mn be the nth "Church numeral"
'h:h n (tt)' and N be `x: if coin ff x' of types (Bool !
We observe that
\Gamman
tt so that the context (\Gamma)N allows us to distinguish
between all the Mn s.
This demonstrates the discriminating power, even in the
purely functional world, of probabilistic contexts, for it is
easily seen that Mn and Mn+2 are contextually equivalent
(for n  2) in PCF.
3.2 The model
We now begin the process of building a model of PA by introducing
the class of single-threaded strategies.
Recall that the current thread of sa 2 L odd
A is written
as dsae. If we have some tab 2 L even
A such that
dtae and the justifier of b occurs in dtae, we denote by
Match(tab; sa) the play sab where b is justified in the same
way as in tab.
We say that a strategy oe is single-threaded iff
ffl for all sab 2 T oe , the justifier of b occurs in dsae.
Note that this condition is expressed in terms of the local
probabilities of oe. It is now a lengthy but routine matter to
verify the following result.
Proposition 3.1 A strategy oe for A ) B is single-threaded
if, and only if, it's a comonoid homomorphism, i.e.
For general reasons [11], this shows that the single-threaded
strategies form a Cartesian closed category C. Fur-
thermore, the CPO-enriched structure all restricts down to
C, i.e. we have a CPO-enriched CCC.
Visibility & bracketing The remaining constraints required
to cut the model down to match well with Algol both
rely on the following definition of the view, written psq, of a
non-empty legal play s.
is an O-move and
justifies m;
is a P-move.
A strategy oe satisfies the visibility condition iff, for all sab 2
oe , the justifier of b occurs in psaq; and oe satisfies the bracketing
condition iff, for all sab 2 T oe where b is an Answer, b
is justified by the pending Question of psaq, i.e. the most recently
asked but, as yet, unanswered Question in psaq. Both
these constraints are preserved by composition.
Our interpretation of PA is in the sub-CCC of C, denoted
by C vb , of (single-threaded) strategies subject to both these
constraints. The interpretation of IA, i.e. the deterministic
fragment of the language, follows that of Abramsky & McCusker
[3]; our probabilistic primitive coin is interpreted
by the strategy coin.
We have the following soundness result for our model of
PA in C vb as a corollary to the usual consistency and adequacy
results.
Theorem 3.2 If M and N are closed terms of PA of type T
such that [[M
3.3 Full abstraction
With the soundness result in place, the path to full abstraction
is relatively standard. First of all, we prove a definabil-
ity result for basis strategies in the model.
Theorem 3.3 If T is some type of PA and oe is a basis strategy
on of PA.
Proof By the factorization theorem,
where Det(oe) is a compact deterministic strategy. By the
definability theorem of Abramsky & McCusker [3], this
strategy is definable in IA. But, since polydie is definable
in PA, we're done. \Xi
We define an equivalence relation on each homset of C vb
as follows. Given f; iff for all "test
where is the name of f , defined by currying

The so-called intrinsic quotient category E vb obtained by
quotienting C vb with this relation is also a CCC and, more-
over, the above soundness result survives the quotient. The
converse to soundness also holds there.
Theorem 3.4 (full abstraction) If M and N are closed
terms of type T then E
Proof We only need to prove the right-to-left direction.
Suppose that E [[M test ff,
homsets in C vb are continuous CPOs,
we can WLOG assume ff to be a basis element. Hence, by
definability,
it follows that this context distinguishes M and N . \Xi



--R

Concurrent games and full completeness.
A fully abstract game semantics for general references.
Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions.

Full abstraction for Idealized Algol with passive expressions.
games.
Bisimulation for labeled Markov processes.
A logical characterization of bisimulation for labeled Markov processes.
Domains for computation in mathematics
PCF extended with real numbers.

A fully abstract game semantics for finite nondeterminism.
On full abstraction for PCF: I
A probabilistic power- domain of evaluations
Full abstraction for functional languages with control.
Generalised flowcharts and games.
A new approach to control flow analysis.

Games and full abstraction for FPC.
Hereditarily sequential functionals.

Probabilistic LCF.
CPOs of measures for nondeter- minism
--TR
Rational probability measures
A probabilistic powerdomain of evaluations
PCF extended with real numbers
Full abstraction for idealized Algol with passive expressions
On full abstraction for PCF
Hereditarily Sequential Functionals
Generalised Flowcharts and Games
A New Approach to Control Flow Analysis
Call-by-Value Games
Reasoning about Idealized ALGOL Using Regular Languages
Games and Full Abstraction for FPC
Bisimulation for Labelled Markov Processes
Full abstraction for functional languages with control
Semantics of Exact Real Arithmetic
A Logical Characterization of Bisimulation for Labeled Markov Processes
A Fully Abstract Game Semantics for General References
A Fully Abstract Game Semantics for Finite Nondeterminism
Non-Deterministic Games and Program Analysis

--CTR
Pierre-Louis Curien, Definability and Full Abstraction, Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.301-310, April, 2007
probabilistic Idealized Algol;games semantics