Completeness for Probabilistic Boolean Tapes

Resumo Técnico: Completude para Fitas Booleanas Probabilísticas

Problema
O artigo aborda o desafio de fornecer uma axiomatização equacional completa para a semântica de circuitos booleanos probabilísticos. Embora circuitos booleanos probabilísticos tenham sido propostos como uma fundação de diagramas de cordas para programação probabilística finita, tentativas anteriores de axiomatização (especificamente em [59]) foram incompletas. A equivalência induzida em trabalhos anteriores era estritamente mais grosseira que a igualdade semântica; ela identificava diagramas $c$ e $d$ se suas semânticas fossem proporcionais ($\langle\langle c \rangle\rangle \propto \langle\langle d \rangle\rangle$), em vez de estritamente iguais. Consequentemente, certos axiomas em trabalhos anteriores eram inconsistentes com respeito à semântica padrão baseada em núcleos de Markov (subdistribuições). Além disso, o artigo observa que circuitos booleanos parciais (circuitos que podem falhar ao produzir uma saída) não haviam sido axiomatizados anteriormente.

Metodologia
Os autores empregam uma abordagem em estágios, movendo-se de estruturas mais simples para a linguagem probabilística completa, aproveitando a teoria de diagramas de cordas e a teoria das categorias:

1. Circuitos Booleanos ($Diag_B$): Os autores primeiro recordam a representação padrão de diagramas de cordas para circuitos booleanos, interpretados como morfismos na categoria de conjuntos e funções. Eles dependem da completude conhecida dos axiomas da álgebra booleana para este fragmento.
2. Circuitos Booleanos Parciais ($Diag_{PB}$): Os autores estendem a assinatura para incluir um gerador de "cocópia" (denotado por $\cap$), que atua como o dual do gerador de "cópia". Este gerador compara duas entradas e produz uma saída apenas se elas concordarem; caso contrário, não produz saída (indefinido). Isso modela funções parciais. Os autores definem uma nova teoria monoidal $PB$ estendendo a álgebra booleana com axiomas que governam esta parcialidade (associatividade, comutatividade, idempotência e leis de Frobenius).
3. Fitas Booleanas Probabilísticas ($T(Diag_{PB})$): Em vez de axiomatizar diretamente a linguagem completa de circuitos probabilísticos ($Diag_{PrB}$), os autores introduzem "fitas booleanas probabilísticas". Este formalismo é construído adicionando livremente biprodutos convexos à categoria de circuitos booleanos parciais. As fitas suportam duas estruturas monoidais: o produto tensorial ($\otimes$) e a soma convexa ($\oplus$). Esta última permite modelar o controle probabilístico (por exemplo, ramificação probabilística) de uma forma que o produto tensorial sozinho não consegue.
4. Estrutura Categórica: A semântica é interpretada em $KL(D_\le)$, a categoria de Kleisli do monad de subdistribuição. Os autores utilizam resultados de [6] que caracterizam diagramas de fitas como matrizes estocásticas de diagramas de cordas. Especificamente, eles dependem do fato de que a categoria de fitas $T(C)$ é isomórfica à categoria de matrizes estocásticas sobre a categoria enriquecida em PCA $C^+$ (denotada $StMat(C^+)$).

Principais Contribuições

1. Axiomatização Completa de Circuitos Booleanos Parciais:
   O artigo apresenta um conjunto completo de axiomas para circuitos booleanos parciais ($Diag_{PB}$). Os axiomas estendem a álgebra booleana padrão com leis que governam o gerador de "cocópia" (Figura 3). Os autores provam a completude (Teorema 9) decompondo qualquer circuito parcial em um circuito de "domínio" (que determina onde a função é definida) e um circuito "total" (que determina o valor da saída), reduzindo o problema à completude conhecida dos circuitos booleanos.

2. Axiomatização Completa de Fitas Booleanas Probabilísticas:
   Os autores fornecem uma axiomatização completa para fitas booleanas probabilísticas (Figuras 4 e 5). Este sistema inclui:

   • Axiomas para a construção de fitas (monoides naturais e coerentes, álgebras convexas apontadas).
   • Axiomas específicos para parcialidade (por exemplo, igualar uma computação falha a uma distribuição nula).
   • Um axioma de implicação crucial (T3) que expressa cancelabilidade, um princípio de raciocínio padrão em estruturas algébricas.
     A prova de completude (Corolário 29) baseia-se no isomorfismo entre fitas e matrizes estocásticas, mostrando que a igualdade semântica em $KL(D_\le)$ corresponde exatamente à igualdade no cálculo de fitas módulo os axiomas definidos.

3. Redução da Igualdade de Circuitos para Igualdade de Fitas:
   Ao utilizar uma codificação $E(-)$ de circuitos booleanos probabilísticos para fitas booleanas probabilísticas (conforme estabelecido em [8]), os autores demonstram que verificar a igualdade semântica de circuitos reduz-se a verificar a igualdade de suas codificações de fita (Corolário 30).

Resultos

• Consistência e Completude: O artigo prova que os sistemas de axiomas propostos são tanto consistentes quanto completos com respeito à semântica em $KL(D_\le)$.
• Correção de Trabalho Anterior: Os autores mostram que a equivalência induzida pelo seu sistema é estritamente mais fina que a de [59]. Especificamente, eles demonstram que os axiomas F2 e F7 do sistema anterior são inconsistentes, enquanto o seu axioma F8 (de [59]) é derivável dentro do seu sistema.
• Expressividade das Fitas: O artigo ilustra que as fitas podem modelar o controle probabilístico de forma mais natural do que os circuitos que dependem apenas de $\otimes$. Por exemplo, uma fita pode modelar uma escolha probabilística entre uma computação válida e uma falha (comportamento nulo) sem que toda a composição se torne nula, uma limitação inerente às abordagens que utilizam apenas o produto monoidal.

Significância
O artigo afirma sua significância ao fornecer a primeira axiomatização completa para circuitos booleanos parciais e uma axiomatização completa para fitas booleanas probabilísticas. Ao estabelecer estes resultados, os autores permitem o raciocínio equacional diretamente ao nível de diagramas para programação probabilística. A mudança para fitas permite uma axiomatização estruturalmente transparente que lida com controle probabilístico e parcialidade de forma uniforme. Os autores observam que, embora o trabalho atual se concentre em programação probabilística finita, o arcabouço (especificamente o uso de traços com $\oplus$) poderia potencialmente fornecer bases algébricas para lógicas de programas probabilísticos e a representação de expressões regulares probabilísticas, embora estas sejam identificadas como direções futuras e não resultados atuais. O trabalho baseia-se na visão de "diagramas de cordas", onde os dados são tratados como um recurso físico, impedindo a cópia ou o descarte livre, o que é central para contextos de computação probabilística e quântica.