Inversion, Iteration, and the Art of Dual Wielding

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

  • Robin Kaarsgaard

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.

Original languageEnglish
Title of host publicationReversible Computation - 11th International Conference, RC 2019, Proceedings
EditorsMathias Soeken, Michael Kirkedal Thomsen
Number of pages17
PublisherSpringer
Publication date2019
Pages34-50
ISBN (Print)9783030214999
DOIs
Publication statusPublished - 2019
Event11th International Conference on Reversible Computation, RC 2019 - Lausanne, Switzerland
Duration: 24 Jun 201925 Jun 2019

Conference

Conference11th International Conference on Reversible Computation, RC 2019
LandSwitzerland
ByLausanne
Periode24/06/201925/06/2019
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11497 LNCS
ISSN0302-9743

    Research areas

  • Dagger categories, Domain theory, Enriched categories, Iteration categories, Reversible computing

Links

ID: 227331432