[Prev][Next][Index][Thread]
Games and sequentiality
Date: Wed, 03 Jun 92 09:57:31 -0700
The following set of preliminary results, which I would like to bring to
the attention of types readers, seems to indicate that there is a nice
relation between games and sequentiality.
CONCRETE DATA STRUCTURES, SEQUENTIAL ALGORITHMS, AND LINEAR LOGIC
P.-L. Curien ENS-CNRS, visiting scientist ate DEC SRC (1-7/92).
Recently the subject of games has arisen (actually come back) from quite
different sources and perspectives at the same time. I am aware of works
or talks by Blass, Joyal (old and recent), Lafont-Streicher and De Paiva
(recent, "abstract"), Coquand, Lamarche, and Abramsky-Jagadeesan (more
recent).
I contribute here to this convergence. What follows is my own, but owes
much to thoughts of Franc,ois Lamarche. It came to me while searching to
integrate Cartwright-Felleisen's decision trees (POPL 92) with the
sequential algorithms of myself and Ge'rard Berry (1978).
The result which I want to announce here is the following:
I do have an interpretation of the following connectives:
- tensor product,
- linear implication,
- of course,
- with,
in terms of concete data structures and sequential algorithms, that has
the flavour or Blass's game semantics. The interest of this connection is
that sequential algorithms relate well to functions, programs (and full
abstraction, see Cartwright-Felleisen, and my LICS 92 paper). Hence it
may be hoped that in light of this connection one will be able to look at
game semantics from the other side of Curry-Howard.
Fortunately for the readers who do not know about sequential algorithms,
the light came from a more symmetric reformulation of (filiform) concrete
data structures, so that the story can be started from here.
The new symmetry calls for a more ambitious modelling of the other
connectives of linear logic, but here the situation is not yet completely
clear, neither is the extent to which the constructions I get are similar
to those of Blass, Abramsky-Jagadeesan, and Lamarche. The exact matching
with sequential algorithms may be lost in the process (this after all may
be desirable, since sequential algorithms are only demand-driven, which is
far too limitative).
Thanks to Martin Abadi, Samson Abramsky, Corky Cartright, Thierry Coquand,
Francois Lamarche for comments on drafts of this message.
The rest of this message is technical and decomposes as follows:
- sequential data structures are described: these are, in a more appealing
presentation, the filiform cds's of my monograph Categorical Combinators,
Sequential Algorithms and Functional Programming, Pitman, and soon
Birkhauser for a revised edition;
- linear implication (o->) is described, and a category Linalgo of
sequential data structures and linear sequential algorithms is presented;
- tensor product (tensor) is described;
- product (x) is described;
- of course (!) is described.
All this has the required structure:
THEOREM: sds's and (linear) sequential algorithms provide a semantics of
Intuitionistic Linear Logic, with connectives tensor, o->, ! and x. In
categorical terms, this means:
1) tensor and o-> make Linalgo monoidal closed (actually cartesian closed,
we are like Blass in an affine situation),
2) ! is a comonad s.t. (!A) tensor (!B) is isomorphic to !(A x B).
And for those caring about history, the category of sequential data
structures and sequential algorithms, i.e. the Cokleisli category of
Linalgo, is equivalent to the category of filiform concrete data
structures and sequential algorithms.
SEQUENTIAL DATA STRUCTURES
A sequential data structure (sds) (C,V,P) consists of the following
components:
C = set of cells,
V = set of values,
P is a subset of (C U V)*. Elements of P must be alternating sequences,
starting with a cell. These elements are called paths. Think of
P as a tree.
P inherits the prefix ordering on words. In particular (p meet q) is the
maximum common prefix of p, q.
The paths ending with a cell are called QUERIES. The set of queries is
written Q(C,V,P) (Q for short). The paths ending with a value are called
ANSWERS. The set of answers is written A(C,V,P) (A for short).
A state of a sds (C,V,P) is a subset x of P which satisfies:
1) x is closed under prefix ordering,
2) If p, q are in x and p, q are incomparable,
then (p meet q) is an answer.
An answer state is a state x s.t. "every query in x is answered in x",
i.e. (p in x, p query) => (p,v in x for some p,v in P). Think of a state
as a subtree of P where branching is allowed only at value nodes.
The following (rough) table of correspondences should help the readers
familiar with game semantics:
game semantics sds framework
game sds
strategy state
opponent cell
player value
LINEAR EXPONENTIALS
The linear exponential is defined as follows:
The sds (C'',V'',P'') = (C,V,P) o-> (C',V',P') of linear sequential
algorithms is defined by:
C'' = (request C') U (is V) ((is V)={is v| v in V}, etc..),
V'' = (valof C) U (output V'),
P'' consists of the paths p which
start with a "request c'"
and are s.t.
the projections of p onto (C,V,P), (C',V',P') are both paths,
a "valof c" can only be followed by a "is v",
a "output v'" can only be followed by a "request c'".
The projection, say projin on (C,V,P), is defined formally as follows:
projin(empty) = empty
projin(request c', p) = projin(p)
projin(output v', p) = projin(p)
projin(valof c, p) = c, proj(p)
projin(is v, p) = v, proj(p)
LINEAR SEQUENTIAL ALGORITHMS
We define the category Linalgo:
- the objects are the sequential data structures,
- the arrows in Linalgo((C,V,P),(C',V',P')) are the answer states
of the linear exponential (C,V,P) o-> (C',V',P').
- the composition (||) is defined operationally, pathwise,
recursively, as follows. Let q be a path of (C,V,P)->(C',V',P') and p be a
path of (C',V',P') o->(C'',V'',P''):
empty || q = empty
(request c'', p) || q = request c'', (p || q)
(output v'', p) || q = output v'', (p || q)
(valof c', p) || (request c',q) = p || q (communication!)
(valof c', p) || (request d',q) = empty (c', d' different)
(is v', p) || (valof c, q) = valof c, ((is v',p) || q)
(is v', p) || (is v, q) = is v, ((is v', p) || q)
(is v', p) || (output v', q) = p || q
(is v', p) || (output w', q) = empty (v', w' different)
Remark: Other presentations of linear algorithms, as pairs (function,
computation strategy) are available from the older frameowrk of cds's and
sequential algorithms. In a setting with explicit errors in the semantics,
it turns out that (observable) linear algorithms are exactly the
sequential and error sensitive functions (see Cartwright-Felleisens' POPL
92 paper, and my LICS 92 paper).
Remark: The above operational description is in the spirit of Abramsky's
"parallel composition with hiding" paradigm. This goes back to CDS0, the
language that Berry and myself had developped from concrete data
structures and sequential algorithms. But in CDS0 the idea was somewhat
buried under technicalities.
TENSOR PRODUCT
(C,V,P) tensor (C',V',P') = (C'',V'',P'') where
C'' = C.1 U C'.2,
V'' = V.1 U V'.2,
P'' consists of the paths p which are s.t.
the projections of p onto (C,V,P), (C',V',P') are both paths,
a "c.1" can only be followed by a "v.1",
a "c'.2" can only be followed by a "v'.2".
PRODUCT
(C'',V'',P'') = (C,V,P) x (C',V',P') is defined by
C'' = C.1 U C'.2,
V'' = V.1 U V'.2,
P'' = P.1 U P'.2 .
OF COURSE
Some motivation to begin with. The "left (or right) strict and" algorithm
has two sequentiality indexes: it is not linear. Let me make this clear:
Let N be the sds {{?},omega,P) where P is the tree
?
tt ff
Then "left strict and" is the tree
request ? valof ?.1
is ff valof ?.2
is ff output ff
is tt output ff
is tt valof ?.2
is ff output ff
is tt output tt
which contains the "path"
request ?
valof ?.1
is ff
valof ?.2
is ff
output ff
whose projection
?.1
ff
?.2
ff
is not a path of the product of N and N.
An extended notion of path is thus needed to describe non linear
algorithms.
Let (C,V,P) be an sds, and let x be a state of (C,V,P). An alternating
sequence p0,...,pn in (Q U A)*, starting with a length one query p0=c is
said to be a state sequence relative to x (or x-sequence) when
x = {p0,...,pn},
p(2m+1)=p(2m),v for some v (2m<n),
p(2m)=p(2q+1),c for some q<m and c, (m>o and 2m<=n).
Here is the of course operation:
!(C,V,P)=(Q,A,{state sequences of (C,V,P)}).
LINEAR NEGATION (not)
It is tempting to write not(C,V,P)=(V,C,P), but things seem more
complicated than that...
END