Completeness for Probabilistic Boolean Tapes

Cipriano Junior Cioffo; Filippo Bonchi

arxiv: 2606.19017 · v1 · pith:BOULT5SAnew · submitted 2026-06-17 · 💻 cs.LO · math.CT

Completeness for Probabilistic Boolean Tapes

Filippo Bonchi , Cipriano Junior Cioffo This is my paper

Pith reviewed 2026-06-26 19:01 UTC · model grok-4.3

classification 💻 cs.LO math.CT

keywords probabilistic boolean circuitsmarkov kernelsstring diagramscompletenessrig categoriesaxiomatizationprobabilistic programmingpartial circuits

0 comments

The pith

Probabilistic Boolean circuits have a complete axiomatization for their Markov kernel semantics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a complete set of axioms for probabilistic Boolean circuits interpreted as Markov kernels, which serve as a string-diagrammatic foundation for finite probabilistic programming. The argument proceeds via two intermediate completeness theorems, one for partial Boolean circuits and one for probabilistic Boolean tapes viewed as a language for rig categories. A reader would care because the axioms let one decide equivalence of probabilistic programs by rewriting diagrams rather than computing distributions explicitly. This supplies a sound and complete calculus that aligns diagrammatic syntax directly with the intended probabilistic semantics.

Core claim

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.

What carries the argument

Probabilistic Boolean tapes as a diagrammatic language for rig categories, which carries the completeness proof for the probabilistic case.

If this is right

Equivalence of finite probabilistic programs becomes decidable by diagrammatic rewriting.
The Markov kernel semantics is fully captured by the string-diagram calculus.
Partial Boolean circuits admit their own complete axiomatization as an intermediate step.
Rig-category structure is faithfully represented by the tape language.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same tape construction might supply completeness results for other rig-category-based models of computation.
Extending the approach beyond finite support could link diagrammatic methods to measure-theoretic probability.

Load-bearing premise

Completeness holds for probabilistic Boolean tapes as a diagrammatic language for rig categories.

What would settle it

Two circuits with identical Markov kernel semantics that cannot be rewritten into each other using the stated axioms would show the axiomatization is incomplete.

read the original 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 \emph{partial} Boolean circuits and completeness for probabilistic Boolean tapes, a diagrammatic language for rig categories.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper delivers a clean completeness theorem for probabilistic Boolean tapes by proving two supporting results on partial circuits and rig-category interpretations.

read the letter

The central result is a set of axioms that are complete for the semantics of probabilistic Boolean circuits when interpreted as Markov kernels. They reach it by first getting completeness for partial Boolean circuits, then for probabilistic Boolean tapes as a diagrammatic language for rig categories, and finally composing the two.

The paper does the technical work properly. It states the axioms explicitly, gives soundness arguments against the kernel semantics, and supplies equational derivations for both intermediate completeness claims. The chain from the rig-category axioms to the final statement looks independent, with no circular steps visible.

The main limitation is that the result sits on top of the recent introduction of the circuits themselves, so it is an extension rather than a standalone foundation. That is not a flaw, just the natural scope. The proofs appear to be carried through with the required detail rather than left as sketches.

This is for readers who already work with string diagrams, rig categories, or finite probabilistic models. Someone outside that niche will not get much from it, but inside the niche the completeness statement is the missing piece that lets the calculus be used with certainty.

The work shows clear engagement with the relevant literature and the proofs are the kind of thing that can be checked. It should go to peer review.

Referee Report

0 major / 2 minor

Summary. The paper claims to establish a complete set of axioms for the semantics of probabilistic Boolean circuits (as a string-diagrammatic foundation for finite probabilistic programming) in terms of Markov kernels. Completeness is obtained by composing two intermediate results: completeness for partial Boolean circuits and completeness for probabilistic Boolean tapes as a diagrammatic language for rig categories. The manuscript supplies the required axioms, soundness arguments, and explicit equational derivations for both intermediate completeness theorems together with their semantic interpretations.

Significance. If the stated completeness theorems hold, the work supplies a sound and complete equational calculus for diagrammatic reasoning about probabilistic Boolean circuits. The explicit provision of the two intermediate completeness proofs with equational derivations and Markov-kernel semantics constitutes a concrete technical contribution that supports verifiable reasoning in probabilistic programming.

minor comments (2)

[Abstract] Abstract: the final completeness statement is not cross-referenced to a numbered theorem; adding the theorem number would help readers locate the main result immediately.
The dependence on rig-category structure is stated clearly, but a one-sentence reminder of the rig-category axioms used (or a pointer to the relevant section) would aid readers who encounter the term for the first time.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for the positive assessment. We are pleased that the referee recommends acceptance.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper states its main result as a completeness theorem for probabilistic Boolean circuits, obtained by composing two intermediate completeness results (partial Boolean circuits; probabilistic Boolean tapes as rig-category language). The provided description indicates that the manuscript itself supplies the axioms, soundness arguments, and explicit equational derivations for both intermediate results, together with semantic interpretations in Markov kernels. No load-bearing step is described as reducing by construction to a fitted parameter, a self-citation chain, or a redefinition of the target quantity. The central claim therefore remains independent of its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract-only review prevents full enumeration; no free parameters or invented entities are mentioned. Relies on standard category-theoretic background for rig categories and Markov kernels.

axioms (1)

standard math Standard axioms and definitions of rig categories and Markov kernels
Invoked implicitly as the semantic target and the structure for probabilistic Boolean tapes.

pith-pipeline@v0.9.1-grok · 5574 in / 926 out tokens · 31928 ms · 2026-06-26T19:01:43.298009+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

37 extracted references · 17 canonical work pages · 1 internal anchor

[1]

Categorical quantum mechanics.CoRR, abs/1401.4973,

1Samson Abramsky and Bob Coecke. Categorical quantum mechanics.CoRR, abs/1401.4973,

Pith/arXiv arXiv
[2]

Sufficient incorrectness logic: SIL and separation SIL.CoRR, abs/2310.18156,

2 Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. Sufficient incorrectness logic: SIL and separation SIL.CoRR, abs/2310.18156,

arXiv
[3]

18156,arXiv:2310.18156,doi:10.48550/ARXIV.2310.18156

URL:https://doi.org/10.48550/arXiv.2310. 18156,arXiv:2310.18156,doi:10.48550/ARXIV.2310.18156. 3 Miriam Backens. The zx-calculus is complete for stabilizer quantum mechanics.New Journal of Physics, 16(9):093021,

work page doi:10.48550/arxiv.2310
[4]

8 Filippo Bonchi, Cipriano Junior Cioffo, Alessandro Di Giorgio, and Elena Di Lavore

URL: https://arxiv.org/abs/2601.01472,arXiv:2601.01472. 8 Filippo Bonchi, Cipriano Junior Cioffo, Alessandro Di Giorgio, and Elena Di Lavore. Tape diagrams for monoidal monads,

arXiv
[5]

9 Filippo Bonchi, Alessandro Di Giorgio, and Elena Di Lavore

URL: https://drops.dagstuhl.de/entities/document/10.4230/ LIPIcs.CALCO.2025.11,doi:10.4230/LIPIcs.CALCO.2025.11. 9 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,

work page doi:10.4230/lipics.calco.2025.11 2025
[6]

de Groot, I

11 Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful mealy machines: Bisimulation and trace. In40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 541–554. IEEE, 2025.doi:10.1109/LICS65433.2025.00047. 12 Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. Str...

work page doi:10.1109/lics65433.2025.00047 2025
[7]

doi:10.1145/ 3502719. F. Bonchi, C.J. Cioffo 23:17 13 Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Soboci´nski, 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.doi:10.1145/3290338. 14 Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The p...

work page doi:10.1145/3290338 2019
[8]

Algebraic effects, linearity, and quantum programming languages,

Association for Computing Machinery.doi:10.1145/2676726.2676993. 16 Francis Borceux.Handbook of categorical algebra. 2, volume 51 ofEncyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge,

work page doi:10.1145/2676726.2676993
[9]

An introduction to effectus theory

18 Kenta Cho, Bart Jacobs, Bas Westerbaan, and Abraham Westerbaan. An introduction to effectus theory. ArXiv, abs/1512.05813,

Pith/arXiv arXiv
[10]

Two Roads to Classicality

arXiv:1701.07400,doi:10.4204/EPTCS.266.7. 21 Cole Comfort, Antonin Delpeuch, and Jules Hedges. Sheet diagrams for bimonoidal categories.arXiv preprint arXiv:2010.13361,

work page internal anchor Pith review Pith/arXiv arXiv doi:10.4204/eptcs.266.7 2010
[11]

Automatic inference of necessary preconditions

23 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
[12]

Springer, 2013.doi:10.1007/978-3-642-35873-9\_10

Proceedings, volume 7737 ofLecture Notes in Computer Science, pages 128–148. Springer, 2013.doi:10.1007/978-3-642-35873-9\_10. 24 Vincent Danos, Elham Kashefi, and Prakash Panangaden. The measurement calculus.Journal of the ACM (JACM), 54(2):8–es,

work page doi:10.1007/978-3-642-35873-9 2013
[13]

Evidential decision theory via partial markov categories

26 Elena Di Lavore and Mario Román. Evidential decision theory via partial markov categories. CoRR, abs/2301.12989,

arXiv
[14]

27 Elena Di Lavore, Mario Román, and Pawel Sobocinski

URL: https://doi.org/10.48550/arXiv.2301.12989, arXiv: 2301.12989,doi:10.48550/ARXIV.2301.12989. 27 Elena Di Lavore, Mario Román, and Pawel Sobocinski. Partial markov categories.CoRR, abs/2502.03477,

work page doi:10.48550/arxiv.2301.12989
[15]

48550/ARXIV.2502.03477

URL: https://doi.org/10.48550/arXiv.2502.03477, arXiv:2502.03477, doi:10. 48550/ARXIV.2502.03477. 28 Gian Luigi Ferrari, Dan Hirsch, Ivan Lanese, Ugo Montanari, and Emilio Tuosto. Synchronised hyperedge replacement as a model for service oriented computing. InInternational Symposium on Formal Methods for Components and Objects, pages 22–43. Springer,

work page doi:10.48550/arxiv.2502.03477
[16]

A categorical approach to open and interconnected dynamical systems

29 Brendan Fong, Paolo Rapisarda, and Paweł Soboci´nski. A categorical approach to open and interconnected dynamical systems. InLICS 2016,

2016
[17]

String diagrams for regular logic (extended abstract)

30 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 ofElectronic Proceedings in Theoretical Computer Science, page 196–229. Open Publishing Association, Sep

2019
[18]

doi:10.4204/eptcs.323

work page doi:10.4204/eptcs.323
[19]

Weakly markov categories and weakly affine monads.arXiv preprint arXiv:2303.14049,

31 Tobias Fritz, Fabio Gadducci, Paolo Perrone, and Davide Trotta. Weakly markov categories and weakly affine monads.arXiv preprint arXiv:2303.14049,

arXiv
[20]

De finetti’s theorem in categorical probability.arXiv preprint arXiv:2105.02639,

CVIT 2016 23:18 Completeness for Probabilistic Boolean Tapes 33 Tobias Fritz, Tomáš Gonda, and Paolo Perrone. De finetti’s theorem in categorical probability.arXiv preprint arXiv:2105.02639,

arXiv 2016
[21]

doi:10.1109/FMCAD.2016.7886655 , url =

37 Dan R. Ghica and Achim Jung. Categorical semantics of digital circuits. In2016 Formal Methods in Computer-Aided Design (FMCAD), pages 41–48, 2016.doi:10.1109/FMCAD.2016.7886659. 38 Amar Hadzihasanovic.A Diagrammatic Axiomatisation for Qubit Entanglement. PhD thesis, University of Oxford,

work page doi:10.1109/fmcad.2016.7886659 2016
[22]

Bimonoidal categories, e_n-monoidal categories, and algebraic k-theory

45 Niles Johnson and Donald Yau. Bimonoidal categories, e_n-monoidal categories, and algebraic k-theory. arXiv preprint arXiv:2107.10526,

arXiv
[23]

The geometry of tensor calculus, I.Advances in Mathematics, 88(1):55–112, July 1991.doi:10.1016/0001-8708(91)90003-P

46 André Joyal and Ross Street. The geometry of tensor calculus, I.Advances in Mathematics, 88(1):55–112, July 1991.doi:10.1016/0001-8708(91)90003-P. 47 Benjamin Lucien Kaminski.Advanced weakest precondition calculi for probabilistic programs. PhD thesis, RWTH Aachen University,

work page doi:10.1016/0001-8708(91)90003-p 1991
[24]

Laplaza (1972):Coherence for distributivity

Springer.doi:10.1007/BFb0059555. 50 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.doi:10.1145/3704890. 51 Saunders Mac Lane.Categories for the Working Mathematician, volume 5 ofGraduate Texts in Math- ematics. Springer-Verlag, New Y...

work page doi:10.1007/bfb0059555 2025
[25]

54 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
[26]

55 Peter W O’Hearn

doi:10.1145/3209108.3209127. 55 Peter W O’Hearn. Incorrectness logic.Proceedings of the ACM on Programming Languages, 4(POPL):1– 32,

work page doi:10.1145/3209108.3209127
[27]

A complete axiomatisation of equivalence for discrete probabilistic programming

59 Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, and Fabio Zanasi. A complete axiomatisation of equivalence for discrete probabilistic programming. InESOP 2025 (to appear),

2025
[28]

60 Robin Piedeleu and Fabio Zanasi

arXiv: 2408.14701. 60 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,

arXiv
[29]

doi:10.1007/978-3-030-71995-1_24

Springer International Publishing. doi:10.1007/978-3-030-71995-1_24. 61Hoifung Poon and Pedro Domingos. Sum-product networks: A new deep architecture. InUAI,

work page doi:10.1007/978-3-030-71995-1_24
[30]

Separation and encodability in mixed choice multiparty sessions

63 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.doi:10.1145/3661814.3662084. 64 P. S...

work page doi:10.1145/3661814.3662084 2024
[31]

65 Peter Selinger

doi: 10.1007/978-3-642-12821-9_4. 65 Peter Selinger. A survey of graphical languages for monoidal categories. InNew structures for physics, pages 289–355. Springer,

work page doi:10.1007/978-3-642-12821-9_4
[32]

CVIT 2016 23:20 Completeness for Probabilistic Boolean Tapes A Additional figures and tables p◁U :U→U⊕U U :U→0σ ⊕ U,V:U⊕V→V⊕U▷ U :U⊕U→U ⊸U : 0→U id0: 0→0id U :U→U c:U→V c :U→V t:P→Qs:Q→R t;s:P→R t:P 1 →Q 1 s:P 2 →Q 2 t⊕s:P 1 ⊕P 2 →Q 1 ⊕Q 2 (a)Typing rules. p◁0 def =id 0 0 def =id 0 U⊕P def = U ⊕ P ▷0 def =id 0 ⊸0 def =id 0 ⊸U⊕P def = ⊸U ⊕ ⊸P p◁U⊕P def =( ...

2016
[33]

def=R U (t1);R U (t2) LU (σ⊕ V,W) def=σ ⊕ UV,UW RU (σ⊕ V,W) def=σ ⊕ VU,WU LU (p◁V ) def= p◁UV LU ( V ) def= UV RU (p◁V ) def= p◁VU RU ( V ) def= VU LU (▷V ) def=▷ UV LU (⊸V ) def= ⊸UV RU (▷V ) def=▷ VU RU (⊸V ) def= ⊸VU L0(t) def=id 0 LW⊕S ′ (t) def=L W (t)⊕L S ′ (t) R0(t) def=id 0 RW⊕S ′ (t) def=δ l P,W,S′ ; (RW (t)⊕R S ′ (t));δ −l Q,W,S′ t1 ⊗t 2 def=L P...

2016
[34]

In the case c⊗d , then assuming that the state- ment holds forcandd, we have 1 n′ m′ (6) =PBn′′ m′′ Dc⊗d Tc⊗d n′ n′′ 1 0 Tc Td m′ m′′ m′′ 0 m′ m′ m′′ (B8) =PB n′ n′′ 0 Tc Td m′ m′′ m′′ 0 m′ m′ m′′ Dc⊗d Dc⊗d 1Dc⊗d Dc⊗d (D5) =PB n′ n′′ 0 Tc Td m′ m′′ m′′ 0 m′ m′ m′′ (D6) =PB 1 Dc⊗d n′ n′′ 0 Tc Td m′ m′′ m′′ 0 m′ m′ m′′ 1Dc⊗d 1 (D2) =PB n′ n′′ Tc Td m′ m′′ 1...

2016
[35]

The base case c = p is proved before the statement of the proposition

By induction on c. The base case c = p is proved before the statement of the proposition. For the base case c∈PB∪ {id A,id 1, σ⊗ A,A}, ⟦E(c)⟧ = c by the definition in Table 2 and c = J(⟨ ⟨c⟩ ⟩PB) by (12). The latter is exactly ⟨ ⟨c⟩ ⟩. The inductive cases follow immediately from the fact that⟦−⟧ is a morphism of rig categories and hence preserve⊗.◀ E Appe...

2016
[36]

Proof.It follows from (17), Theorem 17 and Proposition 10.◀ Proof of Lemma

As proven in [ 6, Theorem 4] it is given by the following CVIT 2016 23:28 Completeness for Probabilistic Boolean Tapes inductive definition on the structure of arrows inT(C): G♭(idU) def =id G(U) G♭( c ) def =G(c) G♭(p◁P) def = p◁G(P) G♭( P) def = G(P) G♭(▷P) def =▷ G(P) G♭(⊸P) def = ⊸G(P) G♭(t;s) def =G ♭(t);G ♭(s)G ♭(t⊕s) def =G ♭(t)⊕G ♭(s) G♭(σ⊕ P,Q) d...

2016
[37]

By Lemma 11, each partial Boolean circuit in DiagPB[A0,A m] is either a Boolean circuit in DiagB[1,A m] or it is of the form ⊥ m

SinceT( DiagPB) StMat (Diag+ PB), t corresponds to a subdistribution on DiagPB[A0,A m]. By Lemma 11, each partial Boolean circuit in DiagPB[A0,A m] is either a Boolean circuit in DiagB[1,A m] or it is of the form ⊥ m. Hence, we can rearrange the subdistribution corres- ponding totinto a tape of the desired form.◀ Proof of Lemma 27.By Lemma 26, we can writ...

2016

[1] [1]

Categorical quantum mechanics.CoRR, abs/1401.4973,

1Samson Abramsky and Bob Coecke. Categorical quantum mechanics.CoRR, abs/1401.4973,

Pith/arXiv arXiv

[2] [2]

Sufficient incorrectness logic: SIL and separation SIL.CoRR, abs/2310.18156,

2 Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. Sufficient incorrectness logic: SIL and separation SIL.CoRR, abs/2310.18156,

arXiv

[3] [3]

18156,arXiv:2310.18156,doi:10.48550/ARXIV.2310.18156

URL:https://doi.org/10.48550/arXiv.2310. 18156,arXiv:2310.18156,doi:10.48550/ARXIV.2310.18156. 3 Miriam Backens. The zx-calculus is complete for stabilizer quantum mechanics.New Journal of Physics, 16(9):093021,

work page doi:10.48550/arxiv.2310

[4] [4]

8 Filippo Bonchi, Cipriano Junior Cioffo, Alessandro Di Giorgio, and Elena Di Lavore

URL: https://arxiv.org/abs/2601.01472,arXiv:2601.01472. 8 Filippo Bonchi, Cipriano Junior Cioffo, Alessandro Di Giorgio, and Elena Di Lavore. Tape diagrams for monoidal monads,

arXiv

[5] [5]

9 Filippo Bonchi, Alessandro Di Giorgio, and Elena Di Lavore

URL: https://drops.dagstuhl.de/entities/document/10.4230/ LIPIcs.CALCO.2025.11,doi:10.4230/LIPIcs.CALCO.2025.11. 9 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,

work page doi:10.4230/lipics.calco.2025.11 2025

[6] [6]

de Groot, I

11 Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful mealy machines: Bisimulation and trace. In40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 541–554. IEEE, 2025.doi:10.1109/LICS65433.2025.00047. 12 Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. Str...

work page doi:10.1109/lics65433.2025.00047 2025

[7] [7]

doi:10.1145/ 3502719. F. Bonchi, C.J. Cioffo 23:17 13 Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Soboci´nski, 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.doi:10.1145/3290338. 14 Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The p...

work page doi:10.1145/3290338 2019

[8] [8]

Algebraic effects, linearity, and quantum programming languages,

Association for Computing Machinery.doi:10.1145/2676726.2676993. 16 Francis Borceux.Handbook of categorical algebra. 2, volume 51 ofEncyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge,

work page doi:10.1145/2676726.2676993

[9] [9]

An introduction to effectus theory

18 Kenta Cho, Bart Jacobs, Bas Westerbaan, and Abraham Westerbaan. An introduction to effectus theory. ArXiv, abs/1512.05813,

Pith/arXiv arXiv

[10] [10]

Two Roads to Classicality

arXiv:1701.07400,doi:10.4204/EPTCS.266.7. 21 Cole Comfort, Antonin Delpeuch, and Jules Hedges. Sheet diagrams for bimonoidal categories.arXiv preprint arXiv:2010.13361,

work page internal anchor Pith review Pith/arXiv arXiv doi:10.4204/eptcs.266.7 2010

[11] [11]

Automatic inference of necessary preconditions

23 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

[12] [12]

Springer, 2013.doi:10.1007/978-3-642-35873-9\_10

Proceedings, volume 7737 ofLecture Notes in Computer Science, pages 128–148. Springer, 2013.doi:10.1007/978-3-642-35873-9\_10. 24 Vincent Danos, Elham Kashefi, and Prakash Panangaden. The measurement calculus.Journal of the ACM (JACM), 54(2):8–es,

work page doi:10.1007/978-3-642-35873-9 2013

[13] [13]

Evidential decision theory via partial markov categories

26 Elena Di Lavore and Mario Román. Evidential decision theory via partial markov categories. CoRR, abs/2301.12989,

arXiv

[14] [14]

27 Elena Di Lavore, Mario Román, and Pawel Sobocinski

URL: https://doi.org/10.48550/arXiv.2301.12989, arXiv: 2301.12989,doi:10.48550/ARXIV.2301.12989. 27 Elena Di Lavore, Mario Román, and Pawel Sobocinski. Partial markov categories.CoRR, abs/2502.03477,

work page doi:10.48550/arxiv.2301.12989

[15] [15]

48550/ARXIV.2502.03477

URL: https://doi.org/10.48550/arXiv.2502.03477, arXiv:2502.03477, doi:10. 48550/ARXIV.2502.03477. 28 Gian Luigi Ferrari, Dan Hirsch, Ivan Lanese, Ugo Montanari, and Emilio Tuosto. Synchronised hyperedge replacement as a model for service oriented computing. InInternational Symposium on Formal Methods for Components and Objects, pages 22–43. Springer,

work page doi:10.48550/arxiv.2502.03477

[16] [16]

A categorical approach to open and interconnected dynamical systems

29 Brendan Fong, Paolo Rapisarda, and Paweł Soboci´nski. A categorical approach to open and interconnected dynamical systems. InLICS 2016,

2016

[17] [17]

String diagrams for regular logic (extended abstract)

30 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 ofElectronic Proceedings in Theoretical Computer Science, page 196–229. Open Publishing Association, Sep

2019

[18] [18]

doi:10.4204/eptcs.323

work page doi:10.4204/eptcs.323

[19] [19]

Weakly markov categories and weakly affine monads.arXiv preprint arXiv:2303.14049,

31 Tobias Fritz, Fabio Gadducci, Paolo Perrone, and Davide Trotta. Weakly markov categories and weakly affine monads.arXiv preprint arXiv:2303.14049,

arXiv

[20] [20]

De finetti’s theorem in categorical probability.arXiv preprint arXiv:2105.02639,

CVIT 2016 23:18 Completeness for Probabilistic Boolean Tapes 33 Tobias Fritz, Tomáš Gonda, and Paolo Perrone. De finetti’s theorem in categorical probability.arXiv preprint arXiv:2105.02639,

arXiv 2016

[21] [21]

doi:10.1109/FMCAD.2016.7886655 , url =

37 Dan R. Ghica and Achim Jung. Categorical semantics of digital circuits. In2016 Formal Methods in Computer-Aided Design (FMCAD), pages 41–48, 2016.doi:10.1109/FMCAD.2016.7886659. 38 Amar Hadzihasanovic.A Diagrammatic Axiomatisation for Qubit Entanglement. PhD thesis, University of Oxford,

work page doi:10.1109/fmcad.2016.7886659 2016

[22] [22]

Bimonoidal categories, e_n-monoidal categories, and algebraic k-theory

45 Niles Johnson and Donald Yau. Bimonoidal categories, e_n-monoidal categories, and algebraic k-theory. arXiv preprint arXiv:2107.10526,

arXiv

[23] [23]

The geometry of tensor calculus, I.Advances in Mathematics, 88(1):55–112, July 1991.doi:10.1016/0001-8708(91)90003-P

46 André Joyal and Ross Street. The geometry of tensor calculus, I.Advances in Mathematics, 88(1):55–112, July 1991.doi:10.1016/0001-8708(91)90003-P. 47 Benjamin Lucien Kaminski.Advanced weakest precondition calculi for probabilistic programs. PhD thesis, RWTH Aachen University,

work page doi:10.1016/0001-8708(91)90003-p 1991

[24] [24]

Laplaza (1972):Coherence for distributivity

Springer.doi:10.1007/BFb0059555. 50 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.doi:10.1145/3704890. 51 Saunders Mac Lane.Categories for the Working Mathematician, volume 5 ofGraduate Texts in Math- ematics. Springer-Verlag, New Y...

work page doi:10.1007/bfb0059555 2025

[25] [25]

54 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

[26] [26]

55 Peter W O’Hearn

doi:10.1145/3209108.3209127. 55 Peter W O’Hearn. Incorrectness logic.Proceedings of the ACM on Programming Languages, 4(POPL):1– 32,

work page doi:10.1145/3209108.3209127

[27] [27]

A complete axiomatisation of equivalence for discrete probabilistic programming

59 Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, and Fabio Zanasi. A complete axiomatisation of equivalence for discrete probabilistic programming. InESOP 2025 (to appear),

2025

[28] [28]

60 Robin Piedeleu and Fabio Zanasi

arXiv: 2408.14701. 60 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,

arXiv

[29] [29]

doi:10.1007/978-3-030-71995-1_24

Springer International Publishing. doi:10.1007/978-3-030-71995-1_24. 61Hoifung Poon and Pedro Domingos. Sum-product networks: A new deep architecture. InUAI,

work page doi:10.1007/978-3-030-71995-1_24

[30] [30]

Separation and encodability in mixed choice multiparty sessions

63 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.doi:10.1145/3661814.3662084. 64 P. S...

work page doi:10.1145/3661814.3662084 2024

[31] [31]

65 Peter Selinger

doi: 10.1007/978-3-642-12821-9_4. 65 Peter Selinger. A survey of graphical languages for monoidal categories. InNew structures for physics, pages 289–355. Springer,

work page doi:10.1007/978-3-642-12821-9_4

[32] [32]

CVIT 2016 23:20 Completeness for Probabilistic Boolean Tapes A Additional figures and tables p◁U :U→U⊕U U :U→0σ ⊕ U,V:U⊕V→V⊕U▷ U :U⊕U→U ⊸U : 0→U id0: 0→0id U :U→U c:U→V c :U→V t:P→Qs:Q→R t;s:P→R t:P 1 →Q 1 s:P 2 →Q 2 t⊕s:P 1 ⊕P 2 →Q 1 ⊕Q 2 (a)Typing rules. p◁0 def =id 0 0 def =id 0 U⊕P def = U ⊕ P ▷0 def =id 0 ⊸0 def =id 0 ⊸U⊕P def = ⊸U ⊕ ⊸P p◁U⊕P def =( ...

2016

[33] [33]

def=R U (t1);R U (t2) LU (σ⊕ V,W) def=σ ⊕ UV,UW RU (σ⊕ V,W) def=σ ⊕ VU,WU LU (p◁V ) def= p◁UV LU ( V ) def= UV RU (p◁V ) def= p◁VU RU ( V ) def= VU LU (▷V ) def=▷ UV LU (⊸V ) def= ⊸UV RU (▷V ) def=▷ VU RU (⊸V ) def= ⊸VU L0(t) def=id 0 LW⊕S ′ (t) def=L W (t)⊕L S ′ (t) R0(t) def=id 0 RW⊕S ′ (t) def=δ l P,W,S′ ; (RW (t)⊕R S ′ (t));δ −l Q,W,S′ t1 ⊗t 2 def=L P...

2016

[34] [34]

In the case c⊗d , then assuming that the state- ment holds forcandd, we have 1 n′ m′ (6) =PBn′′ m′′ Dc⊗d Tc⊗d n′ n′′ 1 0 Tc Td m′ m′′ m′′ 0 m′ m′ m′′ (B8) =PB n′ n′′ 0 Tc Td m′ m′′ m′′ 0 m′ m′ m′′ Dc⊗d Dc⊗d 1Dc⊗d Dc⊗d (D5) =PB n′ n′′ 0 Tc Td m′ m′′ m′′ 0 m′ m′ m′′ (D6) =PB 1 Dc⊗d n′ n′′ 0 Tc Td m′ m′′ m′′ 0 m′ m′ m′′ 1Dc⊗d 1 (D2) =PB n′ n′′ Tc Td m′ m′′ 1...

2016

[35] [35]

The base case c = p is proved before the statement of the proposition

By induction on c. The base case c = p is proved before the statement of the proposition. For the base case c∈PB∪ {id A,id 1, σ⊗ A,A}, ⟦E(c)⟧ = c by the definition in Table 2 and c = J(⟨ ⟨c⟩ ⟩PB) by (12). The latter is exactly ⟨ ⟨c⟩ ⟩. The inductive cases follow immediately from the fact that⟦−⟧ is a morphism of rig categories and hence preserve⊗.◀ E Appe...

2016

[36] [36]

Proof.It follows from (17), Theorem 17 and Proposition 10.◀ Proof of Lemma

As proven in [ 6, Theorem 4] it is given by the following CVIT 2016 23:28 Completeness for Probabilistic Boolean Tapes inductive definition on the structure of arrows inT(C): G♭(idU) def =id G(U) G♭( c ) def =G(c) G♭(p◁P) def = p◁G(P) G♭( P) def = G(P) G♭(▷P) def =▷ G(P) G♭(⊸P) def = ⊸G(P) G♭(t;s) def =G ♭(t);G ♭(s)G ♭(t⊕s) def =G ♭(t)⊕G ♭(s) G♭(σ⊕ P,Q) d...

2016

[37] [37]

By Lemma 11, each partial Boolean circuit in DiagPB[A0,A m] is either a Boolean circuit in DiagB[1,A m] or it is of the form ⊥ m

SinceT( DiagPB) StMat (Diag+ PB), t corresponds to a subdistribution on DiagPB[A0,A m]. By Lemma 11, each partial Boolean circuit in DiagPB[A0,A m] is either a Boolean circuit in DiagB[1,A m] or it is of the form ⊥ m. Hence, we can rearrange the subdistribution corres- ponding totinto a tape of the desired form.◀ Proof of Lemma 27.By Lemma 26, we can writ...

2016