Loading AI tools
système formel de la logique mathématique De Wikipédia, l'encyclopédie libre
À l'instar de la récursion primitive ou le lambda-calcul, le Système T 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 :
La différence majeure est que l'on autorise les paramètres à ê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, , ainsi qu'un type représentant les booléens, [2].
Pour les booléens, on considère deux constantes, (Vrai, en anglais : True) et (Faux, en anglais : False), ainsi qu'une construction avec un booléen et et de même type . Cette opération représente une instruction conditionnelle : si est vrai, on renvoie , sinon . Cela se traduit par les règles et .
Les entiers sont construits soit à partir de la constante , soit comme le successeur d'un autre entier , qui représente . Ainsi, si est un entier naturel usuel, il sera représenté dans le système T par le terme , qui consiste en applications successives de au terme .
Si est un entier, a pour type et est une fonction qui prend un entier et un élément de type et renvoie un élément de type , est de type . L'idée derrière est que le terme représente la fonction définie par récurrence avec et : on considère donc les règles de réduction et .
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 sont tous de la forme pour un certain entier naturel , et les termes clos de type sont et [4].
La fonction prédécesseur vérifie les équations suivantes[5] :
On peut donc l'écrire sous forme de terme comme :
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[6]. 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 :
En transformant un peu on obtient des équations utilisant le schéma souhaité :
Le terme voulu est :
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 :
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[7].
Ainsi, en modifiant un peu la définition, on obtient la forme désirée :
Dans la fonction auxiliaire, la variable contient la fonction . Il n'y a plus qu'à écrire cela sous forme de terme :
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.