A Fully Abstract Game Semantics for Countable Nondeterminism

Authors W. John Gowers , James D. Laird



PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.24.pdf
  • Filesize: 0.54 MB
  • 18 pages

Document Identifiers

Author Details

W. John Gowers
  • Computer Science Department, University of Bath, Claverton Down Road, Bath. BA2 7QY, United Kingdom
James D. Laird
  • Department of Computer Science, University of Bath, Claverton Down Road, Bath. BA2 7QY, United Kingdom

Cite AsGet BibTex

W. John Gowers and James D. Laird. A Fully Abstract Game Semantics for Countable Nondeterminism. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CSL.2018.24

Abstract

The concept of fairness for a concurrent program means that the program must be able to exhibit an unbounded amount of nondeterminism without diverging. Game semantics models of nondeterminism show that this is hard to implement; for example, Harmer and McCusker's model only admits infinite nondeterminism if there is also the possibility of divergence. We solve a long standing problem by giving a fully abstract game semantics for a simple stateful language with a countably infinite nondeterminism primitive. We see that doing so requires us to keep track of infinitary information about strategies, as well as their finite behaviours. The unbounded nondeterminism gives rise to further problems, which can be formalized as a lack of continuity in the language. In order to prove adequacy for our model (which usually requires continuity), we develop a new technique in which we simulate the nondeterminism using a deterministic stateful construction, and then use combinatorial techniques to transfer the result to the nondeterministic language. Lastly, we prove full abstraction for the model; because of the lack of continuity, we cannot deduce this from definability of compact elements in the usual way, and we have to use a stronger universality result instead. We discuss how our techniques yield proofs of adequacy for models of nondeterministic PCF, such as those given by Tsukada and Ong.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
Keywords
  • semantics
  • nondeterminism
  • games and logic

Metrics

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

References

  1. Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. The Journal of Symbolic Logic, 59(2):543-574, 1994. URL: http://arxiv.org/abs/1311.6057.
  2. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation, 163(2):409-470, 2000. URL: http://dx.doi.org/10.1006/inco.2000.2930.
  3. Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions: Extended abstract. Electronic Notes in Theoretical Computer Science, 3:2-14, 1996. Linear Logic 96 Tokyo Meeting. URL: http://dx.doi.org/10.1016/S1571-0661(05)80398-6.
  4. K. R. Apt and G. D. Plotkin. A cook’s tour of countable nondeterminism. In Shimon Even and Oded Kariv, editors, Automata, Languages and Programming, pages 479-494, Berlin, Heidelberg, 1981. Springer Berlin Heidelberg. Google Scholar
  5. Simon Castellan, Pierre Clairambault, and Glynn Winskel. Concurrent Hyland-Ong games. working paper or preprint, 2016. URL: https://hal.archives-ouvertes.fr/hal-01068769.
  6. Pierre-Louis Curien. Definability and full abstraction. Electronic Notes in Theoretical Computer Science, 172:301-310, 2007. Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin. URL: http://dx.doi.org/10.1016/j.entcs.2007.02.011.
  7. Edsger Wybe Dijkstra. A Discipline of Programming. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1st edition, 1997. Google Scholar
  8. R. Harmer and G. McCusker. A fully abstract game semantics for finite nondeterminism. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pages 422-430, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782637.
  9. Russell S. Harmer. Games and full abstraction for nondeterministic languages. Technical report, University of London/Imperial College, 1999. Google Scholar
  10. J.M.E. Hyland and C.-H.L. Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000. URL: http://dx.doi.org/10.1006/inco.2000.2917.
  11. J. Laird. Sequential algorithms for unbounded nondeterminism. Electronic Notes in Theoretical Computer Science, 319:271-287, 2015. URL: http://dx.doi.org/10.1016/j.entcs.2015.12.017.
  12. James Laird. Higher-order programs as coroutines. to appear, 2016. Google Scholar
  13. Paul Blain Levy. Infinite trace equivalence. Annals of Pure and Applied Logic, 151(2):170-198, 2008. URL: http://dx.doi.org/10.1016/j.apal.2007.10.007.
  14. Paul Blain Levy. Morphisms between plays. Lecture slides, GaLoP, 2014. Google Scholar
  15. A. S. Murawski. Reachability games and game semantics: Comparing nondeterministic programs. In 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008)(LICS), volume 00, pages 353-363, 06 2008. URL: http://dx.doi.org/10.1109/LICS.2008.24.
  16. Andrzej S. Murawski and Nikos Tzevelekos. Block structure vs scope extrusion: between innocence and omniscience. Logical Methods in Computer Science, 12(3), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(3:3)2016.
  17. David Park. On the semantics of fair parallelism. In Abstract Software Specifications, pages 504-526. Springer, 1980. Google Scholar
  18. David Park. Concurrency and automata on infinite sequences. In Theoretical computer science, pages 167-183. Springer, 1981. Google Scholar
  19. Corin Pitcher. Functional programming and erratic non-determinism. PhD thesis, University of Oxford/Trinity College, 2001. Google Scholar
  20. A. W. Roscoe. Unbounded non-determinism in CSP. Journal of Logic and Computation, 3(2):131, 1993. URL: http://dx.doi.org/10.1093/logcom/3.2.131.
  21. Takeshi Tsukada and C. H. Luke Ong. Nondeterminism in game semantics via sheaves. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), LICS '15, pages 220-231, Washington, DC, USA, 2015. IEEE Computer Society. URL: http://dx.doi.org/10.1109/LICS.2015.30.
  22. Glynn Winskel. Strategies as profunctors. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures, pages 418-433, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
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