Système T

Système T: À l'instar de la récursion primitive ou le lambda-calcul, le Système T est un langage de programmation théorique. Il a été inventé par le logicien Kurt Gödel.

Ce système consiste en une fusion de la récursion primitive et du lambda-calcul simplement typé. Le système T est plus expressif que les deux précédemment cités étant donné qu'il permet par exemple de définir la fonction d'Ackermann.

Le principe est simple : on garde les schémas récursifs primitifs :

$f(0,\vec y) = g(\vec y)$

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

La différence majeure c'est que l'on autorise 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.

Sommaire

1 Formalisme

2 Quelques théorèmes importants

3 Exemples

3.1 La fonction d'Ackermann

3.2 Un minimum efficace

4 Articles connexes

Formalisme

Le formalisme de Martin-Löf utilise (entre autres) les notations suivantes :

Une expression peut être simple (en : single) ou combinée (en : combined). Une expression simple correspond à un 1-uplet, une expression multiple à un n-uplet.

Une expression peut être saturée (en : satured) ou non-saturée (en : unsatured). Une expression saturée est une variable ou une constante. Inversement, une expression non-saturée est un opérateur qui attend qu'on lui fournisse des paramètres de manière à pouvoir être $β$ -réduit en une variable ou une constante.

Une notion d'arité, dont il est dit : "D'un certain point de vue ça ressemble au lambda calcul simplement typé" [Programming in Martin-Löf type theory, page 21].

Définition :

0 est une arité ; l'arité d'une expression simple et saturée.

si $a_1, a_2, \dots, a_n$ sont des arités, alors $(a_1 \otimes a_2 \otimes \dots \otimes a_n)$ est une arité ; l'arité des expressions combinées.

si $a$ et $b$ sont des arités, alors $a \rightarrow b$ est une arité ; l'arité des expressions non saturées.

Le type d'un élément est noté en exposant. Ex : $a N$

Les arguments attendus par un opérateur (une expression non-saturée) sont notés entre deux parenthèses précédant l'opérateur. Ex : $(m^N, n^{N \rightarrow N})f$

Selon le formalisme de Martin-Löf on peut écrire les termes du système T par récurrence

$0~$ : de type $N~$

si $t~$ est un terme de type $N~$ alors $S(t)~$ est un terme de type $N~$

les variables $x, \; y, \; z,\,\dots~$ de type $T~$ sont des termes de type $T~$

si $x~$ est une variable de type $U~$ et $t~$ un terme de type $V~$ alors $\lambda x.t~$ est un terme de type $U\rightarrow V~$ (abstraction)

si $t~$ est un terme de type $U\rightarrow V~$ et $u~$ un terme de type $U~$ alors $tu~$ est un terme de type $V~$ (application)

si $t~$ un terme de type $N~$ et que $b~$ et $s~$ sont des termes de type $T~$ alors $rec_{T}(t, \; b, \; (x^{N}, \; y^{T})s)~$ est un terme de type $T~$

Pour comprendre comment fonctionne ce système il faut naturellement des règles de réduction.

$(\lambda x.t)u \rightarrow t[x\leftarrow u]~$

$rec_{T}(0, \; b, \; (x^{N}, \; y^{T})s) \rightarrow b~$

$rec_{T}(S(t), \; b, \; (x^{N}, \; y^{T})s) \rightarrow s \left( x\leftarrow t, \; y\leftarrow rec_{T}(t, \; b, \; (x^{N}, \; y^{T})s) \right) ~$

On garde les notions de substitution du lambda-calcul et de la récursion primitive, ainsi que les « règles additionnelles » qui permettent de réduire « à l'intérieur » d'un terme.

Quelques théorèmes importants

tous les termes clos (sans variables libres) de type N sont des numéraux (un Sⁿ(0))

tous les termes clos de type N sont normalisables

Exemples

La fonction d'Ackermann

La fonction d'Ackermann que l'on ne peut pas programmer en récursion primitive est définie par les équations suivantes :

Ack 0 p = S(p)

Ack S(n) 0 = Ack n S(0)

Ack S(n) S(p) = Ack n (Ack S(n) p)

Ces équations n'ont pas la forme voulue mais en modifiant un peu on obtient la forme désirée :

Ack 0 = λp.S(p)

Ack S(n) = λp.Ack' p (Ack n)

Ack' 0 f = f S(0)

Ack' S(p) f = f (Ack' p f)

Il n'y a plus qu'à écrire cela sous forme de terme :

Ack = λn.rec_N→N(n, λp.S(p), (m^N, f^N→N)λp.rec_N(p, f S(0), (q^N, g^N)f g)))

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. C'est très contraignant par exemple si on calcule le minimum de 2 et 1 000 000. Comme avec le système T on peut s'arranger pour faire des récursions sur plusieurs paramètres, ne nous gênons pas.

Équations intuitives :

Min 0 p = 0

Min S(n) 0 = 0

Min S(n) S(p) = S(Min n p)

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

Min 0 = λp.0

Min S(n) = λp.Min' p (Min n)

Min' 0 f = 0

Min' S(p) f = S(f p)

Le terme voulu est :

Min = λn.rec_N→N(n, λp.0, (m^N, f^N→N)λp.rec_N( p, 0, (q^N, g^N) S(f q))))

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

Articles connexes

Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue !

Dialectica interpretation (en)

Portail de l'informatique théorique

Catégories :
Calculabilité
Langage de programmation théorique

Contenu soumis à la licence CC-BY-SA. Source : Article Système T de Wikipédia en français (auteurs)

Игры ⚽ Поможем сделать НИР

Regardez d'autres dictionnaires:

système — [ sistɛm ] n. m. • 1552, repris v. 1650, répandu XIXe; gr. sustêma « assemblage, composition » I ♦ Ensemble organisé d éléments intellectuels. 1 ♦ Hist. Sc. Ensemble conçu par l esprit (à titre d hypothèse, de croyance) d objets de pensée unis… … Encyclopédie Universelle
Systeme — Système Un système est un ensemble d éléments interagissant entre eux selon un certain nombre de principes ou règles. Un système est déterminé par le choix des interactions qui le caractérisent et par sa frontière, c est à dire le critère d… … Wikipédia en Français
Système SI — Système international d unités Pour les articles homonymes, voir SI. Le Système international d unités (abrégé en SI), inspiré du système métrique[1], est le système d unités le plus largement employé du monde. Il s agit d un système d unités… … Wikipédia en Français
Systeme 7 — Système 7 Système 7 est le nom donné à la septième révision majeure du système d exploitation des ordinateurs Apple Macintosh. Caractéristiques du Système 7 C est la première vraie évolution majeure du système Macintosh, apportant une… … Wikipédia en Français
Systeme F — Système F Pour les articles homonymes, voir System F (homonymie). Le système F (également connu sous le nom de lambda calcul polymorphe ou de lambda calcul du second ordre) est une extension du lambda calcul simplement typé introduite… … Wikipédia en Français
Système 7 — est le nom donné à la septième révision majeure du système d exploitation des ordinateurs Apple Macintosh. Caractéristiques du Système 7 C est la première vraie évolution majeure du système Macintosh, apportant une amélioration significative de l … Wikipédia en Français
Systeme 6 — Système 6 Logiciel Système 6, simplifié Système 6, est le nom donné à la sixième version du système d exploitation des ordinateurs Apple Macintosh. Il était fourni avec les Macintosh entre 1988 et 1991, date où est sorti le Système 7. Le Système… … Wikipédia en Français
Systeme U — Système U Système U Création 1975 Personnages clés Serge Papin (président) Yve … Wikipédia en Français
Systeme 5 — Système 5 Le Logiciel Système 5, surnommé abusivement Système 5, est un Système d exploitation des ordinateur Macintosh, publié par Apple en 1987. Il a été le premier du nom à porter un numéro de version unifié (jusqu alors, les systèmes Mac… … Wikipédia en Français
Système 5.0 — Système 5 Le Logiciel Système 5, surnommé abusivement Système 5, est un Système d exploitation des ordinateur Macintosh, publié par Apple en 1987. Il a été le premier du nom à porter un numéro de version unifié (jusqu alors, les systèmes Mac… … Wikipédia en Français
Système U — Logo de Système U Création 1975 Personnages clés Serge Papin (président) Yves Petitpas, Dominique Schelcher, Daniel Gournay, L … Wikipédia en Français

Mark and share
Search through all dictionaries
Translate…
Search Internet

Share the article and excerpts