Completeness for Probabilistic Boolean Tapes

Résumé Technique : Complétude pour les Rubans Booléens Probabilistes

Énoncé du Problème
L'article traite du défi consistant à fournir une axiomatisation équationnelle complète pour la sémantique des circuits booléens probabilistes. Bien que des circuits booléens probabilistes aient été proposés comme fondement diagrammatique par cordes pour la programmation probabiliste finie, les tentatives précédentes d'axiomatisation (spécifiquement dans [59]) étaient incomplètes. L'équivalence induite dans les travaux précédents était strictement plus grossière que l'égalité sémantique ; elle identifiait les diagrammes $c$ et $d$ si leurs sémantiques étaient proportionnelles ($\langle\langle c \rangle\rangle \propto \langle\langle d \rangle\rangle$), plutôt que strictement égales. Par conséquent, certains axiomes dans les travaux précédents étaient infondés par rapport à la sémantique standard basée sur les noyaux de Markov (subdistributions). De plus, l'article note que les circuits booléens partiels (circuits pouvant échouer à produire une sortie) n'avaient pas été axiomatisés auparavant.

Méthodologie
Les auteurs emploient une approche par étapes, passant de structures plus simples au langage probabiliste complet, en exploitant la théorie des diagrammes de cordes et la théorie des catégories :

1. Circuits Booléens ($Diag_B$) : Les auteurs rappellent d'abord la représentation standard par diagrammes de cordes des circuits booléens, interprétés comme des morphismes dans la catégorie des ensembles et des fonctions. Ils s'appuient sur la complétude connue des axiomes de l'algèbre de Boole pour ce fragment.
2. Circuits Booléens Partiels ($Diag_{PB}$) : Les auteurs étendent la signature pour inclure un générateur de « cocopie » (noté $\cap$), qui agit comme le dual du générateur de « copie ». Ce générateur compare deux entrées et produit une valeur uniquement si elles concordent ; sinon, il ne produit aucune sortie (indéfini). Cela modélise les fonctions partielles. Les auteurs définissent une nouvelle théorie monoïdale $PB$ étendant l'algèbre de Boole avec des axiomes régissant cette partialité (associativité, commutativité, idempotence et lois de Frobenius).
3. Rubans Booléens Probabilistes ($T(Diag_{PB})$) : Plutôt que d'axiomatiser directement le langage complet des circuits probabilistes ($Diag_{PrB}$), les auteurs introduisent des « rubans booléens probabilistes ». Ce formalisme est construit en ajoutant librement des biproducts convexes à la catégorie des circuits booléens partiels. Les rubans supportent deux structures monoïdales : le produit tensoriel ($\otimes$) et la somme convexe ($\oplus$). Cette dernière permet de modéliser le contrôle probabiliste (par exemple, le branchement probabiliste) d'une manière que le produit tensoriel seul ne peut pas faire.
4. Cadre Catégorique : La sémantique est interprétée dans $KL(D_\le)$, la catégorie de Kleisli du monade de subdistribution. Les auteurs utilisent les résultats de [6] caractérisant les diagrammes de rubans comme des matrices stochastiques de diagrammes de cordes. Plus précisément, ils s'appuient sur le fait que la catégorie des rubans $T(C)$ est isomorphe à la catégorie des matrices stochastiques sur la catégorie enrichie PCA $C^+$ (notée $StMat(C^+)$).

Contributions Clés

1. Axiomatisation Complète des Circuits Booléens Partiels :
   L'article présente un ensemble complet d'axiomes pour les circuits booléens partiels ($Diag_{PB}$). Les axiomes étendent l'algèbre de Boole standard avec des lois régissant le générateur de « cocopie » (Figure 3). Les auteurs prouvent la complétude (Théorème 9) en décomposant tout circuit partiel en un circuit « domaine » (déterminant où la fonction est définie) et un circuit « total » (déterminant la valeur de sortie), réduisant ainsi le problème à la complétude connue des circuits booléens.

2. Axiomatisation Complète des Rubans Booléens Probabilistes :
   Les auteurs fournissent une axiomatisation complète pour les rubans booléens probabilistes (Figures 4 et 5). Ce système inclut :

   • Des axiomes pour la construction des rubans (monoïdes naturels et cohérents, algèbres convexes pointées).
   • Des axiomes spécifiques pour la partialité (par exemple, équater une exécution échouée avec une distribution nulle).
   • Une implication cruciale (T3) exprimant la cancellativité, un principe de raisonnement standard dans les structures algébriques.
     La preuve de complétude (Corollaire 29) repose sur l'isomorphisme entre les rubans et les matrices stochastiques, montrant que l'égalité sémantique dans $KL(D_\le)$ correspond exactement à l'égalité dans le calcul des rubans modulo les axiomes définis.

3. Réduction de l'Égalité des Circuits à l'Égalité des Rubans :
   En utilisant un encodage $E(-)$ des circuits booléens probabilistes vers les rubans booléens probabilistes (tel qu'établi dans [8]), les auteurs démontrent que vérifier l'égalité sémantique des circuits revient à vérifier l'égalité de leurs encodages en rubans (Corollaire 30).

Résultats

• Correction et Complétude : L'article prouve que les systèmes d'axiomes proposés sont à la fois sains et complets par rapport à la sémantique dans $KL(D_\le)$.
• Correction des Travaux Précédents : Les auteurs montrent que l'équivalence induite par leur système est strictement plus fine que celle de [59]. Plus précisément, ils démontrent que les axiomes F2 et F7 du système précédent sont infondés, tandis que leur axiome F8 (issu de [59]) est dérivable dans leur système.
• Expressivité des Rubans : L'article illustre que les rubans peuvent modéliser le contrôle probabiliste plus naturellement que les circuits reposant uniquement sur $\otimes$. Par exemple, un ruban peut modéliser un choix probabiliste entre une exécution valide et un échec (comportement nul) sans que l'ensemble de la composition ne devienne nul, une limitation inhérente aux approches utilisant uniquement le produit monoïdal.

Signification
L'article affirme sa signification en fournissant la première axiomatisation complète pour les circuits booléens partiels et une axiomatisation complète pour les rubans booléens probabilistes. En établissant ces résultats, les auteurs permettent un raisonnement équationnel direct au niveau des diagrammes pour la programmation probabiliste. Le passage aux rubans permet une axiomatisation structurellement transparente qui gère le contrôle probabiliste et la partialité de manière uniforme. Les auteurs notent que bien que le présent travail se concentre sur la programmation probabiliste finie, le cadre (spécifiquement l'utilisation de traces avec $\oplus$) pourrait potentiellement fournir des fondements algébriques pour les logiques de programmes probabilistes et la représentation d'expressions régulières probabilistes, bien que ceux-ci soient identifiés comme des directions futures plutôt que comme des résultats actuels. Le travail repose sur la vue « diagrammatique par cordes » où les données sont traitées comme une ressource physique, empêchant la copie ou la suppression libre, ce qui est central dans les contextes de l'informatique probabiliste et quantique.