Completeness for Probabilistic Boolean Tapes

Sintesi Tecnica: Completezza per i Nastro Booleani Probabilistici

Enunciato del Problema
Il saggio affronta la sfida di fornire un'assiomatizzazione equazionale completa per la semantica dei circuiti booleani probabilistici. Sebbene i circuiti booleani probabilistici siano stati proposti come una base diagrammatica a stringhe per la programmazione probabilistica finita, i precedenti tentativi di assiomatizzazione (specificamente in [59]) erano incompleti. L'equivalenza indotta nel lavoro precedente era strettamente più grossolana della uguaglianza semantica; identificava i diagrammi $c$ e $d$ se le loro sematiche erano proporzionali ($\langle\langle c \rangle\rangle \propto \langle\langle d \rangle\rangle$), piuttosto che strettamente uguali. Di conseguenza, alcuni assiomi nei lavori precedenti erano non corretti rispetto alla semantica standard basata su kernel di Markov (subdistribuzioni). Inoltre, il saggio nota che i circuiti booleani parziali (circuiti che possono non produrre un output) non erano stati precedentemente assiomatizzati.

Metodologia
Gli autori impiegano un approccio a stadi, passando da strutture più semplici al linguaggio probabilistico completo, sfruttando la teoria dei diagrammi a stringhe e la teoria delle categorie:

1. Circuiti Booleani ($Diag_B$): Gli autori richiamano prima la standard rappresentazione diagrammatica a stringhe dei circuiti booleani, interpretata come morfismi nella categoria degli insiemi e delle funzioni. Si affidano alla nota completezza degli assiomi dell'algebra booleana per questo frammento.
2. Circuiti Booleani Parziali ($Diag_{PB}$): Gli autori estendono la firma includendo un generatore di "cocopia" (denotato $\cap$), che agisce come il duale del generatore di "copia". Questo generatore confronta due input e produce un output solo se concordano; altrimenti, non produce alcun output (indefinito). Questo modella le funzioni parziali. Gli autori definiscono una nuova teoria monoidale $PB$ che estende l'algebra booleana con assiomi che governano questa parzialità (associatività, commutatività, idempotenza e leggi di Frobenius).
3. Nastri Booleani Probabilistici ($T(Diag_{PB})$): Invece di assiomatizzare direttamente il linguaggio completo dei circuiti probabilistici ($Diag_{PrB}$), gli autori introducono i "nastri booleani probabilistici". Questo formalismo è costruito aggiungendo liberamente biprodotti convessi alla categoria dei circuiti booleani parziali. I nastri supportano due strutture monoidali: il prodotto tensoriale ($\otimes$) e la somma convessa ($\oplus$). Quest'ultima permette di modellare il controllo probabilistico (ad esempio, il branching probabilistico) in un modo che il solo prodotto tensoriale non può fare.
4. Framework Categoriale: La semantica è interpretata in $KL(D_\le)$, la categoria di Kleisli del monade di subdistribuzione. Gli autori utilizzano i risultati di [6] che caratterizzano i diagrammi a nastro come matrici stocastiche di diagrammi a stringhe. Specificamente, si affidano al fatto che la categoria dei nastri $T(C)$ è isomorfa alla categoria delle matrici stocastiche sui $PCA$-enriched category $C$ (denotata $StMat(C^+)$).

Contributi Chiave

1. Assiomatizzazione Completa dei Circuiti Booleani Parziali:
   Il saggio presenta un insieme completo di assiomi per i circuiti booleani parziali ($Diag_{PB}$). Gli assiomi estendono la standard algebra booleana con leggi che governano il generatore di "cocopia" (Figura 3). Gli autori dimostrano la completezza (Teorema 9) decomponendo qualsiasi circuito parziale in un circuito "dominio" (che determina dove la funzione è definita) e un circuito "totale" (che determina il valore di output), riducendo il problema alla nota completezza dei circuiti booleani.

2. Assiomatizzazione Completa dei Nastri Booleani Probabilistici:
   Gli autori forniscono un'assiomatizzazione completa per i nastri booleani probabilistici (Figure 4 e 5). Questo sistema include:

   • Assiomi per la costruzione del nastro (monoidi naturali e coerenti, algebre co-puntate).
   • Assiomi specifici per la parzialità (ad esempio, equiparare un fallimento del calcolo a una distribuzione nulla).
   • Un cruciale assioma di implicazione (T3) che esprime la cancellatività, un principio di ragionamento standard nelle strutture algebriche.
     La prova di completezza (Corollario 29) si basa sull'isomorfismo tra nastri e matrici stocastiche, mostrando che l'uguaglianza semantica in $KL(D_\le)$ corrisponde esattamente all'uguaglianza nel calcolo dei nastri modulo gli assiomi definiti.

3. Riduzione dell'Uguaglianza dei Circuiti all'Uguaglianza dei Nastri:
   Utilizzando una codifica $E(-)$ dai circuiti booleani probabilistici ai nastri booleani probabilistici (come stabilito in [8]), gli autori dimostrano che verificare l'uguaglianza semantica dei circuiti si riduce al controllo dell'uguaglianza delle loro codifiche a nastro (Corollario 30).

Risultati

• Correttezza e Completezza: Il saggio dimostra che i sistemi di assiomi proposti sono sia corretti che completi rispetto alla semantica in $KL(D_\le)$.
• Correzione del Lavoro Precedente: Gli autori mostrano che l'equivalenza indotta dal loro sistema è strettamente più fine di quella in [59]. Nello specifico, dimostrano che gli assiomi F2 e F7 del sistema precedente sono non corretti, mentre il loro assioma F8 (da [59]) è derivabile all'interno del loro sistema.
• Espressività dei Nastri: Il saggio illustra come i nastri possano modellare il controllo probabilistico in modo più naturale rispetto ai circuiti che si affidano esclusivamente a $\otimes$. Ad esempio, un nastro può modellare una scelta probabilistica tra un calcolo valido e un fallimento (comportamento nullo) senza che l'intero composto diventi nullo, un limite inerente agli approcci che utilizzano solo il prodotto monoidale.

Significatività
Il saggio rivendica la sua significatività fornendo la prima assiomatizzazione completa per i circuiti booleani parziali e un'assiomatizzazione completa per i nastri booleani probabilistici. Stabilendo questi risultati, gli autori consentono il ragionamento equazionale direttamente al livello dei diagrammi per la programmazione probabilistica. Il passaggio ai nastri permette un'assiomatizzazione strutturalmente trasparente che gestisce il controllo probabilistico e la parzialità in modo uniforme. Gli autori osservano che, sebbene il presente lavoro si concentri sulla programmazione probabilistica finita, il framework (specificamente l'uso di tracce con $\oplus$) potrebbe potenzialmente fornire basi algebriche per le logiche di programmi probabilistici e la rappresentazione di espressioni regolari probabilistiche, sebbene queste siano identificate come direzioni future piuttosto che risultati attuali. Il lavoro si basa sulla visione "diagrammatica a stringhe" in cui i dati sono trattati come una risorsa fisica, impedendo la copia o lo scarto libero, un aspetto centrale nei contesti dell'informatica probabilistica e quantistica.