A graph model for imperative computation

Research output: Contribution to journalArticle

  • 8 Citations

Abstract

Scott's graph model is a lambda-algebra based on the observation that continuous endofunctions on the lattice of sets of natural numbers can be represented via their graphs. A graph is a relation mapping finite sets of input values to output values. We consider a similar model based on relations whose input values are finite sequences rather than sets. This alteration means that we are taking into account the order in which observations are made. This new notion of graph gives rise to a model of affine lambda-calculus that admits an interpretation of imperative constructs including variable assignment, dereferencing and allocation. Extending this untyped model, we construct a category that provides a model of typed higher-order imperative computation with an affine type system. An appropriate language of this kind is Reynolds's Syntactic Control of Interference. Our model turns out to be fully abstract for this language. At a concrete level, it is the same as Reddy's object spaces model, which was the first "state-free" model of a higher-order imperative programming language and an important precursor of games models. The graph model can therefore be seen as a universal domain for Reddy's model.
LanguageEnglish
Article numberPaper 2
Number of pages35
JournalLogical Methods in Computer Science
Volume6
Issue number1
DOIs
StatusPublished - 12 Jan 2010

Fingerprint

Graph Model
Model
Graph in graph theory
Higher Order
Affine Systems
Lambda Calculus
Type Systems
Natural number
Precursor
Programming Languages
Finite Set
Assignment
Syntactics
Interference
Game
Model-based
Computer programming languages
Algebra
Output
Concretes

Cite this

A graph model for imperative computation. / McCusker, Guy A.

In: Logical Methods in Computer Science, Vol. 6, No. 1, Paper 2, 12.01.2010.

Research output: Contribution to journalArticle

@article{0d5c83d51eb343de874072fa9eb76002,
title = "A graph model for imperative computation",
abstract = "Scott's graph model is a lambda-algebra based on the observation that continuous endofunctions on the lattice of sets of natural numbers can be represented via their graphs. A graph is a relation mapping finite sets of input values to output values. We consider a similar model based on relations whose input values are finite sequences rather than sets. This alteration means that we are taking into account the order in which observations are made. This new notion of graph gives rise to a model of affine lambda-calculus that admits an interpretation of imperative constructs including variable assignment, dereferencing and allocation. Extending this untyped model, we construct a category that provides a model of typed higher-order imperative computation with an affine type system. An appropriate language of this kind is Reynolds's Syntactic Control of Interference. Our model turns out to be fully abstract for this language. At a concrete level, it is the same as Reddy's object spaces model, which was the first {"}state-free{"} model of a higher-order imperative programming language and an important precursor of games models. The graph model can therefore be seen as a universal domain for Reddy's model.",
author = "McCusker, {Guy A}",
year = "2010",
month = "1",
day = "12",
doi = "10.2168/LMCS-6(1:2)2010",
language = "English",
volume = "6",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "1",

}

TY - JOUR

T1 - A graph model for imperative computation

AU - McCusker,Guy A

PY - 2010/1/12

Y1 - 2010/1/12

N2 - Scott's graph model is a lambda-algebra based on the observation that continuous endofunctions on the lattice of sets of natural numbers can be represented via their graphs. A graph is a relation mapping finite sets of input values to output values. We consider a similar model based on relations whose input values are finite sequences rather than sets. This alteration means that we are taking into account the order in which observations are made. This new notion of graph gives rise to a model of affine lambda-calculus that admits an interpretation of imperative constructs including variable assignment, dereferencing and allocation. Extending this untyped model, we construct a category that provides a model of typed higher-order imperative computation with an affine type system. An appropriate language of this kind is Reynolds's Syntactic Control of Interference. Our model turns out to be fully abstract for this language. At a concrete level, it is the same as Reddy's object spaces model, which was the first "state-free" model of a higher-order imperative programming language and an important precursor of games models. The graph model can therefore be seen as a universal domain for Reddy's model.

AB - Scott's graph model is a lambda-algebra based on the observation that continuous endofunctions on the lattice of sets of natural numbers can be represented via their graphs. A graph is a relation mapping finite sets of input values to output values. We consider a similar model based on relations whose input values are finite sequences rather than sets. This alteration means that we are taking into account the order in which observations are made. This new notion of graph gives rise to a model of affine lambda-calculus that admits an interpretation of imperative constructs including variable assignment, dereferencing and allocation. Extending this untyped model, we construct a category that provides a model of typed higher-order imperative computation with an affine type system. An appropriate language of this kind is Reynolds's Syntactic Control of Interference. Our model turns out to be fully abstract for this language. At a concrete level, it is the same as Reddy's object spaces model, which was the first "state-free" model of a higher-order imperative programming language and an important precursor of games models. The graph model can therefore be seen as a universal domain for Reddy's model.

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

UR - http://dx.doi.org/10.2168/LMCS-6(1:2)2010

UR - http://arxiv.org/pdf/0910.5399.pdf

U2 - 10.2168/LMCS-6(1:2)2010

DO - 10.2168/LMCS-6(1:2)2010

M3 - Article

VL - 6

JO - Logical Methods in Computer Science

T2 - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 1

M1 - Paper 2

ER -