Sur la Métathéorie Formelle des Systèmes de Types Purs utilisant des Noms de Variables Monosortés et des Substitutions Multiples

Informations Fondamentales

• ID de l'article: 2510.12300
• Titre: On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
• Auteur: Sebastián Urciuoli (Universidad ORT Uruguay, Uruguay)
• Classification: cs.LO (Logique en Informatique)
• Conférence de publication: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2025)
• Lien de l'article: https://arxiv.org/abs/2510.12300
• Lien du code: https://github.com/surciuoli/pts-metatheory

Résumé

Cet article développe une théorie formelle de la conversion pour les termes λ de style Church avec types Π, en utilisant une syntaxe du premier ordre, des noms de variables monosortés et les substitutions multiples de Stoughton. La formalisation des systèmes de types purs (Pure Type Systems, PTS) et de certaines propriétés métathéoriques fondamentales est ensuite présentée : affaiblissement, validité syntaxique, fermeture sous conversion α et substitution. Enfin, les travaux de formalisation connexes sont comparés. L'ensemble du développement a été vérifié mécaniquement à l'aide du système Agda. Le travail démontre la faisabilité de la mécanisation de la théorie des types dépendants utilisant une syntaxe traditionnelle sans identification des termes λ convertibles-α.

Contexte de Recherche et Motivation

Contexte du Problème

1. Défis de formalisation: La vérification mécanique de la théorie des types dépendants a toujours été un défi, particulièrement lors du traitement de la liaison de variables et de l'équivalence α
2. Dilemme du choix syntaxique: Les approches existantes adoptent généralement les indices de de Bruijn ou les noms de variables bisortés pour éviter les problèmes de capture de noms, mais ces méthodes s'écartent des implémentations réelles
3. Complexité des opérations de substitution: La définition traditionnelle de la substitution unaire n'est pas structurellement récursive, nécessitant des méthodes d'induction complexes dans les preuves mécanisées

Motivation de la Recherche

1. Test de scalabilité: Vérifier si le cadre basé sur la théorie de substitution de Stoughton peut s'étendre à des langages plus complexes (comme PTS)
2. Réduire l'écart théorie-pratique: Utiliser une syntaxe traditionnelle avec noms de variables monosortés, plus proche des implémentations réelles des vérificateurs de types
3. Simplifier les méthodes de preuve: Grâce à une définition améliorée de la conversion α, utiliser des méthodes d'induction structurelle plus simples pour prouver les lemmes clés

Contributions Principales

1. Extension du cadre de substitution de Stoughton: Extension du cadre λ-calcul pur existant pour supporter les abstractions λ de style Church et les types Π
2. Définition améliorée de la conversion α: Proposition d'une nouvelle définition de la conversion α permettant aux lemmes clés d'être prouvés par induction structurelle
3. Formalisation de la métathéorie PTS: Vérification mécanique des propriétés métathéoriques fondamentales de PTS, incluant l'affaiblissement, la validité syntaxique, la fermeture sous conversion α et la fermeture sous substitution
4. Preuve d'équivalence: Démonstration de l'équivalence bidirectionnelle entre le système de règles infinies utilisant l'induction généralisée et le système de règles finies standard
5. Implémentation Agda complète: Fourniture d'une vérification mécanique complète avec environ 3000 lignes de code

Explication Détaillée de la Méthode

Définition de la Syntaxe

L'article utilise une définition syntaxique du premier ordre traditionnelle pour les termes λ:

data Λ : Set where
  c : C → Λ                    -- constantes
  v : V → Λ                    -- variables  
  λ[_:_]_ : V → Λ → Λ → Λ      -- abstraction λ de style Church
  Π[_:_]_ : V → Λ → Λ → Λ      -- type Π
  _·_ : Λ → Λ → Λ              -- application

Fonctions de Sélection et Substitution

L'innovation centrale réside dans l'utilisation des substitutions multiples de Stoughton, évitant la capture de noms par des fonctions de sélection:

X : Res → V
X (σ, xs) = X' (concat (map (fv ∘ σ) xs))

L'opération de substitution est définie comme une récursion structurelle:

λ[ x : A ] M • σ = λ[ y : A • σ ](M • σ , x := v y) 
  where y = X (σ , fv M - x)

Définition Améliorée de la Conversion α

La nouvelle définition de la conversion α utilise l'équivalence syntaxique plutôt qu'une définition récursive:

∼λ : ∀ {x x' y A A' M M'} → A ∼α A' → y ∉ fv M - x → y ∉ fv M' - x'
   → M [ x := v y ] ≡ M' [ x' := v y ] → λ[ x : A ] M ∼α λ[ x' : A' ] M'

Système de Types PTS

Utilisation de l'induction généralisée pour définir PTS, avec les règles clés:

⊢abs : Γ ⊢ A : s₁ → ∀z → z ∉ domΓ → Γ,z : A ⊢ B[y := z] : s₂
     → ∀z → z ∉ domΓ → Γ,z : A ⊢ M[x := z] : B[y := z]
     → R s₁ s₂ s₃
     → Γ ⊢ λ[x : A]M : Π[y : A]B

Points d'Innovation Technique

1. Redéfinition des Types de Restriction

Redéfinition de la restriction de Sub × Λ à Sub × List V, offrant une plus grande flexibilité:

Res = Sub × List V

2. Preuve de Conversion α Structurée

Le lemme clé iotaAlpha peut maintenant être prouvé par induction structurelle:

iotaAlpha : ∀ {M M'} → M • ι ≡ M' • ι → M ∼α M'

3. Prémisses Renforcées de la Règle d'Application

Ajout de prémisses de validité de type dans la règle d'application, simplifiant les preuves ultérieures:

⊢app : Γ ⊢ M : Π[x : A]B → Γ ⊢ N : A → Γ ⊢ B[x := N] : s
     → Γ ⊢ M·N : B[x := N]

Configuration Expérimentale

Environnement de Formalisation

• Assistant de preuve: Système Agda
• Échelle du code: Environ 3000 lignes de code
• Division modulaire: Cadre et métathéorie PTS occupant chacun la moitié

Contenu de la Vérification

1. Théorie fondamentale: Propriétés des opérations de substitution, équivalence de la conversion α
2. Métathéorie PTS: Affaiblissement, validité syntaxique, théorèmes de fermeture
3. Équivalence: Équivalence entre le système de règles infinies et le système de règles finies

Résultats Expérimentaux

Réalisations Principales

1. Mécanisation complète: Vérification mécanique réussie des propriétés métathéoriques fondamentales de PTS
2. Simplification des preuves: Tous les résultats (à l'exception de la complétude de la conversion α) sont prouvés par induction structurelle
3. Efficacité du code: 3000 lignes de code implémentant la théorie complète, plus concis que d'autres travaux

Théorèmes Clés

• Lemme 4.1 (Affaiblissement): thinning : ∀ {Γ Δ M A} → Γ ⊆ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M : A
• Lemme 4.3 (Validité syntaxique): syntacticValidity : ∀ {Γ M A} → Γ ⊢ M : A → ∃ λ s → A ≡ c s ⊎ Γ ⊢ A : c s
• Lemme 4.4 (Fermeture sous conversion α): closAlphaAsg : ∀ {Γ Δ M N A} → Γ ≈α Δ → M ∼α N → Γ ⊢ M : A → Δ ⊢ N : A
• Lemme 4.6 (Fermeture sous substitution): closureSub : ∀ {Γ Δ M A σ} → σ : Γ ⇀ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M • σ : A • σ

Résultats d'Équivalence

• Théorèmes 4.9-4.11: Preuve de l'équivalence bidirectionnelle entre le système de règles infinies et le système de règles finies standard

Travaux Connexes

Comparaisons Principales

1. McKinna & Pollack: Utilisation de noms de variables bisortés, évitant la conversion α mais nécessitant des prédicats de bonne formation
2. Barras & Werner: Utilisation de la notation de de Bruijn, environ 2600 lignes de code pour une fonctionnalité similaire
3. Urban et al.: Utilisation de Nominal Isabelle, environ 15K lignes de code, dont 1800 pour la métathéorie
4. Développements modernes: Formalisations de théories de types plus grandes par Abel et al., Adjedj et al., Sozeau et al.

Analyse des Avantages

• Directivité: La fermeture sous substitution de la conversion β peut être prouvée directement par induction structurelle
• Concision: Pas besoin de preuves d'équivalence supplémentaires ou de lemmes de renommage
• Praticité: Plus proche de l'implémentation réelle des vérificateurs de types

Conclusion et Discussion

Conclusions Principales

1. Vérification de faisabilité: Démonstration de la faisabilité de la mécanisation de la théorie des types dépendants utilisant une syntaxe traditionnelle et des noms de variables monosortés
2. Avantages de la méthode: La méthode de substitution de Stoughton reste efficace pour traiter les systèmes de types complexes
3. Contribution théorique: La définition améliorée de la conversion α simplifie les preuves clés

Limitations

1. Limitation d'échelle: Actuellement, seule la métathéorie fondamentale de PTS est traitée, sans propriétés plus complexes comme la normalisation forte
2. Considérations de performance: La complexité computationnelle des substitutions multiples peut affecter les applications pratiques
3. Extensibilité: L'extension à des systèmes de types plus grands (avec univers, grandes éliminations, etc.) reste à vérifier

Directions Futures

1. Extension à des systèmes plus complexes: Tels que ceux avec types inductifs et hiérarchies d'univers
2. Optimisation des performances: Recherche d'implémentations efficaces des opérations de substitution
3. Applications pratiques: Application des résultats théoriques aux implémentations réelles de vérificateurs de types

Évaluation Approfondie

Points Forts

1. Innovation théorique: La définition améliorée de la conversion α est une contribution théorique importante, simplifiant la complexité des preuves
2. Valeur pratique: L'utilisation de la syntaxe traditionnelle réduit l'écart entre théorie et pratique
3. Complétude: Fourniture d'une vérification mécanique complète de la métathéorie PTS
4. Clarté: Rédaction claire de l'article avec description précise des détails techniques
5. Reproductibilité: Fourniture du code Agda complet, facilitant la vérification et l'extension

Insuffisances

1. Portée de couverture: Comparée à certains travaux de formalisation à grande échelle, la couverture du contenu théorique est relativement limitée
2. Analyse de performance: Manque d'analyse approfondie de la complexité computationnelle des opérations de substitution
3. Vérification pratique: Absence de vérification comparative avec les implémentations réelles de vérificateurs de types
4. Discussion d'extensibilité: Discussion insuffisante des défis d'extension à des systèmes plus complexes

Influence

1. Contribution académique: Fourniture d'une nouvelle voie technique pour la mécanisation de la théorie des types dépendants
2. Valeur pratique: Fourniture d'une base théorique pour la vérification de la correction des vérificateurs de types
3. Méthodologie: L'application réussie de la méthode de substitution de Stoughton peut inspirer davantage de travaux connexes
4. Valeur des outils: La bibliothèque Agda peut fournir une infrastructure de base pour les recherches ultérieures

Scénarios d'Application

1. Vérification de vérificateurs de types: Applicable aux scénarios nécessitant la vérification de la correction des vérificateurs de types
2. Recherche pédagogique: Peut servir de bon cas d'étude pour l'apprentissage de la formalisation de la théorie des types dépendants
3. Recherche théorique: Fournit une base pour l'étude de la métathéorie de systèmes de types plus complexes
4. Développement d'outils: Peut servir d'implémentation de référence pour le développement d'outils de vérification formelle

Références

L'article cite 31 références importantes, incluant principalement:

• Stoughton (1988): Théorie originale des substitutions multiples
• Barendregt (1992): Théorie classique de PTS
• McKinna & Pollack (1993, 1999): Formalisation de PTS dans LEGO
• Barras & Werner: Formalisation de CC dans Coq
• Urban et al. (2011): Métathéorie de LF utilisant Nominal Isabelle
• Tasistro et al. (2015): Travail original sur le cadre de substitution de Stoughton

Évaluation générale: Cet article est un travail de haute qualité en informatique théorique, apportant des contributions importantes à la vérification mécanique de la théorie des types dépendants. Les points d'innovation technique de l'article sont clairs, l'implémentation est complète, et il fournit une base théorique et une expérience pratique précieuses pour les recherches ultérieures dans ce domaine.