Système T

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 ${\displaystyle \beta }$-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 ${\displaystyle a_{1},a_{2},\dots ,a_{n}}$ sont des arités, alors ${\displaystyle (a_{1}\otimes a_{2}\otimes \dots \otimes a_{n})}$ est une arité ; l'arité des expressions combinées.
• si ${\displaystyle a}$ et ${\displaystyle b}$ sont des arités, alors ${\displaystyle a\rightarrow b}$ est une arité ; l'arité des expressions non saturées.

• Le type d'un élément est noté en exposant. Ex : ${\displaystyle 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 : ${\displaystyle (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

• ${\displaystyle 0~}$ : de type ${\displaystyle N~}$
• si ${\displaystyle t~}$ est un terme de type ${\displaystyle N~}$ alors ${\displaystyle S(t)~}$ est un terme de type ${\displaystyle N~}$
• les variables ${\displaystyle x,\;y,\;z,\,\dots ~}$ de type ${\displaystyle T~}$ sont des termes de type ${\displaystyle T~}$
• si ${\displaystyle x~}$ est une variable de type ${\displaystyle U~}$ et ${\displaystyle t~}$ un terme de type ${\displaystyle V~}$ alors ${\displaystyle \lambda x.t~}$ est un terme de type ${\displaystyle U\rightarrow V~}$ (abstraction)
• si ${\displaystyle t~}$ est un terme de type ${\displaystyle U\rightarrow V~}$ et ${\displaystyle u~}$ un terme de type ${\displaystyle U~}$ alors ${\displaystyle tu~}$ est un terme de type ${\displaystyle V~}$ (application)
• si ${\displaystyle t~}$ un terme de type ${\displaystyle N~}$ et que ${\displaystyle b~}$ et ${\displaystyle s~}$ sont des termes de type ${\displaystyle T~}$ alors ${\displaystyle rec_{T}(t,\;b,\;(x^{N},\;y^{T})s)~}$ est un terme de type ${\displaystyle T~}$

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

• ${\displaystyle (\lambda x.t)u\rightarrow t[x\leftarrow u]~}$
• ${\displaystyle rec_{T}(0,\;b,\;(x^{N},\;y^{T})s)\rightarrow b~}$
• ${\displaystyle 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.

• 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

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