Towards Weak Stratification for Logics of Definitions

Resumo Técnico: Rumo à Estratificação Fraca para Lógicas de Definições

Declaração do Problema
A lógica de definições é uma família de lógicas utilizadas para codificar e raciocinar sobre julgamentos especificados por regras de inferência, onde predicados atômicos são associados a fórmulas lógicas que podem depender do próprio predicado. Para resolver a circularidade aparente inerente a tais definições, as abordagens padrão impõem uma condição de estratificação, garantindo que um predicado não apareça negativamente (à esquerda de uma implicação) no corpo de sua própria definição. Esta condição trata efetivamente as definições como operadores de ponto fixo monotônicos.

No entanto, muitas especificações úteis, particularmente as que envolvem relações lógicas para provar propriedades de linguagens de programação, requerem definições onde o predicado aparece negativamente. Na lógica $\mathcal{G}$, que fundamenta o assistente de prova Abella, tais definições são proibidas. Embora Tiu [19] tenha introduzido anteriormente uma lógica chamada $\mathcal{LD}$ que relaxa a condição de estratificação para uma estratificação fraca (permitindo ocorrências negativas, desde que o nível da cabeça seja estritamente maior que o nível da ocorrência negativa), a $\mathcal{LD}$ era limitada a um fragmento central. Ela carecia de suporte para o quantificador nabla ($\nabla$), essencial para raciocinar sobre nomes e frescor via constantes nominais, e para definições indutivas gerais além da indução sobre números naturais. O desafio abordado neste trabalho é estender a lógica de definições para incluir a estratificação fraca, mantendo a consistência na presença de $\nabla$ e definições indutivas gerais.

Metodologia
O artigo define uma nova lógica, $\mathcal{LD}\mu\nabla$, que estende a $\mathcal{LD}$ de Tiu com quantificação nabla e definições indutivas gerais. A metodologia procede em três estágios principais:

1. Sintaxe e Semântica de $\mathcal{LD}\mu\nabla$:
   A lógica é formulada como uma extensão do cálculo de sequentes de primeira ordem com um conjunto de definições $\mathcal{D}$ e um conjunto de definições indutivas $\mathcal{I}$.

   • Estratificação Fraca: Um conjunto de definições $\mathcal{D}$ é fracamente estratificado se, para cada cláusula $H \triangleq_X B$ e substituição de enraizamento $\rho$, $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$. Crucialmente, isso permite ocorrências negativas do predicado definido se o nível da cabeça for estritamente maior que o nível da ocorrência negativa.
   • Estratificação Estrita para Indução: O artigo impõe uma condição mais estrita para as definições indutivas $\mathcal{I}$: elas devem ser estritamente estratificadas (o nível de um predicado atômico de base deve ser independente de seus argumentos). Esta restrição é necessária para evitar inconsistência ao combinar indução com estratificação fraca.
   • Quantificador Nabla: A lógica incorpora o quantificador $\nabla$ para lidar com constantes nominais e frescor, distinguindo entre instâncias genéricas e específicas de nomes.

2. Lógica de Base e Interpretação:
   Para provar a consistência, os autores constroem uma versão de base da lógica, $\mathcal{LD}\mu\nabla_\infty$, onde todas as fórmulas são de base (sem variáveis próprias).

   • Lema de Enraizamento: Um passo técnico fundamental é provar que qualquer derivação em $\mathcal{LD}\mu\nabla$ pode ser interpretada como uma derivação em $\mathcal{LD}\mu\nabla_\infty$ via uma substituição de enraizamento. Isso reduz o problema de consistência da lógica completa para a consistência da lógica de base.
   • Regras Infinitárias: Em $\mathcal{LD}\mu\nabla_\infty$, as regras padrão $\forall R$ e $\exists L$ são substituídas por regras infinitárias que quantificam sobre todos os termos de base, e a regra $\mu L$ para indução é similarmente expandida para cobrir todas as instâncias de base.

3. Eliminação de Corte:
   O núcleo da prova de consistência é a eliminação da regra de corte (especificamente, a regra de multicut) em $\mathcal{LD}\mu\nabla_\infty$.

   • Relação de Redução: Uma relação de redução é definida sobre as derivações, especificando como os cortes podem ser empurrados para cima ou eliminados.
   • Redutibilidade: Seguindo a técnica de Tait-Martin-Löf adaptada por McDowell e Miller, os autores definem uma noção de redutibilidade (e normalizabilidade) para as derivações. Eles provam que toda derivação em $\mathcal{LD}\mu\nabla_\infty$ é redutível.
   • Tratamento de Casos Indutivos: Um aspecto crítico da prova é o tratamento da interação entre estratificação fraca e indução. Os autores mostram que, embora a estratificação fraca seja suficiente para definições gerais, as definições indutivas devem permanecer estritamente estratificadas. Eles fornecem um contraexemplo (Seção 3.3) demonstrando que permitir definições indutivas fracamente estratificadas leva à inconsistência lógica.

Principais Contribuições

• Definição de $\mathcal{LD}\mu\nabla$: O artigo define formalmente uma lógica que combina estratificação fraca, quantificação nabla e definições indutivas gerais.
• Prova de Consistência: A principal contribuição é a prova de que $\mathcal{LD}\mu\nabla$ é consistente. Isso é alcançado provando a eliminação de corte para a lógica de base $\mathcal{LD}\mu\nabla_\infty$ e estabelecendo uma interpretação de enraizamento.
• Restrições de Estratificação: O trabalho esclarece a fronteira entre definições permitidas e impermissíveis. Demonstra que, embora a estratificação fraca baste para definições gerais (permitindo relações lógicas), as definições indutivas exigem estratificação estrita para preservar a consistência.
• Contraexemplo: O artigo fornece um contraexemplo específico mostrando que relaxar a condição de estratificação para definições indutivas leva à inconsistência lógica, justificando a restrição imposta sobre $\mathcal{I}$.

Resultos

• Consistência: A lógica $\mathcal{LD}\mu\nabla$ é provada consistente. Consequentemente, a lógica $\mathcal{LD}\mu\nabla_\infty$ admite derivações sem corte para todas as sequentes prováveis.
• Propriedades de Inversão: O artigo estabelece propriedades metateóricas para $\mathcal{LD}\mu\nabla_\infty$, incluindo a invertibilidade de várias regras de introdução (ex: $\wedge R$, $\vee L$, $\nabla R$) e a parcial invertibilidade específica para $\vee R$, $\exists R$ e regras de definição ($\Delta R$) quando o contexto está vazio. Estas propriedades são cruciais para procedimentos de busca de prova.
• Limitações: O teorema de eliminação de corte é estabelecido apenas para a lógica de base $\mathcal{LD}\mu\nabla_\infty$. O artigo observa que estender este resultado para a lógica completa $\mathcal{LD}\mu\nabla$ (com variáveis próprias) permanece um desafio em aberto.

Significância
A significância deste trabalho reside no seu potencial para estender as capacidades do assistente de prova Abella. O Abella é baseado na lógica $\mathcal{G}$, que atualmente restringe as definições para serem estritamente estratificadas. Ao justificar a inclusão de definições fracamente estratificadas, esta pesquisa pavimenta o caminho para que o Abella suporte nativamente relações lógicas, uma técnica fundamental para provar propriedades semânticas de linguagens de programação (como segurança de tipos e correção de compiladores).

O artigo posiciona este trabalho como um passo fundamental para uma extensão mais ampla do $\mathcal{G}$. Embora o resultado atual trate de estratificação fraca com $\nabla$ e indução, os autores observam que uma justificativa completa para o Abella exigiria extensões adicionais para incluir co-indução e abstração nominal. O trabalho também destaca a necessidade de manter a estratificação estrita para definições indutivas, uma restrição que evita as inconsistências que, de outra forma, surgiriam ao misturar estratificação fraca com indução.