💻 computer science

A formalization of System I with type Top in Agda

Cet article propose une variante du système I incluant le type Top et présente sa formalisation complète en Agda, incluant les preuves de progression et de normalisation forte.

Auteurs originaux : Agustín Séttimo, Cristian Sottile, Cecilia Manzino

Publié 2026-03-26

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Agustín Séttimo, Cristian Sottile, Cecilia Manzino

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes dans une cuisine très sophistiquée où les recettes (les programmes) sont écrites dans un langage mathématique strict. Jusqu'à présent, si vous aviez deux recettes qui faisaient exactement la même chose mais qui étaient écrites avec un ordre d'ingrédients légèrement différent, le chef (l'ordinateur) les considérait comme deux plats totalement différents.

C'est là qu'intervient System I, un nouveau système culinaire (ou logique) où l'on décide que si deux plats sont "isomorphes" (c'est-à-dire qu'ils sont essentiellement identiques, juste présentés différemment), alors c'est le même plat.

Les auteurs de cet article, Agustín, Cristian et Cecilia, ont pris ce système et y ont ajouté une nouvelle épice magique : le type Top (qui représente "tout" ou "vrai"). Ensuite, ils ont tout construit, brique par brique, dans un langage de programmation très rigoureux appelé Agda, pour prouver que ce système ne va jamais se bloquer et qu'il finira toujours par donner un résultat.

Voici une explication simple de leur travail, avec quelques analogies :

1. Le problème des "Isomorphismes" (Les recettes interchangeables)

Dans la vie de tous les jours, si vous dites "Je veux un café et un croissant" ou "Je veux un croissant et un café", c'est la même commande.
Dans les langages de programmation classiques, l'ordre compte. Mais dans System I, on dit : "Peu importe l'ordre, c'est le même type".

L'analogie : Imaginez un jeu de Lego. Si vous avez un mur de briques rouges et un mur de briques bleues, peu importe si vous construisez le mur rouge à gauche ou à droite, la structure globale est la même. Le système permet de transformer librement ces structures sans casser le code.

2. L'ajout du "Top" (La boîte magique)

Les auteurs ont ajouté un type spécial appelé Top (ou ⊤).

L'analogie : Imaginez une boîte magique qui contient "tout". Si vous avez une recette qui demande "n'importe quoi" (Top), vous pouvez y mettre n'importe quel ingrédient. Inversement, si vous avez une recette qui ne produit rien de spécifique, elle peut être considérée comme une boîte Top.
Le défi : Ajouter cette boîte magique rend les règles de transformation beaucoup plus compliquées. Il faut s'assurer que le chef ne se perde pas en essayant de mélanger des ingrédients infinis.

3. La preuve de sécurité : "Pas de boucle infinie !"

Le plus grand défi en informatique est d'éviter les boucles infinies (un programme qui tourne éternellement sans rien faire).

L'analogie : Imaginez un labyrinthe. Si vous entrez dedans, voulez-vous être sûr de pouvoir en sortir un jour, ou risquez-vous de tourner en rond pour toujours ?
La solution des auteurs : Ils ont prouvé mathématiquement (dans Agda) que dans leur cuisine, chaque chemin de réduction mène inévitablement à une sortie. C'est ce qu'on appelle la normalisation forte. Même avec la boîte magique (Top), on ne peut pas créer un plat qui se mange lui-même à l'infini.

4. Les "Témoins" (Les étiquettes de transformation)

Pour que tout cela fonctionne, les auteurs ont dû ajouter de petits "témoins" ou "étiquettes" dans le code.

L'analogie : Quand vous transformez une recette "café + croissant" en "croissant + café", vous devez coller une étiquette qui dit : "J'ai fait cette transformation parce que la règle 'commutativité' l'autorise".
Pourquoi ? Sans ces étiquettes, l'ordinateur pourrait faire des transformations infinies (A devient B, B devient A, A devient B...). En ajoutant l'étiquette, on force le système à "consommer" la transformation. Une fois l'étiquette utilisée, elle disparaît, et on avance vers la fin. C'est comme une pièce de monnaie que l'on dépense pour avancer dans le labyrinthe.

5. La formalisation en Agda (Le constructeur rigoureux)

Agda est un outil qui permet d'écrire du code qui est aussi une preuve mathématique.

L'analogie : C'est comme si les auteurs ne se contentaient pas de dire "Je pense que ce pont est solide". Ils ont construit le pont, brique par brique, et chaque brique est certifiée par un ingénieur en chef (le compilateur Agda) avant d'être posée. Si une brique n'est pas parfaite, le pont ne se construit pas.
Le résultat : Ils ont prouvé deux choses essentielles :
1. Progress : Le programme ne se bloque jamais (il avance toujours ou il est fini).
2. Normalisation forte : Le programme finit toujours par s'arrêter avec un résultat.

En résumé

Cet article raconte l'histoire de trois chercheurs qui ont pris un système de logique un peu abstrait (System I), y ont ajouté une notion de "tout" (Top), et ont utilisé un outil ultra-sécurisé (Agda) pour construire une preuve inébranlable que ce système est sûr, logique et ne tournera jamais en boucle.

C'est comme avoir garanti que votre nouvelle voiture électrique, même avec un moteur capable de faire n'importe quel trajet (Top), ne s'enfermera jamais dans un tunnel sans issue. C'est une avancée importante pour la fiabilité des logiciels et des preuves mathématiques futures.

1. Problématique et Contexte

Le calcul lambda simplement typé (STLC) est un fondement théorique majeur pour les langages de programmation et les systèmes de preuve. Cependant, dans les systèmes standards, des types isomorphes (par exemple, $A \times B$ et $B \times A$ , ou $A \to (B \to C)$ et $(A \times B) \to C$ ) sont considérés comme distincts, bien qu'ils aient la même sémantique.

System I, introduit par Díaz-Caro et Dowek, est un calcul lambda simplement typé avec des paires où les types isomorphes sont considérés comme égaux. Cette égalité permet une programmation plus flexible (ex: arguments d'une fonction dans n'importe quel ordre) et une forme d'irréférence de preuve.

Cependant, l'ajout de l'isomorphisme pose deux défis majeurs pour la formalisation et la sémantique opérationnelle :

Non-déterminisme et préservation des types : Les règles de réduction classiques (comme la projection $\pi_1$ sur une paire) deviennent ambiguës si l'ordre des éléments d'une paire peut changer via l'isomorphisme.
Normalisation forte : L'introduction de règles d'équivalence entre termes (pour refléter l'égalité des types) risque de briser la propriété de normalisation forte (chaque séquence de réduction doit être finie), en particulier avec l'ajout du type universel Top ( $\top$ ). Le type Top introduit des cas pathologiques (comme l'auto-application sur $\top$ ) qui peuvent mener à des boucles infinies si le système n'est pas rigoureusement contrôlé.

L'objectif de ce travail est de proposer une variante de System I incluant le type Top, et de fournir une formalisation complète et vérifiée dans Agda de ce calcul, incluant les preuves de progression et de normalisation forte.

2. Méthodologie

Les auteurs adoptent une approche rigoureuse basée sur la théorie des types dépendants en utilisant l'assistant de preuve Agda.

Représentation Intrinsèque des Termes : Contrairement à une approche extrinsèque (où les termes et les types sont définis séparément), les auteurs utilisent une représentation intrinsèque. Chaque terme est défini comme une dérivation de typage. Cela garantit par construction que seuls les termes bien typés peuvent être manipulés, éliminant ainsi la nécessité de prouver la préservation des types (subject reduction) pour chaque relation de réduction.
Indices de De Bruijn : Pour gérer les variables, l'approche utilise des indices de De Bruijn plutôt que des noms, ce qui rend la formalisation plus compacte et évite les problèmes de capture de variables.
Témoins Explicites d'Isomorphisme : Pour gérer l'égalité des types de manière constructive, le système introduit un constructeur de terme explicite [ρ]≡t. Ici, ρ est un témoin (witness) qui prouve l'isomorphisme entre le type de t et le nouveau type visé. Cela permet de suivre syntactiquement chaque application d'isomorphisme.
Réécriture Dirigée : Au lieu de définir une relation d'équivalence symétrique et transitive entre termes, les auteurs définissent une relation de réécriture dirigée. Les règles d'équivalence (comme comm, asso, dist) sont orientées pour éliminer les constructeurs de témoins [ρ]≡. Cela transforme l'équivalence en étapes de réduction, essentiel pour prouver la terminaison.
Stratégie de Preuve de Normalisation : Pour prouver la normalisation forte, les auteurs s'inspirent de la technique de réductibilité (Tait/Girard), mais en suivant l'approche de Schäfer (adaptée par Kovács pour Agda). Cette méthode utilise une interprétation des termes dans un ensemble de termes fortement normalisants (SN), enrichie par un prédicat pour gérer les cas d'élimination (applications, projections) et d'introduction (abstractions, paires).

3. Contributions Clés

Extension de System I avec Top :
- Introduction du type $\top$ et de ses isomorphismes associés (ex: $A \times \top \equiv A$ , $A \to \top \equiv \top$ ).
- Définition d'un ensemble complet de règles d'isomorphisme de termes (y compris des règles de "split" et d'expansion $\eta$ contrôlées) pour garantir que le calcul ne reste pas bloqué (progression) tout en préservant la normalisation.
- Gestion du paradoxe potentiel de l'auto-application sur $\top$ (le terme $\Omega$ ) grâce à la présence explicite des témoins d'isomorphisme qui empêchent les réductions infinies.
Formalisation Complète en Agda :
- Définition de la syntaxe, de la sémantique, des règles de typage et des relations de réduction.
- Implémentation de la substitution et du renommage de variables.
- Définition de la relation de réduction $\rightsquigarrow$ comme l'union de la réduction $\beta$ et des réécritures d'isomorphisme.
Preuves de Propriétés Fondamentales :
- Progression : Preuve que tout terme typé et clos est soit une valeur, soit peut réduire (soit par $\beta$ , soit par une règle d'isomorphisme).
- Normalisation Forte : Preuve que toute séquence de réduction partant d'un terme typé est finie. C'est la contribution la plus complexe, nécessitant la définition d'une interprétation des termes et la preuve d'un théorème d'adéquation.
Fonction d'Évaluation Totale :
- Grâce à la preuve constructive de normalisation forte, les auteurs définissent une fonction d'évaluation totale en Agda. Cette fonction prend un terme clos et renvoie sa séquence de réduction jusqu'à la valeur normale.

4. Résultats

Correction du Calcul : La formalisation démontre que le système étendu avec $\top$ est cohérent et ne permet pas de boucles infinies, même avec des termes comme $\Omega = (\lambda x. x x)(\lambda x. x x)$ typés sur $\top$ . La présence des témoins d'isomorphisme force une réduction spécifique qui élimine les redondances.
Exemple d'Évaluation : Le papier illustre l'évaluation du terme $\Omega$ , montrant comment les règles d'isomorphisme (comme sym abs) sont utilisées pour transformer le terme en une forme où la réduction $\beta$ peut s'appliquer, menant finalement à la valeur $\star$ (la valeur de type $\top$ ).
Code Disponible : L'intégralité du code Agda est disponible publiquement, servant de référence pour d'autres formalisations de calculs modulo isomorphismes.

5. Signification et Impact

Ce travail est significatif à plusieurs niveaux :

Avancée en Formalisation : C'est, à la connaissance des auteurs, la première formalisation complète de la preuve de normalisation forte pour un calcul lambda modulo isomorphismes (avec Top). Cela démontre la faisabilité de formaliser des systèmes complexes avec des règles d'équivalence non triviales dans un assistant de preuve.
Robustesse des Preuves : L'utilisation de la représentation intrinsèque et des indices de De Bruijn simplifie considérablement les preuves de préservation des types et de substitution, qui sont souvent sources d'erreurs dans les formalisations extrinsèques.
Implications pour la Théorie des Types : La gestion explicite des témoins d'isomorphisme offre une nouvelle perspective sur la manière de traiter l'égalité des types dans les systèmes de preuves. Cela suggère que pour maintenir la normalisation forte, il peut être nécessaire de "dépouiller" les isomorphismes de manière syntaxique plutôt que de les traiter comme une égalité purement extensionnelle.
Base pour le Futur : Ce travail ouvre la voie à l'extension vers des systèmes plus complexes, tels que le System I polymorphe (System F modulo isomorphismes) ou des variantes non typées comme le calcul lambda distributif, ainsi que l'étude de l'extensionnalité ( $\eta$ ) dans ce contexte.

En résumé, ce papier fournit une fondation solide et vérifiée pour l'étude des calculs lambda où l'isomorphisme des types est une égalité première, résolvant les problèmes de terminaison et de sémantique par une ingénierie de preuve rigoureuse en Agda.