Nominal Type Theory by Nullary Internal Parametricity

Resumo Técnico: Teoria de Tipos Nominais por Parametricidade Interna Nula

Declaração do Problema
Formalizar a sintaxe de linguagens com ligadores (por exemplo, cálculo lambda) exige lidar com equivalência-$\alpha$, abstração de nomes e frescura. Frameworks nominais abordam isso usando tipos de "abstração de nome" (denotados $\@N \multimap -$). No entanto, abordagens existentes enfrentam um trade-off:

1. Apresentação Existencial: Trata abstracções como pares nome-termo $\langle x, a \rangle$. Isso suporta "correspondência de padrões nominal" conveniente (destruir ligadores), mas sofre de regras de tipagem incômodas que exigem propagação complexa de frescura.
2. Apresentação Universal: Trata abstracções como funções que consomem nomes frescos (funções afins). Isso oferece regras de inferência limpas, mas aparentemente carece da capacidade de realizar correspondência de padrões nominal.

Frameworks nominais atuais frequentemente dependem de semântica externa (por exemplo, conjuntos nominais) ou mecanismos internos complexos para preencher essa lacuna. O artigo busca uma fundação que una as regras limpas da apresentação universal com as capacidades de correspondência de padrões da existencial, inteiramente dentro de um contexto de teoria de tipos.

Metodologia
Os autores propõem a Teoria de Tipos Nominais Paramétrica (PNTT), uma teoria de tipos dependente construída sobre a Teoria de Tipos Paramétrica Interna Nula (nullary PTT). Esta abordagem adapta a teoria de tipos paramétrica interna binária de Cavallo e Harper (CH) reduzindo a aridade da parametricidade de 2 para 0.

A metodologia central envolve:

1. Pontes Nulas: Substituir os tipos de caminho/ponte binários padrão por pontes nulas. Uma ponte nula $q : \text{Bridge } A \dots$ é tratada como uma função afim a partir de um intervalo de ponte $\@N$. Essas pontes representam variáveis "frescas".
2. Princípio de Abstração Estrutural (SAP): A teoria internaliza a parametricidade via SAP, que estabelece equivalências entre um tipo $K$ e seu "tipo de ponte" $\@N \multimap K$. Crucialmente, o SAP afirma que o formador de tipo de ponte comuta com todos os outros formadores de tipo.
3. Indução de Nomes: O intervalo de ponte $\@N$ é estendido para um tipo de primeira classe de nomes, $\text{Nm}$. Um eliminador novo, indução de nome ($\text{ind}_{\text{Nm}}$), é introduzido. Isso permite análise de casos em um nome $n$: ou $n$ é a variável afim específica $x$ atualmente em escopo, ou $x$ é fresco em $n$.
4. Tipos de Dados Nominais: Tipos de dados nominais padrão (como a sintaxe do cálculo lambda não tipado) são definidos usando construtores que podem tomar nomes como argumentos.

Principais Contribuições

1. Recuperação da Correspondência de Padrões Nominal: O artigo demonstra que a correspondência de padrões nominal, tipicamente associada a abstracções existenciais, pode ser recuperada no contexto universal. Ao aplicar o SAP a um tipo de dados nominal $D$, o tipo de ponte $\@N \multimap D$ é mostrado como equivalente a uma "tradução paramétrica" $D_1$ (por exemplo, $Ltm_1$). $D_1$ contém construtores explícitos de "buraco". A correspondência de padrões em um ligador em $D$ é assim reduzida à indução em $D_1$, onde o caso "buraco" corresponde à variável ligada.
2. Primitivas Unificadas: Os autores mostram que a PNTT suporta naturalmente:
   • Abstração de Nome Universal: Via tipos de ponte nula.
   • Frescura Tipal: Via tipos $\text{Gel}$, que classificam termos onde um nome específico é fresco.
   • Abstração Existencial: Derivada não primitivamente via SAP e tipos de frescura.
   • Troca de Nomes e Escopo Local: Implementados usando funções afins e o ligador $\nu$ (implementado como $\text{ung}(\lambda x. t)$).
3. Parametricidade Sintética de Kripke: O artigo conecta a parametricidade nula à parametricidade binária de Kripke. Ao combinar parametricidade nula (para raciocínio nominal) com um axioma padrão de parametricidade binária, os autores emulam modelos de Kripke. Isso é demonstrado provando a equivalência entre a sintaxe de De Bruijn do cálculo lambda não tipado e sua codificação de Sintaxe Abstrata de Ordem Superior (HOAS).
4. Princípio de Abstração Estrutural (SAP) em Nomes: Uma prova específica é fornecida mostrando que $\@N \multimap \text{Nm} \simeq 1 + \text{Nm}$. Esta equivalência é central para o princípio de indução de nome e a recuperação da correspondência de padrões.

Resultados

• Correção Teórica: Os autores fornecem um modelo semântico para PNTT na categoria de pré-feixes $\text{Psh}(\square_2 \times \square_0)$, onde $\square_0$ é a categoria de ordinais finitos e injecções (a base do topos de Schanuel). Isso confirma a consistência do sistema.
• Viabilidade de Implementação: O artigo argumenta que, como a teoria CH binária foi implementada em Cubical Agda, implementar PNTT (essencialmente CH nula + indução de nome) é viável.
• Estudos de Caso:
  • Substituição no Cálculo $\pi$: Os autores definem uma função de substituição para processos do cálculo $\pi$ correspondendo a padrões de ligação, demonstrando a utilidade da abordagem baseada em SAP.
  • Adequação HOAS: Uma prova é esboçada (confiando em um axioma externo de parametricidade binária) mostrando que a sintaxe nominal do cálculo lambda é equivalente à sua codificação HOAS, espelhando os resultados de parametricidade de Kripke de Atkey.

Significado e Alegações
O artigo alega fornecer um "framework nominal legítimo" que resolve a tensão histórica entre abstracções de nome existenciais e universais.

• Unificação: Unifica as regras de inferência limpas da abstracção universal com as capacidades práticas de correspondência de padrões da abstracção existencial sem exigir meta-teoria externa.
• Internalização: Ao contrário de abordagens anteriores onde a parametricidade é uma propriedade meta-teórica, a PNTT internaliza a parametricidade via SAP, permitindo que resultados de parametricidade sejam provados dentro da teoria.
• Novidade: Os autores afirmam ser os primeiros a fazer uso explícito e ativo da parametricidade nula como fundação para teoria de tipos nominais.
• Modéstia: O artigo reconhece limitações. As provas SAP para termos complexos são "manhosas" e atualmente exigem reprodução manual de estruturas de termos. Os autores sugerem que trabalhos futuros poderiam envolver a automação da construção de provas SAP ou a migração para uma versão "observacional" da PNTT (como no assistente de prova Narya) para evitar a necessidade de provas SAP explícitas. Eles também observam que as regras completas de troca de nomes do FreshMLTT (comutando com substituição) ainda não são totalmente acomodadas sem restrições ad hoc.

Em resumo, o artigo estabelece a parametricidade interna nula como uma fundação robusta para teoria de tipos nominais, oferecendo uma maneira principista de lidar com ligadores, frescura e correspondência de padrões dentro de um único sistema coerente de teoria de tipos.