Completeness for Probabilistic Boolean Tapes

Technische Samenvatting: Volledigheid voor Probabilistische Booleaanse Tapes

Probleemstelling
Het artikel behandelt de uitdaging van het bieden van een volledige equationele axiomatisering voor de semantiek van probabilistische Booleaanse circuits. Hoewel probabilistische Booleaanse circuits zijn voorgesteld als een string-diagrammatische basis voor eindige probabilistische programmering, waren eerdere pogingen tot axiomatisering (specifiek in [59]) incompleet. De geïnduceerde equivalentie in eerder werk was strikt grover dan semantische gelijkheid; het identificeerde diagrammen $c$ en $d$ indien hun semantiek proportioneel was ($\langle\langle c \rangle\rangle \propto \langle\langle d \rangle\rangle$), in plaats van strikt gelijk. Bijgevolg waren bepaalde axioma's in eerder werk onjuist met betrekking tot de standaardsemantiek gebaseerd op Markov-kernels (subdistributies). Bovendien merkt het artikel op dat partiële Booleaanse circuits (circuits die mogelijk geen output produceren) voorheen niet geaxiomatiseerd waren.

Methodologie
De auteurs hanteren een gefaseerde aanpak, waarbij ze van eenvoudigere structuren naar de volledige probabilistische taal bewegen, gebruikmakend van de theorie van string-diagrammen en categorietheorie:

1. Booleaanse Circuits ($Diag_B$): De auteurs herinneren eerst de standaard string-diagrammatische representatie van Booleaanse circuits, geïnterpreteerd als morfismen in de categorie van verzamelingen en functies. Ze vertrouwen op de bekende volledigheid van Booleaanse algebra-axioma's voor dit fragment.
2. Partiële Booleaanse Circuits ($Diag_{PB}$): De auteurs breiden de signatuur uit door een "cocopy"-generator toe te voegen (aangeduid met $\cap$), die fungeert als het dual van de "copy"-generator. Deze generator vergelijkt twee inputs en geeft een waarde uit alleen als ze overeenkomen; anders produceert hij geen output (ongedefinieerd). Dit modelleert partiële functies. De auteurs definiëren een nieuwe monoidale theorie $PB$ die de Booleaanse algebra uitbreidt met axioma's die deze partialiteit beheersen (associativiteit, commutativiteit, idempotentie en Frobenius-wetten).
3. Probabilistische Booleaanse Tapes ($T(Diag_{PB})$): In plaats van de volledige probabilistische circuittaal ($Diag_{PrB}$) direct te axiomatiseren, introduceren de auteurs "probabilistische Booleaanse tapes". Deze formalisme wordt geconstrueerd door vrij convex biproducten toe te voegen aan de categorie van partiële Booleaanse circuits. Tapes ondersteunen twee monoidale structuren: het tensorproduct ($\otimes$) en de convexe som ($\oplus$). De laatste maakt het modelleren van probabilistische controle mogelijk (bijv. probabilistische vertakking) op een manier die het tensorproduct alleen niet kan.
4. Categoriaal Kader: De semantiek wordt geïnterpreteerd in $KL(D_\le)$, de Kleisli-categorie van de subdistributie-monade. De auteurs maken gebruik van resultaten uit [6] die tape-diagrammen karakteriseren als stochastische matrices van string-diagrammen. Specifiek vertrouwen ze op het feit dat de categorie van tapes $T(C)$ isomorf is aan de categorie van stochastische matrices over de PCA-verrijkte categorie $C^+$ (aangeduid als $StMat(C^+)$).

Belangrijkste Bijdragen

1. Volledige Axiomatisering van Partiële Booleaanse Circuits:
   Het artikel presenteert een volledige set axioma's voor partiële Booleaanse circuits ($Diag_{PB}$). De axioma's breiden de standaard Booleaanse algebra uit met wetten die de "cocopy"-generator beheersen (Figuur 3). De auteurs bewijzen de volledigheid (Theorema 9) door elk partieel circuit te deconstrueren in een "domein"-circuit (dat bepaalt waar de functie gedefinieerd is) en een "totale" circuit (die de outputwaarde bepaalt), waardoor het probleem wordt gereduceerd tot de bekende volledigheid van Booleaanse circuits.

2. Volledige Axiomatisering van Probabilistische Booleaanse Tapes:
   De auteurs bieden een volledige axiomatisering voor probabilistische Booleaanse tapes (Figuren 4 en 5). Dit systeem omvat:

   • Axioma's voor de tape-constructie (natuurlijke en coherente monoïden, co-gepointe convexe algebra's).
   • Specifieke axioma's voor partialiteit (bijv. het gelijkstellen van een mislukte berekening met een nul-distributie).
   • Een cruciaal implicatie-axioma (T3) dat cancellativiteit uitdrukt, een standaard redeneerprincipe in algebraïsche structuren.
     Het volledigheidsbewijs (Corollary 29) berust op de isomorfie tussen tapes en stochastische matrices, waarbij wordt aangetoond dat semantische gelijkheid in $KL(D_\le)$ exact overeenkomt met gelijkheid in de tape-calculus modulo de gedefinieerde axioma's.

3. Reductie van Circuit-gelijkheid naar Tape-gelijkheid:
   Door gebruik te maken van een codering $E(-)$ van probabilistische Booleaanse circuits naar probabilistische Booleaanse tapes (zoals vastgesteld in [8]), demonstreren de auteurs dat het controleren van semantische gelijkheid van circuits gereduceerd kan worden tot het controleren van de gelijkheid van hun tape-coderingen (Corollary 30).

Resultaten

• Soundness en Completeness: Het artikel bewijst dat de voorgestelde axioma-systemen zowel sound als compleet zijn met betrekking tot de semantiek in $KL(D_\le)$.
• Correctie van Voorgaand Werk: De auteurs tonen aan dat de door hen geïnduceerde equivalentie strikt fijner is dan die in [59]. Specifiek demonstreren zij dat de axioma's F2 en F7 uit het vorige systeem onjuist (unsound) zijn, terwijl hun axioma F8 (uit [59]) afleidbaar is binnen hun systeem.
• Expressiviteit van Tapes: Het artikel illustreert dat tapes probabilistische controle natuurlijker kunnen modelleren dan circuits die uitsluitend vertrouwen op $\otimes$. Bijvoorbeeld, een tape kan een probabilistische keuze modelleren tussen een geldige berekening en een falen (nul-gedrag) zonder dat de gehele compositie nul wordt, een beperking die inherent is aan benaderingen die enkel het monoidale product gebruiken.

Significantie
Het artikel claimt significant te zijn door de eerste volledige axiomatisering te bieden voor partiële Booleaanse circuits en een volledige axiomatisering voor probabilistische Booleaanse tapes. Door deze resultaten te vestigen, stellen de auteurs in staat om direct op het niveau van diagrammen te redeneren over de gelijkheid van probabilistische programmering. De verschuiving naar tapes maakt een structureel transparante axiomatisering mogelijk die probabilistische controle en partialiteit uniform behandelt. De auteurs merken op dat hoewel het huidige werk zich richt op eindige probabilistische programmering, het framework (met name het gebruik van traces met $\oplus$) potentieel een algebraïsche basis kan bieden voor probabilistische programmalogica's en de representatie van probabilistische reguliere expressies, hoewel deze worden geïdentificeerd als toekomstige richtingen in plaats van huidige resultaten. Het werk steunt op de "string-diagrammatische" visie waarbij data wordt behandeld als een fysieke bron, wat het vrije kopiëren of weggooien voorkomt, wat centraal staat in de context van probabilistische en kwantumcomputing.