Proof Nets for PiL (Full Version)

Resumo Técnico: Redes de Prova para PiL

Declaração do Problema
O artigo aborda o desafio de fornecer uma representação canônica, baseada em grafos, para provas em PiL, um sistema lógico que estende a lógica linear multiplicativa aditiva de primeira ordem (MALL1). PiL foi introduzido para oferecer uma codificação rasa de processos no $\pi$-cálculo, especificamente para provar a completude da programação coreográfica em relação a processos livres de corrida e livres de deadlock.

A dificuldade central reside nos operadores únicos do PiL:

1. O operador $\blacktriangleleft$: Um conectivo não-comutativo, não-associativo e autodual que modela a composição sequencial.
2. Quantificadores Nominais ($\new$ e $\ya$): Quantificadores que modelam ligação de nomes e frescor, exigindo um controle rigoroso do uso de variáveis para garantir que os nomes sejam compartilhados por no máximo um par de quantificadores duais.

As formalizações existentes de redes de prova para MALL (como as redes de Girard ou redes de conflito) lutam com a combinação de aditivos, quantificadores e conectivos não-comutativos/não-associativos. Além disso, as derivações padrão do cálculo de sequentes sofrem de não-canonicidade devido a permutações independentes de regras, o que obscurece a semântica subjacente das árvores de execução de processos. O artigo busca definir redes de prova que colapsem essas permutações em um único objeto sintático, ao mesmo tempo em que lidam com as restrições específicas dos quantificadores nominais e do operador $\blacktriangleleft$.

Metodologia
Os autores adotam redes de conflito como estrutura fundamental, estendendo-as ao cenário de primeira ordem do PiL. A metodologia envolve três componentes principais:

1. Definição de Estrutura (Pré-estruturas e Redes de Prova):

   • Ligações e Dualizadores: Os autores definem ligações (conexões axiomáticas entre sub-sequentes) e as associam a dualizadores (substituições). Dualizadores mapeiam variáveis em uma ligação para testemunhas existenciais ou nominais, impondo dualidade e lidando com a unificação exigida pelos quantificadores.
   • Árvores Coco: A estrutura subjacente é uma "árvore de concordância-conflito" (árvore coco) onde as folhas são ligações e os nós internos são rotulados com relações de concordância ($\smile$) ou conflito ($\#$).
   • Coalescência: Um procedimento de reescrita (coalescência) é definido para reduzir uma estrutura de prova a uma forma trivial (uma única folha). Este processo imita a construção de baixo para cima de uma derivação de sequente. Uma rede de prova é definida como uma estrutura de prova que admite um caminho de coalescência para uma pré-estrutura trivial.

2. Correção e Sequencialização:

   • Um critério de correção em tempo polinomial é estabelecido: uma estrutura é uma rede de prova válida se e somente se for coalescente.
   • Um procedimento de sequencialização é fornecido, que traduz uma rede de prova válida de volta para uma derivação no cálculo de sequentes em PiL. Isso prova a completude da formalização de redes em relação à lógica.
   • Um algoritmo de tradução de prova traduz derivações do PiL em redes de conflito, estabelecendo a correção.

3. Redes de Fatia e Achamento:

   • Para alcançar uma forma mais canônica, os autores introduzem redes de fatia, uma subclasse de redes de conflito onde a árvore coco subjacente é "plana" (contendo no máximo um nó-$\#$ na raiz).
   • Um procedimento de achamento é definido como uma regra de reescrita que move nós de concordância acima de nós de conflito. Os autores provam que o achamento é fortemente normalizante, confluinte e preserva a coalescência. Isso permite que qualquer rede de conflito seja transformada em uma única rede de fatia canônica.

Principais Contribuições

• Definição de Redes de Conflito para PiL: O artigo define a primeira formalização de redes de prova para uma lógica que combina aditivos, quantificadores de primeira ordem e o conectivo não-comutativo/não-associativo $\blacktriangleleft$.
• Correção em Tempo Polinomial: Fornece um critério de correção em tempo polinomial (especificamente $O(n^5)$) baseado na coalescência de árvores coco com mapas de testemunhas.
• Sequencialização e Tradução: Estabelece uma tradução bidirecional entre derivações de sequentes do PiL e redes de prova, provando que as redes são tanto corretas quanto completas.
• Representação Canônica (Redes de Fatia): Introduz redes de fatia e o procedimento de achamento, provando que toda rede de conflito reduz-se a uma única rede de fatia.
• Resultados de Canonicidade: O artigo prova dois níveis distintos de canonicidade:
  • Canonicidade Local: Redes de conflito fornecem uma representação canônica de derivações módulo permutações de regras locais (trocas de regras independentes).
  • Canonicidade Forte: Redes de fatia fornecem uma representação canônica módulo tanto permutações de regras locais quanto não-locais.

Resultados

• Teorema 1: Um sequente $\Gamma$ é provável em PiL se e somente se existir uma rede de conflito para $\Gamma$.
• Teorema 2: O achamento preserva a coalescência, garantindo que a transformação de redes de conflito para redes de fatia mantenha a validade.
• Teorema 3: Um sequente $\Gamma$ é provável em PiL se e somente se existir uma rede de fatia para $\Gamma$.
• Teorema 4:
  • Duas derivações $D$ e $D'$ são localmente equivalentes ($D \approx D'$) se e somente se suas redes de conflito associadas forem isomorfas.
  • Duas derivações $D$ e $D'$ são fortemente equivalentes ($D \simeq D'$) se e somente se suas redes de fatia associadas forem isomorfas.

Significado e Alegações
O artigo alega que as redes de prova para PiL fornecem uma representação canônica de derivações no cálculo de sequentes, efetivamente colapsando classes de derivações que diferem apenas por permutações independentes de regras. Isso é significativo para a semântica dos cálculos de processos porque:

• Alinha-se com a semântica das árvores de execução no $\pi$-cálculo, onde a ordem de ações independentes não deve afetar o significado do processo.
• Distingue entre canonicidade local (relevante onde a ordem de ramificação importa) e canonicidade forte (relevante para equivalências como bisimulação onde a ordem de ramificação é irrelevante).
• Oferece uma base para desenvolver novas ferramentas para estudar a semântica de sistemas concorrentes e coreografias, tratando redes de prova como representantes de árvores de execução, ignorando intercalações irrelevantes enquanto preserva fenômenos observáveis como condições de corrida.

Os autores afirmam explicitamente que não estudam a eliminação de cortes neste trabalho, pois seu foco está em provas sem cortes que representam árvores de computação. Eles observam que a eliminação de cortes para PiL envolve um tratamento não trivial de quantificadores nominais e armazenamentos, o que é deixado para trabalhos futuros. Da mesma forma, embora sugiram que sua estrutura poderia ser estendida para MALL de primeira ordem geral, não alegam ter resolvido o caso geral neste artigo.