💻 computer science

Definitional Inversion, Without Normalisation

Este artigo introduz uma nova técnica de prova baseada em teoria de domínios que estabelece propriedades de inversão definicional para sistemas de tipos dependentes sem depender de normalização, permitindo, assim, a análise metateórica de sistemas não normalizantes como Idris e Lean, bem como daqueles com type-in-type.

Autores originais: Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

Publicado 2026-07-16

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está construindo uma biblioteca mágica e massiva, onde cada livro é uma prova matemática e as próprias prateleiras são feitas de lógica. Este é o mundo dos sistemas de tipos dependentes, o motor secreto por trás de assistentes de prova modernos como o Lean e linguagens de programação como o Idris. Neste mundo, as regras são incrivelmente rígidas: se você tentar colocar um "gato" em uma prateleira rotulada como "números", o sistema de segurança da biblioteca (o verificador de tipos) deve gritar imediatamente "Erro!" e parar você. Esta segurança baseia-se num conceito chamado igualdade definicional, que é a forma da biblioteca decidir se duas coisas são essencialmente a mesma. Por exemplo, um "quadrado" é apenas um "retângulo com lados iguais"? Se o sistema diz que sim, ele os trata como idênticos.

No entanto, verificar estas regras é complicado. Tradicionalmente, para provar que a biblioteca era segura, os matemáticos tinham de mostrar que cada um dos livros podia ser simplificado até à sua forma mais básica e simples (um processo chamado normalização). Mas muitas bibliotecas modernas e poderosas são desenhadas para serem infinitas ou autorreferenciais, o que significa que não podem ser simplificadas até um ponto final. É como tentar achatar um fractal; você continua a encontrar mais detalhes. Durante muito tempo, se um sistema não pudesse ser simplificado, não podíamos provar que era seguro. Este artigo introduz uma nova forma de verificar a segurança da biblioteca sem precisar de achatar o fractal primeiro.

O Enigma Infinito e o Espelho Mágico

Pense num sistema de tipos dependentes como um enorme puzzle de auto-verificação. As peças são tipos (como "números" ou "funções") e o objetivo é garantir que, quando você encaixa duas peças, elas se ajustam perfeitamente. A regra mais crítica neste puzzle é a inversão definicional. É a lógica que diz: "Se duas estruturas complexas parecem iguais, as suas partes também devem ser iguais". Por exemplo, se você tem dois tipos de função que são idênticos, o artigo prova que os seus tipos de entrada e de saída também devem ser idênticos. Isto é crucial porque permite que o computador decomponha com segurança código complexo em partes menores sem se confundir.

Durante décadas, a única forma de provar que estas peças se encaixavam era usar um método chamado confluência (verificar se diferentes caminhos de simplificação levam ao mesmo resultado) ou relações lógicas (uma forma complexa de comparar como os termos se comportam). Mas estas ferramentas antigas bateram numa parede. A confluência falha quando se adicionam certas regras "extensionais" (como as leis $\eta$ , que dizem que uma função é definida inteiramente pelo que ela faz, não por como é escrita). As relações lógicas geralmente exigem que o sistema seja "normalizador" (capaz de parar de simplificar), o que exclui muitas linguagens de programação poderosas e do mundo real que permitem loops infinitos ou tipos autorreferenciais.

A Nova Abordagem: Um Mapa de Possibilidades

Os autores, uma equipa de cientistas da computação e matemáticos, propõem uma nova estratégia baseada na teoria dos domínios. Em vez de tentar forçar as peças do puzzle a simplificarem-se numa única forma final, eles constroem um mapa de todos os comportamentos possíveis.

Imagine que está a tentar identificar uma criatura misteriosa numa floresta escura.

A Forma Antiga: Você espera que a criatura pare de se mover e revele a sua verdadeira forma final. Se a criatura nunca parar de se mover (porque é um loop infinito), você não consegue identificá-la, e a floresta torna-se insegura.
A Nova Forma: Você não espera que a criatura pare. Em vez disso, você observa as suas pegadas. Você nota que ela deixa uma pegada de "pé esquerdo", depois uma de "pé direito", depois outra de "pé esquerdo" novamente. Mesmo que a criatura nunca pare de caminhar, você ainda pode deduzir a sua forma olhando para o padrão dos seus passos.

Na linguagem do artigo, estas "pegadas" são chamadas de elementos compactos ou observações finitas. Os autores constroem um "domínio" matemático (um espaço estruturado) onde cada tipo é representado não por uma resposta final, mas pelo conjunto de todas as coisas finitas que podemos observar sobre ele. Eles utilizam uma técnica chamada projetores finitos para fatiar este domínio em pedaços geríveis.

O Que Eles Descobriram

Usando este método de "pegadas", a equipa provou com sucesso que a inversão definicional se mantém verdade mesmo em sistemas que:

Nunca param de simplificar (não-normalizadores), tais como aqueles com uma regra de "tipo-em-tipo" (onde um tipo pode conter a si próprio).
Incluem leis $\eta$ , que são regras complicadas que fazem com que funções e pares se comportem de forma mais intuitiva, mas que quebram os métodos de prova tradicionais.

Eles demonstraram isto num pequeno núcleo de uma teoria de tipos chamada MLTT $\eta$ (Teoria de Tipos de Martin-Löf com leis $\eta$ ). Mostraram que, mesmo neste sistema caótico e potencialmente infinito, se dois tipos forem iguais, os seus blocos de construção também devem ser iguais. Isto é um grande feito porque prova que a "rede de segurança" do sistema de tipos funciona mesmo quando o sistema é permitido ser desordenado e infinito.

Por Que Isto Importa

Os autores não resolveram apenas um puzzle para um sistema de brinquedo minúsculo; eles mostraram que o seu método é robusto. Eles estenderam a sua prova para incluir:

Somas dependentes (pares de dados).
Tipos unitários (um tipo com apenas um valor).
Combinadores de ponto fixo (ferramentas que permitem recursão infinita).
Números naturais com correspondência de padrões (pattern matching).
Tipos de identidade (provar que duas coisas são a mesma).
Proposições de irrelevância de prova (onde o conteúdo de uma prova não importa, apenas o seu facto de existir).

Eles até construíram um modelo para um "universo de proposições estritas", mostrando que a sua técnica pode lidar com as características complexas encontradas em ferramentas do mundo real como Lean, Agda e Rocq.

Os Limites e o Futuro

O artigo é muito claro sobre o que ele não faz. Ele não prova que estes sistemas são "normalizadores" (que sempre param). De facto, ele trabalha explicitamente para sistemas que não param. Também não resolve o problema dos "neutros" (variáveis que ainda não foram preenchidas) da mesma forma que resolve para termos fechados, embora sugira como isso poderá ser feito no futuro.

Os autores já transformaram as suas provas matemáticas em código, verificando-as três vezes em três assistentes de prova diferentes (Agda, Lean e Rocq). Isto sugere que o seu método não é apenas uma ideia teórica, mas uma ferramenta prática.

A Conclusão

Este artigo é como entregar aos construtores da biblioteca mágica uns novos óculos. Antes, eles só podiam verificar a segurança da biblioteca se os livros fossem estáticos e acabados. Agora, podem verificar a segurança de livros que ainda estão a ser escritos, ou livros que se referem a si mesmos para sempre. Ao focar-se no comportamento observável (as pegadas) em vez do destino final (a paragem), eles abriram a porta para verificar os sistemas de tipos mais poderosos, complexos e potencialmente infinitos que podemos imaginar. Isto prepara o caminho para o "Lean4Lean" e "MetaRocq" — projetos onde os assistentes de prova verificam o seu próprio código — tornando as ferramentas que usamos para construir a matemática e o software ainda mais confiáveis.

Resumo Técnico: Inversão Definicional, Sem Normalização

Problema
Sistemas de tipos dependentes sustentam assistentes de prova críticos (Agda, Lean, Rocq) e linguagens de programação (Idris, Haskell dependente). Estabelecer suas propriedades metateóricas, particularmente os princípios de inversão definicional (injetividade e ausência de confusão de construtores de tipos), é essencial para provar correção, unicidade de tipos e verificação de kernel. No entanto, as ferramentas metateóricas existentes enfrentam limitações severas:

Abordagens baseadas em confluência: Têm dificuldade com recursos modernos como leis $\eta$ . Embora a confluência funcione para redução $\beta$ , misturá-la com conversão tipada e leis $\eta$ (por exemplo, para funções ou pares) frequentemente leva a sistemas não confluentes ou exige apresentações complexas e não padronizadas.
Abordagens baseadas em normalização (Relações Lógicas): As relações lógicas tradicionais dependem da existência de formas normais. Elas falham para teorias de tipos não normalizáveis (comuns na prática, ex: uso de Type:Type ou combinadores de ponto fixo). Além disso, provar a normalização requer uma lógica ambiente mais forte que a lógica objeto (frequentemente envolvendo indução-recursão ou impredicatividade), o que torna impossível estudar a metateoria de assistentes de prova dentro de si mesmos (ex: Lean4Lean, MetaRocq).

O artigo aborda o caso específico de MLTT $\eta$ , uma variação da teoria de tipos de Martin-Löf com produtos dependentes, equações $\beta$ e $\eta$ , e um universo Type:Type. Este sistema derrota a confluência (devido a $\eta$ ) e a normalização (devido a Type:Type), deixando suas propriedades de inversão definicional não provadas.

Metodologia
Os autores propõem uma nova técnica de prova baseada em teoria dos domínios, especificamente utilizando projeções finitárias. O insight central é interpretar tipos não por suas formas normais (que podem não existir), mas por seu "comportamento observável" via elementos compactos em um domínio de Scott.

Construção do Domínio: Os autores constroem um domínio $D$ $D$ como a solução de uma equação de domínio recursiva representando os construtores de tipos ( $\Pi$ $Π$ , $\mathcal{U}$ $U$ , etc.). O domínio é construído como o limite de uma sequência crescente de aproximações finitas ( $C_n$ $C_{n}$ ), onde os elementos são compactos (representando observações finitas).
- Crucialmente, o modelo identifica $\bot$ com $\lambda x.\bot$ para satisfazer as leis $\eta$ para funções, mantendo os construtores $\Pi$ distintos de $\mathcal{U}$ para garantir a disjunção.
Tipagem Semântica: Uma relação de tipagem semântica é definida sobre os elementos compactos do domínio. Esta relação é formulada usando projetores finitários (mapas contínuos $p: D \to D$ tais que $p(\alpha) \le \alpha$ e $p(p(\alpha)) = p(\alpha)$ ). Um tipo é interpretado como um projetor finitário, e um termo é relacionado a um tipo se sua denotação é um ponto fixo desse projetor.
Relação Lógica: Uma relação lógica é definida sobre os termos sintáticos e as testemunhas semânticas (elementos compactos). Diferente das relações lógicas tradicionais que recursam nas formas normais dos tipos, esta relação recursa no estágio $n$ $n$ dos elementos compactos e na estrutura da testemunha semântica.
- A relação lida com termos abertos interpretando termos neutros como $\bot$ , evitando a complexidade da quantificação estilo Kripke, mas ainda suportando inversão em contextos abertos.
- A relação é definida até a redução de cabeça (head reduction), incorporando regras $\beta$ e $\eta$ diretamente na estrutura da relação lógica.
Adequação: Os autores provam um teorema de adequação: se dois termos são definicionalmente iguais na sintaxe, eles estão relacionados na relação lógica. Isso permite derivar propriedades sintáticas (como injetividade) das propriedades semânticas (disjunção de elementos do domínio).

Principais Contribuições

Nova Técnica de Prova: Um método de teoria dos domínios para provar inversão definicional (injetividade e ausência de confusão) sem depender de normalização ou confluência.
Tratamento de $\eta$ e Não-Normalização: A técnica prova com sucesso a injetividade para sistemas com leis $\eta$ e Type:Type (ou combinadores de ponto fixo), uma combinação anteriormente intratável para métodos padrão.
Lógica Ambiente Fraca: A prova depende apenas de indução básica sobre números naturais, evitando princípios lógicos fortes (como indução-recursão) exigidos para provas de normalização. Isso torna o trabalho adequado para projetos de autoverificação (ex: provar propriedades do Lean dentro do próprio Lean).
Extensibilidade: A técnica é demonstrada em MLTT $\eta$ e mostra-se escalável para teorias mais ricas incluindo:
- Somas dependentes ( $\Sigma$ ) e Tipo Unidade ($1$) com leis $\eta$ .
- Recursão geral via um combinador de ponto fixo ( $Y$ ).
- Números naturais ( $\mathbb{N}$ ) com correspondência de padrões (pattern matching).
- Tipos de identidade prova-relevantes ($Id$) com transporte.
- Um universo de proposições estritas ($Prop$) com irrelevância de prova definicional.
Mecanização: Os resultados foram mecanizados em Agda, Lean e Rocq, cobrindo as várias extensões listadas acima.

Resultos

Injetividade de $\Pi$ : O artigo prova que se $\Pi x:A.B \equiv \Pi x:A'.B'$ , então $A \equiv A'$ e $B \equiv B'$ .
Disjunção: Construtores de tipos são disjuntos (ex: $\Pi x:A.B \not\equiv \mathcal{U}$ ).
Redução de Sujeito e Progresso: Como consequências dos princípios de inversão, os autores derivam teoremas de progresso e preservação, estabelecendo a correção do sistema como uma linguagem de programação.
Falha de UIP: O modelo demonstra que a Unicidade de Provas de Identidade (UIP/regra-K) não é derivável neste sistema, pois o modelo de domínio distingue entre diferentes provas de identidade.

Significância
O artigo afirma preencher um "ponto cego" na metateoria dos sistemas de tipos dependentes. Ao desacoplar a inversão definicional da normalização, a técnica permite o estudo rigoroso de sistemas não-normalizáveis e sistemas com teorias equacionais ricas (como $\eta$ ) que são prevalentes em assistentes de prova modernos e linguagens de programação.

Os autores posicionam este trabalho como um passo fundamental para projetos como Lean4Lean e MetaRocq, que visam verificar a metateoria de assistentes de prova dentro de si mesmos. Como esses projetos não podem assumir a normalização da lógica objeto (devido ao segundo teorema de Gödel), esta abordagem de teoria dos domínios oferece um caminho viável para verificar kernels e garantir a correção de algoritmos de tipagem sem exigir uma lógica ambiente mais forte. Os autores também sugerem aplicações potenciais para linguagens de programação dependentes que utilizam recursos de não-terminação ou tipagem gradual, onde a metateoria tradicional baseada em terminação falha.