[Prev][Next][Index][Thread]
Announce
GOI and strategies
Patrick Baillot
We announce the following result: by broadening AJM's definition of
plays and strategies on a LL formula we show that Girard's matrix of
partial functions associated to a proof-net R as defined in [2]
induces a valid history-free strategy on the game F=A1 par ... par An,
where A1,...,An are the conclusions of R. In the case of a proof-net
translated from a PCF- (PCF deprived of the fixed-point operator )
term we obtain the same interpretation as AJM in [1]. This enlightens
the link between AJM's model and the geometry of interaction.
The paper will be prochainly available on FTP at the location
ftp://ftp.logique.jussieu.fr/pub/scratch/baillot.
[1] S. Abramsky, R. Jagadeesan and P. Malacaria.
Full abstraction for PCF (extend abstract).
Lectures Notes in Computer Science, Sendai,
Japan. Springer-Verlag. (1994), no. 789, 1-15.
[2] J.-Y. Girard.
Geometry of interaction I: an interpretation of system ${F}$.
In Ferro & al., editor, Proceedings of A.S.L. Meetings.
North-Holland, 1988.