Join inverse categories as models of reversible recursion

TY - GEN

T1 - Join inverse categories as models of reversible recursion

AU - Axelsen, Holger Bock

AU - Kaarsgaard, Robin

N1 - Conference code: 19

PY - 2016

Y1 - 2016

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 modelling 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 modelling 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.1007/978-3-662-49630-5_5

DO - 10.1007/978-3-662-49630-5_5

M3 - Article in proceedings

SN - 978-3-662-49629-9

T3 - Lecture notes in computer science

SP - 73

EP - 90

BT - Foundations of Software Science and Computation Structures

A2 - Jacobs, Bart

A2 - Löding, Christof

PB - Springer

T2 - Foundations of Software Science and Computation Structures

Y2 - 2 April 2016 through 8 April 2016

ER -