Inversion, Iteration, and the Art of Dual Wielding

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Abstract

The humble (Formula presented) (“dagger”) is used to denote two different operations in category theory: Taking the adjoint of a morphism (in dagger categories) and finding the least fixed point of a functional (in categories enriched in domains). While these two operations are usually considered separately from one another, the emergence of reversible notions of computation shows the need to consider how the two ought to interact. In the present paper, we wield both of these daggers at once and consider dagger categories enriched in domains. We develop a notion of a monotone dagger structure as a dagger structure that is well behaved with respect to the enrichment, and show that such a structure leads to pleasant inversion properties of the fixed points that arise as a result. Notably, such a structure guarantees the existence of fixed point adjoints, which we show are intimately related to the conjugates arising from a canonical involutive monoidal structure in the enrichment. Finally, we relate the results to applications in the design and semantics of reversible programming languages.

OriginalsprogEngelsk
TitelReversible Computation - 11th International Conference, RC 2019, Proceedings
RedaktørerMichael Kirkedal Thomsen, Mathias Soeken
Publikationsdato2019
Sider34-50
ISBN (Trykt)9783030214999
DOI
StatusUdgivet - 2019

Bibliografisk note

DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

Fingeraftryk

Dyk ned i forskningsemnerne om 'Inversion, Iteration, and the Art of Dual Wielding'. Sammen danner de et unikt fingeraftryk.

Citationsformater