Système T
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

A 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 (Le lambda-calcul (ou λ-calcul) est un langage de programmation théorique inventé par Alonzo Church dans les années 1930. Ce langage a été le premier utilisé pour définir et caractériser les fonctions...) simplement typé. Le but est d'augmenter le pouvoir expressif et c'est gagné car on peut programmer facilement 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. Ceci change tout (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) car par rapport à la récursion primitive on va pouvoir faire une récurrence sur plusieurs paramètres et c'est exactement ce qu'il manquait.

Formalisme

Selon le formalisme de Martin-Löf on peut écrire les termes du système T (A 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.) 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, ... de type T sont des termes de type T
  • si x est une variable (En mathématiques et en logique, une variable est représentée par un symbole. Elle est utilisée pour marquer un rôle dans une formule, un prédicat ou un algorithme. ...) de type U et t un terme de type V alors λx.t est un terme de type U→V
  • si t est un terme de type U→V et u un terme de type U alors tu est un terme de type V
  • si t un terme de type N et que b et s sont des termes de type T alors recT(t,b,(xN,yT)s) est un terme de type T

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

  • (λx.t)u → t[x←u]
  • recT(0,b,(xN,yT)s) → b
  • recT(S(t),b,(xN,yT)s) → s[x←t, y←recT(t,b,(xN,yT)s)

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 Sn(0))
  • tous les termes clos de type N sont normalisables

Exemples

La fonction d'Ackermann

Notre fameuse 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.recN→N(n, λp.S(p), (mN, fN→N)λp.recN(p, f S(0), (qN, gN)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 (Le temps est un concept développé par l'être humain pour appréhender le changement dans le monde.) 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.

Equations 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.recN→N(n, λp.0, (mN, fN→N)λp.recN( p, 0, (qN, gN) S(f q))))

De la même manière on peut obtenir facilement un programme optimisé pour l'addition (L'addition est une opération élémentaire, permettant notamment de décrire la réunion de quantités ou l'adjonction de grandeurs...) et la soustraction (La soustraction est l'une des opérations basiques de l'arithmétique. La soustraction combine deux ou plusieurs grandeurs du même type, appelées opérandes, pour donner un seul nombre,...).

Page générée en 0.070 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique