Substitution Sans Copier-Coller

Informations Fondamentales

• ID de l'article: 2510.12304
• Titre: Substitution Without Copy and Paste
• Auteurs: Thorsten Altenkirch (University of Nottingham), Nathaniel Burke (Imperial College London), Philip Wadler (University of Edinburgh and Input Output)
• Classification: cs.LO (Logique en Informatique)
• Conférence de publication: LFMTP 2025 (International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice)
• Lien de l'article: https://arxiv.org/abs/2510.12304

Résumé

Lors de la définition d'opérations de substitution pour les langages comportant des liants (comme le λ-calcul simplement typé), il est généralement nécessaire de définir séparément les opérations de substitution et de renommage, ce qui entraîne une duplication considérable de code. Pour vérifier les propriétés catégoriques du calcul, les mêmes arguments doivent être répétés plusieurs fois. Cet article propose une approche légère pour éviter cette redondance et construit une CwF simplement typée isomorphe à la famille initiale de CwF simplement typées. L'article est présenté sous la forme d'un script de programmation littéraire en Agda.

Contexte et Motivation de la Recherche

Problème Central

Lors de la définition mécanique d'opérations de substitution pour les langages avec liants, la méthode traditionnelle nécessite:

1. Définition séparée du renommage de variables (∆ ⊩v Γ) et de la substitution de termes (∆ ⊩ Γ)
2. Implémentation répétée de quatre opérations de substitution différentes: variable-pour-variable, variable-pour-terme, terme-pour-variable, terme-pour-terme
3. Preuve répétée de toutes les lois fonctorielles pour les combinaisons, entraînant 8 cas de preuve distincts

Motivation de la Recherche

1. Principes d'ingénierie logicielle: Éviter le copier-coller de code, ce qui est particulièrement important dans les preuves formalisées
2. Signification théorique: Fournir une base pour les définitions de substitution dans la théorie des types dépendants
3. Applications pratiques: Interprétation dans les catégories d'ordre supérieur et résolution des problèmes de cohérence des types dépendants

Limitations des Approches Existantes

• Duplication de code: Nécessité de définir des opérations similaires séparément pour les variables et les termes
• Duplication de preuves: Les preuves des lois catégoriques doivent couvrir toutes les combinaisons, entraînant de nombreux arguments répétés
• Difficultés de maintenance: Les modifications à un endroit nécessitent une mise à jour synchronisée de plusieurs définitions similaires

Contributions Principales

1. Cadre unifié: Proposition d'une opération de substitution unifiée basée sur un paramètre Sort, fusionnant le traitement des variables et des termes en une seule définition
2. Garantie de terminaison: Utilisation astucieuse de la récursion structurelle d'Agda et de la vérification de terminaison par ordre lexicographique pour assurer le bien-fondé de la définition
3. Vérification théorique catégorique: Preuve que la substitution définie récursivement satisfait toutes les lois de la CwF simplement typée
4. Résultat d'initialité: Établissement d'un isomorphisme entre la syntaxe de substitution récursive et la CwF initiale
5. Théorème de normalisation: La forme standard de substitution des λ-termes correspond aux λ-termes sans substitution explicite

Détails de la Méthode

Définition de la Tâche

Construction d'un système de substitution unifié tel que:

• Entrée: Toute combinaison de termes/variables et de substitutions/renommages
• Sortie: Le résultat de substitution du type correspondant
• Contraintes: Maintien de la sécurité des types et de la terminaison

Technologie Centrale: Système de Sort

Définition du Type Sort

data Sort : Set where
  V : Sort
  T>V : (s : Sort) → IsV s → Sort

data IsV : Sort → Set where
  isV : IsV V

pattern T = T>V V isV

Cette définition rend astucieusement V structurellement plus petit que T, satisfaisant les exigences de vérification de terminaison d'Agda.

Définition Unifiée des Termes et Substitutions

data _ ⊢ [_]_ : Con → Sort → Ty → Set where
  zero : Γ ▷ A ⊢ [ V ] A
  suc : Γ ⊢ [ V ] A → (B : Ty) → Γ ▷ B ⊢ [ V ] A
  `_ : Γ ⊢ [ V ] A → Γ ⊢ [ T ] A
  _ ·_ : Γ ⊢ [ T ] A ⇒ B → Γ ⊢ [ T ] A → Γ ⊢ [ T ] B
  λ_ : Γ ▷ A ⊢ [ T ] B → Γ ⊢ [ T ] A ⇒ B

Où Γ ⊢ [ V ] A correspond aux variables et Γ ⊢ [ T ] A correspond aux termes.

Structure de Treillis sur Sort

data _ ⊑ _ : Sort → Sort → Set where
  rfl : s ⊑ s
  v⊑t : V ⊑ T

_⊔_ : Sort → Sort → Sort
V ⊔ r = r
T ⊔ r = T

Opération de Substitution Unifiée

Fonction de Substitution Centrale

_[_] : Γ ⊢ [ q ] A → ∆ ⊩ [ r ] Γ → ∆ ⊢ [ q ⊔ r ] A

Intuition clé: Le sort du résultat est la borne supérieure minimale des sorts d'entrée, garantissant que le résultat n'est une variable que lorsque les deux entrées sont des variables/renommages.

Traitement de la Terminaison

Résolution du problème de terminaison par une fonction identité polymorphe sur Sort:

id-poly : Γ ⊩ [ q ] Γ
id : Γ ⊩ [ V ] Γ
id = id-poly {q = V}

Points d'Innovation Technique

1. Récursion structurée: Utilisation de l'ordre structurel de Sort et de la mesure lexicographique pour assurer la terminaison
2. Polymorphisme paramétrique: Traitement unifié des différents cas de variables et de termes via le paramètre Sort
3. Application de la théorie des treillis: Utilisation élégante de l'opération ⊔ pour gérer l'élévation de type
4. Règles de réécriture: Utilisation de la fonctionnalité REWRITE d'Agda pour simplifier le raisonnement équationnel

Vérification Théorique

Preuve des Lois Catégoriques

Loi d'Identité

[id] : x [ id ] ≡ x

Preuve par induction structurelle, avec comme point clé le lemme de naturalité dans le cas des variables.

Loi d'Associativité

[◦] : x [ xs ◦ ys ] ≡ x [ xs ] [ ys ]

Nécessite une preuve mutuellement récursive avec la loi d'identité à gauche, reflétant les connexions intrinsèques de la structure catégorique.

Vérification de la Structure CwF

L'article prouve que la syntaxe de substitution récursive satisfait tous les axiomes de la CwF simplement typée:

• Structure catégorique: Les contextes et substitutions forment une catégorie
• Structure de préfaisceau: Chaque type correspond à un préfaisceau
• Objet terminal: Le contexte vide
• Extension de contexte: Structure analogue au produit catégorique

Théorème d'Initialité

Établissement de mappages dans les deux directions:

1. Normalisation norm : Γ ⊢I A → Γ ⊢ [ T ] A
2. Plongement ⌜_⌝ : Γ ⊢ [ q ] A → Γ ⊢I A

Preuve qu'ils sont des inverses mutuels:

• Stabilité norm ⌜ t ⌝ ≡ t
• Complétude ⌜ norm t ⌝ ≡ t

Détails d'Implémentation

Utilisation des Caractéristiques d'Agda

1. Types inductifs-inductifs: Définition mutuelle de Sort et IsV
2. Terminaison lexicographique: Support de motifs de récursion complexes
3. Règles de réécriture: Automatisation du raisonnement équationnel
4. Synonymes de motifs: Simplification de l'utilisation de types complexes

Analyse de Terminaison

Preuve de terminaison par analyse du graphe d'appel, avec pour chaque fonction une mesure:

• _[_]: (r, t)
• id: (r, Γ)
• _+_: (r, σ)
• suc[_]: (q)

Dans tous les cycles, soit Sort décroît strictement, soit Sort se maintient tandis que les autres paramètres décroissent.

Comparaison avec les Travaux Connexes

Différences avec les Méthodes Existantes

1. Méthode Kit18,5: Abstraction des motifs communs du renommage et de la substitution via des kits, mais nécessite toujours des preuves répétées
2. Perspective monadique6,9: Codage de la substitution comme fonction des variables vers les termes, mais difficile à étendre aux types dépendants
3. Outils d'automatisation21,22: La bibliothèque Autosubst génère automatiquement les lemmes de substitution, mais la base contient toujours de la duplication

Analyse des Avantages

1. Simplicité: Plus simple dans les langages supportant la récursion lexicographique
2. Unicité: Une seule définition couvrant tous les cas
3. Extensibilité: Pose les fondations pour le traitement des types dépendants

Conclusion et Discussion

Conclusions Principales

1. Contribution méthodologique: Preuve que la paramétrisation par Sort permet d'unifier élégamment les opérations de substitution
2. Contribution théorique: Établissement de l'initialité de la syntaxe de substitution récursive
3. Contribution pratique: Fourniture d'une solution technique concrète pour éviter la duplication

Limitations

1. Dépendance aux caractéristiques d'Agda: Nécessite le support de la vérification de terminaison lexicographique
2. Transfert de complexité: Bien que la duplication soit évitée, la complexité du système de Sort augmente
3. Défis d'extension: L'extension aux types dépendants nécessite des recherches supplémentaires

Directions Futures

1. Extension aux types dépendants: Application de la méthode à la théorie complète des types dépendants
2. Cohérence d'ordre supérieur: Applications dans les catégories d'ordre supérieur
3. Portage vers d'autres assistants de preuve: Migration vers Lean, Coq et autres systèmes

Évaluation Approfondie

Points Forts

1. Innovativité technique: La conception du système de Sort résout astucieusement les problèmes de terminaison et d'unicité
2. Complétude théorique: Développement théorique complet allant des définitions fondamentales à l'initialité
3. Valeur pratique: Fourniture d'une solution pratique aux problèmes courants en vérification formalisée
4. Clarté de présentation: En tant que script de programmation littéraire, le code et les explications s'intègrent bien

Insuffisances

1. Dépendance à la plateforme: Dépendance sérieuse aux caractéristiques spécifiques d'Agda, portabilité limitée
2. Compromis de complexité: Bien que la duplication soit évitée, de nouveaux concepts complexes sont introduits
3. Extensibilité inconnue: L'extension vers des systèmes de types plus complexes reste à vérifier

Impact Potentiel

1. Contribution théorique: Offre de nouvelles perspectives pour la mécanisation de la théorie des types
2. Orientation pratique: Fourniture d'outils utiles aux praticiens de la vérification formalisée
3. Inspiration pour la recherche: Pose les fondations pour des recherches ultérieures sur la théorie des types dépendants

Scénarios d'Application

1. Vérification formalisée: Définition de langages nécessitant le traitement de liants
2. Recherche en théorie des types: Étude des CwF et des algèbres initiales
3. Théorie des langages de programmation: Mécanisation du λ-calcul et de ses extensions

Références Bibliographiques

L'article cite les travaux importants du domaine, notamment:

• Les travaux originaux de De Bruijn12
• La méthode kit de McBride18
• L'approche type-safe d'Allais et al.5
• La série de travaux Autosubst21,22
• Les recherches connexes sur les monades relatives6

Ces références reflètent la compréhension approfondie de l'auteur de l'évolution du domaine et l'investigation complète des travaux existants.