Système T

À l'instar de la récursion primitive ou le lambda-calcul, le système T ou l'arithmétique dans les types finis, parfois notée $\mathbf {HA} ^{\omega }$ est un système formel. Il a été inventé par le logicien Kurt Gödel pour montrer la cohérence de l'arithmétique de Heyting au moyen de son interprétation Dialectica (en).

Ce système consiste en une extension du lambda-calcul simplement typé avec des entiers naturels et la possibilité de définir des fonctions par récurrence. Le système T est plus expressif que le lambda-calcul simplement typé et que la récursion primitive étant donné qu'il permet de définir la fonction d'Ackermann. En fait, les fonctions définissables dans le système T sont exactement les fonctions prouvablement totales dans l'arithmétique de Peano, ou de façon équivalente, dans l'arithmétique de Heyting.

Le principe est simple : on garde les schémas récursifs primitifs, notamment celui de la récurrence primitive :

• $f(0,{\vec {y}})=g({\vec {y}})$

• $f(x+1,{\vec {y}})=h(x,f(x,{\vec {y}}),{\vec {y}})$

La différence majeure est que l'on autorise désormais les paramètres ${\vec {y}}$ à être des fonctions. Par rapport à la récursion primitive, il est alors possible, par exemple, de faire une récurrence sur plusieurs paramètres.

Formalisme

Le formalisme se base sur celui du lambda-calcul simplement typé. On y ajoute un type représentant les entiers naturels, $\mathbb {N}$, ainsi qu'un type représentant les booléens, $\mathbb {B}$. Il est également possible d'ajouter des types produits.

Pour les booléens, on considère deux constantes, $\operatorname {True}$ (Vrai en anglais) et $\operatorname {False}$ (Faux en anglais), ainsi qu'une construction $\operatorname {if} _{A}u~v~w$ avec $u$ un booléen et $v$ et $w$ de même type $A$. Cette opération représente une instruction conditionnelle : si $u$ est vrai, on renvoie $v$, sinon $w$. Cela se traduit par les règles $\operatorname {if} _{A}\operatorname {True} v~w\to v$ et $\operatorname {if} _{A}\operatorname {False} v~w\to w$.

$(\operatorname {T} )\;{\frac {}{\Gamma \vdash \operatorname {True} :\mathbb {B} }}$	$(\operatorname {F} )\;{\frac {}{\Gamma \vdash \operatorname {False} :\mathbb {B} }}$
$(\operatorname {if} )\;{\frac {\Gamma \vdash u:\mathbb {B} \quad \Gamma \vdash v:A\quad \Gamma \vdash w:A}{\Gamma \vdash \operatorname {if} _{A}u~v~w:A}}$

Les entiers sont construits soit à partir de la constante $0$, soit comme le successeur $\operatorname {S} u$ d'un autre entier $u$, qui représente $u+1$. Ainsi, si $n$ est un entier naturel usuel, il sera représenté dans le système T par le terme $\operatorname {S} ^{n}0=\overbrace {\operatorname {S} \cdots \operatorname {S} } ^{n}~0$, qui consiste en $n$applications successives de $\operatorname {S}$ au terme $0$.

Si $u$ est un entier, $v$ a pour type $A$ et $w$ est une fonction qui prend un entier et un élément de type $A$ et renvoie un élément de type $A$, $\operatorname {rec} _{A}u~v~w$ est de type $A$. L'idée derrière $\operatorname {rec}$ est que le terme $\lambda u^{\mathbb {N} }.\operatorname {rec} _{A}u~v~w$ représente la fonction $f$ définie par récurrence avec $f(0)=u$ et $f(n+1)=w(n,f(n))$ : on considère donc les règles de réduction $\operatorname {rec} _{A}0~v~w\to v$ et $\operatorname {rec} _{A}(\operatorname {S} u)~v~w\to wu(\operatorname {rec} _{A}u~v~w)$.

$(0)\;{\frac {}{\Gamma \vdash 0:\mathbb {N} }}$	$(\operatorname {S} )\;{\frac {\Gamma \vdash u:\mathbb {N} }{\Gamma \vdash \operatorname {S} ~u:\mathbb {N} }}$
$(\operatorname {rec} )\;{\frac {\Gamma \vdash u:\mathbb {N} \quad \Gamma \vdash v:A\quad \Gamma \vdash w:\mathbb {N} \to A\to A}{\Gamma \vdash \operatorname {rec} _{A}u~v~w:A}}$

On peut de montrer que les termes clos — c'est-à-dire sans variable libre — de type $\mathbb {N}$ sont tous de la forme $\operatorname {S} ^{n}0$ pour un certain entier naturel $n$, et les termes clos de type $\mathbb {B}$ sont $\operatorname {True}$ et $\operatorname {False}$. De plus, on peut noter que la réduction est confluente, préserve les types et est fortement normalisante, ce dernier résultat a été démontré en premier par Tait.

Combinateurs typés

L'article originel de Gödel présente un formalisme basé sur des combinateurs typés plutôt que sur le lambda-calcul simplement typé. Tait considère que c'est parce qu'il est plus facile de raisonner avec des combinateurs plutôt qu'avec le lambda-calcul, qui évitent de devoir gérer la substitution et les variables libres et liées, mais Troelstra et lui définissent les lambda-termes à partir des combinateurs. Girard quant à lui présente le système T uniquement avec le lambda-calcul dans sa thèse et dans son livre, en ajoutant un type des booléens et un type produit.

Exemples

Le prédécesseur

La fonction prédécesseur vérifie les équations suivantes :

• ${\mathsf {Pred}}~0=0$ ;
• ${\mathsf {Pred}}~(\operatorname {S} n)=n$.

On peut donc l'écrire sous forme de terme comme :

${\mathsf {Pred}}=\lambda n^{\mathbb {N} }.\operatorname {rec} _{\mathbb {N} }n~0~\left(\lambda n'^{\mathbb {N} }.\lambda r^{\mathbb {N} }.n'\right).$

Un minimum efficace

En récursion primitive, on ne peut pas faire une fonction qui retourne le minimum de deux entiers en temps de calcul minimum de ces deux entiers, pour la stratégie d'évaluation d'appel par nom. C'est très contraignant si on calcule, par exemple, le minimum de 2 et 1 000 000. Comme le système T permet les récursions sur plusieurs paramètres, on peut trouver un algorithme plus efficace.

Intuitivement, la fonction minimum vérifie les équations suivantes :

• ${\mathsf {Min}}~0~0=0$ ;
• ${\mathsf {Min}}~(\operatorname {S} 0)~0=0$ ;
• ${\mathsf {Min}}~(\operatorname {S} m)~(\operatorname {S} n)=\operatorname {S} ({\mathsf {Min}}~m~n)$.

En transformant un peu on obtient des équations utilisant le schéma souhaité :

• ${\mathsf {Min}}~0=\lambda m^{\mathbb {N} }.~0$ ;
• ${\mathsf {Min}}~(\operatorname {S} m)=\lambda n^{\mathbb {N} }.{\mathsf {Min'}}({\mathsf {Min}}~m)~n$ ;
• ${\mathsf {Min'}}f~0=0$ ;
• ${\mathsf {Min'}}f~(\operatorname {S} ~n)=\operatorname {S} (f~n)$.

Le terme voulu est :

${\mathsf {Min}}=\lambda m^{\mathbb {N} }.\operatorname {rec} _{\mathbb {N} \to \mathbb {N} }m~(\lambda n^{\mathbb {N} }.~0)~\left(\lambda m'^{\mathbb {N} }.\lambda f^{\mathbb {N} \to \mathbb {N} }.\lambda n^{\mathbb {N} }.\operatorname {rec} _{\mathbb {N} }n~0~\left(\lambda n'^{\mathbb {N} }.\lambda r^{\mathbb {N} }.\operatorname {S} (f~n')\right)\right).$

De la même manière, on peut obtenir facilement un programme optimisé pour l'addition et la soustraction.

La fonction d'Ackermann

La fonction d'Ackermann est définie ainsi :

• ${\mathsf {Ack}}(m,n)={\begin{cases}n+1&{\mbox{si }}m=0\\{\mathsf {Ack}}(m-1,1)&{\mbox{si }}m>0{\mbox{ et }}n=0\\{\mathsf {Ack}}(m-1,{\mathsf {Ack}}(m,n-1))&{\mbox{si }}m>0{\mbox{ et }}n>0.\end{cases}}$

On remarque que cette définition n'est pas une instance valide du schéma de récurrence primitive récursive : en effet, la récurrence primitive n'autorise pas à définir par récurrence une fonction qui renvoie autre chose qu'un entier (en l'occurence, il faudrait pouvoir renvoyer une fonction), mais ce n'est pas une limitation de système T. En fait, la fonction d'Ackermann n'est pas une fonction primitive récursive.

Ainsi, en modifiant un peu la définition, on obtient la forme désirée :

• ${\mathsf {Ack}}~0=\lambda n^{\mathbb {N} }.\operatorname {S} n$ ;
• ${\mathsf {Ack}}~(\operatorname {S} m)=\lambda n^{\mathbb {N} }.{\mathsf {Ack'}}~({\mathsf {Ack}}~m)~n$ ;
• ${\mathsf {Ack'}}~f~0=f(\operatorname {S} 0)$ ;
• ${\mathsf {Ack'}}~f~(\operatorname {S} n)=f({\mathsf {Ack'}}~f~n)$.

Dans la fonction auxiliaire, la variable $f$ contient la fonction ${\mathsf {Ack}}~m$. Il n'y a plus qu'à écrire cela sous forme de terme :

${\mathsf {Ack}}=\lambda m^{\mathbb {N} }.\operatorname {rec} _{\mathbb {N} \to \mathbb {N} }~m~\left(\lambda n^{\mathbb {N} }.\operatorname {S} n\right)~\left(\lambda m'^{\mathbb {N} }.\lambda f^{\mathbb {N} \to \mathbb {N} }.\lambda n^{\mathbb {N} }.\operatorname {rec} _{\mathbb {N} }~n~\left(f~(\operatorname {S} 0)\right)~\left(\lambda n'^{\mathbb {N} }.\lambda r^{\mathbb {N} }.fr\right)\right).$

Formules

On peut introduire une théorie $\mathbf {HA} ^{\omega }$ dont les termes sont décrits par ceux de système T. Gödel a introduit la première version intensionnelle de cette théorie, qui a été étudiée de façon plus extensive par Tait, qui en prouve la cohérence. Dans sa thèse, Girard présente également $\mathbf {HA} ^{\omega }$ avec plusieurs extensions, notamment un passage à l'ordre supérieur (ce qui correpspond au système F. Enfin, Troelstra présente de façon extensives toutes les variantes connues de $\mathbf {HA} ^{\omega }$ dans son livre, ainsi que différents résultats de cohérence relative et la compatibilité de chacune de ces variantes avec l'interprétation Dialectica (en). Ces variantes sont résumées par van den Berg, qui commente l'importance du fait l'égalité est observationnelle dans chacune de ces théories, sauf dans le système neutre.

Les formules sont formées par quantification universelle et existentielle, conjonction, disjonction, négation et implication, à partir des formules atomiques $\top$ (la formule toujours vraie), $\bot$ (la formule toujours fausse) et $s=_{T}t$ où $T$ est un type et $s$ et $t$ deux termes de types $T$, qui désigne la formule vraie si $s$ et $t$ sont égaux et fausse s'ils sont différents. Les règles de démonstration sont celles de la déduction naturelle dans sa variante intuitionniste, c'est-à-dire sans la règle de démonstration par l'absurde. Les règles de démonstration comprennent également la récurrence sur les entiers, qui énonce que si une formule $A$ est vraie pour 0 et que si pour tout $n$, si $A$ est vraie pour $n$ elle est vraie pour $n+1$, alors elle est vraie pour tout entier :

$A[x:=0]\land (\forall n^{\mathbb {N} },A[x:=n]\implies A[x:=\operatorname {S} n])\implies \forall n^{\mathbb {N} },A[x:=n]$,

et la règle d'élimination des booléens, qui énonce que l'on peut prouver une formule en faisant une disjonction de cas sur un booléen :

$A[x:=\operatorname {True} ]\land A[x:=\operatorname {False} ]\implies \forall b^{\mathbb {B} },A[x:=b]$.

Égalité

Dans cette théorie, l'égalité est une relation d'équivalence. De plus, deux termes égaux sont substituables : si $t=u$ et $A[x:=t]$ alors $A[x:=u]$.

En plus de cela, l'égalité des entiers utilise les mêmes axiomes que l'arithmétique de Peano, c'est-à-dire que $\operatorname {S} x\neq 0$ et $x=y\iff \operatorname {S} x=\operatorname {S} y$, que les deux constantes booléennes sont différentes : $\operatorname {True} \neq \operatorname {False}$.

Enfin, on considère que la réduction est incluse dans l'égalité, c'est-à-dire que si $M\to N$ alors $M=N$. On suppose également que l'égalité est préservée par les diverses constructions du système :

• $M=N\implies OM=ON$ ;
• $M=N\implies MO=NO$ ;

• $M=N\implies \lambda x^{T}.M=\lambda x^{T}.N$;
• $M=\lambda x^{S}.Mx$ si $M$ est de type $S\to T$ est que $x$ n'est pas libre dans $M$.

• De plus, l'égalité est préservée par les constructions $\operatorname {S}$, $\operatorname {if}$ et $\operatorname {rec}$, c'est-à-dire que si $x=_{\mathbb {N} }y$ alors $\operatorname {S} ~x=_{\mathbb {N} }\operatorname {S} ~y$, etc.

Néanmoins toutes ces règles ne suffisent pas à décrire l'égalité entre fonctions. En effet, dans un système intuitionniste, il n'est pas clair que l'on puisse décider de l'égalité de deux fonctions. Ceci amène donc plusieurs variantes au système présenté jusqu'alors, qu'on appellera le système neutre. Tous les systèmes suivants sont des extensions de l'arithmétique de Heyting, et dans tous les systèmes sauf le système extensionnel, chaque formule sans quantificateurs est équivalente à une formule de la forme $b=_{\mathbb {B} }\operatorname {True}$.

Égalité intensionnelle

Dans le système utilisé par Gödel à l'origine, l'égalité est supposée intensionnelle, c'est-à-dire que deux termes de fonctions sont égaux si c'est le même algorithme qu'ils décrivent. Formellement, il y a dans le système une règle de déduction qui dit que si $f\equiv g$, alors $f=g$, où $\equiv$ est clotûre réflexive, symétrique et transitive de la relation de réduction $\to$ décrite précédemment. Comme $\to$ est confluente et fortement normalisante, $\equiv$ correspond à la relation « a la même forme normale que ».

De plus, dans ce système, on ajoute, pour chaque type $T$, un terme $E_{T}:T\to T\to \mathbb {B}$ qui représente une fonction qui teste l'égalité entre deux termes : on a ajoute l'axiome $E_{T}~f~g=_{\mathbb {B} }\operatorname {True} \iff f=_{T}g$. En particulier, l'égalité est décidable, c'est-à-dire que $\mathbf {HA} ^{\omega }\vdash f=_{T}g\lor \neg (f=_{T}g)$ pour tous termes $f$ et $g$ de type $T$, et si $f$ et $g$ sont deux termes de type $T$ qui ont la même forme normale, alors ils sont égaux.

Égalité extensionnelle et faiblement extensionnelle

On peut également considérer une variante extensionnelle où deux fonctions sont égales si elles sont égales en tout point :

$\forall f^{S\to T}\forall g^{S\to T},f=_{S\to T}g\iff (\forall x^{S},fx=_{T}gx)$

Dans ce système, on peut en fait supposer que l'égalité pour les types de fonctions n'est pas une notion primitive, mais seulement une définition, c'est-à-dire que la formule $f=_{S\to T}g$ est définie comme étant une notation pour la formule $\forall x^{S},fx=_{T}gx$.

Néanmoins dans ce système, l'égalité n'est plus décidable, et l'interprétation Dialectica (en) ne fonctionne pas. Pour remédier à cela, on peut limiter la règle usuelle d'élimination de l'égalité, disant que si $u=t$ et $A[x:=u]$ sont prouvables sans hypothèses, alors $A[x:=t]$ aussi, en ne l'autorisant que pour les formules $A$ sans quantificateurs. Ce système est alors dit « faiblement extensionnel ».

Égalité observationnelle

Enfin, on peut considérer un système où il n'y a pas de symbole pour l'égalité des types de fonctions. Dans ce système, on ne garde les axiomes concernant l'égalité du système neutre que ceux qui concernent les entiers et les booléens (notamment, $f=_{T}g\implies A[x:=f]\implies A[x:=g]$ n'est pas un axiome si $T$ est un type de fonction), ainsi que les règles de pour $\operatorname {S}$, $\operatorname {if}$ et $\operatorname {rec}$, le fait que si $M\to N$ alors $M=N$, et le fait que l'application d'une fonction préserve l'égalité entre deux termes de type entier ou booléen : $x=_{T}y\implies f~x=_{S}f~y$ si $T$ et $S$ ne sont pas des types de fonctions.

L'égalité entre deux fonctions $f$ et $g$ de type $S\to T$ est définie par la formule $\forall C^{(S\to T)\to \mathbb {B} },C~f=_{\mathbb {B} }C~g$. En fait, puisque l'égalité des entiers naturels et des booléens est décidable dans le système T, cela vaut pour tous les types, et l'égalité est dite observationnelle : deux éléments d'un même type sont égaux si et seulement si aucun algorithme ne peut les discerner. Mathématiquement, cela donne :

$t=_{S}u\iff \forall C^{S\to \mathbb {B} },C~t=_{\mathbb {B} }C~u$.

Interprétation Dialectica

Chacun de ces systèmes (sauf le système extensionnel) permettent de faire de système T une théorie logique à part entière $\mathbf {HA} ^{\omega }$, qui étend l'arithmétique de Heyting, et dans laquelle l'interprétation Dialectica (en) est valide. Cette interprétation consiste à traduire chaque formule $A$ par une formule sans quantificateur $A_{D}$ à deux variables libres $x$ et $y$ de types $A$ et $B$, de sorte que si $\mathbf {HA} ^{\omega }\vdash A$ alors ${\text{qf}}-\mathbf {HA} ^{\omega }\vdash \exists x^{A}\forall y^{B}A_{D}(x,y)$, où ${\text{qf}}-\mathbf {HA} ^{\omega }$ est la variante de $\mathbf {HA} ^{\omega }$ sans les quantificateurs. De plus, ce système étant intuitionniste, on en déduit qu'il existe un terme $t$ de type $A$ tel que ${\text{qf}}-\mathbf {HA} ^{\omega }\vdash \forall y^{B}A_{D}(t,x)$. Vu la remarque précédente, on en déduit que dans le système avec l'égalité intensionnelle, l'interprétation Dialectica revient à trouver pour chaque formule $A$ un terme $u_{A}:\mathbb {B}$ de système T — étendu avec la fonction $E_{T}$ définie précédemment et la réductions $E_{T}~f~f\to \operatorname {True}$ — à une variable libre $x^{U}$ que si $\mathbf {HA} ^{\omega }\vdash A$ alors il existe un terme $M$ de type $U$ tel que $u_{A}[x:=M]\equiv \operatorname {True}$.

Le but de cette traduction, inventée par Gödel en 1958, était de faire reposer la preuve de cohérence de l'arithmétique sur des fondations plus simples que celles connues jusqu'à présent, qui se basaient sur une preuve de Gerhard Gentzen utilisant de l'analyse ordinale et de la récurrence transfinie jusqu'à l'ordinal $\varepsilon _{0}$. Une preuve de cohérence de système T utilisant un modèle de termes (l'univers est l'ensembles des termes, quotientés par la relation $\equiv$) a été produite par William Tait en 1967, dans laquelle il introduit les base de la méthode des candidats de réducibilité développée plus tard par Jean-Yves Girard pour prouver la cohérence de système F, et en particulier sa terminaison.

Cette interprétaton permet par exemple de montrer que toutes les fonctions calculables de $\mathbb {N}$ dans $\mathbb {N}$ que l'arithmétique de Peano prouve être des fonctions totales sont données par des termes de système T.

Enfin, si $\exists x^{A}\forall y^{B}A_{D}(x,y)$ est vraie dans un modèle de système T, on dit que la formule $A$ est Dialectica-interprétable. Cela permet de montrer la cohérence relative de plusieurs systèmes logiques, par exemple :

• l'axiome du choix (dans sa forme $\forall x^{A}\exists y^{B}P(x,y)\implies \exists f^{A\to B}\forall x^{A}P(x,f(x))$, souvent accepté dans les mathématiques constructives), et l'axiome de Spector $\forall x^{A}\neg \neg P(x)\implies \neg \neg \forall x^{A}P(x)$, sont interprétables dans le système T muni de la bar-récursion, et définit les mêmes fonctions que ce système-ci.
• la thèse de Church, qui dit que toutes les fonctions sont calculables, est compatible avec le système T étendu avec un codage de Gödel des fonctions $\mathbb {N} \to \mathbb {N}$ et une arithmétisation de la réduction, et définit les mêmes fonctions ce que celui-ci;
• le principe de Markov, qui dit que si $A(n)$ est un prédicat décidable (c'est-à-dire que $\forall n^{\mathbb {N} }A(n)\lor \neg A(n)$), et qu'il y a un algorithme dont on sait qu'il termine qui cherche un $n$ tel que $A(n)$, alors on peut trouver un tel $n$. Il s'énonce ainsi : $(\forall n^{\mathbb {N} }A(n)\lor \neg A(n))\implies \neg \neg \exists n^{\mathbb {N} }A(n)\implies \exists n^{\mathbb {N} }A(n)$. L'interprétation Dialectica de ce principe est valide dans l'arithmétique de Heyting.

Articles connexes

• Lambda-calcul
• Récursion Primitive
• Système F
• interprétation Dialectica (en)

Bibliographie

• (en) Morten Heine Sørensen et Pawel Urzyczyn, Lectures on the Curry-Howard Isomorphism, vol. 149, Elsevier Science, coll. « Studies in Logic and the Foundations of Mathematics », 4 juillet 2006, 456 p. (ISBN 978-0-444-52077-7, 9780444545961 et 9780080478920, lire en ligne [PDF]), Chapitre 11 : First-order arithmetic and Gödel's T : présentation du lambda-calcul simplement typé, de l'arithmétique de Peano, du système T et de l'interprétation Dialectica.
• (en) Jean-Yves Girard, Paul Taylor et Yves Lafont, Proofs and Types, Cambridge University Press, 1989, 183 p. (ISBN 0-521-37181-3, lire en ligne ) : présentation de système T et du lambda-calcul simplement typé.
• Jean-Yves Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972, 230 p. (lire en ligne) : thèse de Girard dans laquelle il revisite système T et développe système F, et présente l'interprétation Dialectica y compris pour ces deux systèmes.
• (en) Anne Sjerp Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer Berlin, Heidelberg, coll. « Lecture Notes in Mathematics » (n^o 344), 1973, 503 p. (ISBN 978-3-540-06491-6, ISSN 0075-8434, e-ISSN 1617-9692, DOI 10.1007/BFb0066739 ) : ouvrage de théorie de la démonstration très complet qui présente les différentes systèmes arithmétiques dans la logique intuitionniste et différents résultats à leur sujet, notamment au moyen de la réalisabilité (notamment par l'interprétation Dialectica), de la théorie des modèles et de la norminalisation.