Completeness for Probabilistic Boolean Tapes

Resumen Técnico: Completitud para Cintas Booleanas Probabilísticas

Planteamiento del Problema
El artículo aborda el desafío de proporcionar una axiomatización ecuacional completa para la semántica de los circuitos booleanos probabilísticos. Aunque se han propuesto circuitos booleanos probabilísticos como un fundamento de diagramas de cuerdas para la programación probabilística finita, los intentos previos de axiomatización (específicamente en [59]) fueron incompletos. La equivalencia inducida en trabajos previos era estrictamente más gruesa que la igualdad semántica; identificaba diagramas $c$ y $d$ si sus semánticas eran proporcionales ($\langle\langle c \rangle\rangle \propto \langle\langle d \rangle\rangle$), en lugar de estrictamente iguales. En consecuencia, ciertos axiomas en trabajos anteriores eran unsound (no válidos) con respecto a la semántica estándar basada en núcleos de Markov (subdistribuciones). Además, el artículo señala que los circuitos booleanos parciales (circuitos que pueden fallar al producir una salida) no habían sido axiomatizados previamente.

Metodología
Los autores emplean un enfoque por etapas, moviéndose desde estructuras más simples hacia el lenguaje probabilístico completo, aprovechando la teoría de diagramas de cuerdas y la teoría de categorías:

1. Circuitos Booleanos ($Diag_B$): Los autores recuerdan primero la representación estándar de diagramas de cuerdas de los circuitos booleanos, interpretados como morfismos en la categoría de conjuntos y funciones. Se apoyan en la completitud conocida de los axiomas del álgebra booleana para este fragmento.
2. Circuitos Booleanos Parciales ($Diag_{PB}$): Los autores extienden la firma para incluir un generador de "cocopia" (denotado $\cap$), que actúa como el dual del generador de "copia". Este generador compara dos entradas y produce un valor solo si coinciden; de lo contrario, no produce salida (indefinido). Esto modela funciones parciales. Los autores definen una nueva teoría monoidal $PB$ que extiende el álgebra booleana con axiomas que gobiernan esta parcialidad (asociatividad, conmutatividad, idempotencia y leyes de Frobenius).
3. Cintas Booleanas Probabilísticas ($T(Diag_{PB})$): En lugar de axiomatizar directamente el lenguaje completo de circuitos probabilísticos ($Diag_{PrB}$), los autores introducen "cintas booleanas probabilísticas". Este formalismo se construye añadiendo libremente biproductos convexos a la categoría de circuitos booleanos parciales. Las cintas soportan dos estructuras monoidales: el producto tensorial ($\otimes$) y la suma convexa ($\oplus$). Esta última permite modelar el control probabilístico (por ejemplo, ramificación probabilística) de una manera que el producto tensorial por sí solo no puede.
4. Marco Categórico: La semántica se interpreta en $KL(D_\le)$, la categoría de Kleisli del monad de subdistribución. Los autores utilizan resultados de [6] que caracterizan los diagramas de cintas como matrices estocásticas de diagramas de cuerdas. Específicamente, se apoyan en el hecho de que la categoría de cintas $T(C)$ es isomórfica a la categoría de matrices estocásticas sobre la categoría enriquecida con PCA $C^+$ (denotada $StMat(C^+)$).

Contribuciones Clave

1. Axiomatización Completa de Circuitos Booleanos Parciales:
   El artículo presenta un conjunto completo de axiomas para los circuitos booleanos parciales ($Diag_{PB}$). Los axiomas extienden el álgebra booleana estándar con leyes que gobiernan el generador de "cocopia" (Figura 3). Los autores demuestran la completitud (Teorema 9) descomponiendo cualquier circuito parcial en un circuito de "dominio" (que determina dónde está definida la función) y un circuito "total" (que determina el valor de salida), reduciendo el problema a la completitud conocida de los circuitos booleanos.

2. Axiomatización Completa de Cintas Booleanas Probabilísticas:
   Los autores proporcionan una axiomatización completa para las cintas booleanas probabilísticas (Figuras 4 y 5). Este sistema incluye:

   • Axiomas para la construcción de cintas (monoides naturales y coherentes, álgebras convexas con punto).
   • Axiomas específicos para la parcialidad (por ejemplo, igualar un fallo de computación con una distribución nula).
   • Un axioma de implicación crucial (T3) que expresa la cancelatividad, un principio de razonamiento estándar en estructuras algebraicas.
     La prueba de completitud (Corolario 29) se basa en el isomorfismo entre cintas y matrices estocásticas, mostrando que la igualdad semántica en $KL(D_\le)$ corresponde exactamente a la igualdad en el cálculo de cintas módulo los axiomas definidos.

3. Reducción de la Igualdad de Circuitos a la Igualdad de Cintas:
   Al utilizar una codificación $E(-)$ de circuitos booleanos probabilísticos a cintas booleanas probabilísticas (como se establece en [8]), los autores demuestran que verificar la igualdad semántica de los circuitos se reduce a verificar la igualdad de sus codificaciones de cintas (Corolario 30).

Resultos

• Validez y Completitud: El artículo demuestra que los sistemas de axiomas propuestos son tanto válidos (sound) como completos (complete) con respecto a la semántica en $KL(D_\le)$.
• Corrección de Trabajo Previo: Los autores muestran que la equivalencia inducida por su sistema es estrictamente más fina que la de [59]. Específicamente, demuestran que los axiomas F2 y F7 del sistema anterior son unsound, mientras que su axioma F8 (de [59]) es derivable dentro de su sistema.
• Expresividad de las Cintas: El artículo ilustra que las cintas pueden modelar el control probabilístico de manera más natural que los circuitos que dependen únicamente de $\otimes$. Por ejemplo, una cinta puede modelar una elección probabilística entre una computación válida y un fallo (comportamiento nulo) sin que toda la composición se vuelva nula, una limitación inherente a los enfoques que usan solo el producto monoidal.

Significancia
El artículo afirma su significancia al proporcionar la primera axiomatización completa para circuitos booleanos parciales y una axiomatización completa para cintas booleanas probabilísticas. Al establecer estos resultados, los autores permiten el razonamiento ecuacional directamente al nivel de diagramas para la programación probabilística. El cambio hacia las cintas permite una axiomatización estructuralmente transparente que maneja el control probabilístico y la parcialidad de manera uniforme. Los autores señalan que, aunque el trabajo actual se centra en la programación probabilística finita, el marco (específicamente el uso de trazas con $\oplus$) podría potencialmente proporcionar bases algebraicas para lógicas de programas probabilísticos y la representación de expresiones regulares probabilísticas, aunque estas se identifican como direcciones futuras más que resultados actuales. El trabajo se apoya en la visión de "diagramas de cuerdas" donde los datos se tratan como un recurso físico, lo que impide la copia o el descarte libre, algo central en los contextos de computación probabilística y cuántica.