Document Open Access Logo

Positional Injectivity for Innocent Strategies

Authors Lison Blondeau-Patissier, Pierre Clairambault

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.17.pdf
  • Filesize: 0.89 MB
  • 22 pages

Document Identifiers

Author Details

Lison Blondeau-Patissier
  • Université Lyon, EnsL, UCBL, CNRS, LIP, F-69342, Lyon Cedex 07, France
Pierre Clairambault
  • Université Lyon, EnsL, UCBL, CNRS, LIP, F-69342, Lyon Cedex 07, France

Funding

Work supported by the ANR project DyVerSe (ANR-19-CE48-0010-01); and by the Labex MiLyon (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007), operated by the French National Research Agency (ANR).

Acknowledgements

We thank the reviewers, whose comments greatly helped improve the paper.

Cite As Get BibTex

Lison Blondeau-Patissier and Pierre Clairambault. Positional Injectivity for Innocent Strategies. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSCD.2021.17

Abstract

In asynchronous games, Melliès proved that innocent strategies are positional: their behaviour only depends on the position, not the temporal order used to reach it. This insightful result shaped our understanding of the link between dynamic (i.e. game) and static (i.e. relational) semantics.
In this paper, we investigate the positionality of innocent strategies in the traditional setting of Hyland-Ong-Nickau-Coquand pointer games. We show that though innocent strategies are not positional, total finite innocent strategies still enjoy a key consequence of positionality, namely positional injectivity: they are entirely determined by their positions. Unfortunately, this does not hold in general: we show a counter-example if finiteness and totality are lifted. For finite partial strategies we leave the problem open; we show however the partial result that two strategies with the same positions must have the same P-views of maximal length.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
Keywords
  • Game Semantics
  • Innocence
  • Relational Semantics
  • Positionality

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409-470, 2000. URL: https://doi.org/10.1006/inco.2000.2930.
  2. Samson Abramsky and Paul-André Melliès. Concurrent games and full completeness. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 431-442. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782638.
  3. Pierre Boudes. Thick subtrees, games and experiments. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, volume 5608 of Lecture Notes in Computer Science, pages 65-79. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02273-9_7.
  4. Simon Castellan, Pierre Clairambault, Hugo Paquet, and Glynn Winskel. The concurrent game semantics of probabilistic PCF. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 215-224. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209187.
  5. Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. Logical Methods in Computer Science, 13(3), 2017. URL: https://doi.org/10.23638/LMCS-13(3:35)2017.
  6. Simon Castellan, Pierre Clairambault, and Glynn Winskel. Symmetry in concurrent games. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 28:1-28:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603141.
  7. Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract games model of PCF. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 232-243. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.31.
  8. Pierre Clairambault. A tale of additives and concurrency in game semantics. To appear, 2021. Google Scholar
  9. Pierre Clairambault and Marc de Visme. Full abstraction for the quantum lambda-calculus. Proc. ACM Program. Lang., 4(POPL):63:1-63:28, 2020. URL: https://doi.org/10.1145/3371131.
  10. Daniel de Carvalho. The relational model is injective for multiplicative exponential linear logic. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, pages 41:1-41:19, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.41.
  11. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci., 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  12. Thomas Ehrhard. The Scott model of linear logic is the extensional collapse of its relational model. Theor. Comput. Sci., 424:20-45, 2012. URL: https://doi.org/10.1016/j.tcs.2011.11.027.
  13. Russell Harmer, Martin Hyland, and Paul-André Melliès. Categorical combinatorics for innocent strategies. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 379-388. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.14.
  14. Tom Hirschowitz and Damien Pous. Innocent strategies as presheaves and interactive equivalences for CCS. Sci. Ann. Comput. Sci., 22(1):147-199, 2012. URL: https://doi.org/10.7561/SACS.2012.1.147.
  15. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285-408, 2000. URL: https://doi.org/10.1006/inco.2000.2917.
  16. Paul-André Melliès. Asynchronous games 2: The true concurrency of innocence. Theor. Comput. Sci., 358(2-3):200-228, 2006. URL: https://doi.org/10.1016/j.tcs.2006.01.016.
  17. Takeshi Tsukada and C.-H. Luke Ong. Innocent strategies are sheaves over plays - deterministic, non-deterministic and probabilistic innocence. CoRR, abs/1409.2764, 2014. URL: http://arxiv.org/abs/1409.2764.
  18. Takeshi Tsukada and C.-H. Luke Ong. Nondeterminism in game semantics via sheaves. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 220-231. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.30.
  19. Takeshi Tsukada and C.-H. Luke Ong. Plays as resource terms via non-idempotent intersection types. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 237-246. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934553.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact