Modelling local variables: possible worlds and object spaces

Research output: Contribution to journalArticle

Abstract

Local variables in imperative languages have been given denotational semantics in at least two fundamentally different ways. One is by use of functor categories, focusing on the idea of possible worlds. The other might be termed event-based, exemplified by Reddy’s object spaces and models based on game semantics. O’Hearn and Reddy have related the two approaches by giving functor category models whose worlds are ob ject spaces, then showing that their model is fully abstract for Idealised Algol programs up to order two. But the category of ob ject spaces is not small, and so in order to construct a functor category that is locally small, and hence Cartesian closed, they need to work with a restricted collection of ob ject spaces. This weakens the connection between the object spaces model and the functor-category model: the Yoneda embedding no longer provides a full embedding of the original category of object spaces into the functor-category. Moreoever the choice of the restricted collection of object spaces is ad hoc. In this paper, we refine the approach by proving that the finite objects form a small dense subcategory of a simplified object-spaces model. The functor category over these finite objects is therefore locally small and Cartesian closed, and contains the object-spaces category as a full subcategory. All this work is necessarily enriched in Cpo. We further refine their full abstraction result by showing that full abstraction fails at order three.
LanguageEnglish
Pages389-402
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
Volume265
DOIs
StatusPublished - 6 Sep 2010

Fingerprint

Functor
Modeling
Model Category
Semantics
Cartesian
Game Semantics
Object
Denotational Semantics
Closed
Model
Model-based
Abstraction

Cite this

Modelling local variables: possible worlds and object spaces. / McCusker, Guy A; Power, John.

In: Electronic Notes in Theoretical Computer Science, Vol. 265, 06.09.2010, p. 389-402.

Research output: Contribution to journalArticle

@article{0ec154bc34a743eb9b0817e847eec3ec,
title = "Modelling local variables: possible worlds and object spaces",
abstract = "Local variables in imperative languages have been given denotational semantics in at least two fundamentally different ways. One is by use of functor categories, focusing on the idea of possible worlds. The other might be termed event-based, exemplified by Reddy’s object spaces and models based on game semantics. O’Hearn and Reddy have related the two approaches by giving functor category models whose worlds are ob ject spaces, then showing that their model is fully abstract for Idealised Algol programs up to order two. But the category of ob ject spaces is not small, and so in order to construct a functor category that is locally small, and hence Cartesian closed, they need to work with a restricted collection of ob ject spaces. This weakens the connection between the object spaces model and the functor-category model: the Yoneda embedding no longer provides a full embedding of the original category of object spaces into the functor-category. Moreoever the choice of the restricted collection of object spaces is ad hoc. In this paper, we refine the approach by proving that the finite objects form a small dense subcategory of a simplified object-spaces model. The functor category over these finite objects is therefore locally small and Cartesian closed, and contains the object-spaces category as a full subcategory. All this work is necessarily enriched in Cpo. We further refine their full abstraction result by showing that full abstraction fails at order three.",
author = "McCusker, {Guy A} and John Power",
note = "Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)",
year = "2010",
month = "9",
day = "6",
doi = "10.1016/j.entcs.2010.08.023",
language = "English",
volume = "265",
pages = "389--402",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - Modelling local variables: possible worlds and object spaces

AU - McCusker,Guy A

AU - Power,John

N1 - Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010)

PY - 2010/9/6

Y1 - 2010/9/6

N2 - Local variables in imperative languages have been given denotational semantics in at least two fundamentally different ways. One is by use of functor categories, focusing on the idea of possible worlds. The other might be termed event-based, exemplified by Reddy’s object spaces and models based on game semantics. O’Hearn and Reddy have related the two approaches by giving functor category models whose worlds are ob ject spaces, then showing that their model is fully abstract for Idealised Algol programs up to order two. But the category of ob ject spaces is not small, and so in order to construct a functor category that is locally small, and hence Cartesian closed, they need to work with a restricted collection of ob ject spaces. This weakens the connection between the object spaces model and the functor-category model: the Yoneda embedding no longer provides a full embedding of the original category of object spaces into the functor-category. Moreoever the choice of the restricted collection of object spaces is ad hoc. In this paper, we refine the approach by proving that the finite objects form a small dense subcategory of a simplified object-spaces model. The functor category over these finite objects is therefore locally small and Cartesian closed, and contains the object-spaces category as a full subcategory. All this work is necessarily enriched in Cpo. We further refine their full abstraction result by showing that full abstraction fails at order three.

AB - Local variables in imperative languages have been given denotational semantics in at least two fundamentally different ways. One is by use of functor categories, focusing on the idea of possible worlds. The other might be termed event-based, exemplified by Reddy’s object spaces and models based on game semantics. O’Hearn and Reddy have related the two approaches by giving functor category models whose worlds are ob ject spaces, then showing that their model is fully abstract for Idealised Algol programs up to order two. But the category of ob ject spaces is not small, and so in order to construct a functor category that is locally small, and hence Cartesian closed, they need to work with a restricted collection of ob ject spaces. This weakens the connection between the object spaces model and the functor-category model: the Yoneda embedding no longer provides a full embedding of the original category of object spaces into the functor-category. Moreoever the choice of the restricted collection of object spaces is ad hoc. In this paper, we refine the approach by proving that the finite objects form a small dense subcategory of a simplified object-spaces model. The functor category over these finite objects is therefore locally small and Cartesian closed, and contains the object-spaces category as a full subcategory. All this work is necessarily enriched in Cpo. We further refine their full abstraction result by showing that full abstraction fails at order three.

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

UR - http://dx.doi.org/10.1016/j.entcs.2010.08.023

U2 - 10.1016/j.entcs.2010.08.023

DO - 10.1016/j.entcs.2010.08.023

M3 - Article

VL - 265

SP - 389

EP - 402

JO - Electronic Notes in Theoretical Computer Science

T2 - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -