Well-Scoped Locally Nameless Representation of Syntax

Resumo Técnico: Representação Localmente Nomeada Bem Escopada de Sintaxe

Declaração do Problema
Ao formalizar linguagens com construtos de ligação (por exemplo, $\lambda$-cálculo, sistemas de tipos) em provadores de teoremas interativos baseados em teoria de tipos dependentes (como Agda, Lean ou Rocq), um desafio central é gerenciar a ligação de variáveis e a equivalência $\alpha$. A abordagem "localmente nomeada", que representa variáveis livres como nomes explícitos e variáveis ligadas como índices de de Bruijn, mostrou-se capaz de satisfazer os critérios PoplMark para baixa sobrecarga de infraestrutura, transparência e facilidade de entrada. No entanto, representações localmente nomeadas padrão sofrem de uma falha crítica: a definição indutiva de termos permite índices "pendentes" (índices que excedem o escopo atual). Para garantir a correção, é necessário restringir o domínio a um subconjunto de termos "localmente fechados". Isso exige provas repetitivas e manuais de que operações (como substituição) preservam o fechamento local, criando um ônus significativo e uma fonte de erros potenciais em desenvolvimentos formais.

Metodologia
O artigo propõe uma variante "bem escopada" da representação localmente nomeada que aproveita o sistema de tipos dependentes do Agda para impor o fechamento local intrinsecamente, em vez de como um predicado separado.

1. Tipos Indutivos Indexados: Em vez de um único tipo de termos, a biblioteca define uma família de tipos Trm[n] indexada por um número natural $n$. Um "n-termo" é um termo onde todos os índices de de Bruijn são extraídos do tipo finito Fin n (números naturais menores que $n$).
2. Termos Localmente Fechados como 0-Termos: Neste framework, termos "localmente fechados" (aqueles sem índices pendentes) correspondem precisamente a Trm[0]. Termos com variáveis livres são representados como Trm[n], onde $n$ corresponde ao número de variáveis livres em escopo.
3. Parametrização por Assinaturas de Ligação: A biblioteca é genérica, parametrizada por uma assinatura de ligação no estilo de Plotkin. Isso permite a definição de operadores, suas aridades e o número de nomes ligados em cada posição de argumento.
4. Operações via Tipos Dependentes:
   • Enfraquecimento de Escopo: Uma função Trm[m] -> Trm[n] (para $m \le n$) que injeta índices, lidando com o deslocamento necessário ao mover-se para um escopo maior.
   • Concretização (Abertura): Substituir um índice $i$ em um "(1+n)-termo" por um 0-termo para produzir um "n-termo". Isso envolve deslocar índices maiores que $i$ para baixo em uma unidade.
   • Abstração (Fechamento): Substituir um nome livre em um "n-termo" por um índice para produzir um "(1+n)-termo". Isso envolve deslocar índices para cima.
   • Substituição: Definida estruturalmente. Como a função de substituição mapeia nomes para 0-termos (Trm), a condição de "localmente fechado" é imposta automaticamente pelo sistema de tipos. A substituição em um "n-termo" produz outro "n-termo".

Contribuições Principais

• A Biblioteca WSLN: Uma biblioteca genérica em Agda que implementa termos localmente nomeados bem escopados. Ela fornece a infraestrutura para definir sintaxe, operações (enfraquecimento, substituição, abstração, concretização) e princípios de raciocínio para qualquer linguagem especificada por uma assinatura de ligação de Plotkin.
• Prova de Adequação Formal: O artigo fornece uma prova rigorosa estabelecendo uma bijeção entre:
  1. O tipo de 0-termos localmente nomeados bem escopados (Trm[0]).
  2. As classes de equivalência $\alpha$ de termos "nomeados" (termos com nomes explícitos para variáveis livres e ligadas).
     Esta bijeção demonstra que a representação bem escopada captura corretamente a semântica da substituição que evita captura e da equivalência $\alpha$.
• Eliminação de Provas de Fechamento Local: Ao codificar restrições de escopo nos índices de tipos, a necessidade de predicados explícitos de "localmente fechado" e as obrigações de prova associadas (por exemplo, provar que a substituição preserva o fechamento local) é eliminada. Essas propriedades tornam-se consequências das regras de tipagem.
• Tratamento de Frescor: A biblioteca integra-se com técnicas nominais, usando um conjunto "finitamente inexaurível" de átomos (números naturais) para gerar nomes frescos via quantificação cofinita, garantindo que as condições de frescor sejam tratadas sistematicamente.

Resultados
O artigo valida a abordagem através de três exemplos distintos implementados em Agda:

1. Cálculo $\pi$: Demonstra a aplicabilidade da biblioteca além do $\lambda$-cálculo, lidando com expressões de processo e nomes de canal. Destaca que, embora a biblioteca lide com a estrutura de ligação, a verificação de tipos para bem-formação (por exemplo, garantir que canais sejam usados onde esperado) permanece um julgamento separado, definido pelo usuário.
2. Teoria de Tipos de Martin-Löf (MLTT): Mostra como a biblioteca facilita a definição de regras de tipagem. Contrasta regras "existe-fresco" (que exigem suposições explícitas de frescor) com regras de "quantificação cofinita" (onde o frescor é implícito), demonstrando que a representação bem escopada suporta esta última, levando a formalizações mais limpas e transparentes.
3. Sistema T de Gödel (Normalização por Avaliação): Um desenvolvimento substancial provando a decidibilidade da conversão $\beta\eta$. Este exemplo ilustra como a representação bem escopada simplifica a semântica da abstração e o tratamento do frescor em construções semânticas complexas (pré-feixes com valores em setoides), evitando a necessidade de objetos semânticos com suporte finito.

Significado e Alegações
O artigo alega que a representação localmente nomeada bem escopada oferece uma solução "direta" mas poderosa para a "armadilha" dos índices pendentes encontrada em abordagens localmente nomeadas tradicionais. Seu significado principal reside em transferir o ônus de garantir a correção do escopo do usuário (via provas manuais) para o verificador de tipos do provador de teoremas (via tipos dependentes).

Os autores enfatizam que esta abordagem mantém a transparência exigida pelos critérios PoplMark: definições formais espelham de perto convenções informais, e o "yoga de índices" (manipulação de índices de de Bruijn) é encapsulado dentro das operações da biblioteca. Embora a implementação exija tratamento cuidadoso de ordinais finitos (Fin n) e deslocamento de índices, a biblioteca parametriza essa complexidade, permitindo que os usuários definam linguagens e provem propriedades sem gerenciar mecânicas de escopo de baixo nível. O artigo nota modestamente que, embora as assinaturas de ligação atuais sejam não ordenadas e modelam escopos de ligação simples, a abordagem é robusta o suficiente para lidar com sistemas de tipos complexos e provas semânticas, conforme evidenciado pelo desenvolvimento do Sistema T.