Reversible Monadic Computing

Research output: Contribution to journalArticle

Researchers

  • Chris Heunen
  • Martti Karvonen

Research units

  • University of Oxford

Abstract

We extend categorical semantics of monadic programming to reversible computing, by considering monoidal closed dagger categories: the dagger gives reversibility, whereas closure gives higher-order expressivity. We demonstrate that Frobenius monads model the appropriate notion of coherence between the dagger and closure by reinforcing Cayley's theorem; by proving that effectful computations (Kleisli morphisms) are reversible precisely when the monad is Frobenius; by characterizing the largest reversible subcategory of Eilenberg-Moore algebras; and by identifying the latter algebras as measurements in our leading example of quantum computing. Strong Frobenius monads are characterized internally by Frobenius monoids.

Details

Original languageEnglish
Pages (from-to)217-237
Number of pages21
JournalELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
Volume319
Publication statusPublished - 21 Dec 2015
MoE publication typeA1 Journal article-refereed

    Research areas

  • dagger category, Frobenius monad, quantum measurement, reversible computing

Download statistics

No data available

ID: 9505191