Completeness for Probabilistic Boolean Tapes

Technical Summary: Completeness for Probabilistic Boolean Tapes

Problem Statement
The paper addresses the challenge of providing a complete equational axiomatization for the semantics of probabilistic Boolean circuits. While probabilistic Boolean circuits have been proposed as a string-diagrammatic foundation for finite probabilistic programming, previous attempts at axiomatization (specifically in [59]) were incomplete. The induced equivalence in prior work was strictly coarser than semantic equality; it identified diagrams $c$ and $d$ if their semantics were proportional ($\langle\langle c \rangle\rangle \propto \langle\langle d \rangle\rangle$), rather than strictly equal. Consequently, certain axioms in previous works were unsound with respect to the standard semantics based on Markov kernels (subdistributions). Furthermore, the paper notes that partial Boolean circuits (circuits that may fail to produce an output) had not been previously axiomatized.

Methodology
The authors employ a staged approach, moving from simpler structures to the full probabilistic language, leveraging the theory of string diagrams and category theory:

1. Boolean Circuits ($Diag_B$): The authors first recall the standard string-diagrammatic representation of Boolean circuits, interpreted as morphisms in the category of sets and functions. They rely on the known completeness of Boolean algebra axioms for this fragment.
2. Partial Boolean Circuits ($Diag_{PB}$): The authors extend the signature to include a "cocopy" generator (denoted $\cap$), which acts as the dual of the "copy" generator. This generator compares two inputs and outputs a value only if they agree; otherwise, it produces no output (undefined). This models partial functions. The authors define a new monoidal theory $PB$ extending Boolean algebra with axioms governing this partiality (associativity, commutativity, idempotence, and Frobenius laws).
3. Probabilistic Boolean Tapes ($T(Diag_{PB})$): Rather than axiomatizing the full probabilistic circuit language ($Diag_{PrB}$) directly, the authors introduce "probabilistic Boolean tapes." This formalism is constructed by freely adding convex biproducts to the category of partial Boolean circuits. Tapes support two monoidal structures: the tensor product ($\otimes$) and the convex sum ($\oplus$). The latter allows for the modeling of probabilistic control (e.g., probabilistic branching) in a way that the tensor product alone cannot.
4. Categorical Framework: The semantics are interpreted in $KL(D_\le)$, the Kleisli category of the subdistribution monad. The authors utilize results from [6] characterizing tape diagrams as stochastic matrices of string diagrams. Specifically, they rely on the fact that the category of tapes $T(C)$ is isomorphic to the category of stochastic matrices over the PCA-enriched category $C^+$ (denoted $StMat(C^+)$).

Key Contributions

1. Complete Axiomatization of Partial Boolean Circuits:
   The paper presents a complete set of axioms for partial Boolean circuits ($Diag_{PB}$). The axioms extend standard Boolean algebra with laws governing the "cocopy" generator (Figure 3). The authors prove completeness (Theorem 9) by decomposing any partial circuit into a "domain" circuit (determining where the function is defined) and a "total" circuit (determining the output value), reducing the problem to the known completeness of Boolean circuits.

2. Complete Axiomatization of Probabilistic Boolean Tapes:
   The authors provide a complete axiomatization for probabilistic Boolean tapes (Figures 4 and 5). This system includes:

   • Axioms for the tape construction (natural and coherent monoids, co-pointed convex algebras).
   • Specific axioms for partiality (e.g., equating a failed computation with a null distribution).
   • A crucial implication axiom (T3) expressing cancellativity, a standard reasoning principle in algebraic structures.
     The completeness proof (Corollary 29) relies on the isomorphism between tapes and stochastic matrices, showing that semantic equality in $KL(D_\le)$ corresponds exactly to equality in the tape calculus modulo the defined axioms.

3. Reduction of Circuit Equality to Tape Equality:
   By utilizing an encoding $E(-)$ from probabilistic Boolean circuits to probabilistic Boolean tapes (as established in [8]), the authors demonstrate that checking semantic equality of circuits reduces to checking equality of their tape encodings (Corollary 30).

Results

• Soundness and Completeness: The paper proves that the proposed axiom systems are both sound and complete with respect to the semantics in $KL(D_\le)$.
• Correction of Previous Work: The authors show that the equivalence induced by their system is strictly finer than the one in [59]. Specifically, they demonstrate that the previous system's axioms F2 and F7 are unsound, while their axiom F8 (from [59]) is derivable within their system.
• Expressivity of Tapes: The paper illustrates that tapes can model probabilistic control more naturally than circuits relying solely on $\otimes$. For instance, a tape can model a probabilistic choice between a valid computation and a failure (null behavior) without the entire composition becoming null, a limitation inherent in approaches using only the monoidal product.

Significance
The paper claims significance in providing the first complete axiomatization for partial Boolean circuits and a complete axiomatization for probabilistic Boolean tapes. By establishing these results, the authors enable equational reasoning directly at the level of diagrams for probabilistic programming. The shift to tapes allows for a structurally transparent axiomatization that handles probabilistic control and partiality uniformly. The authors note that while the current work focuses on finite probabilistic programming, the framework (specifically the use of traces with $\oplus$) could potentially provide algebraic foundations for probabilistic program logics and the representation of probabilistic regular expressions, though these are identified as future directions rather than current results. The work relies on the "string-diagrammatic" view where data is treated as a physical resource, preventing free copying or discarding, which is central to probabilistic and quantum computing contexts.