Document Open Access Logo

Completeness for Probabilistic Boolean Tapes

Authors Filippo Bonchi , Cipriano Junior Cioffo

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.21.pdf
  • Filesize: 1.06 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • String diagrams
  • Rig categories
  • synthetic probability theory

Metrics

Abstract

Probabilistic Boolean circuits have recently been proposed as a string-diagrammatic foundation for finite probabilistic programming. In this paper, we present a complete set of axioms for their semantics in terms of Markov kernels. Our approach is based on two intermediate results: completeness for partial Boolean circuits and completeness for probabilistic Boolean tapes, a diagrammatic language for rig categories.

Cite As Get BibTex

Filippo Bonchi and Cipriano Junior Cioffo. Completeness for Probabilistic Boolean Tapes. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.21

Author Details

Filippo Bonchi
  • University of Pisa, Italy
Cipriano Junior Cioffo
  • University of Pisa, Italy

Funding

This research was partly funded by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme.
  • Bonchi, Filippo: Bonchi is supported by the Ministero dell'Università e della Ricerca of Italy grant PRIN 2022 PNRR No. P2022HXNSC - RAP (Resource Awareness in Programming). This study was carried out within the National Centre on HPC, Big Data and Quantum Computing - SPOKE 10 (Quantum Computing) and received funding from the European Union Next-GenerationEU - National Recovery and Resilience Plan (NRRP) – MISSION 4 COMPONENT 2, INVESTMENT N. 1.4 – CUP N. I53C22000690001.

References

  1. Samson Abramsky and Bob Coecke. Categorical quantum mechanics. CoRR, abs/1401.4973, 2008. URL: https://arxiv.org/abs/1401.4973.
  2. Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. Sufficient incorrectness logic: SIL and separation SIL. CoRR, abs/2310.18156, 2023. URL: https://doi.org/10.48550/arXiv.2310.18156.
  3. Miriam Backens. The zx-calculus is complete for stabilizer quantum mechanics. New Journal of Physics, 16(9):093021, 2014. Google Scholar
  4. John Baez and Jason Erbele. Categories in control. Theory and Applications of Categories, 30:836-881, 2015. URL: https://arxiv.org/abs/1405.6881.
  5. Corrado Böhm and Giuseppe Jacopini. Flow diagrams, turing machines and languages with only two formation rules. Communications of the ACM, 9(5):366-371, 1966. URL: https://doi.org/10.1145/355592.365646.
  6. Filippo Bonchi and Cipriano Junior Cioffo. Completeness for Probabilistic Boolean Tapes, 2026. URL: https://arxiv.org/abs/2606.19017.
  7. Filippo Bonchi and Cipriano Junior Cioffo. Tapes as stochastic matrices of string diagrams. In Nathalie Bertrand and Stefan Milius, editors, Foundations of Software Science and Computation Structures, pages 88-109, Cham, 2026. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-032-22730-0_5.
  8. Filippo Bonchi and Cipriano Junior Cioffo. Tapes as stochastic matrices of string diagrams, 2026. URL: https://doi.org/10.48550/arXiv.2601.01472.
  9. Filippo Bonchi, Cipriano Junior Cioffo, Alessandro Di Giorgio, and Elena Di Lavore. Tape diagrams for monoidal monads, 2025. URL: https://doi.org/10.4230/LIPIcs.CALCO.2025.11.
  10. Filippo Bonchi, Alessandro Di Giorgio, and Elena Di Lavore. A diagrammatic algebra for program logics. In Parosh Aziz Abdulla and Delia Kesner, editors, Foundations of Software Science and Computation Structures, pages 308-330, Cham, 2025. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-90897-2_15.
  11. Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria. Deconstructing the calculus of relations with tape diagrams. Proceedings of the ACM on Programming Languages, 7(POPL):1864-1894, 2023. URL: https://doi.org/10.1145/3571257.
  12. Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful mealy machines: Bisimulation and trace. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 541-554. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00047.
  13. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: rewriting with frobenius structure. J. ACM, 69(2):14:1-14:58, 2022. URL: https://doi.org/10.1145/3502719.
  14. Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi. Diagrammatic algebra: From linear to concurrent systems. Proceedings of the ACM on Programming Languages, 3(POPL):25:1-25:28, January 2019. URL: https://doi.org/10.1145/3290338.
  15. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The power of convex algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017), pages 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.23.
  16. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full Abstraction for Signal Flow Graphs. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 515-526, New York, NY, USA, January 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676726.2676993.
  17. Francis Borceux. Handbook of categorical algebra. 2, volume 51 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 1994. Categories and structures. Google Scholar
  18. Kenta Cho and Bart Jacobs. Disintegration and bayesian inversion via string diagrams. Mathematical Structures in Computer Science, 29(7):938-971, 2019. URL: https://doi.org/10.1017/S0960129518000488.
  19. Kenta Cho, Bart Jacobs, Bas Westerbaan, and Abraham Westerbaan. An introduction to effectus theory. ArXiv, abs/1512.05813, 2015. URL: https://arxiv.org/abs/1512.05813.
  20. Bob Coecke and Ross Duncan. Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics, 13(4):043016, 2011. Google Scholar
  21. Bob Coecke, John Selby, and Sean Tull. Two Roads to Classicality. Electronic Proceedings in Theoretical Computer Science, 266:104-118, February 2018. URL: https://doi.org/10.4204/EPTCS.266.7.
  22. Cole Comfort, Antonin Delpeuch, and Jules Hedges. Sheet diagrams for bimonoidal categories. arXiv preprint, 2020. URL: https://arxiv.org/abs/2010.13361.
  23. Andrea Corradini, Ugo Montanari, Francesca Rossi, Hartmut Ehrig, Reiko Heckel, Michael Löwe, et al. Algebraic approaches to graph transformation-part i: Basic concepts and double pushout approach, 1997. Google Scholar
  24. Patrick Cousot, Radhia Cousot, Manuel Fähndrich, and Francesco Logozzo. Automatic inference of necessary preconditions. In Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni, editors, Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings, volume 7737 of Lecture Notes in Computer Science, pages 128-148. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-35873-9_10.
  25. Vincent Danos, Elham Kashefi, and Prakash Panangaden. The measurement calculus. Journal of the ACM (JACM), 54(2):8-es, 2007. Google Scholar
  26. Adnan Darwiche. A differential approach to inference in bayesian networks. In UAI, 2003. Google Scholar
  27. Elena Di Lavore and Mario Román. Evidential decision theory via partial markov categories. CoRR, abs/2301.12989, 2023. URL: https://doi.org/10.48550/arXiv.2301.12989.
  28. Elena Di Lavore, Mario Román, and Pawel Sobocinski. Partial markov categories. CoRR, abs/2502.03477, 2025. URL: https://doi.org/10.48550/arXiv.2502.03477.
  29. Gian Luigi Ferrari, Dan Hirsch, Ivan Lanese, Ugo Montanari, and Emilio Tuosto. Synchronised hyperedge replacement as a model for service oriented computing. In International Symposium on Formal Methods for Components and Objects, pages 22-43. Springer, 2005. URL: https://doi.org/10.1007/11804192_2.
  30. Brendan Fong, Paolo Rapisarda, and Paweł Sobociński. A categorical approach to open and interconnected dynamical systems. In LICS 2016, 2016. Google Scholar
  31. Brendan Fong and David Spivak. String diagrams for regular logic (extended abstract). In John Baez and Bob Coecke, editors, Applied Category Theory 2019, volume 323 of Electronic Proceedings in Theoretical Computer Science, pages 196-229. Open Publishing Association, September 2020. URL: https://doi.org/10.4204/eptcs.323.14.
  32. Tobias Fritz, Fabio Gadducci, Paolo Perrone, and Davide Trotta. Weakly markov categories and weakly affine monads. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023, Indiana University Bloomington, IN, USA, June 19-21, 2023, volume 270 of LIPIcs, pages 16:1-16:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CALCO.2023.16.
  33. Tobias Fritz, Tomáš Gonda, Nicholas Gauguin Houghton-Larsen, Antonio Lorenzin, Paolo Perrone, and Dario Stein. Dilations and information flow axioms in categorical probability. Mathematical Structures in Computer Science, 33(10):913-957, 2023. URL: https://doi.org/10.1017/S0960129523000324.
  34. Tobias Fritz, Tomáš Gonda, and Paolo Perrone. De Finetti’s theorem in categorical probability. arXiv preprint, 2021. URL: https://arxiv.org/abs/2105.02639.
  35. Tobias Fritz and Andreas Klingler. The d-separation criterion in categorical probability. Journal of Machine Learning Research, 24(46):1-49, 2023. URL: https://jmlr.org/papers/v24/22-0916.html.
  36. Tobias Fritz and Paolo Perrone. Bimonoidal structure of probability monads. Electronic notes in theoretical computer science, 341:121-149, 2018. URL: https://doi.org/10.1016/J.ENTCS.2018.11.007.
  37. Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. Combining effects and coeffects via grading. ACM SIGPLAN Notices, 51(9):476-489, 2016. URL: https://doi.org/10.1145/2951913.2951939.
  38. Dan R. Ghica and Achim Jung. Categorical semantics of digital circuits. In 2016 Formal Methods in Computer-Aided Design (FMCAD), pages 41-48, 2016. URL: https://doi.org/10.1109/FMCAD.2016.7886659.
  39. Amar Hadzihasanovic. A Diagrammatic Axiomatisation for Qubit Entanglement. PhD thesis, University of Oxford, 2015. Google Scholar
  40. Masahito Hasegawa. The uniformity principle on traced monoidal categories. Electronic Notes in Theoretical Computer Science, 69:137-155, 2003. URL: https://doi.org/10.1016/S1571-0661(04)80563-2.
  41. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3, 2007. URL: https://doi.org/10.2168/LMCS-3(4:11)2007.
  42. Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  43. Bart Jacobs. From coalgebraic to monoidal traces. Electronic Notes in Theoretical Computer Science, 264(2):125-140, 2010. URL: https://doi.org/10.1016/J.ENTCS.2010.07.017.
  44. Bart Jacobs, Aleks Kissinger, and Fabio Zanasi. Causal inference by string diagram surgery. In International conference on foundations of software science and computation structures, pages 313-329. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_18.
  45. Bart Jacobs, Fabio Zanasi, et al. The logical essentials of Bayesian reasoning. Cambridge University Press, 2021. Google Scholar
  46. Niles Johnson and Donald Yau. Bimonoidal categories, e_n-monoidal categories, and algebraic k-theory. arXiv preprint, 2021. URL: https://arxiv.org/abs/2107.10526.
  47. André Joyal and Ross Street. The geometry of tensor calculus, I. Advances in Mathematics, 88(1):55-112, July 1991. URL: https://doi.org/10.1016/0001-8708(91)90003-P.
  48. Benjamin Lucien Kaminski. Advanced weakest precondition calculi for probabilistic programs. PhD thesis, RWTH Aachen University, 2019. Google Scholar
  49. Frank R. Kschischang, Brendan J. Frey, and Hans-Andrea Loeliger. Factor graphs and the sum-product algorithm. IEEE Transactions on Information Theory, 47(2):498-519, 2001. URL: https://doi.org/10.1109/18.910572.
  50. Miguel L. Laplaza. Coherence for distributivity. In G. M. Kelly, M. Laplaza, G. Lewis, and Saunders Mac Lane, editors, Coherence in Categories, Lecture Notes in Mathematics, pages 29-65, Berlin, Heidelberg, 1972. Springer. URL: https://doi.org/10.1007/BFb0059555.
  51. Jack Liell-Cock and Sam Staton. Compositional imprecise probability: A solution from graded monads and markov categories. Proc. ACM Program. Lang., 9(POPL):1596-1626, 2025. URL: https://doi.org/10.1145/3704890.
  52. Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1978. URL: //www.springer.com/gb/book/9780387984032.
  53. Robin Milner. The space and motion of communicating agents. Cambridge University Press, 2009. Google Scholar
  54. Sean Moss and Paolo Perrone. A category-theoretic proof of the ergodic decomposition theorem. Ergodic Theory and Dynamical Systems, 43(12):4166-4192, 2023. Google Scholar
  55. Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica. The geometry of computation-graph abstraction. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 749-758. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209127.
  56. Peter W O'Hearn. Incorrectness logic. Proceedings of the ACM on Programming Languages, 4(POPL):1-32, 2019. URL: https://doi.org/10.1145/3371078.
  57. Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Reasoning about recursive probabilistic programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 672-681, 2016. URL: https://doi.org/10.1145/2933575.2935317.
  58. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proceedings of the ACM on Programming Languages, 3(ICFP):1-30, 2019. URL: https://doi.org/10.1145/3341714.
  59. Paolo Perrone. Markov categories and entropy. IEEE Transactions on Information Theory, 70(3):1671-1692, 2023. URL: https://doi.org/10.1109/TIT.2023.3328825.
  60. Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, and Fabio Zanasi. A complete axiomatisation of equivalence for discrete probabilistic programming. In Viktor Vafeiadis, editor, Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part II, volume 15695 of Lecture Notes in Computer Science, pages 202-229. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-91121-7_9.
  61. Robin Piedeleu and Fabio Zanasi. A String Diagrammatic Axiomatisation of Finite-State Automata. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, pages 469-489, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-71995-1_24.
  62. Hoifung Poon and Pedro Domingos. Sum-product networks: A new deep architecture. In UAI, 2011. Google Scholar
  63. Robert Raussendorf and Hans J. Briegel. A one-way quantum computer. Physical Review Letters, 86(22):5188-5191, 2001. Google Scholar
  64. Wojciech Rozowski and Alexandra Silva. A completeness theorem for probabilistic regular expressions. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 66:1-66:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662084.
  65. Peter Selinger. A Survey of Graphical Languages for Monoidal Categories, volume 813 of Lecture Notes in Physics, pages 289-355. Springer, Berlin, Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  66. Ana Sokolova and Harald Woracek. Termination in convex sets of distributions. Logical Methods in Computer Science, 14, 2018. URL: https://doi.org/10.23638/LMCS-14(4:17)2018.
  67. Dario Stein and Sam Staton. Probabilistic programming with exact conditions. Journal of the ACM, 71(1):1-53, 2024. URL: https://doi.org/10.1145/3632170.
  68. Marshall Harvey Stone. Postulates for the barycentric calculus. Annali di Matematica Pura ed Applicata, 29(1):25-30, 1949. Google Scholar
  69. Alejandro Villoria, Henning Basold, and Alfons Laarman. Enriching diagrams with algebraic operations. In International Conference on Foundations of Software Science and Computation Structures, pages 121-143. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57228-9_7.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact