A Classical Linear $λ$-Calculus based on Contraposition

Resumo Técnico: Um Cálculo $\lambda$ Linear Clássico baseado na Contraposição

Enunciado do Problema
O artigo aborda o desafio de harmonizar as simetrias clássicas da Lógica Linear (LL) com o formalismo computacional do cálculo $\lambda$. A Lógica Linear exibe fortes simetrias (por exemplo, a dualidade entre regras à esquerda e à direita, negação involutiva onde $\neg\neg A = A$), enquanto as apresentações de dedução natural padrão frequentemente falham em preservar essas simetrias mantendo boas propriedades computacionais como confluência e normalização forte. Os sistemas existentes geralmente se enquadram em duas categorias:

1. Fragmentos intuicionistas: Sistemas como ILL ou DILL restringem a lógica a sequentes de conclusão única, perdendo as simetrias clássicas e a capacidade de modelar certos passos de prova.
2. Sistemas baseados em sequentes: Sistemas derivados do cálculo de sequentes (por exemplo, proof-nets, cálculo de processos) preservam as simetrias, mas frequentemente tratam provas como processos paralelos em vez de programas funcionais, tornando-os menos adequados para paradigmas de programação funcional.

Especificamente, os autores observam que, na lógica clássica, afirmar uma proposição $A$ como uma tese é equivalente a negá-la como uma hipótese. No contexto da Lógica Linear, isso implica que $A \multimap B$ e $B^\perp \multimap A^\perp$ devem compartilhar as mesmas provas. No entanto, os cálculos $\lambda$ padrão para a lógica clássica (como o $\lambda\mu$ de Parigot) são confluentes, mas não simétricos (a negação não é involutiva), enquanto sistemas simétricos (como os de Barbanera e Berardi) frequentemente carecem de confluência. O artigo busca um sistema de dedução natural de conclusão única para a Lógica Linear Exponencial Multiplicativa (MELL) que retenha as simetrias clássicas e desfrute das propriedades padrão de linguagens de programação tipadas.

Metodologia
Os autores propõem uma nova atribuição de termos para MELL, denominada cálculo $\lambda$MELL, fundamentada no paradigma "proposições-como-tipos". A metodologia central envolve:

1. Fundação Lógica: Partindo do fragmento intuicionista da Lógica Linear Multiplicativa (MLL), os autores introduzem uma regra de modus tollens linear. Enquanto a eliminação padrão de implicação linear (modus ponens) permite derivar $B$ de $A \multimap B$ e $A$, a nova regra permite derivar $A^\perp$ de $A \multimap B$ e $B^\perp$. Esta adição recupera a MLL clássica.
2. Operação Inovadora: Contra-Substituição: Para fornecer uma interpretação computacional para a regra do modus tollens, os autores definem uma nova operação chamada contra-substituição, denotada por $t\{a \backslash s\}$.
   • Intuição: Se a substituição padrão $t\{a := s\}$ substitui uma ocorrência única da variável $a$ em $t$ por $s$, a contra-substituição "agarra" a ocorrência única de $a$ em $t$ e "puxa" dela, efetivamente virando o termo $t$ "do avesso" (como uma meia) antes de substituir $a$ por $s$.
   • Mecanismo: Esta operação é definida por indução estrutural em termos lineares. Por exemplo, se $t = \langle u, a \rangle$ e $s : A \multimap B^\perp$, então $\langle u, a \rangle\{a \backslash s\}$ resulta em $s \bullet u : B^\perp$.
3. Construção do Cálculo: O cálculo inclui construtos lineares padrão (tensor, implicação linear, abstração lambda) juntamente com o novo contra-aplicação ($t \blacktriangledown s$), que corresponde à eliminação do modus tollens. Para MELL, o cálculo é estendido para incluir modalidades exponenciais ($!$ e $?$) e unidades, exigindo uma definição refinada de linearidade e uma relação de equivalência estrutural.
4. Equivalência Estrutural: Para garantir a confluência na presença de exponenciais e caminhos de redução complexos, os autores definem uma equivalência estrutural ($\equiv$) que atua como uma bisimulação forte em relação à pré-redução. Esta equivalência inclui axiomas para propagar eliminadores e lidar com unidades (por exemplo, $t[\star := s] \equiv s[\star := t]$ para termos do tipo 1).

Principais Contribuições

1. O Cálculo $\lambda$MELL: Uma apresentação de dedução natural de um lado para MELL onde as provas são modeladas como expressões funcionais. Ele introduz o construto de contra-aplicação e a operação de contra-substituição.
2. Correção e Completude: Os autores provam que o cálculo é correto e completo em relação à MELL. Especificamente, qualquer sequente válido de MELL pode ser lido como um juízo de tipagem em $\lambda$MELL ao selecionar qualquer fórmula como tese e as negações das outras como hipóteses.
3. Propriedades Metateóricas: O cálculo satisfaz as propriedades padrão de uma linguagem de programação tipada:
   • Redução de Sujeito: A redução preserva a tipagem.
   • Confluência: A relação de redução é confluente (módulo equivalência estrutural).
   • Normalização Forte: Toda sequência de redução termina.
4. Codificação de Sistemas Clássicos: O artigo demonstra que várias atribuições de termos bem conhecidas para a lógica clássica podem ser codificadas em $\lambda$MELL, incluindo:
   • O cálculo $\lambda\mu$ de Parigot (via traduções T e Q).
   • O cálculo $\lambda\mu\tilde{\mu}$ de Curien e Herbelin.
   • O $\mu$DCLL de Hasegawa.

Resultados
Os resultados primários são as provas das propriedades metateóricas. Os autores estabelecem a normalização forte usando a técnica de candidatos de reducibilidade, definindo conjuntos de termos associados a cada tipo. A confluência é provada via o Lema de Newman, estabelecendo a confluência local, que depende da equivalência estrutural atuando como uma bisimulação forte para a pré-redução. O artigo também fornece provas construtivas para a completude do cálculo, mostrando como recuperar termos de derivações de MLL sem cortes.

Significância
O artigo afirma sua significância ao oferecer uma interpretação "funcional" da lógica linear clássica que preserva suas simetrias inerentes sem recorrer a cálculos de processos ou dedução natural de múltiplos conclusões. Ao introduzir a contra-substituição, os autores fornecem um mecanismo para lidar computacionalmente com o princípio clássico da contraposição dentro de um framework de conclusão única. Este trabalho sugere uma base para linguagens de programação funcional linear e assistentes de prova que possam suportar nativamente o raciocínio clássico e a sensibilidade de recursos. Os autores observam que estender a abordagem para conectivos aditivos é não trivial devido à dependência da linearidade para a contra-substituição, mas o sistema atual lida com sucesso com os fragmentos multiplicativos e exponenciais. O trabalho preenche a lacuna entre a simetria do cálculo de sequentes e a natureza funcional dos cálculos $\lambda$.