Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

Título: Codificando Aritmética de Peano em um Fragmento Mínimo de Lógica de Separação

Autores: Sohei Ito (Universidade de Nagasaki) e Makoto Tatsuta (Instituto Nacional de Informática / Sokendai).

1. Problema e Contexto

A Lógica de Separação (Separation Logic - SL) é amplamente utilizada para verificar programas que manipulam estruturas de memória (heap). No entanto, a verificação de sistemas que envolvem cálculos numéricos exige a extensão da SL com aritmética.

• O Desafio: A comunidade frequentemente assume que combinar um fragmento decidível da SL com aritmética decidível (como a Aritmética de Presburger) resultaria em um sistema decidível.
• A Questão Central: Este artigo investiga se é possível obter indecidibilidade mesmo em um fragmento extremamente restrito da lógica de separação, quando estendido apenas com os conceitos básicos de aritmética (zero e função sucessor). Especificamente, os autores questionam se a adição de apenas 0 e s (sucessor) a um fragmento mínimo de SL é suficiente para codificar toda a Aritmética de Peano (PA) e, consequentemente, tornar o problema de validade indecidível.

2. Metodologia

Os autores definem um fragmento mínimo de lógica de separação chamado SLN (Separation Logic with Numbers), que contém:

• O predicado de apontamento intuitivo (intuitionistic points-to): t1 ↦ t2.
• A constante 0.
• A função sucessor s.
• Conectivos booleanos e quantificadores de primeira ordem.
• Nota: O fragmento exclui a conjunção separadora (*) e o "magic wand" (-∗), tornando-o sintaticamente muito simples.

Técnica de Codificação (O Núcleo da Prova):
Para demonstrar que o SLN é expressivo o suficiente, os autores desenvolvem uma tradução de fórmulas da Aritmética de Peano (especificamente da classe $\Pi^0_1$) para o SLN. A estratégia central é codificar tabelas de operações aritméticas dentro do heap (memória):

1. Estrutura do Heap: O heap é utilizado para armazenar entradas que representam resultados de adição, multiplicação e desigualdade.
2. Tags de Operação:
   • 0: Indica uma entrada de adição.
   • 1: Indica uma entrada de multiplicação.
   • 2: Indica uma entrada de desigualdade ($\leq$).
3. Offset: Os valores são deslocados em +3 para evitar colisões com as tags (0, 1, 2).
4. Condição de Tabela (H): Uma fórmula lógica $H$ é construída para garantir que, se o heap contém entradas para operações, elas sejam consistentes com as regras de indução da aritmética (ex: $s(x) + y = s(x+y)$).
5. Tradução: As operações aritméticas ($+, \times, \leq$) são substituídas por consultas a essas tabelas no heap. Se o heap não contiver uma entrada específica (por ser "pequeno"), a tradução é projetada para ser trivialmente verdadeira, permitindo que a validade global dependa da existência de heaps "suficientemente grandes" que simulam a aritmética correta.

3. Contribuições Principais

1. Teorema de Representação ($\Pi^0_1$):
   Os autores provam que existe uma tradução que preserva a validade e a não-valididade para fórmulas $\Pi^0_1$ da Aritmética de Peano. Ou seja, uma fórmula $\Pi^0_1$ é válida no modelo padrão da aritmética se e somente se sua tradução for válida na interpretação padrão do fragmento SLN.

2. Indecidibilidade da Validade em SLN:
   Como consequência direta do teorema de representação, o problema de validade no fragmento SLN é indecidível. Isso é surpreendente, pois o fragmento sem aritmética (apenas com ↦) é conhecido por ser decidível. A adição mínima de 0 e s é suficiente para elevar a complexidade à indecidibilidade.

3. Limites da Tradução (Contraponto para $\Sigma^0_1$):
   O artigo demonstra que essa tradução não preserva a validade para fórmulas da classe $\Sigma^0_1$. Eles fornecem um contraexemplo onde uma fórmula $\Sigma^0_1$ não válida na PA torna-se válida na tradução SLN, devido à natureza permissiva da condição de tabela em heaps pequenos. Isso delimita precisamente a fronteira da expressividade do fragmento.

4. Completude $\Pi^0_1$:
   O problema de validade do SLN é estabelecido como $\Pi^0_1$-completo.

   • Dificuldade (Hardness): Derivada da codificação da PA.
   • Pertencimento (Membership): Provado demonstrando que o problema de model-checking (verificação de modelo) no SLN é decidível. Como a verificação de modelos é decidível, a validade (que exige que a fórmula seja verdadeira para todos os heaps e atribuições) pode ser expressa como uma fórmula $\Pi^0_1$.

5. Prova Alternativa de Indecidibilidade:
   Os autores apresentam uma segunda prova de indecidibilidade baseada em uma redução da teoria de modelos finitos (usando o Teorema de Trakhtenbrot), codificando estruturas finitas diretamente no heap, reforçando a robustez do resultado principal.

4. Resultados Chave

• Expressividade Surpreendente: Um fragmento de lógica de separação contendo apenas o predicado de apontamento, zero e sucessor é capaz de simular toda a lógica aritmética de nível $\Pi^0_1$.
• Mecanismo de "Tabela no Heap": A capacidade de simular a aritmética não depende de operadores complexos de separação, mas sim da capacidade de estruturar o heap para armazenar e verificar relações aritméticas recursivas.
• Complexidade Computacional: O problema de validade para SLN é $\Pi^0_1$-completo, situando-se no mesmo nível de complexidade que o problema da parada de Turing (para a negação de $\Sigma^0_1$).

5. Significado e Impacto

• Teórico: O trabalho redefine os limites da expressividade da lógica de separação. Mostra que a combinação de lógica de separação com aritmética básica é extremamente poderosa, mesmo sem os operadores de conjunção separadora (*). Isso desafia a intuição de que a simplicidade sintática garante a decidibilidade.
• Prático (Verificação de Programas): O resultado tem implicações profundas para a verificação automática de programas. Sugere que ferramentas de verificação que tentam combinar lógica de separação com raciocínio aritmético devem ter cuidado extremo, pois mesmo fragmentos aparentemente inofensivos podem levar a problemas indecidíveis.
• Propriedades de Sistemas: A capacidade de codificar $\Pi^0_1$ implica que o fragmento pode expressar propriedades como consistência de sistemas lógicos e normalização forte, conectando a verificação de memória com problemas fundamentais da teoria da computação.

Em resumo, o artigo demonstra que a barreira entre a decidibilidade e a indecidibilidade na lógica de separação com aritmética é muito mais tênue do que se pensava, sendo rompida apenas pela adição de zero e sucessor a um núcleo espacial mínimo.