Join inverse categories and reversible recursion

Robin Kaarsgaard; Holger Bock Axelsen; Robert Glück

doi:10.1016/j.jlamp.2016.08.003

Join inverse categories and reversible recursion

Robin Kaarsgaard, Holger Bock Axelsen, Robert Glück

12 Citationer (Scopus)

Abstract

Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modeling reversible functional programming, notably morphism schemes for reversible recursion, a †-trace, and algebraic ω-compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.

Originalsprog	Engelsk
Tidsskrift	Journal of Logical and Algebraic Methods in Programming
Vol/bind	87
Sider (fra-til)	33-50
Antal sider	18
ISSN	2352-2208
DOI	https://doi.org/10.1016/j.jlamp.2016.08.003
Status	Udgivet - 1 feb. 2017

Adgang til dokumentet

10.1016/j.jlamp.2016.08.003

Citationsformater

@article{888c23ba2822406aa98df935692396f5,

title = "Join inverse categories and reversible recursion",

abstract = "Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modeling reversible functional programming, notably morphism schemes for reversible recursion, a †-trace, and algebraic ω-compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.",

author = "Robin Kaarsgaard and Axelsen, {Holger Bock} and Robert Gl{\"u}ck",

year = "2017",

month = feb,

day = "1",

doi = "10.1016/j.jlamp.2016.08.003",

language = "English",

volume = "87",

pages = "33--50",

journal = "Journal of Logical and Algebraic Methods in Programming",

issn = "2352-2208",

publisher = "Elsevier",

}

TY - JOUR

T1 - Join inverse categories and reversible recursion

AU - Kaarsgaard, Robin

AU - Axelsen, Holger Bock

AU - Glück, Robert

PY - 2017/2/1

Y1 - 2017/2/1

N2 - Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modeling reversible functional programming, notably morphism schemes for reversible recursion, a †-trace, and algebraic ω-compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.

AB - Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modeling reversible functional programming, notably morphism schemes for reversible recursion, a †-trace, and algebraic ω-compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.

U2 - 10.1016/j.jlamp.2016.08.003

DO - 10.1016/j.jlamp.2016.08.003

M3 - Journal article

SN - 2352-2208

VL - 87

SP - 33

EP - 50

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

ER -

Join inverse categories and reversible recursion

Abstract

Adgang til dokumentet

Fingeraftryk

Citationsformater