Reversible Effects as Inverse Arrows

Chris Heunen; Robin Kaarsgaard; Martti Karvonen

doi:10.1016/j.entcs.2018.11.009

Reversible Effects as Inverse Arrows

Chris Heunen, Robin Kaarsgaard, Martti Karvonen

2 Citationer (Scopus)

46 Downloads (Pure)

Abstract

Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.

Originalsprog	Engelsk
Tidsskrift	Electronic Notes in Theoretical Computer Science
Vol/bind	341
Sider (fra-til)	179-199
ISSN	1571-0661
DOI	https://doi.org/10.1016/j.entcs.2018.11.009
Status	Udgivet - 1 dec. 2018
Begivenhed	34th Conference on the Mathematical Foundations of Programming Semantics - Dalhousie University, Halifax, Canada Varighed: 6 jun. 2018 → 9 jun. 2018 Konferencens nummer: 34 https://www.mathstat.dal.ca/mfps2018/

Konference

Konference	34th Conference on the Mathematical Foundations of Programming Semantics
Nummer	34
Lokation	Dalhousie University
Land/Område	Canada
By	Halifax
Periode	06/06/2018 → 09/06/2018
Internetadresse	https://www.mathstat.dal.ca/mfps2018/

Adgang til dokumentet

10.1016/j.entcs.2018.11.009Licens: CC BY

ArticleKaarsgaardForlagets udgivne version, 288 KBLicens: CC BY

Andre filer og links

Link to publication in Scopus

Citationsformater

@inproceedings{4df5fb2916c34c37b13bb772b1ae7ccf,

title = "Reversible Effects as Inverse Arrows",

abstract = "Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.",

keywords = "Arrow, Inverse Category, Involutive Monoid, Reversible Effect",

author = "Chris Heunen and Robin Kaarsgaard and Martti Karvonen",

year = "2018",

month = dec,

day = "1",

doi = "10.1016/j.entcs.2018.11.009",

language = "English",

volume = "341",

pages = "179--199",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

note = "34th Conference on the Mathematical Foundations of Programming Semantics, MFPS ; Conference date: 06-06-2018 Through 09-06-2018",

url = "https://www.mathstat.dal.ca/mfps2018/",

}

TY - GEN

T1 - Reversible Effects as Inverse Arrows

AU - Heunen, Chris

AU - Kaarsgaard, Robin

AU - Karvonen, Martti

N1 - Conference code: 34

PY - 2018/12/1

Y1 - 2018/12/1

N2 - Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.

AB - Reversible computing models settings in which all processes can be reversed. Applications include low-power computing, quantum computing, and robotics. It is unclear how to represent side-effects in this setting, because conventional methods need not respect reversibility. We model reversible effects by adapting Hughes' arrows to dagger arrows and inverse arrows. This captures several fundamental reversible effects, including serialization and mutable store computations. Whereas arrows are monoids in the category of profunctors, dagger arrows are involutive monoids in the category of profunctors, and inverse arrows satisfy certain additional properties. These semantics inform the design of functional reversible programs supporting side-effects.

KW - Arrow

KW - Inverse Category

KW - Involutive Monoid

KW - Reversible Effect

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

U2 - 10.1016/j.entcs.2018.11.009

DO - 10.1016/j.entcs.2018.11.009

M3 - Conference article

SN - 1571-0661

VL - 341

SP - 179

EP - 199

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - 34th Conference on the Mathematical Foundations of Programming Semantics

Y2 - 6 June 2018 through 9 June 2018

ER -

Reversible Effects as Inverse Arrows

Abstract

Konference

Adgang til dokumentet

Andre filer og links

Fingeraftryk

Citationsformater