Ordered Adjoint Logic (Extended Version)

Resumo Técnico de "Lógica Adjunta Ordenada"

Enunciado do Problema
Lógicas ordenadas e sistemas de tipos são essenciais para aplicações que vão desde a linguística computacional até a aplicação de protocolos de segurança, onde a ordem de uso dos recursos é significativa. Na maioria das formulações, os tipos ordenados são também lineares, exigindo que os recursos sejam usados exatamente uma vez. Embora trabalhos anteriores de Kanovich et al. tenham investigado cálculos que relaxam essa restrição via subexponenciais dentro de uma lógica ordenada linear, essa abordagem depende de um "modo base" onde todas as inferências ocorrem. Para lógicas ordenadas, esse modo base deve proibir todas as regras estruturais (enfraquecimento, contração, troca), forçando as aplicações a alternar frequentemente para dentro e para fora desse modo restritivo. Além disso, os sistemas de subexponenciais existentes não exploram plenamente a possibilidade de propriedades estruturais unilaterais (por exemplo, mobilidade à esquerda sem mobilidade à direita). Os autores visam generalizar essas estruturas para suportar uma pré-ordem de modos com propriedades estruturais variadas e de granularidade fina — incluindo controle independente sobre enfraquecimento, contração à esquerda/direita e mobilidade à esquerda/direita — sem depender de um único modo base restritivo.

Metodologia
Os autores introduzem a Lógica Adjunta Ordenada, um sistema que combina a flexibilidade estrutural das modalidades adjuntas com as restrições de ordenação das lógicas ordenadas. A metodologia prossegue em duas etapas principais:

1. Formulação do Cálculo de Sequente:
   Os autores definem um cálculo de sequente onde os antecedentes são sequências ordenadas de hipóteses rotuladas. As regras estruturais não são globais, mas governadas por uma pré-ordem de modos ($k \geq m$). Cada modo $m$ está associado a um conjunto de propriedades estruturais $\sigma(m) \subseteq \{W, C, M_{\leftarrow}, M_{\rightarrow}\}$ (Enfraquecimento, Contração, Mobilidade à Esquerda, Mobilidade à Direita).

   • Modalidades de Deslocamento: Em vez de um modo base, o sistema usa modalidades de deslocamento ($\downarrow^k_m$ e $\uparrow^m_l$) para alternar entre raciocínio em modos diferentes. Esses deslocamentos são derivados da lógica adjunta de Benton, mas generalizados para lidar com contextos ordenados.
   • Regras Estruturais: Os autores decompõem a mobilidade e a contração em variantes unilaterais. As regras de mobilidade permitem que uma única proposição se mova arbitrariamente para a esquerda ou para a direita dentro da sequência de antecedentes, desde que o modo da proposição admita a mobilidade direcional correspondente. A contração é permitida de forma não local (fundindo duplicatas não adjacentes) para garantir a eliminação do corte, distinguindo-se da contração local na lógica linear padrão.
   • Conectivos Lógicos: A linguagem inclui implicações ordenadas ($\multimap$ e $\multimap$), conjunções fundidas e torcidas, e deslocamentos. As regras são paramétricas em seus modos, com condições específicas garantindo a preservação da independência de modos (por exemplo, $k \geq m \geq r$) ao ler as regras da conclusão para as premissas.

2. Dedução Natural e Decidibilidade:
   Os autores transitam para uma formulação de dedução natural onde as regras estruturais são implícitas, visando uma fundação adequada para linguagens de programação.

   • Explícito vs. Implícito: Inicialmente, eles apresentam um sistema com regras estruturais explícitas para fazer a ponte com o cálculo de sequente. Em seguida, definem um sistema onde as regras estruturais (enfraquecimento, contração, mobilidade) são implícitas.
   • Algoritmo para Verificação de Provas: Para abordar a não determinismo introduzido pelas regras estruturais implícitas (especificamente a aplicação ilimitada de enfraquecimento e o posicionamento de variáveis nas regras de eliminação), os autores definem um julgamento de "forma normal" ($\Omega \gg_{\Gamma, r} \Omega_{nf}$). Esse algoritmo computa o conjunto de todas as formas normais possíveis (contextos sem variáveis repetidas) para um dado contexto $\Omega$, conjunto de hipóteses $\Gamma$ e modo $r$.
   • Judgmentos Baseados em Conjuntos: As regras de dedução natural são elevadas para operar em conjuntos de contextos de forma normal ($\Xi$). Por exemplo, a introdução de conjunção computa o produto cartesiano de conjuntos de contextos, enquanto a interseção é usada para regras que exigem concordância de contexto (como a conjunção aditiva).

Principais Contribuições

• Lógica Adjunta Generalizada: O artigo generaliza a lógica adjunta para contextos ordenados, introduzindo uma pré-ordem de modos onde cada modo controla independentemente enfraquecimento, contração e mobilidade unilateral.
• Propriedades Estruturais Unilaterais: O sistema modela e prova explicitamente propriedades para mobilidade e contração à esquerda e à direita como propriedades estruturais separadas e independentes, uma característica antecipada, mas não explorada, em trabalhos anteriores sobre subexponenciais.
• Eliminação de Corte: Os autores provam que o cálculo de sequente adjunto ordenado admite eliminação de corte (via multicorte) e eliminação de identidade, estabelecendo o sistema como um quadro lógico bem comportado.
• Decidibilidade da Verificação de Provas: O artigo fornece um sistema de dedução natural com regras estruturais implícitas e prova que a verificação de provas para esse sistema é decidível. Isso é alcançado construindo um algoritmo terminante que computa o conjunto de contextos de forma normal.

Resultados

• Corretude Teórica: O cálculo de sequente é mostrado como satisfazendo a eliminação de corte e de identidade. O sistema de dedução natural é provado como correto e completo em relação ao cálculo de sequente.
• Decidibilidade: O algoritmo para computar formas normais ($NF_{\Gamma, r}(\Omega)$) é provado como terminante. Consequentemente, o problema de verificar provas no sistema de dedução natural implícito é decidível.
• Subsunção Subestrutural: Os resultados implicam a decidibilidade da subsunção subestrutural, um componente central dos algoritmos de verificação de tipos para linguagens como QRTT (que usa semântica de Kripke com mundos explícitos).

Significado e Alegações
Os autores alegam que a Lógica Adjunta Ordenada fornece uma fundação adequada para uma linguagem de programação adjunta expressiva ou um quadro lógico. Ao desacoplar propriedades estruturais de um único modo base e usar deslocamentos adjuntos, o sistema permite raciocínio nativo em várias disciplinas (linear, ordenada, irrestrita) com alternância transparente. A decidibilidade da verificação de provas com regras estruturais implícitas é destacada como um passo crítico para a implementação de verificadores de tipos bidirecionais para linguagens de programação funcional que podem lidar com propriedades estruturais de granularidade fina de código. O artigo observa que, embora o procedimento de decisão esteja estabelecido, a eficiência prática (por exemplo, evitar complexidade exponencial decorrente de enfraquecimentos desnecessários) permanece um assunto para otimização futura. O trabalho é posicionado como uma generalização direta da lógica ordenada subexponencial de Kanovich et al. e uma extensão dos tipos adjuntos de Jang et al. para incluir ordem.