Reversible monadic computing. (English) Zbl 1351.68100
Ghica, Dan (ed.), Proceedings of the 31st conference on the mathematical foundations of programming semantics (MFPS XXXI), Nijmegen, The Netherlands,
June 22–25, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 319, 217-237, electronic only (2015).
Summary: 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.
For the entire collection see [Zbl 1342.68016].
For the entire collection see [Zbl 1342.68016].
MSC:
| 68Q05 | Models of computation (Turing machines, etc.) (MSC2010) |
| 18C20 | Eilenberg-Moore and Kleisli constructions for monads |
| 18C50 | Categorical semantics of formal languages |
| 18D15 | Closed categories (closed monoidal and Cartesian closed categories, etc.) |
| 81P15 | Quantum measurement theory, state operations, state preparations |
| 81P68 | Quantum computation |
Software:
QMLReferences:
| [1] | Abramsky, S., Abstract scalars, loops, and free traced and strongly compact closed categories, Algebra and Coalgebra in Computer Science (2005) (2005) · Zbl 1151.81002 |
| [2] | Abramsky, S.; Coecke, B., A categorical semantics of quantum protocols, (Logic in Computer Science, 19 (2004)), 415-425 |
| [3] | Altenkirch, T.; Grattage, J., A functional quantum programming language, (Logic in Computer Science (2005)), 249-258 |
| [4] | Altenkirch, T.; Green, A. S., Semantics Techniques in Quantum Computation, 173-205 (2010), Cambridge University Press · Zbl 1209.68103 |
| [5] | Barr, M.; Wells, C., Category Theory for Computing Science (1990), Prentice-Hall · Zbl 0714.18001 |
| [6] | Bowman, W. J.; James, R. P.; Sabry, A., Dagger traced symmetric monoidal categories and reversible programming, Reversible Computation (2011) |
| [7] | Coecke, B.; Paquette, E. O.; Pavlovic, D., Semantic Techniques in Quantum Computation, 29-69 (2009), Cambridge University Press · Zbl 1192.81016 |
| [8] | Coecke, B.; Pavlovic, D., Quantum measurements without sums, Taylor and Francis, 559-596 (2008) · Zbl 1139.81307 |
| [9] | Coecke, B.; Pavlović, D.; Vicary, J., A new description of orthogonal bases, Mathematical Structures in Computer Science, 23, 555-567 (2012) · Zbl 1276.46016 |
| [10] | Day, B., On closed category of functors II, (Sydney Category Theory Seminar. Sydney Category Theory Seminar, Lecture Notes in Mathematics, vol. 420 (1974)), 20-54 · Zbl 0367.18008 |
| [11] | de Vos, A.; de Baerdemacker, S., Matrix calculus for classical and quantum circuits, ACM Journal on Emerging Technologies in Computing Systems, 11, 9 (2014) |
| [12] | Di Pierro, A.; Hankin, C.; Wiklicky, H., Quantitative relations and approximate process equivalences, (CONCUR 14. CONCUR 14, Lecture Notes in Computer Science, vol. 2761 (2003)), 508-522 · Zbl 1274.68227 |
| [13] | Di Pierro, A.; Wiklicky, H., Operator algebras and the operational semantics of probabilistic languages, (MFCSIT 3. MFCSIT 3, Electronic Notes in Theoretical Computer Science, vol. 161 (2006)), 131-150 · Zbl 1276.68050 |
| [14] | Green, A. S.; Lumsdaine, P. L.; Ross, N. J.; Selinger, P.; Valiron, B., A scalable quantum programming language, ACM SIGPLAN Notices, 48, 333-342 (2013) |
| [15] | Hasuo, I.; Hoshino, N., Semantics of higher-order quantum computation via geometry of interaction, Logic in Computer Science, 237-246 (2011) |
| [16] | Heunen, C., Categorical quantum models and logics (2009), Radboud University Nijmegen, Ph.D. thesis |
| [17] | Heunen, C., An embedding theorem for Hilbert categories, Theory and Applications of Categories, 22, 321-344 (2009) · Zbl 1181.18004 |
| [18] | Heunen, C.; Contreras, I.; Cattaneo, A., Relative Frobenius algebras are groupoids, Journal of Pure and Applied Algebra, 217, 114-124 (2013) · Zbl 1271.18004 |
| [19] | Heunen, C.; Vicary, J., Categories for Quantum Theory: An Introduction (2015), Oxford University Press |
| [20] | Jacobs, B., Involutive categories and monoids, with a GNS-correspondence, Foundations of Physics, 42, 874-895 (2012) · Zbl 1259.81032 |
| [21] | Jacobs, B., On block structures in quantum computation, (Mathematical Foundations of Program Semantics. Mathematical Foundations of Program Semantics, Electronic Notes in Theoretical Computer Science, vol. 298 (2013)), 233-255 · Zbl 1334.68074 |
| [22] | Jacobs, B.; Rutten, J., A tutorial on (co)algebras and (co)induction, EATCS Bulletin, 62, 222-259 (1997) · Zbl 0880.68070 |
| [23] | Jacobs, B. P.F., Semantics of weakening and contraction, Annals of Pure and Applied Logic, 69, 73-106 (1994) · Zbl 0814.03007 |
| [24] | Jacobs, B. P.F., Coalgebraic walks, in quantum and Turing computation, (FoSSaCS. FoSSaCS, Lecture Notes in Computer Science, vol. 6604 (2011)), 12-26 · Zbl 1326.68192 |
| [25] | Jacobs, B. P.F.; Heunen, C.; Hasuo, I., Categorical semantics for arrows, Journal of Functional Programming, 19, 403-438 (2009) · Zbl 1191.68406 |
| [26] | Kammar, O.; Lindley, S.; Oury, N., Handlers in action, (International Conference on Functional Programming XVIII (2013)), 145-148 · Zbl 1323.68126 |
| [27] | Kelly, G. M.; Laplaza, M. L., Coherence for compact closed categories, Journal of Pure and Applied Algebra, 19, 193-213 (1980) · Zbl 0447.18005 |
| [28] | Keyl, M., Fundamentals of quantum information theory, Physical Reports, 369, 431-548 (2002) · Zbl 0998.81014 |
| [29] | Kock, A., Strong functors and monoidal monads, Archiv der Mathematik, 23, 113-120 (1972) · Zbl 0253.18007 |
| [30] | Kozen, D., Semantics of probabilistic programs, Journal of Computer and System Sciences, 22, 328-350 (1981) · Zbl 0476.68019 |
| [31] | Lambek, J.; Scott, P., Introduction to higher order categorical logic (1986), Cambridge University Press · Zbl 0596.03002 |
| [32] | Lauda, A., Frobenius algebras and ambidextrous adjunctions, Theory and Applicatoins of Categories, 16, 84-122 (2006) · Zbl 1092.18003 |
| [33] | Lindner, H., Adjunctions in monoidal categories, Manuscripta Mathematica, 26, 123-139 (1978) · Zbl 0389.18004 |
| [34] | Marsden, D., Category theory using string diagrams (2014) |
| [35] | Mislove, M.; Ouaknine, J.; Pavlovic, D.; Worrell, J., Duality for labelled Markov processes, (FOSSACS 7. FOSSACS 7, Lecture Notes in Computer Science, vol. 2987 (2004)), 393-407 · Zbl 1126.68460 |
| [36] | Moggi, E., Notions of computation and monads, Information and Computation, 93, 55-92 (1991) · Zbl 0723.68073 |
| [37] | Moshier, M. A.; Petrişan, D., A duality theorem for real C*-algebras, (CALCO 3. CALCO 3, Lecture Notes in Computer Science, vol. 5728 (2009)), 284-299 · Zbl 1239.68042 |
| [38] | Panangaden, P., Labelled Markov processes (2009), Imperial College Press · Zbl 1190.60001 |
| [39] | Pavlović, D., Quantum and classical structures in nondeterministic computation, (Bruza, P.; etal., Third International symposium on Quantum Interaction. Third International symposium on Quantum Interaction, Lecture Notes in Artificial Intelligence, vol. 5494 (2009)), 143-157 · Zbl 1229.68039 |
| [40] | Pavlovic, D., Relating toy models of quantum computation: comprehension, complementarity and dagger mix autonomous categories, (Quantum Physics and Logic VI. Quantum Physics and Logic VI, Electronic Notes in Theoretical Computer Science, vol. 270 (2009)), 121-139 · Zbl 1348.81174 |
| [41] | Pavlovic, D., Geometry of abstraction in quantum computation, (Classical and Quantum Information Assurance Foundations and Practice, Dagstuhl Seminar Proceedings (2010)), 09311 |
| [42] | Plotkin, G. D.; Pretnar, M., Handling algebraic effects, Logical Methods in Computer Science, 9, 23 (2013) · Zbl 1314.68191 |
| [43] | Saheb-Djahromi, N., Cpo’s of measure for nondeterminism, Theoretical Computer Science, 12, 19-37 (1980) · Zbl 0433.68017 |
| [44] | Selinger, P., A survey of graphical languages for monoidal categories, Lecture Notes in Physics, 813, 289-356 (2009) · Zbl 1217.18002 |
| [45] | Selinger, P.; Valiron, B., A lambda calculus for quantum computation with classical control, Mathematical Structures in Computer Science, 16, 527-552 (2006) · Zbl 1122.68033 |
| [46] | Street, R., Frobenius monads and pseudomonoids, Journal of Mathematical Physics, 45, 3930-3948 (2004) · Zbl 1071.18006 |
| [47] | Szabo, M. E., Algebra of Proofs, (Studies in Logic and the Foundations of Mathematics, vol. 88 (1978), North-Holland) · Zbl 0532.03030 |
| [48] | Toffoli, T., Reversible computing, Automata, Languages and Programming, 85, 632-644 (1980) · Zbl 0443.68038 |
| [50] | Vicary, J., Categorical formulation of quantum algebras, Communications in Mathematical Physics, 304, 765-796 (2011) · Zbl 1221.81146 |
| [51] | Wadler, P., Comprehending monads, Mathematical Structures in Computer Science, 2, 461-493 (1992) · Zbl 0798.68040 |
| [52] | Wolff, H., Monads and monoids on symmetric monoidal closed categories, Archiv der Mathematik, 24, 113-120 (1973) · Zbl 0263.18010 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
