💻 computer science

Initial Algebras of Domains via Quotient Inductive-Inductive Types

Cet article présente un cadre général pour construire des effets algébriques en théorie des domaines en définissant les algèbres DCPO initiales comme des types inductifs-inductifs quotient (QIITs) formalisés en Cubical Agda, et démontre que plusieurs constructions classiques s'inscrivent dans cette approche.

Auteurs originaux : Simcha van Collem, Niels van der Weide, Herman Geuvers

Publié 2026-03-03

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Simcha van Collem, Niels van der Weide, Herman Geuvers

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

🌟 Le Grand Projet : Construire des Mondes de Calcul

Imaginez que vous êtes un architecte de l'univers. Votre but n'est pas de construire des maisons en briques, mais des mondes de calcul (ce qu'on appelle la "théorie des domaines"). Dans ces mondes, les programmes informatiques vivent, grandissent et interagissent.

Le problème, c'est que les programmes ne sont pas toujours parfaits. Ils peuvent planter, s'arrêter en cours de route, ou faire plusieurs choses à la fois de manière imprévisible. La théorie des domaines est la boîte à outils mathématique qui permet de donner un sens précis à ces comportements "bizarres".

Ce papier propose une nouvelle façon de construire ces mondes, en utilisant une technique très moderne appelée QIIT (Types Inductifs-Inductifs Quotientés).

🧱 L'Analogie du Lego et de la Règle du Jeu

Pour comprendre l'idée principale, imaginons que nous voulons construire un nouveau type de jeu de Lego.

1. Le Problème des anciennes méthodes (Les "Ensembles de Puissance")

Avant, pour construire ces mondes mathématiques, les chercheurs utilisaient une méthode qui ressemblait à prendre tous les Lego possibles dans l'univers, les mettre dans un immense sac, et essayer de trier ce qui est valide.

Le problème : C'est énorme, inefficace, et cela demande des règles mathématiques très puissantes (qu'on appelle "impredicatives") qui ne fonctionnent pas bien dans les systèmes de logique modernes et sûrs. C'est comme vouloir construire une maison en essayant de manipuler tout l'univers d'un coup.

2. La Nouvelle Méthode : Les QIITs (Le Kit de Construction Intelligent)

Les auteurs disent : "Stop ! Construisons le monde brique par brique, en même temps que nous écrivons les règles du jeu."

C'est là qu'interviennent les QIITs. C'est une technique magique qui permet de faire deux choses en même temps :

Définir les briques (les opérations du programme).
Définir les règles de collage (les équations et les inégalités qui disent comment les briques s'assemblent).

L'analogie du Chef d'Orchestre :
Imaginez un chef d'orchestre (le type QIIT). Il ne se contente pas de dire "jouez la note Do". Il dit :

"Voici une note Do."
"Voici une note Sol."
"Et voici la règle : Si vous jouez Do puis Sol, c'est la même chose que Sol puis Do."
"Et une autre règle : Si vous jouez la même note deux fois, c'est comme si vous ne l'aviez jouée qu'une fois."

Le chef définit qui joue (les opérations) et comment ils doivent s'entendre (les règles) au même instant. Le résultat est un orchestre parfait qui respecte toutes les règles dès sa naissance.

🚀 Pourquoi c'est génial ? (Les Avantages)

A. Pas de "Sacs Infinis" (Prédicativité)

L'ancienne méthode utilisait des "sacs infinis" (ensembles de puissance) pour tout stocker. La nouvelle méthode construit le monde de manière constructive. C'est comme construire une maison avec des briques réelles plutôt que d'essayer de dessiner la maison en imaginant tous les murs possibles en même temps. C'est plus propre, plus sûr et plus facile à vérifier par ordinateur.

B. La Flexibilité (Les Signatures)

Les auteurs ont créé un modèle universel appelé "Signature". C'est comme un menu de construction.

Vous voulez un monde où les programmes peuvent s'arrêter (partialité) ? Vous choisissez le menu "Arrêt".
Vous voulez un monde où les programmes peuvent faire plusieurs choix (non-déterminisme) ? Vous choisissez le menu "Choix".
Vous voulez un monde où les programmes peuvent ajouter des états ? Vous choisissez le menu "État".

Grâce à ce papier, on peut créer n'importe lequel de ces mondes en suivant simplement le même processus de construction (le QIIT), sans avoir à réinventer la roue à chaque fois.

🎨 Des Exemples Concrets dans le Papier

Le papier montre que cette méthode fonctionne pour des constructions célèbres :

La Somme Coalescée (Coalesced Sums) :
Imaginez deux jeux de Lego séparés. Vous voulez les fusionner en un seul, mais vous voulez que leur point de départ (le sol) soit le même. C'est comme souder deux châteaux de sable par leur base. Le QIIT fait cela automatiquement en définissant que les deux "bas" sont identiques.
Le Produit "Smash" (Smash Product) :
C'est comme prendre deux dimensions (hauteur et largeur) et dire : "Si l'une est nulle, l'autre devient nulle aussi". C'est une façon de combiner des mondes où le "vide" domine tout.
Les Domaines de Puissance (Powerdomains) :
C'est la gestion du chaos. Imaginez un programme qui peut dire "Je vais faire A, ou B, ou C, je ne sais pas encore". Le QIIT permet de construire un monde où ce choix multiple est géré proprement, en respectant des règles comme "A ou B est pareil que B ou A".

🤖 La Preuve par l'Ordinateur (Cubical Agda)

Le plus cool, c'est que les auteurs n'ont pas juste écrit des théories sur du papier. Ils ont codé toute cette construction dans un langage spécial appelé Cubical Agda.
C'est comme si un robot très strict a vérifié chaque brique, chaque règle et chaque collage pour s'assurer qu'il n'y a aucune erreur logique. Si le robot dit "OK", c'est que le monde mathématique est solide à 100 %.

🏁 En Résumé

Ce papier est une boîte à outils universelle pour les mathématiciens et les informaticiens.

Avant : On construisait des mondes de calcul avec des méthodes lourdes et compliquées.
Maintenant : On utilise une technique élégante (QIIT) qui permet de construire n'importe quel type de comportement de programme (pannes, choix multiples, états) brique par brique, tout en garantissant que les règles sont respectées dès le début.

C'est un peu comme passer de la construction d'une maison en argile (qui peut s'effondrer) à la construction d'un château de Lego avec des pièces qui s'assemblent parfaitement et qui ne peuvent pas se tromper de place.

1. Problématique

La théorie des domaines, développée par Dana Scott, fournit un cadre mathématique pour la sémantique dénotationnelle des langages de programmation, permettant de modéliser des effets computationnels tels que la non-détermination, les fonctions partielles et les effets de bord. Ces effets sont souvent représentés par des algèbres de domaines (des DCPOs - Directed Complete Partial Orders - munis d'opérations obéissant à une théorie inéquationnelle).

Le problème central abordé par les auteurs réside dans la construction d'algèbres initiales pour ces signatures d'opérations :

Limites des constructions existantes : Les méthodes classiques pour construire ces algèbres (notamment via la complétion par idéaux ronds ou les présentations de DCPO) reposent souvent sur l'utilisation d'ensembles de parties (power sets). Cela les rend imprédicatives et les rend inapplicables dans des fondations constructives ou prédicatives strictes (comme la théorie des types homotopique sans axiome d'imprédicativité).
Besoin de généralité : Les travaux antérieurs, comme celui d'Altenkirch, Danielsson et Kraus sur le monade de partialité, utilisaient des types inductifs-inductifs quotients (QIIT) mais se limitaient aux $\omega$ -CPO (où les supremums sont définis sur des chaînes dénombrables). Or, la théorie des domaines standard requiert des DCPOs (supremums pour toute famille dirigée, pas seulement les chaînes), ce qui est une notion constructivement plus forte.
Objectif : Développer un cadre général, prédicatif, pour construire des algèbres initiales de DCPOs pour n'importe quelle signature d'opérations et d'inéquations, sans recourir aux ensembles de parties.

2. Méthodologie

Les auteurs proposent une construction basée sur les Types Inductifs-Inductifs Quotients (QIITs), un concept issu de la théorie des types homotopique (HoTT), formalisé dans Cubical Agda.

Approche par QIIT : Au lieu de construire les domaines via des complétions d'idéaux sur des bases abstraites, les auteurs définissent simultanément :
1. Un type (le domaine lui-même).
2. Une relation d'ordre sur ce type.
3. Des relations d'équivalence (quotients) et des règles de continuité.
Signature et Algèbres :
- Ils définissent une notion de signature ( $\Sigma$ ) composée de noms de constructeurs, de monômes (définissant l'arité et des constantes DCPO) et d'inéquations formelles.
- Une pré-algèbre est un DCPO muni d'opérations Scott-continues correspondant aux constructeurs.
- Une algèbre est une pré-algèbre où toutes les inéquations formelles de la signature sont valides.
Construction de l'Algèbre Initiale :
- L'algèbre initiale $Initial_\Sigma$ est définie comme un QIIT.
- Les constructeurs du QIIT sont divisés en trois groupes :
  1. Structure DCPO : Définition de l'ordre partiel, de l'antisymétrie, et de l'existence de supremums pour toute famille dirigée (quantification universelle sur les types d'indexation, garantissant la complétude dirigée).
  2. Structure de pré-algèbre : Introduction des opérations ( $app_a$ ) et garantie de leur continuité Scott (les opérations préservent les supremums dirigés).
  3. Structure d'algèbre : Ajout de constructeurs de chemin (path constructors) pour valider les inéquations de la signature (ex: $t_1 \sqsubseteq t_2$ ).
Preuve d'Initialité : Les auteurs établissent des principes de récursion et d'induction pour le QIIT, démontrant que $Initial_\Sigma$ est bien l'objet initial dans la catégorie des algèbres pour $\Sigma$ .

3. Contributions Clés

Cadre Général Prédicatif : La principale contribution est la généralisation de la construction des algèbres initiales de domaines à n'importe quelle signature d'opérations et d'inéquations, en restant dans un cadre prédicatif (sans utiliser de puissances d'ensembles).
Extension aux DCPOs : Contrairement aux travaux précédents sur les $\omega$ -CPO, cette méthode gère correctement les DCPOs complets, ce qui est crucial pour la sémantique dénotationnelle générale. Cela implique de quantifier sur toutes les familles dirigées, pas seulement les suites.
Formalisation en Cubical Agda : L'ensemble de la théorie, y compris les définitions, les preuves d'initialité et les exemples, est formalisé dans Cubical Agda, assurant une vérification mécanique rigoureuse.
Unification des Constructions : Le cadre unifie la construction de divers objets mathématiques (sommes, produits, domaines libres) sous une même approche basée sur les signatures et les QIITs.

4. Résultats et Exemples

Les auteurs démontrent la puissance de leur cadre en reconstruisant plusieurs constructions classiques de la théorie des domaines :

Constructions Catégoriques :
- Somme coalescée (Coalesced Sum) : Construction du coproduit de DCPOs pointés.
- Égaliseur (Coequalizer) : Construction de l'égaliseur de deux morphismes continus.
- Produit Smash (Smash Product) : Construction du produit tensoriel de DCPOs pointés.
Algèbres Libres et Domaines Spécifiques :
- Domaines Partiels (Partiality) : Reconstruction de la monade de partialité (lift) comme domaine libre.
- Powerdomains (Domaines de Puissance) : Construction du Powerdomain de Plotkin (modélisant la non-détermination) comme l'algèbre initiale d'une signature avec une opération d'union formelle commutative, associative et idempotente.
- Généralité : La construction permet de définir un foncteur adjoint à gauche $F : \mathbf{DCPO} \to \mathbf{Alg}_\Sigma$ , produisant l'algèbre libre pour n'importe quel DCPO de départ.

5. Signification et Impact

Fondations Constructives : Ce travail offre une alternative robuste aux constructions imprédicatives classiques. Il permet de développer la théorie des domaines dans des fondations constructives (comme HoTT) sans sacrifier la puissance expressive nécessaire à la sémantique des langages de programmation modernes.
Modélisation des Effets Algébriques : En fournissant un mécanisme systématique pour définir des effets algébriques (non-détermination, exceptions, etc.) via des signatures et des inéquations, le papier facilite la modélisation formelle de nouveaux paradigmes de programmation.
Outil pour la Sémantique Dénotationnelle : La capacité à construire des algèbres initiales pour des signatures arbitraires permet de donner un sens précis à des constructions de langages complexes, en s'assurant que les propriétés de continuité et d'ordre sont respectées par construction.
Futur : Les auteurs suggèrent que cette base peut être étendue pour traiter les handlers (gestionnaires) d'effets algébriques, complétant ainsi la sémantique dénotationnelle complète des langages avec effets.

En résumé, cet article établit un pont solide entre la théorie des types homotopique (via les QIITs) et la théorie des domaines classique, offrant une méthode constructive, prédicative et généralisable pour la sémantique des langages de programmation.