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 est un système formel. Il a été inventé par le logicien Kurt Gödel^[1] 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 :

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

${\displaystyle f(Succ(x),{\vec {y}})=h(x,f(x,{\vec {y}}),{\vec {y}})}$

La différence majeure est que l'on autorise les paramètres ${\displaystyle {\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.

Le formalisme se base sur celui du lambda-calcul simplement typé. On y ajoute un type représentant les entiers naturels, ${\displaystyle {\mathsf {Nat}}}$, ainsi qu'un type représentant les booléens, ${\displaystyle {\mathsf {Bool}}}$^[2].

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

${\displaystyle (\operatorname {T} )\;{\frac {}{\Gamma \vdash \operatorname {True} :{\mathsf {Bool}}}}}$	${\displaystyle (\operatorname {F} )\;{\frac {}{\Gamma \vdash \operatorname {False} :{\mathsf {Bool}}}}}$
${\displaystyle (\operatorname {if} )\;{\frac {\Gamma \vdash u:{\mathsf {Bool}}\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 ${\displaystyle 0}$, soit comme le successeur ${\displaystyle \operatorname {S} u}$ d'un autre entier ${\displaystyle u}$, qui représente ${\displaystyle u+1}$. Ainsi, si ${\displaystyle n}$ est un entier naturel usuel, il sera représenté dans le système T par le terme ${\displaystyle \operatorname {S} ^{n}0=\overbrace {\operatorname {S} \cdots \operatorname {S} } ^{n}~0}$, qui consiste en ${\displaystyle n}$applications successives de ${\displaystyle \operatorname {S} }$ au terme ${\displaystyle 0}$.

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

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

On peut noter que la réduction est confluente, préserve les types et est fortement normalisante^[3]. On peut de plus montrer que les termes clos — c'est-à-dire sans variable libre — de type ${\displaystyle {\mathsf {Nat}}}$ sont tous de la forme ${\displaystyle \operatorname {S} ^{n}0}$ pour un certain entier naturel ${\displaystyle n}$, et les termes clos de type ${\displaystyle {\mathsf {Bool}}}$ sont ${\displaystyle \operatorname {True} }$ et ${\displaystyle \operatorname {False} }$^[4].

La relation de réduction est confluente et fortement normalisante^[5].

L'article originel de Gödel^[1] 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^[5], mais Troelstra^[6] 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^[7] et dans son livre^[2], en ajoutant un type des booléens et un type produit.

La fonction prédécesseur vérifie les équations suivantes^[8] :

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

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

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

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^[9]. 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 :

• ${\displaystyle {\mathsf {Min}}~0~0=0}$ ;
• ${\displaystyle {\mathsf {Min}}~(\operatorname {S} 0)~0=0}$ ;
• ${\displaystyle {\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é :

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

Le terme voulu est :

${\displaystyle {\mathsf {Min}}=\lambda m^{\mathsf {Nat}}.\operatorname {rec} _{{\mathsf {Nat}}\to {\mathsf {Nat}}}m~(\lambda n^{\mathsf {Nat}}.~0)~\left(\lambda m'^{\mathsf {Nat}}.\lambda f^{{\mathsf {Nat}}\to {\mathsf {Nat}}}.\lambda n^{\mathsf {Nat}}.\operatorname {rec} _{\mathsf {Nat}}n~0~\left(\lambda n'^{\mathsf {Na}}.\lambda r^{\mathsf {Nat}}.\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 est définie ainsi :

• ${\displaystyle {\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^[10].

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

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

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

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

On peut introduire une théorie dont les termes sont décrits par ceux de système T^{[1],[5],[11],[12]}. Les formules sont alors formées par quantification universelle et existentielle, conjonction, disjonction, négation et implication, à partir des formules atomiques ${\displaystyle \top }$ (la formule toujours vraie), ${\displaystyle \bot }$ (la formule toujours fausse) et ${\displaystyle s=_{T}t}$ où ${\displaystyle T}$ est un type et ${\displaystyle s}$ et ${\displaystyle t}$ deux termes de types ${\displaystyle T}$, qui désigne la formule vraie si ${\displaystyle s}$ et ${\displaystyle 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

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

et la règle d'élimination des booléens, qui énonce que

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

Pour l'égalité^[13], on considère les règles de l'arithmétique de Peano pour les entiers, c'est-à-dire que ${\displaystyle \operatorname {S} x\neq 0}$ et ${\displaystyle x=y\iff \operatorname {S} x=\operatorname {S} y}$, que les deux constantes booléennes sont différentes : ${\displaystyle \operatorname {True} \neq \operatorname {False} }$, que l'égalité est une relation réflexive, symétrique et transitive : ${\displaystyle x=x}$, ${\displaystyle x=y\implies y=x}$, ${\displaystyle x=y\land y=z\implies x=z}$, que deux termes égaux sont substituables : si ${\displaystyle t=u}$ et ${\displaystyle A[x:=t]}$ alors ${\displaystyle A[x:=u]}$, et que les règles de réduction de ${\displaystyle \operatorname {if} }$ et ${\displaystyle \operatorname {rec} }$ sont valides, c'est-à-dire que ${\displaystyle \operatorname {if} _{A}\operatorname {True} v~w=v}$, ${\displaystyle \operatorname {if} _{A}\operatorname {False} v~w=w}$, ${\displaystyle \operatorname {rec} _{A}0~v~w=v}$ et ${\displaystyle \operatorname {rec} _{A}(\operatorname {S} u)~v~w=wu(\operatorname {rec} _{A}u~v~w)}$. Pour les fonctions, on considère ${\displaystyle (\lambda x^{T}.M)N=M[x:=N]}$ si ${\displaystyle x}$ n'est pas libre dans ${\displaystyle N}$ et ${\displaystyle M=N\implies \lambda x^{T}.M=\lambda x^{T}.N}$, mais cela ne suffit pas forcément à décrire l'égalité entre fonctions.

Dans le système utilisé par Gödel à l'origine^[1], l'égalité est supposée intensionnelle^[14], c'est-à-dire que deux fonctions sont égales si c'est le même algorithme qui les décrivent, par exemple, au travers de la clotûre réflexive, symétrique et transitive ${\displaystyle \equiv }$ de la relation de réduction ${\displaystyle \to }$ décrite précédemment pour les termes bien typés, sans la règle ${\displaystyle \eta }$ du lambda-calcul. Comme ${\displaystyle \to }$ est confluente et fortement normalisante, ${\displaystyle \equiv }$ correspond à la relation « a la même forme normale que ». De plus, il y a un symbole de fonction ${\displaystyle E_{T}:T\to T\to {\mathsf {Bool}}}$ pour chaque type ${\displaystyle T}$ tel que ${\displaystyle E_{T}~f~g\iff f=_{T}g}$. En particulier, l'égalité est décidable et si ${\displaystyle f}$ et ${\displaystyle g}$ sont deux termes de type ${\displaystyle T}$ qui ont la même forme normale, alors ils sont égaux.

On peut également considérer une variante extensionnelle^[15] où deux fonctions sont égales si elles sont égales en tout point : cela revient à rajouter la règle d'${\displaystyle \eta }$-réduction pour les fonctions. Néanmoins dans ce système, l'égalité n'est plus décidable, et l'interprétation Dialectica (en) ne fonctionne pas^[16]. Pour remédier à cela, on peut limiter la substitution aux formules sans quantificateurs.

Enfin, on peut considérer un système où il n'y a pas de symbole pour l'égalité des types de fonctions^[17].

Tous ces systèmes sont des extensions de l'arithmétique de Heyting, et dans tous les systèmes sauf le système extensionnel avec la règle de substitution complète, chaque formule sans quantificateurs est équivalente à une formule de la forme ${\displaystyle b=_{\mathsf {Bool}}\operatorname {True} }$ ^[18].

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

• (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 ).
• Jean-Yves Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972, 230 p. (lire en ligne).
• (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 , lire en ligne ).

• Portail de l'informatique théorique
• Portail de la logique