Reversible Monadic Computing
Finna-arvio
Reversible Monadic Computing
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.
Tallennettuna:
Kieli |
englanti |
---|---|
Sarja | ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE |
Aiheet | |
ISSN |
1571-0661 |
DOI | 10.1016/j.entcs.2015.12.014 |