Resumo Técnico: ZX-Calculus

Declaração do Problema

A lógica epistêmica clássica e a semântica operacional padrão enfrentam três limitações fundamentais ao modelar sistemas dinâmicos de evolução de conhecimento:

1. Traços como Meta-Objetos: Traços de execução são tipicamente tratados como objetos de meta-nível em vez de dados de primeira classe dentro do sistema de tipos. Embora a Teoria dos Tipos Homotópicos (HoTT) ofereça caminhos invertíveis e os tipos de sessão caracterizem protocolos, eles carecem de um mecanismo nativo para representar histórias causais direcionadas e não-invertíveis onde a sequência específica de eventos é um constituinte primário do tipo.
2. Monotonicidade vs. Não-Monotonicidade: As teorias de tipos padrão são monotônicas; adicionar informação nunca invalida provas anteriores. No entanto, o conhecimento epistêmico é inerentemente não-monotônico (retratável). Adicionar diretamente regras de prova não-monotônicas a uma teoria de tipos destrói a normalização e a consistência.
3. Revisão AGM Construtiva: As abordagens construtivas existentes para revisão de crenças (ex: em Lógica Epistêmica Dinâmica ou raciocínio não-monotônico) frequentemente carecem de algoritmos executáveis para contração de encontro parcial, falham em empacotar resultados de contração com testemunhas de correção como tipos dependentes, ou operam em estruturas estáticas sem semântica indexada por traço.

Metodologia

O artigo propõe o ZX-Calculus, uma extensão conservativa da Teoria dos Tipos Dependentes de Martin-Löf (MLTT). Ele não altera as regras estruturais principais da MLTT, mas introduz novas estruturas de tipos e interpretações semânticas para integrar três camadas:

1. Tipos Indexados por Traço: Uma família indutiva FinTrace representando traços de execução finitos como objetos construtivos.
2. Semântica de Feixes (Sheaf Semantics): Interpretando proposições indexadas por traço como feixes contravariantes sobre uma categoria de traço livre, permitindo a não-monotonicidade semântica via mapas de restrição não-surjetivos enquanto preserva a monotonicidade da prova.
3. Revisão AGM Construtiva: Uma implementação tipológica de tipos para o framework de revisão de crenças AGM (Alchourrón–Gärdenfors–Makinson), utilizando $\Sigma$-tipos para empacotar conjuntos de crenças com provas construtivas de adesão aos postulados AGM.

O framework é verificado usando uma mecanização em Coq composta por 34 provas completas, com foco específico na falha de composição de feixes em revisão sequencial e na coerência de sistemas de revisão de passo único.

Contribuições Principais

1. Tipos de Traço e Design de Interface

O artigo introduz FinTrace, uma família indutiva de traços finitos entre estados.

• Comparação com Star(Step): Os autores provam que FinTrace é isomórfico ao fechamento de Kleene Star(Step) como coleções de caminhos (Proposição 3.2). No entanto, eles não são julgadamente iguais.
• Vantagem de Interface: O eliminador estrutural TraceElim toma o rótulo do evento e : Event como um parâmetro explícito em sua função de passo. Isso contrasta com StarElim, que requer o desempacotamento de um $\Sigma$-tipo para recuperar a informação do evento. Essa escolha de design eleva a estrutura causal do evento a um componente nativo da indução de traço, facilitando a semântica de feixe orientada a eventos e o replay determinístico.
• Meta-Teoria: O artigo estabelece um framework de Canonicidade via relações lógicas e candidatos de reducibilidade. Uma contribuição técnica crítica é o Lema de Transporte (Lema 3.12), que garante que a reducibilidade é transportada estavelmente sob extensão de traço. A mecanização completa do passo RC-elim para motivos de ordem superior é anotada como trabalho futuro.

2. Semântica de Feixes e Não-Monotonicidade

O artigo interpreta o conhecimento como um pré-feixe sobre a categoria de traço $\mathbf{bTf}$.

• Teorema de Separação: O Teorema 4.5 demonstra uma separação clara entre a monotonicidade de prova (que é preservada) e a não-monotonicidade semântica. A invalidação do conhecimento é modelada como a não-surjetividade dos mapas de restrição, não como contradição lógica.
• CwF Inicial: O modelo de termo é provado como o CwF (Categoria com Famílias) inicial (Teorema 4.8), estabelecendo uma propriedade universal sintática onde a sintaxe determina unicamente a interpretação semântica.

3. Revisão de Crença AGM Construtiva

O artigo fornece o primeiro algoritmo construtivo explícito para contração de encontro parcial em MLTT (Algoritmo 6.3).

• Algoritmo 6.3: Este algoritmo remove iterativamente as crenças de menor entranhamento para satisfazer as condições de contração (C1–C4). Ele é totalmente verificado para habitar o $\Sigma$-tipo Selτ(ψ), que empacota o conjunto de crenças resultante com provas de sua correção.
• Lema de Entranhamento Disjuntivo: O Lema 6.7 fornece uma prova construtiva totalmente autossuficiente de que o entranhamento de uma disjunção é equivalente ao entranhamento máximo de seus disjuntos. Este lema é essencial para provar os complexos postulados AGM R7 e R8.
• Postulados AGM Completos: O artigo prova que o sistema de revisão indexado por traço satisfaz todos os oito postulados clássicos da AGM (Teoremas 6.9–6.12), embarcando a teoria AGM clássica em um framework dinâmico e orientado a eventos.

4. Integração e Coerência

Uma tensão central é identificada: o "princípio da mudança mínima" da revisão AGM é sensível ao caminho, enquanto a semântica de feixe exige composição invariante de caminho (BP-comp).

• Falha de BP-comp: O Teorema 7.1 prova que o funtor de revisão de crença $B_{AGM}$ não é um feixe; a lei de composição falha para a revisão AGM sequencial. Um contramodelo verificado em Coq é forneado.
• Sistemas de Revisão de Passo Único (SSRS): Para resolver isso, o artigo introduz o SSRS (Definição 7.2), uma estrutura mais fraca que descarta restrições de composição global, mas retém atualizações de passo único bem definidas. O Teorema 7.4 prova que $B_{AGM}$ é um SSRS válido, estabelecendo uma integração coerente de traços, feixes e revisão de crença dentro deste framework intermediário.

Resultados e Verificação

• Mecanização em Coq: O artigo inclui uma formalização em Coq com 34 provas completas e zero admits para os resultados de integração central (Teorema da Falha de BP-comp e Coerência do SSRS).
• Status da Prova:
  • Completa: Proposição 3.2, Lemas 3.12/3.13, corretude do Algoritmo 6.3, postulados AGM R1–R8, Lema de Entranhamento Disjuntivo, Falha de BP-comp e Coerência do SSRS.
  • Pendência de Mecanização: O passo RC-elim do Teorema de Canonicidade (Teorema 3.14) é atualmente suportado por um argumento verificado manualmente; a mecanização total é listada como trabalho futuro.

Significância e Alegações

O artigo afirma fornecer uma extensão conservativa da MLTT que unifica rastros históricos, evolução de conhecimento não-monotônica e revisão de crença construtiva sem interromper a estabilidade meta-teórica da teoria de tipos subjacente.

• Unificação: Demonstra que "como o sistema chegou ao seu estado atual" pode ser um constituinte nativo do sistema de tipos, permitindo o raciocínio construtivo sobre propriedades dependentes de histórico.
• Lógica Epistêmica Dinâmica: Ao embarcar a revisão AGM em um framework indexado por traço, o sistema generaliza a teoria AGM clássica para descrever a evolução do conhecimento de agentes cognitivos reais, onde diferentes sequências de eventos induzem diferentes estruturas de entranhamento epistêmico.
• Rigor Fundamental: O trabalho esclarece a tensão estrutural entre a funtorialidade de feixe e a revisão de crença, propondo o SSRS como o modelo categórico correto para sistemas de crença dinâmicos.
• Verificação Construtiva: Diferente da AGM clássica que depende de definições existenciais, este framework fornece algoritmos executáveis e testemunhas construtivas para a contração de crenças, tornando o processo de revisão computacionalmente verificável.

O artigo conclui que o ZX-Calculus oferece uma base verificável para conhecimento dinâmico, mecanismos de retração e monitoramento de tempo de execução, com trabalhos futuros direcionados à completude semântica total, extensões de traço infinitas e conclusão das obrigações restantes do Coq.