💻 computer science

Well-Scoped Locally Nameless Representation of Syntax

Cet article présente une représentation générique et bien délimitée de la syntaxe localement sans nom pour Agda, paramétrée par des signatures de liaison de style Plotkin, en prouvant son adéquation par rapport à une syntaxe nommée naïve modulo la conversion alpha et en démontrant son utilité à travers des exemples.

Auteurs originaux : Andrew M. Pitts

Publié 2026-05-12

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Andrew M. Pitts

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 soyez bibliothécaire tentant d'organiser une bibliothèque massive et chaotique où les livres peuvent faire référence à d'autres livres à l'intérieur d'eux-mêmes. Certains livres ont des titres inscrits sur leurs couvertures (comme « Le Grand Gatsby »), tandis que d'autres sont simplement des étagères numérotées à l'intérieur d'une section spécifique (comme « Étagère 3, Rangée 2 »).

Ce papier, écrit par Andrew Pitts, traite d'une nouvelle méthode plus intelligente pour organiser cette bibliothèque afin que les ordinateurs (spécifiquement, les « prouveurs de théorèmes interactifs » comme Agda) puissent vérifier les règles de la bibliothèque sans se confondre ni commettre d'erreurs.

Voici la décomposition des idées du papier en utilisant de simples analogies :

1. Le Problème : Le Dilemme « Sans Nom » vs « Avec Nom »

Lorsque les informaticiens tentent d'enseigner à un ordinateur des langages (comme les langages de programmation ou la logique), ils doivent faire face aux variables.

La méthode « Avec Nom » : Vous donnez un nom à chaque variable, comme x, y ou z. C'est facile à lire pour les humains, mais les ordinateurs se confondent lorsque vous échangez des noms (un problème appelé « conversion alpha »). x est-il le même que y si vous les renommez ?
La méthode « Sans Nom » (Indices de De Bruijn) : Vous arrêtez complètement d'utiliser des noms. À la place, vous dites simplement « la 1re variable », « la 2e variable », etc., en comptant de l'intérieur vers l'extérieur. C'est excellent pour les ordinateurs mais terrible pour les humains car cela ressemble à un fouillis de chiffres.

2. L'Ancienne Solution : « Localement Nommé »

Il y a quelques années, des chercheurs ont proposé une idée hybride appelée Lokalement Nommé.

Les variables libres (choses non liées à l'intérieur d'une boucle ou d'une fonction) conservent leurs noms (comme x).
Les variables liées (choses à l'intérieur d'une boucle) utilisent des nombres (comme 0, 1).

L'Écueil : Ce système possède un « piège ». Il vous permet de créer des termes « brisés » où les nombres ne correspondent pas à la portée. Imaginez un livre disant « Allez à l'Étagère 5 », mais vous êtes actuellement dans une pièce qui n'a que 3 étagères. L'ordinateur doit constamment vérifier : « Ce terme est-il « localement clos » (valide) ? » Cela nécessite beaucoup de travail de preuve supplémentaire, comme un bibliothécaire vérifiant constamment si un livre est dans le bon allée avant de permettre à quiconque de l'emprunter.

3. La Nouvelle Solution : « Localement Nommé Bien Porté »

Ce papier propose une meilleure méthode : Lokalement Nommé Bien Porté.

Au lieu d'utiliser simplement des nombres, l'ordinateur utilise des types pour faire respecter les règles.

Imaginez la bibliothèque comme ayant différentes « pièces ».
Si vous êtes dans la Pièce 0, vous ne pouvez voir que les étagères numérotées 0 à 0 (ce qui signifie aucune étagère, seulement des noms libres).
Si vous êtes dans la Pièce 1, vous pouvez voir les étagères 0 et 1.
Si vous êtes dans la Pièce 5, vous pouvez voir les étagères 0 à 5.

La Magie : Dans ce système, vous ne pouvez littéralement pas construire un livre brisé. Si vous essayez d'écrire « Allez à l'Étagère 10 » tout en étant debout dans la Pièce 2, le système de types de l'ordinateur dit : « Non, c'est impossible. Vous ne pouvez même pas écrire cette phrase. »

Le papier soutient que cette approche :

Élimine le « Piège » : Vous n'avez pas besoin d'écrire des preuves supplémentaires pour vérifier si un terme est valide. Le fait que le terme existe prouve qu'il est valide.
Est Transparent : Il ressemble encore principalement à la méthode « Avec Nom » à laquelle les humains sont habitués, il n'est donc pas aussi confus que la méthode purement « Sans Nom ».
Est Générique : Les auteurs ont construit une « bibliothèque » (un ensemble d'outils) qui fonctionne pour n'importe quel langage que vous souhaitez définir, tant que vous décrivez les règles de liaison (comme le fonctionnement des instructions if ou des fonctions lambda) en utilisant un modèle standard.

4. Comment Cela Fonctionne (L'« Ouverture » et la « Fermeture »)

Le papier décrit deux opérations principales, qui sont comme déplacer des livres entre les pièces :

Abstraction (Fermeture) : Prendre un nom libre (comme x) et le transformer en un index lié (comme 0). C'est comme retirer un livre de l'étagère et le placer dans un emplacement numéroté spécifique dans une nouvelle pièce.
Concrétion (Ouverture) : Prendre un index lié et le remplacer par un livre spécifique (terme). C'est comme retirer un livre d'un emplacement et mettre un vrai livre à sa place.

Les auteurs prouvent que leur mathématique « Bien Portée » fonctionne parfaitement. Ils montrent que leur nouveau système est mathématiquement équivalent à l'ancien système « Avec Nom », ce qui signifie qu'ils représentent exactement les mêmes concepts, simplement organisés de manière plus sûre.

5. Exemples du Monde Réel

Le papier ne parle pas seulement de théorie ; ils ont testé leur « bibliothèque » sur trois types différents de langages :

Le Calcul Pi : Un langage utilisé pour décrire comment les programmes informatiques communiquent entre eux (comme des appels téléphoniques). Ici, les noms sont des « canaux » de communication.
La Théorie des Types de Martin-Löf : Un système complexe pour les preuves mathématiques. Ils ont montré comment écrire des règles pour les nombres naturels et les types sans se perdre dans la « fraîcheur » des noms.
Le Système T de Gödel : Un système pour prouver que les calculs finiront éventuellement (décidabilité). Ils ont utilisé leur méthode pour prouver qu'un algorithme spécifique fonctionne correctement.

La Conclusion

Le papier dit : « Arrêtez de vérifier manuellement si vos variables sont au bon endroit. Laissez le système de types de l'ordinateur faire le gros du travail pour vous. »

En utilisant des types dépendants (une fonctionnalité du langage de programmation Agda), ils ont créé un système où la syntaxe invalide est impossible à écrire. Cela économise aux chercheurs l'écriture de milliers de lignes de code de preuve ennuyeux juste pour dire : « Oui, cette variable est dans la portée ». Cela rend la vérification formelle (prouver qu'un logiciel est exempt de bugs) plus facile, plus sûre et plus proche de la façon dont les humains pensent naturellement au langage.

Résumé Technique : Représentation Localement Nommée Bien Scopiée de la Syntaxe

Énoncé du Problème
Lors de la formalisation de langages dotés de constructions de liaison (par exemple, le $\lambda$ -calcul, les systèmes de types) dans des prouveurs de théorèmes interactifs basés sur la théorie des types dépendants (tels qu'Agda, Lean ou Rocq), un défi central réside dans la gestion de la liaison des variables et de l'équivalence $\alpha$ . L'approche « localement nommée », qui représente les variables libres par des noms explicites et les variables liées par des indices de de Bruijn, a démontré sa capacité à satisfaire les critères PoplMark en termes de faible surcharge d'infrastructure, de transparence et de facilité d'accès. Cependant, les représentations localement nommées standard souffrent d'un défaut critique : la définition inductive des termes autorise des indices « en suspens » (des indices qui dépassent la portée actuelle). Pour garantir la correction, il faut restreindre le domaine à un sous-ensemble de termes « localement clos ». Cela nécessite des preuves répétitives et manuelles que les opérations (comme la substitution) préservent la clôture locale, créant une charge significative et une source d'erreurs potentielles dans les développements formels.

Méthodologie
L'article propose une variante « bien scopiée » de la représentation localement nommée qui exploite le système de types dépendants d'Agda pour imposer intrinsèquement la clôture locale, plutôt que comme un prédicat séparé.

Types Inductifs Indexés : Au lieu d'un unique type de termes, la bibliothèque définit une famille de types Trm[n] indexée par un nombre naturel $n$ . Un « $n$ -terme » est un terme où tous les indices de de Bruijn sont tirés du type fini Fin n (nombres naturels inférieurs à $n$ ).
Termes Localement Clos comme 0-Termes : Dans ce cadre, les termes « localement clos » (ceux sans indices en suspens) correspondent précisément à Trm[0]. Les termes avec des variables libres sont représentés comme Trm[n] où $n$ correspond au nombre de variables libres en scope.
Paramétrage par Signatures de Liaison : La bibliothèque est générique, paramétrée par une signature de liaison de style Plotkin. Cela permet de définir les opérateurs, leurs arités et le nombre de noms liés dans chaque position d'argument.
Opérations via Types Dépendants :
- Affaiblissement de Portée : Une fonction Trm[m] -> Trm[n] (pour $m \le n$ ) qui injecte les indices, gérant le décalage requis lors du passage à une portée plus large.
- Concrétion (Ouverture) : Remplacer un indice $i$ dans un terme de type (1+n) par un 0-terme pour produire un $n$ -terme. Cela implique de décaler les indices supérieurs à $i$ vers le bas d'une unité.
- Abstraction (Fermeture) : Remplacer un nom libre dans un $n$ -terme par un indice pour produire un (1+n)-terme. Cela implique de décaler les indices vers le haut.
- Substitution : Définie structurellement. Parce que la fonction de substitution mappe des noms vers des 0-termes (Trm), la condition de « clôture locale » est imposée automatiquement par le système de types. La substitution sur un $n$ -terme produit un autre $n$ -terme.

Contributions Clés

La Bibliothèque WSLN : Une bibliothèque générique Agda implémentant des termes localement nommés bien scopiés. Elle fournit l'infrastructure pour définir la syntaxe, les opérations (affaiblissement, substitution, abstraction, concrétion) et les principes de raisonnement pour tout langage spécifié par une signature de liaison Plotkin.
Preuve d'Adéquation Formelle : L'article fournit une preuve rigoureuse établissant une bijection entre :
1. Le type des 0-termes localement nommés bien scopiés (Trm[0]).
2. Les classes d'équivalence $\alpha$ de termes « nommés » (termes avec des noms explicites pour les variables libres et liées).
  Cette bijection démontre que la représentation bien scopiée capture correctement la sémantique de la substitution évitant la capture et de l'équivalence $\alpha$ .
Élimination des Preuves de Clôture Locale : En encodant les contraintes de portée dans les indices de type, la nécessité de prédicats explicites de « clôture locale » et des obligations de preuve associées (par exemple, prouver que la substitution préserve la clôture locale) est éliminée. Ces propriétés deviennent des conséquences des règles de typage.
Gestion de la Fraîcheur : La bibliothèque s'intègre aux techniques nominales, utilisant un ensemble « finiment inépuisable » d'atomes (nombres naturels) pour générer des noms frais via une quantification cofinie, garantissant que les conditions de fraîcheur sont traitées systématiquement.

Résultats
L'article valide l'approche à travers trois exemples distincts implémentés en Agda :

$\pi$ -Calcul : Démontre l'applicabilité de la bibliothèque au-delà du $\lambda$ -calcul, en gérant les expressions de processus et les noms de canaux. Il met en évidence que, bien que la bibliothèque gère la structure de liaison, le typage pour la validité (par exemple, s'assurer que les canaux sont utilisés là où attendu) reste un jugement séparé, défini par l'utilisateur.
Théorie des Types de Martin-Löf (MLTT) : Montre comment la bibliothèque facilite la définition des règles de typage. Elle oppose les règles « existe-frais » (nécessitant des hypothèses de fraîcheur explicites) aux règles de « quantification cofinie » (où la fraîcheur est implicite), démontrant que la représentation bien scopiée soutient cette dernière, conduisant à des formalisations plus claires et plus transparentes.
Système T de Gödel (Normalisation par Évaluation) : Un développement substantiel prouvant la décidabilité de la conversion $\beta\eta$ . Cet exemple illustre comment la représentation bien scopiée simplifie la sémantique de l'abstraction et la gestion de la fraîcheur dans des constructions sémantiques complexes (préfaisceaux à valeurs en ensembles), évitant le besoin d'objets sémantiques à support fini.

Signification et Revendications
L'article revendique que la représentation localement nommée bien scopiée offre une solution « directe » mais puissante au « piège » des indices en suspens trouvé dans les approches localement nommées traditionnelles. Sa signification principale réside dans le transfert de la charge d'assurer la correction de la portée de l'utilisateur (via des preuves manuelles) vers le vérificateur de types du prouveur de théorèmes (via les types dépendants).

Les auteurs soulignent que cette approche maintient la transparence requise par les critères PoplMark : les définitions formelles reflètent étroitement les conventions informelles, et le « yoga des indices » (manipulation des indices de de Bruijn) est encapsulé au sein des opérations de la bibliothèque. Bien que l'implémentation nécessite une manipulation attentive des ordinaux finis (Fin n) et du décalage d'indices, la bibliothèque paramétrise cette complexité, permettant aux utilisateurs de définir des langages et de prouver des propriétés sans gérer les mécanismes de portée de bas niveau. L'article note modestement que, bien que les signatures de liaison actuelles soient non triées et modélisent des scopes de liaison simples, l'approche est suffisamment robuste pour gérer des systèmes de types complexes et des preuves sémantiques, comme en témoigne le développement du Système T.