Constructing differential categories and deconstructing categories of games

James Laird, Giulio Manzonetto, Guy McCusker

Research output: Contribution to journalArticle

  • 10 Citations

Abstract

Differential categories were introduced by Blute, Cockett and Seely to axiomatize categorically Ehrhard and Regnierʼs syntactic differential operator. We present an abstract construction that takes a symmetric monoidal category and yields a differential category, and show how this construction may be applied to categories of games. In one instance, we recover the category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model, and shows how the differential combinator may be encoded in the imperative language. A second instance corresponds to a new cartesian differential category of games. We give a model of a simply-typed resource calculus, Resource PCF, in this category and show that it possesses the finite definability property. Comparison with a semantics based on Bucciarelli, Ehrhard and Manzonettoʼs relational model reveals that the latter also possesses this property and is fully abstract.
LanguageEnglish
Pages247-264
Number of pages18
JournalInformation and Computation
Volume222
Early online date26 Oct 2012
DOIs
StatusPublished - Jan 2013

Fingerprint

Game
Syntactics
Monoidal Category
Resources
Relational Model
Definability
Semantics
Cartesian
Differential operator
Calculus
Model
Language

Keywords

  • differential categories
  • game semantics
  • full abstraction

Cite this

Constructing differential categories and deconstructing categories of games. / Laird, James; Manzonetto, Giulio; McCusker, Guy.

In: Information and Computation, Vol. 222, 01.2013, p. 247-264.

Research output: Contribution to journalArticle

@article{497b74e060314298ae12711e09885522,
title = "Constructing differential categories and deconstructing categories of games",
abstract = "Differential categories were introduced by Blute, Cockett and Seely to axiomatize categorically Ehrhard and Regnierʼs syntactic differential operator. We present an abstract construction that takes a symmetric monoidal category and yields a differential category, and show how this construction may be applied to categories of games. In one instance, we recover the category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model, and shows how the differential combinator may be encoded in the imperative language. A second instance corresponds to a new cartesian differential category of games. We give a model of a simply-typed resource calculus, Resource PCF, in this category and show that it possesses the finite definability property. Comparison with a semantics based on Bucciarelli, Ehrhard and Manzonettoʼs relational model reveals that the latter also possesses this property and is fully abstract.",
keywords = "differential categories, game semantics, full abstraction",
author = "James Laird and Giulio Manzonetto and Guy McCusker",
year = "2013",
month = "1",
doi = "10.1016/j.ic.2012.10.015",
language = "English",
volume = "222",
pages = "247--264",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier",

}

TY - JOUR

T1 - Constructing differential categories and deconstructing categories of games

AU - Laird,James

AU - Manzonetto,Giulio

AU - McCusker,Guy

PY - 2013/1

Y1 - 2013/1

N2 - Differential categories were introduced by Blute, Cockett and Seely to axiomatize categorically Ehrhard and Regnierʼs syntactic differential operator. We present an abstract construction that takes a symmetric monoidal category and yields a differential category, and show how this construction may be applied to categories of games. In one instance, we recover the category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model, and shows how the differential combinator may be encoded in the imperative language. A second instance corresponds to a new cartesian differential category of games. We give a model of a simply-typed resource calculus, Resource PCF, in this category and show that it possesses the finite definability property. Comparison with a semantics based on Bucciarelli, Ehrhard and Manzonettoʼs relational model reveals that the latter also possesses this property and is fully abstract.

AB - Differential categories were introduced by Blute, Cockett and Seely to axiomatize categorically Ehrhard and Regnierʼs syntactic differential operator. We present an abstract construction that takes a symmetric monoidal category and yields a differential category, and show how this construction may be applied to categories of games. In one instance, we recover the category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model, and shows how the differential combinator may be encoded in the imperative language. A second instance corresponds to a new cartesian differential category of games. We give a model of a simply-typed resource calculus, Resource PCF, in this category and show that it possesses the finite definability property. Comparison with a semantics based on Bucciarelli, Ehrhard and Manzonettoʼs relational model reveals that the latter also possesses this property and is fully abstract.

KW - differential categories

KW - game semantics

KW - full abstraction

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

UR - http://dx.doi.org/10.1016/j.ic.2012.10.015

U2 - 10.1016/j.ic.2012.10.015

DO - 10.1016/j.ic.2012.10.015

M3 - Article

VL - 222

SP - 247

EP - 264

JO - Information and Computation

T2 - Information and Computation

JF - Information and Computation

SN - 0890-5401

ER -