Strong normalization through idempotent intersection types: a new syntactical approach

1. Problématique

L'article aborde la propriété de normalisation forte (SN) dans le cadre des systèmes de types d'intersection idempotents (où $A \land A \equiv A$). Il est bien établi que ces systèmes caractérisent la normalisation forte : un terme $\lambda$ est typable si et seulement si toutes ses séquences de réduction terminent.

Cependant, les preuves existantes de cette propriété reposent majoritairement sur des techniques sémantiques (comme les candidats de réductibilité ou la computabilité). Bien que ces preuves soient standard, elles manquent d'intuition sur le mécanisme dynamique de la réduction et ne fournissent pas de mesure explicite décroissante.

Il existe quelques preuves purement syntaxiques (basées sur une mesure décroissante) pour les types d'intersection, mais elles présentent des limitations :

• Elles utilisent souvent des langages intermédiaires ad hoc ou des règles de réduction complexes.
• Les mesures définies sont parfois des structures de données lourdes (multisets de nombres naturels, paires de nombres).
• Certaines approches reposent sur des traductions vers des types simples, ce qui entraîne une perte d'information et empêche d'obtenir une mesure aussi fine que possible.

L'objectif de cet article est de fournir une nouvelle preuve syntaxique de la normalisation forte pour les types d'intersection idempotents, utilisant une mesure simple (un nombre naturel) et opérant directement au sein du système de types, sans passer par des traductions ou des règles de réduction ad hoc complexes.

2. Méthodologie

Les auteurs adoptent une approche structurée en plusieurs étapes, s'inspirant des travaux récents sur le calcul $\lambda$ simplement typé (notamment [2]), mais en les adaptant aux spécificités des types d'intersection.

A. Conception d'un système intrinsèquement typé ($\Lambda^i_\cap$)

Contrairement aux systèmes classiques de Curry (extrinsèques) où les termes sont non typés et les règles attribuent des types, les auteurs définissent un système de style Church (intrinsèque), noté $\Lambda^i_\cap$.

• Syntaxe : Les termes et les ensembles de termes sont décorés par des types. L'idée centrale est de traiter l'intersection idempotente comme un ensemble de types. Ainsi, si $t$ et $s$ sont des termes de types $A$ et $B$, l'ensemble $\{t, s\}$ est un terme de type $\{A, B\}$.
• Correspondance : Ce système est conçu pour simuler le système extrinsèque $\Lambda^e_\cap$ (une variante du système original de Coppo et Dezani). Il existe une bijection entre les dérivations de typage dans $\Lambda^e_\cap$ et les termes dans $\Lambda^i_\cap$.

B. Introduction du calcul mémoire ($\Lambda^{im}_\cap$)

Pour définir une mesure décroissante, les auteurs enrichissent la syntaxe avec un calcul mémoire $\Lambda^{im}_\cap$.

• Enveloppes (Wrappers) : Ce calcul introduit des « enveloppes » notées $\langle \vec{s} \rangle$ qui mémorisent les sous-termes qui seraient autrement effacés lors d'une réduction $\beta$.
• Réduction non effaçante : Dans $\Lambda^{im}_\cap$, chaque étape de réduction $\beta$ crée une enveloppe contenant une copie de l'argument. Cela transforme une réduction effaçante (qui perd de l'information) en une réduction non effaçante, permettant de suivre l'histoire de la réduction.

C. Simplification complète et Définition de la mesure

Les auteurs définissent une opération de simplification complète ($S^*$) sur les termes de $\Lambda^{im}_\cap$.

• Cette opération réduit en parallèle tous les redexes d'un degré donné, en commençant par le degré maximal et en descendant jusqu'à 1.
• Grâce à l'observation de Turing (la contraction d'un redex ne crée pas de redex de degré supérieur ou égal), cette simplification aboutit à une forme normale unique.
• La mesure $W$ : La mesure de normalisation forte est définie comme le nombre d'enveloppes restantes dans la forme normale obtenue après simplification complète d'un terme typé dans $\Lambda^i_\cap$.
  $$W(t) = w(S^*(t))$$
  où $w$ compte le nombre d'enveloppes.

3. Contributions Clés

1. Système $\Lambda^i_\cap$ : La conception d'une version de style Church pour les types d'intersection idempotents, où les termes sont des ensembles décorés par des types. Ce système possède de bonnes propriétés (réduction du sujet, confluence) et simule fidèlement le système de Curry.
2. Preuve syntaxique par mesure simple : La définition d'une mesure de normalisation forte qui est un nombre naturel unique, contrairement aux multisets ou paires utilisés dans les travaux précédents ([22], [9]).
3. Universalité de la décroissance : La preuve montre que la mesure $W$ décroît strictement pour toute stratégie de réduction, et pas seulement pour une stratégie spécifique (comme la réduction intérieure ou extérieure).
4. Technique de « mémoire » : L'utilisation d'un calcul auxiliaire avec des enveloppes pour gérer l'effacement des termes tout en conservant une trace quantitative de la réduction, permettant d'éviter les techniques sémantiques lourdes.

4. Résultats Principaux

• Théorème de Normalisation Forte pour $\Lambda^i_\cap$ : Le système intrinsèque $\Lambda^i_\cap$ est fortement normalisant. Cela est prouvé en montrant que pour tout terme $t$, si $t \to_i s$, alors $W(t) > W(s)$.
• Correspondance et Simulation : Les systèmes $\Lambda^e_\cap$ (extrinsèque) et $\Lambda^i_\cap$ (intrinsèque) se simulent mutuellement. Une séquence de réduction infinie dans $\Lambda^e_\cap$ induirait une séquence infinie dans $\Lambda^i_\cap$, ce qui est impossible.
• Caractérisation de la Normalisation Forte : Le système $\Lambda^e_\cap$ caractérise exactement les termes fortement normalisables (un terme est typable si et seulement s'il est SN).
• Simplicité de la mesure : La mesure obtenue est plus fine et plus simple que celles basées sur des traductions vers des types simples, car elle opère directement dans le système d'intersection sans perte d'information structurelle.

5. Signification et Impact

Ce travail est significatif pour plusieurs raisons :

• Intuition Syntaxique : Il offre une compréhension plus intuitive de la normalisation forte dans les types d'intersection en fournissant une mesure explicite qui décroît à chaque étape, évitant le « mystère » des preuves sémantiques.
• Simplicité et Efficacité : La nature de la mesure (un simple entier naturel) la rend potentiellement plus facile à implémenter ou à analyser que les mesures complexes basées sur des structures de données imbriquées.
• Fondation pour l'Analyse Quantitative : En évitant les traductions qui perdent de l'information, cette approche ouvre la voie à des analyses computationnelles plus précises (par exemple, calculer des bornes exactes sur la longueur des réductions), ce qui est difficile avec les méthodes de traduction actuelles.
• Perspectives Futures : Les auteurs suggèrent que cette technique pourrait être adaptée pour caractériser d'autres propriétés, comme la solvabilité des termes, et vise à affiner la mesure pour obtenir une borne exacte (et non plus seulement une majoration) de la longueur des chaînes de réduction.

En résumé, cet article propose une avancée méthodologique majeure en démontrant la normalisation forte des types d'intersection idempotents par une approche purement syntaxique, élégante et quantitative, reliant directement la structure des dérivations de typage à la dynamique de la réduction.