Utilisateur:JeanCASPAR/Brouillon/candidats de réductibilité

Candidats de réductibilité

La méthode des candidats de réductibilité a été développée William W. Tait (en) pour prouver la forte normalisation du système T et étendue ensuite par Jean-Yves Girard pour montrer la forte normalisation du système F, plus particulièrement, sa terminaison. En effet, une simple récurrence sur la taille du type ou du terme n'est pas suffisante, pour deux raisons. Premièrement, si $\lambda x.M$ et $N$ sont fortement normalisables, ce n'est pas nécessairement le cas de $(\lambda x.M)N$. Deuxièmement, pour montrer que $\Lambda \alpha .M:\forall \alpha .T$ est fortement normalisable, il faut montrer que pour tout type $U$, $M\{\alpha :=U\}:T\{\alpha :=U\}$ est fortement normalisable, or $T\{\alpha :=U\}$ n'est pas nécessairement un type plus petit que $\forall \alpha .T$, ce qu'on peut constater en choisissant $T=\alpha \to \alpha$, $U=\forall \alpha .T$, on a alors $T\{\alpha :=U\}=(\forall \alpha .T)\to (\forall \alpha .T)$.

Un candidat de réductibilité $C$ de type $T$ est un ensemble de termes de type $A$ qui vérifie un certain nombre de propriétés :

• tous les termes d'un candidat sont fortement normalisables,
• un candidat est stable par réduction,
• si $t$ est un terme neutre et que tous les réduits de $t$ sont dans $C$, alors $t\in C$. Un terme neutre est une variable, appliquée à une liste potentiellement vide de types et de termes en forme normale.

En particulier, l'ensemble $SN_{A}$ des termes fortement normalisables de type $A$ est un candidat de réductibilité de type $A$.

Soit $A$ un type dont les variables libres sont incluses dans $\alpha _{1},\dots ,\alpha _{n}$ et $R_{1},\dots ,R_{n}$ des candidats de réductibilité de type $\alpha _{1},\dots ,\alpha _{n}$ respectivement. On définit par induction sur $A$ l'ensemble $RED_{A}^{(R_{i})_{i}}$, qui est un candidat de réductibilité de type $A$ :

• Si $A$ est la variable $X_{i}$, $RED_{A}^{(R_{i})_{i}}=R_{i}$.
• Si $A=T\to U$, $RED_{A}^{(R_{i})_{i}}=\{M\mid \forall N\in RED_{T}^{(R_{i})_{i}},MN\in RED_{U}^{(R_{i})_{i}}\}$.
• Si $A=\forall \alpha .T$, $RED_{A}^{(R_{i})_{i}}=\bigcap _{U~{\textrm {type}}}\bigcap _{R'\in {\mathcal {C}}_{U}}RED_{T\{\alpha :=U\}}^{R_{1},\dots ,R_{n},R'}$, où ${\mathcal {C}}_{U}$ désigne l'ensemble des candidats de réductibilité de type $U$.

Ensuite, on montre, par induction sur la dérivation, que si $\Gamma \vdash M:A$, $M\in RED_{A}^{SN_{\alpha _{1}},\dots ,SN_{\alpha _{n}}}$. On peut en déduire que si $M$ est typable alors $M$ est fortement normalisable.

Les candidats de réductibilité connaissent plusieurs variantes, par exemple les candidats peuvent être non-typés, et cette technique a été largement déclinée pour divers systèmes de types, présentant des caractéristiques variées : intersections de types, types récursifs, types modaux, types dépendants.