A graphical foundation for interleaving in game semantics

Guy McCusker, John Power, Cai Wingfield

Research output: Contribution to journalArticle

Abstract

In 2007, Harmer, Hyland and Melliès gave a formal mathematical foundation for game semantics using a notion they called a {multimap}-schedule, and the similar notion of ⊗-schedule, both structures describing interleavings of plays in games. Their definition was combinatorial in nature, but researchers often draw pictures when describing schedules in practice. Moreover, several proofs of key properties, such as that the composition of {multimap}-schedules is associative, involve cumbersome combinatorial detail, whereas in terms of pictures the proof is straightforward, reflecting the geometry of the plane. Here, we give a geometric formulation of {multimap}-schedules and ⊗-schedules, prove that they are isomorphic to Harmer et al.'s definitions, and illustrate their value by giving such geometric proofs. Harmer et al.'s notions may be combined to describe plays in multi-component games, and researchers have similarly developed intuitive graphical representations of plays in these games. We give a characterisation of these diagrams and explicitly describe how they relate to the underlying schedules, finally using this relation to provide new, intuitive proofs of key categorical properties.

LanguageEnglish
Pages1131-1174
Number of pages44
JournalJournal of Pure and Applied Algebra
Volume219
Issue number4
Early online date9 Jun 2014
DOIs
StatusPublished - 1 Apr 2015

Fingerprint

Game Semantics
Interleaving
Schedule
Multimap (map)
Game
Intuitive
Geometric proof
Graphical Representation
Graphics
Categorical
Diagram
Isomorphic
Formulation

Keywords

  • game semantics, geometry, schedules, composites, associativity, symmetric monoidal closed category

Cite this

A graphical foundation for interleaving in game semantics. / McCusker, Guy; Power, John; Wingfield, Cai.

In: Journal of Pure and Applied Algebra, Vol. 219, No. 4, 01.04.2015, p. 1131-1174.

Research output: Contribution to journalArticle

@article{b65934f6a0ab4abdad534c4247b31ec9,
title = "A graphical foundation for interleaving in game semantics",
abstract = "In 2007, Harmer, Hyland and Melli{\`e}s gave a formal mathematical foundation for game semantics using a notion they called a {multimap}-schedule, and the similar notion of ⊗-schedule, both structures describing interleavings of plays in games. Their definition was combinatorial in nature, but researchers often draw pictures when describing schedules in practice. Moreover, several proofs of key properties, such as that the composition of {multimap}-schedules is associative, involve cumbersome combinatorial detail, whereas in terms of pictures the proof is straightforward, reflecting the geometry of the plane. Here, we give a geometric formulation of {multimap}-schedules and ⊗-schedules, prove that they are isomorphic to Harmer et al.'s definitions, and illustrate their value by giving such geometric proofs. Harmer et al.'s notions may be combined to describe plays in multi-component games, and researchers have similarly developed intuitive graphical representations of plays in these games. We give a characterisation of these diagrams and explicitly describe how they relate to the underlying schedules, finally using this relation to provide new, intuitive proofs of key categorical properties.",
keywords = "game semantics, geometry, schedules, composites, associativity, symmetric monoidal closed category",
author = "Guy McCusker and John Power and Cai Wingfield",
year = "2015",
month = "4",
day = "1",
doi = "10.1016/j.jpaa.2014.05.040",
language = "English",
volume = "219",
pages = "1131--1174",
journal = "Journal of Pure and Applied Algebra",
issn = "0022-4049",
publisher = "Elsevier",
number = "4",

}

TY - JOUR

T1 - A graphical foundation for interleaving in game semantics

AU - McCusker,Guy

AU - Power,John

AU - Wingfield,Cai

PY - 2015/4/1

Y1 - 2015/4/1

N2 - In 2007, Harmer, Hyland and Melliès gave a formal mathematical foundation for game semantics using a notion they called a {multimap}-schedule, and the similar notion of ⊗-schedule, both structures describing interleavings of plays in games. Their definition was combinatorial in nature, but researchers often draw pictures when describing schedules in practice. Moreover, several proofs of key properties, such as that the composition of {multimap}-schedules is associative, involve cumbersome combinatorial detail, whereas in terms of pictures the proof is straightforward, reflecting the geometry of the plane. Here, we give a geometric formulation of {multimap}-schedules and ⊗-schedules, prove that they are isomorphic to Harmer et al.'s definitions, and illustrate their value by giving such geometric proofs. Harmer et al.'s notions may be combined to describe plays in multi-component games, and researchers have similarly developed intuitive graphical representations of plays in these games. We give a characterisation of these diagrams and explicitly describe how they relate to the underlying schedules, finally using this relation to provide new, intuitive proofs of key categorical properties.

AB - In 2007, Harmer, Hyland and Melliès gave a formal mathematical foundation for game semantics using a notion they called a {multimap}-schedule, and the similar notion of ⊗-schedule, both structures describing interleavings of plays in games. Their definition was combinatorial in nature, but researchers often draw pictures when describing schedules in practice. Moreover, several proofs of key properties, such as that the composition of {multimap}-schedules is associative, involve cumbersome combinatorial detail, whereas in terms of pictures the proof is straightforward, reflecting the geometry of the plane. Here, we give a geometric formulation of {multimap}-schedules and ⊗-schedules, prove that they are isomorphic to Harmer et al.'s definitions, and illustrate their value by giving such geometric proofs. Harmer et al.'s notions may be combined to describe plays in multi-component games, and researchers have similarly developed intuitive graphical representations of plays in these games. We give a characterisation of these diagrams and explicitly describe how they relate to the underlying schedules, finally using this relation to provide new, intuitive proofs of key categorical properties.

KW - game semantics, geometry, schedules, composites, associativity, symmetric monoidal closed category

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

UR - http://dx.doi.org/10.1016/j.jpaa.2014.05.040

U2 - 10.1016/j.jpaa.2014.05.040

DO - 10.1016/j.jpaa.2014.05.040

M3 - Article

VL - 219

SP - 1131

EP - 1174

JO - Journal of Pure and Applied Algebra

T2 - Journal of Pure and Applied Algebra

JF - Journal of Pure and Applied Algebra

SN - 0022-4049

IS - 4

ER -