A fully abstract game semantics for countable nondeterminism

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationComputer Science Logic 2018, CSL 2018
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume119
ISBN (Print)9783959770880
DOIs
Publication statusPublished - 1 Aug 2018
Event27th Annual EACSL Conference Computer Science Logic, CSL 2018 - Birmingham, UK United Kingdom
Duration: 4 Sep 20187 Sep 2018

Conference

Conference27th Annual EACSL Conference Computer Science Logic, CSL 2018
CountryUK United Kingdom
CityBirmingham
Period4/09/187/09/18

Fingerprint

Semantics

Keywords

  • Games and logic
  • Nondeterminism
  • Semantics

ASJC Scopus subject areas

  • Software

Cite this

Gowers, W. J., & Laird, J. D. (2018). A fully abstract game semantics for countable nondeterminism. In Computer Science Logic 2018, CSL 2018 (Vol. 119). [24] Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2018.24

A fully abstract game semantics for countable nondeterminism. / Gowers, W. John; Laird, James D.

Computer Science Logic 2018, CSL 2018. Vol. 119 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2018. 24.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Gowers, WJ & Laird, JD 2018, A fully abstract game semantics for countable nondeterminism. in Computer Science Logic 2018, CSL 2018. vol. 119, 24, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 27th Annual EACSL Conference Computer Science Logic, CSL 2018, Birmingham, UK United Kingdom, 4/09/18. https://doi.org/10.4230/LIPIcs.CSL.2018.24
Gowers WJ, Laird JD. A fully abstract game semantics for countable nondeterminism. In Computer Science Logic 2018, CSL 2018. Vol. 119. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2018. 24 https://doi.org/10.4230/LIPIcs.CSL.2018.24
Gowers, W. John ; Laird, James D. / A fully abstract game semantics for countable nondeterminism. Computer Science Logic 2018, CSL 2018. Vol. 119 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2018.
@inproceedings{8c40970690154cf4be237560bb215d5f,
title = "A fully abstract game semantics for countable nondeterminism",
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.",
keywords = "Games and logic, Nondeterminism, Semantics",
author = "Gowers, {W. John} and Laird, {James D.}",
year = "2018",
month = "8",
day = "1",
doi = "10.4230/LIPIcs.CSL.2018.24",
language = "English",
isbn = "9783959770880",
volume = "119",
booktitle = "Computer Science Logic 2018, CSL 2018",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
address = "Germany",

}

TY - GEN

T1 - A fully abstract game semantics for countable nondeterminism

AU - Gowers, W. John

AU - Laird, James D.

PY - 2018/8/1

Y1 - 2018/8/1

N2 - 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.

AB - 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.

KW - Games and logic

KW - Nondeterminism

KW - Semantics

UR - http://www.scopus.com/inward/record.url?scp=85053073148&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2018.24

DO - 10.4230/LIPIcs.CSL.2018.24

M3 - Conference contribution

SN - 9783959770880

VL - 119

BT - Computer Science Logic 2018, CSL 2018

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -