💻 computer science

A Graded Modal Dependent Type Theory with Erasure, Formalized

Este artigo apresenta uma teoria de tipos dependentes modais graduados com eliminação de código, formalizada em Agda, que estabelece propriedades meta-teóricas fundamentais e prova a correção de uma função de extração que remove argumentos marcados como elimináveis.

Autores originais: Andreas Abel, Nils Anders Danielsson, Oskar Eriksson

Publicado 2026-04-01

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Andreas Abel, Nils Anders Danielsson, Oskar Eriksson

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 casa muito complexa, não com tijolos comuns, mas com blocos mágicos. Alguns desses blocos são essenciais para a estrutura (como vigas e fundações), enquanto outros são apenas decorativos (como cortinas ou pinturas na parede).

O papel que você leu trata de uma nova maneira de organizar essas "construções" no mundo da programação, chamada Teoria de Tipos Modal Graduada. Vamos simplificar os conceitos técnicos usando analogias do dia a dia.

1. O Grande Problema: O que é "lixo" e o que é "essencial"?

Em programação, às vezes escrevemos códigos que são necessários para provar que algo está correto (como uma licença de construção), mas que o computador não precisa executar de verdade. É como ter um manual de instruções gigante que você precisa ler para saber como montar o móvel, mas que você joga fora assim que a montagem termina.

O problema é: como o computador sabe exatamente o que pode jogar fora sem quebrar a casa? Se ele jogar fora uma viga por engano, a casa cai. Se ele mantiver a decoração, o computador fica lento e gasta energia à toa.

2. A Solução: Etiquetas de "Grau" (Grades)

Os autores criaram um sistema onde cada variável (cada bloco da construção) recebe uma etiqueta ou um grau. Pense nisso como um sistema de cores ou números:

Grau 0 (Invisível/Apagável): É como um fantasma. O código existe para provar que a lógica está certa, mas pode ser apagado completamente antes do programa rodar.
Grau 1 (Essencial): É o tijolo de verdade. Precisa estar lá.
Grau Infinito (Usado muitas vezes): É um recurso que pode ser copiado e usado quantas vezes quiser.

A grande inovação deste trabalho é que eles criaram uma fórmula matemática flexível (chamada de "semianel ordenado") que permite misturar essas regras. Não é apenas "apagar ou não apagar"; é um sistema que pode lidar com "apagar", "usar uma vez", "usar duas vezes" ou "não usar nada".

3. A "Mágica" da Formalização (O Agda)

Os autores não apenas inventaram essa teoria; eles a construíram dentro de um assistente de prova chamado Agda.

A Analogia: Imagine que eles não apenas desenhou o plano da casa no papel, mas construíram uma réplica digital perfeita da casa em um videogame super avançado. Nesse jogo, se você tentar colocar um tijolo onde não deveria, o jogo avisa: "Erro! A casa vai cair!".
Por que isso importa? Porque eles provaram matematicamente, passo a passo, que as regras deles nunca vão falhar. Eles garantiram que, se você seguir as regras de "apagamento", o programa final vai funcionar exatamente como o original, só que mais rápido e leve.

4. O "Extrator" (O Cozinheiro)

Uma das partes mais legais do trabalho é a função de extração.

A Analogia: Imagine um chef de cozinha que prepara um prato complexo. O prato tem ingredientes reais (carne, legumes) e ingredientes de "prova" (uma folha de papel com a receita escrita, usada apenas para garantir que o tempero está certo).
O "Extrator" é como um robô que entra na cozinha, olha para o prato e remove todos os ingredientes de prova, deixando apenas a carne e os legumes.
O trabalho prova que, mesmo sem a folha de receita, o prato final tem o mesmo sabor (o mesmo valor numérico) que o prato original. O robô sabe exatamente o que pode tirar sem estragar a comida.

5. Casos Especiais: O "Casamento" de Blocos

O papel também discute como lidar com pares de blocos (como dois tijolos colados).

Pares Fortes: Se você tem dois tijolos colados, você precisa dos dois para manter a estrutura.
Pares Fracos: Às vezes, você só precisa de um tijolo, e o outro é apenas um "enfeite" que pode sumir.
Os autores mostraram como lidar com situações onde você tenta "abrir" um par fraco que foi marcado para sumir. Eles provaram que, se você tiver cuidado (garantindo que o contexto seja consistente), você pode abrir esses pares sem causar desastres.

Resumo em uma Frase

Os autores criaram um sistema de etiquetas matemáticas que permite aos programadores dizerem ao computador exatamente o que pode ser descartado antes de rodar um programa, e eles provaram matematicamente (usando um assistente digital) que essa "limpeza" nunca vai estragar o resultado final do programa.

É como ter um assistente de limpeza superinteligente que sabe exatamente quais móveis são apenas decoração e pode removê-los de uma casa cheia de segredos, garantindo que a casa continue segura e habitável.

Título: Uma Teoria de Tipos Dependente Modal Graduada com Apagamento, Formalizada

Autores: Andreas Abel, Nils Anders Danielsson e Oskar Eriksson (Universidade de Goteborg e Chalmers University of Technology, Suécia).

1. O Problema

Linguagens de programação fortemente tipadas frequentemente necessitam de análises estáticas para determinar como as variáveis são utilizadas (ex: irrelevância, linearidade, apagamento/erasure). Embora teorias como a Quantitative Type Theory (QTT) existam para rastrear o uso de recursos através de um semianel de quantidades, a formalização completa das propriedades meta-teóricas (como redução de sujeito, normalização e decidibilidade) em sistemas de tipos dependentes com universos e eliminação grande (large elimination) é complexa e muitas vezes incompleta na literatura.

Especificamente, há desafios em:

Garantir que o apagamento de argumentos de funções (marcados como irrelevantes para a execução) não altere o comportamento do programa.
Lidar com programas abertos (que contêm variáveis livres) em contextos consistentes, onde variáveis apagadas podem aparecer.
Formalizar a distinção entre tipos "fortes" (com projeções e igualdade $\eta$ ) e "fracos" (com pattern matching), e como o apagamento afeta a correspondência em pares apagados (erased matches).
Evitar que a adição de grades (rótulos de uso) quebre a semântica padrão da igualdade definicional.

2. Metodologia

Os autores desenvolveram uma teoria de tipos dependente genérica, parametrizada por uma estrutura de modalidade baseada em um semianel parcialmente ordenado.

Sistema Formal: A linguagem $\lambda\Sigma\Pi^{\mathcal{U}}_{\mathcal{N}}$ $λ Σ Π_{N}^{U}$ estende tipos dependentes com:
- Tipos $\Pi$ (funções) e $\Sigma$ (pares), tanto fortes quanto fracos.
- Números naturais com eliminação grande (que pode computar tipos).
- Um universo, tipo vazio ( $\bot$ ) e tipos unitários (fortes e fracos).
- Anotações de "grades" (grades) que rastreiam o uso de variáveis.
Separação de Julgamentos: Diferente de abordagens unificadas, o sistema separa o julgamento de tipagem ( $\Gamma \vdash t : A$ ) do julgamento de uso/atribuição de grade ( $\gamma \triangleright t$ ). Isso permite que a semântica de tipos dependente seja definida independentemente das grades inicialmente, sendo refinada posteriormente.
Formalização em Agda: Todo o trabalho foi formalizado no assistente de provas Agda. A formalização utiliza uma relação lógica de Kripke como núcleo para provar propriedades meta-teóricas.
Estudo de Caso (Apagamento): O foco principal é a instância de apagamento, onde a grade $0$ indica que um termo é computacionalmente irrelevante e pode ser removido, e $\omega$ indica relevância.
Prova de Correção: A correção do apagamento é provada através de uma relação lógica que conecta o sistema de origem (tipado e graduado) a um cálculo- $\lambda$ não tipado (alvo). O sistema suporta tanto semântica estrita (call-by-value) quanto não estrita (call-by-name).

3. Principais Contribuições

Extensão da Estrutura de Modalidades:
- Introduziram uma função nr (para recursão em números naturais) que generaliza operadores anteriores (como natrec-star), permitindo modelar corretamente a contagem de uso em recursão e iteração para diferentes instâncias de modalidades (ex: linear, afim, apagamento).
Formalização Completa da Meta-Teoria:
- É a primeira formalização completa da meta-teoria de uma teoria de tipos dependente graduada que inclui um universo e eliminação grande.
- Provaram propriedades fundamentais: redução de sujeito (preservação de tipos sob redução), consistência, normalização e decidibilidade da igualdade definicional.
Julgamento de Atribuição de Grade:
- Apresentaram um julgamento de uso ( $\gamma \triangleright t$ ) que classifica o uso de variáveis livres.
- Demonstraram que esse julgamento é decidível e possui a propriedade de principalidade (existe um contexto de uso mais específico para qualquer termo bem-resourçado).
- Provaram um lema de substituição para grades, essencial para a prova de redução de sujeito.
Prova de Correção de Apagamento (Erasure):
- Desenvolveram uma relação lógica de apagamento que prova que a extração de termos (removendo partes marcadas com grade 0) preserva o valor dos programas de tipo natural.
- Inovação: A prova suporta programas abertos, desde que todas as variáveis livres no contexto sejam apagáveis e o contexto seja consistente (não contenha termos do tipo vazio).
- Trataram o problema de "correspondências apagadas" (erased matches) em pares fracos, mostrando que, se permitidas, podem quebrar a canonicidade em certos contextos, e discutiram as restrições necessárias para manter a correção.
Extensões e Tipos Unitários:
- Implementaram tipos unitários fortes e fracos, com regras de uso distintas que refletem a lógica linear (unidade multiplicativa vs. aditiva).
- Discutiram uma extensão com tipos $\Sigma$ graduados (com grades separadas para os componentes), inspirada no trabalho de Atkey, permitindo modelar registros com campos apagados.

4. Resultados

Correção Formal: A formalização em Agda (com cerca de 110.000 linhas de código) valida que o sistema é consistente e que a extração de código apagado é segura.
Preservação de Comportamento: Para programas que computam números naturais, o valor final é idêntico antes e depois da extração, mesmo na presença de variáveis livres apagáveis em contextos consistentes.
Flexibilidade de Modalidades: O sistema suporta múltiplas instâncias (apagamento, tipos lineares, tipos afins, fluxos de informação) através da parametrização pela estrutura do semianel, sem reescrever a meta-teoria.
Limitações Identificadas: A prova de correção para programas abertos depende da proibição de correspondências apagadas em pares fracos (erased matches em $\Sigma$ -fracos) para garantir que o lema fundamental da relação lógica se mantenha. Se permitidas, a canonicidade pode ser perdida.

5. Significância

Este trabalho é significativo por várias razões:

Rigor na Formalização: Ao formalizar a meta-teoria de tipos dependentes graduados com eliminação grande, os autores fornecem uma base sólida e verificada por computador para o desenvolvimento de linguagens de programação futuras que integram análise de recursos e tipos dependentes.
Segurança em Extração de Código: A prova de que o apagamento de argumentos não altera o comportamento de programas (inclusive abertos) é crucial para compiladores de linguagens como Agda e Idris, permitindo otimizações agressivas sem comprometer a correção.
Generalidade: A abordagem baseada em semianéis e a separação entre tipagem e uso de recursos oferecem um framework flexível que pode ser adaptado para outras análises estáticas além do apagamento, como controle de fluxo de informação e linearidade.
Impacto na Comunidade: O código formalizado está disponível e pode servir como ponto de partida para verificadores de tipos verificados, extensões para tipos indutivos recursivos e integração com meta-variáveis em assistentes de prova reais.

Em resumo, o artigo estabelece um marco na teoria de tipos dependentes, provando matematicamente e computacionalmente que é possível rastrear e eliminar recursos computacionais de forma segura e correta em um sistema de tipos rico e expressivo.