Principal Typing for Intersection Types, Forty-Five Years Later

1. Problématique et Contexte

L'article s'intéresse à la propriété de typage principal dans le cadre des types d'intersection pour le $\lambda$-calcul.

• Définition du problème : Un système d'attribution de types possède la propriété de typage principal si, pour tout terme typable $M$, il existe un type (ou une paire de contexte et de type) « principal » tel que tous les autres types dérivables pour $M$ puissent être obtenus à partir de ce type principal via des opérations spécifiques (généralement la substitution).
• Historique et difficultés : Bien que l'existence de typages principaux ait été établie depuis plus de 40 ans (notamment par Coppo, Dezani et Venneri), les preuves et les algorithmes d'inférence associés ont toujours été complexes. Ils reposaient sur des notions techniques subtiles, notamment l'opération d'expansion, nécessaire car, contrairement au typage simple, les dérivations de types dans les systèmes d'intersection peuvent différer non seulement par les types aux nœuds, mais aussi par la structure même de l'arbre de dérivation.
• Objectif : Les auteurs visent à fournir une formulation plus accessible et moderne de ces résultats, en simplifiant les mécanismes techniques et en clarifiant les opérations fondamentales nécessaires à la construction de typages principaux.

2. Méthodologie

Les auteurs proposent une approche syntaxique basée sur trois concepts clés :

A. Les Pré-types et les Pseudo-dérivations

Pour gérer la complexité des ensembles (multisets) de types, les auteurs introduisent les pré-types, où les multisets sont remplacés par des listes ordonnées.

• Une pseudo-dérivation est un arbre de jugements attribuant des pré-types aux termes, associé à un système d'équations entre pré-types ($E_\Pi$).
• Ces équations capturent les contraintes nécessaires pour transformer la pseudo-dérivation en une dérivation valide.

B. Trois Opérations Fondamentales

L'article identifie trois opérations élémentaires permettant de construire n'importe quelle dérivation de type à partir d'une dérivation minimale :

1. Substitution : Pour résoudre les équations entre pré-types (unification).
2. Expansion : Une opération structurelle qui augmente le nombre de prémisses d'une règle d'intersection (règle many). Elle permet d'ajuster la structure de l'arbre pour résoudre des équations « bloquées » (où la longueur des listes ne correspond pas).
3. Effacement (Erasure) : L'opération inverse de l'expansion, réduisant le nombre de prémisses. Elle est nécessaire dans le système général $\mathcal{N}$ (caractérisant la normalisation par tête), mais non nécessaire dans le système fort $\mathcal{N}_s$.

C. L'Algorithme d'Inférence Semi-Algorithmique (InferStrong)

Les auteurs conçoivent un algorithme non déterministe, InferStrong, conçu pour le système fort $\mathcal{N}_s$ (qui caractérise la normalisation forte).

• Fonctionnement :
  1. Il part de la pseudo-dérivation minimale du terme d'entrée.
  2. Il tente de résoudre le système d'équations associé par unification.
  3. Si l'unification échoue car une équation est « bloquée » (différence de longueur de listes), l'algorithme applique une expansion minimale sur la règle concernée pour rééquilibrer les listes.
  4. Ce processus se répète jusqu'à ce que le système soit résolvable (forme résolue) ou que le terme ne soit pas normalisable fortement.

3. Contributions Clés

1. Formulation Simplifiée : La réintroduction des notions classiques (expansion, substitution) via les pseudo-dérivations et les listes permet de contourner la complexité bureaucratique des approches antérieures (comme les variables d'expansion de Kfoury et Wells).
2. Correction et Complétude :
   • Théorème de Correction : Tout résultat produit par l'application des opérations sur une pseudo-dérivation correspond à une dérivation valide dans le système $\mathcal{N}$ (ou $\mathcal{N}_s$).
   • Théorème de Complétude : Toute dérivation valide pour un terme $M$ peut être obtenue à partir de la pseudo-dérivation minimale de $M$ par une séquence d'expansions/effacements et une substitution.
3. Algorithme d'Inférence pour la Normalisation Forte : L'algorithme InferStrong calcule le typage principal pour tous et seulement les termes fortement normalisants.
4. Propriétés de Confluence et d'Unicité : Bien que l'algorithme soit non déterministe (choix de l'équation bloquée), les auteurs prouvent que le résultat final (le typage principal) est unique à renommage de variables près.

4. Résultats Principaux

• Terminaison : L'algorithme InferStrong termine si et seulement si le terme d'entrée est fortement normalisant (Théorème 30 et Corollaire 31). La preuve repose sur une stratégie de réduction perpétuelle ($F_\infty$) qui relie la structure de la dérivation de type à la réduction du terme $\lambda$.
• Typage Principal : Si l'algorithme termine, il produit un typage principal. Tout autre typage pour ce terme peut être dérivé de ce résultat par des expansions supplémentaires et une substitution (Théorème 34).
• Distinction Systèmes :
  • Dans le système général $\mathcal{N}$ (normalisation par tête), les opérations d'expansion et d'effacement sont toutes deux nécessaires.
  • Dans le système fort $\mathcal{N}_s$ (normalisation forte), seule l'expansion est requise, car l'effacement n'est pas nécessaire pour les termes fortement normalisants dans ce contexte.

5. Signification et Impact

• Perspective Moderne : Ce travail offre une vue d'ensemble plus claire et pédagogique de résultats fondamentaux datant de plus de 40 ans, rendant les concepts d'intersection types plus accessibles.
• Lien Réduction-Typage : L'article renforce le lien profond entre la réduction des termes $\lambda$ et l'inférence de types. L'algorithme se comporte essentiellement comme un interpréteur non déterministe qui construit le type en parallèle de la réduction du terme.
• Fondation pour d'autres Systèmes : La méthodologie proposée sert de « modèle » (blueprint) pour concevoir des algorithmes d'inférence pour d'autres systèmes de types, y compris les systèmes à types d'intersection idempotents (où les ensembles remplacent les multisets, mais où la logique des opérations reste similaire grâce aux conditions de disjointness).
• Apport à la Théorie : En prouvant que l'unification sur les pré-types ne génère pas de formes non résolubles (circularités) dans ce contexte spécifique, les auteurs clarifient un point technique souvent sous-estimé dans la littérature antérieure.

En résumé, cet article redéfinit l'inférence de typage principal pour les types d'intersection en utilisant une approche syntaxique élégante basée sur des opérations structurelles (expansion/effacement) et des contraintes d'équations, offrant ainsi un cadre robuste pour caractériser la normalisation forte.