Résumé technique : Graphes cycliques et mémoïsation dans le $\lambda$-calcul pur

1. Énoncé du problème

Le $\lambda$-calcul pur, dans sa sémantique opérationnelle standard, est fondamentalement incapable de représenter ou de manipuler efficacement des structures de données cycliques et des calculs infinis sans extensions externes.

• Représentation de données cycliques : La réduction standard (par exemple, $Y(\text{cons } 0)$) déroule les flux infinis en arbres infinis ($0, 0, 0, \dots$) plutôt qu'en repliant ces derniers en graphes cycliques finis. Pour obtenir un cycle fini, les approches traditionnelles nécessitent l'ajout de constructions de récursion comme letrec ou des $\mu$-liaisons.
• Mémoïsation et programmation dynamique : Les programmes fonctionnels purs implémentant la programmation dynamique (par exemple, la distance d'édition) ou les parcours de graphes (par exemple, une carte sur une liste cyclique) souffrent d'une complexité temporelle exponentielle ou d'une non-terminaison. Les solutions standards nécessitent des mécanismes impurs : des caches mutables pour la mémoïsation, des primitives d'égalité de référence pour la détection de cycles, ou des structures de suivi d'état explicites. Ces méthodes violent la transparence référentielle, un pilier des langages fonctionnels purs.
• L'obstacle central : L'article identifie que la réduction ordinaire manque d'un mécanisme pour reconnaître si un terme a déjà été visité auparavant. Sans moyen de détecter l'« identité d'état » de manière pure, le calcul ne peut pas automatiquement partager les sous-problèmes répétés ou replier les déroulements infinis en cycles finis.

2. Méthodologie

Les auteurs proposent une nouvelle sémantique opérationnelle pour le $\lambda$-calcul pur basée sur le tablage de la réduction faible tête (weak-head reduction). Cette approche ne nécessite aucune extension du calcul (pas de letrec, pas d'impureté) mais modifie la manière dont l'interprète exécute les termes.

2.1 Réduction faible tête avec tabulation (Tabling)

La méthodologie combine deux concepts :

1. Réduction faible tête (Weak-Head Reduction) : L'interprète expose une « couche » d'un terme à la fois (le constructeur supérieur de sa forme normale faible tête) sur ses sous-termes immédiats. Cela définit une « carte d'une couche » ($out$).
2. Tablage (Mémoïsation par identité d'état) : L'interprète maintient une table d'états (sous-termes) rencontrés lors de la réduction.
   • Identité d'état : Les états sont identifiés par leur identité structurelle (via l'internage/hash-consing de termes de dé Bruijn). Il s'agit d'un test de pointeur constant et décidable.
   • Résolution : Lorsqu'un terme est rencontré :
     • S'il s'agit d'un nouvel état, l'interprète calcule sa couche et récurse.
     • S'il s'agit d'un état récurrent déjà présent dans la table, l'interprète réutilise l'entrée existante.
     • S'il s'agit d'un état récurrent actuellement sur la pile (un arc de retour/back-edge), l'interprète ferme un cycle dans le graphe plutôt que de le dérouler indéfiniment.

2.2 L'algorithme

L'évaluation procède via une itération de Kleene de $\bot$ (indéfini) vers un point fixe inférieur :

• Algorithme 1 (Pilote) : Résout les termes de manière itérative. Il fusionne les couches calculées dans une approximation courante en utilisant un opérateur de fusion profonde ($\sqcup$). Si un terme est réentré alors qu'il est encore sur la pile, il retourne l'approximation actuelle (initialement $\bot$).
• Algorithme 2 (WHNF) : La carte d'une couche spécifique pour la réduction faible tête. Elle contracte les redex de tête jusqu'à ce qu'un constructeur (variable, abstraction ou application) soit exposé.
• Algorithme 3 (Évaluateur) : Compose le pilote et la carte. Il retourne un graphe fini (potentiellement cyclique) où les nœuds représentent des termes et les arêtes représentent des sous-termes.

2.3 Fondement théorique

• Correction (Soundness) : Le graphe retourné par l'évaluateur se déroule en l'arbre de Lévy–Longo du terme. Le graphe est une représentation finie de la sémantique dénotationlle du terme.
• Unicité : La solution est unique car la réduction est « gardée » (la racine est engagée avant la lecture des sous-termes). Cela garantit que le point fixe inférieur (calculé par l'évaluateur) est égal au point fixe supérieur (l'arbre coinductif), rendant le résultat indépendant de l'ordre de réduction.
• Terminaison : Si un terme atteint un nombre fini d'états distincts (identité structurelle), l'évaluateur se termine avec un graphe cyclique fini. S'il atteint un nombre infini d'états distincts, il se comporte comme la réduction standard (divergence potentielle).

3. Résultats clés et études de cas

Les auteurs ont implémenté cette sémantique sous la forme d'un interprète (Co-Lambda) et ont démontré ses capacités sur trois régimes :

1. Programmation dynamique (Distance d'édition) :

   • Un terme $\lambda$ pur pour la distance d'édition, qui prendrait naïvement un temps exponentiel, est évalué en $O(mn)$ en temps et en espace.
   • L'interprète partage automatiquement les sous-problèmes (paires de suffixes) car ils sont des nœuds internés structurellement identiques. Aucune table de mémoïsation ou ensemble de visites n'est écrit dans le code source ; la « table » est la table d'état interne de l'interprète.
   • Résultat : L'arbre d'appel exponentiel se réduit en un graphe fini représentant la table de DP standard.

2. Données cycliques (Flux de zéros) :

   • Le terme $r = Y(\text{cons } 0)$, que la réduction standard déroule en un flux infini de zéros, est évalué comme un graphe cyclique fini.
   • L'interprète détecte que la queue du flux est le même nœud interné que la computation actuelle, fermant ainsi un arc de retour.
   • Résultat : Le terme $r$ est évalué comme un graphe fini avec une auto-boucle, représentant le flux infini sans consommation de mémoire infinie.

3. Boucles improductives ($\Omega$) :

   • Le terme $\Omega = (\lambda x. x x)(\lambda x. x x)$ se réduit à lui-même sans exposer de couche de constructeur.
   • La réduction standard diverge. L'évaluateur avec tabulation détecte la réentrée dans la pile sans couche exposée, identifie l'état comme improductif, et retourne $\bot$ en un temps fini.
   • Résultat : L'interprète décide de la non-terminaison pour les boucles spécifiques qui ne produisent aucune donnée.

4. Contributions

• Construction : Une sémantique opérationnelle basée sur le tablage pour le $\lambda$-calcul pur qui replie automatiquement les arbres infinis rationnels en graphes cycliques finis et décide les boucles improductives.
• Théorie : Preuves de correction (le graphe se déroule en arbre de Lévy–Longo), d'unicité (point fixe inférieur = supérieur) et de bornes de terminaison (graphe fini si et seulement si le nombre d'états atteignables est fini).
• Applications :
  • DSL pour le calcul sur graphes : L'interprète agit comme un langage de domaine spécifique où la mémoïsation, les tables de transposition (recherche de jeux) et les ensembles de visites (accessibilité de graphe) sont des conséquences implicites de l'identité d'état.
  • Compilateur auto-compilé : Les auteurs ont construit un compilateur bootstrap (écrit en terme $\lambda$ pur) qui compile son propre code source en Python. Le compilateur utilise le même mécanisme de tabulation pour optimiser le processus de compilation (défunctionalisation), atteignant des gains de vitesse significatifs (environ 5x) et des réductions de mémoire par rapport à la version interprétée.

5. Signification et affirmations

Le papier affirme résoudre le « prix de la pureté » de deux manières :

1. Élimination des extensions : Il démontre que les graphes cycliques et la mémoïsation peuvent être obtenus sans ajouter de constructions de récursion (letrec) ou de primitives impures (égalité de pointeur) au langage. La « reconnaissance » des cycles est effectuée par le solveur (l'interprète), et non par le terme.
2. Fragment rationnel : Le calcul devient un petit DSL pour les calculs « rationnels » (ceux possédant un nombre fini de sous-arbres distincts). Pour ces calculs, l'interprète fournit automatiquement la programmation dynamique et le repli de cycles.
3. Limitations : Le papier reconnaît un « plafond rationnel ». La méthode repose sur l'identité structurelle (décidable). Elle ne peut pas replier des termes qui sont équivalents par comportement ($\beta$-égaux) mais structurellement distincts, car la $\beta$-égalité est indécidable. Elle résout donc le fragment rationnel, mais pas l'espace complet de tous les comportements infinis possibles.

Ce travail recadre le $\lambda$-calcul non pas seulement comme un langage pour des calculs impératifs (réduction étape par étape) mais comme un langage pour déclarer des calculs (spécifier le graphe à construire), où le solveur gère l'efficacité et la terminaison de la construction du graphe.