Notes de cours « Preuves et Types », DEA MDFI

Version préliminaire

28 juin 2015

2

Table des matières

1 Théorèmes de Gödel 5 1.1 Le langage de l’arithmétique. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2 Fonctions (primitive) récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

Fonctions récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Définissabilité des fonctions récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Fonctions primitives récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Programmation de fonctions primitives récursives. . . . . . . . . . . . . . . . . . . . . . . . . . 9

1.3 Codage de Gödel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Codage du formalisme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Fonctions et prédicats manipulant le formalisme . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Résultats élémentaires sur les fonctions récursives . . . . . . . . . . . . . . . . . . . . . . . . . . 15

1.4 Le prédicat de prouvabilité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

L’arithmétique élémentaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 1.5 Théorèmes d’indécidabilité et d’incomplétude . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 1.6 Le second théorème de Gödel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

2 Lambda-calcul 23

2.1 Le lambda-calcul pur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Généralités sur les relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 La β-réduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Le théorème de Church-Rosser . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Réduction de tête et réduction gauche . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

2.2 Représentation des fonctions récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.3 Le modèle de Engeler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

Fonctions continues . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Modèle de Engeler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Une application du modèle de Engeler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

4  TABLE DES MATIÈRES

Chapitre 1

Théorèmes de Gödel

Ce chapitre reproduit pour l’essentiel le premier chapitre du livre de Girard [2] dont il suit grosso modo le plan. Le lecteur pourra aussi se reporter au Shoenfield [4] pour élucider ou compléter l’exposé.

1.1 Le langage de l’arithmétique.

Le langage de l’arithmétique est défini par

— les symboles de fonctions \underline{0} (symbole de constante, i.e., fonction d’arité 0), \underline{S} (symbole de fonction unaire), \underline{+} et \underline{.} (symboles de fonction binaire) ;

— les symboles de prédicats = et <.

En toute rigueur les termes et les formules de l’arithmétique sont construits en utilisant la notation polonaise préfixée (c’est à dire que la formule qui exprime que x est égale à y s’écrit =xy). En pratique on utilisera des parenthèses et les symboles binaires en notation infixe.

Vérité, équivalence de formules. On dira que deux formules A et B sont logiquement équivalentes si le séquent ⊢ A ↔ B est prouvable dans LK (le calcul des séquents). On dira qu’une formule A de l’arithmétique est vraie, ou simplement que l’on a A si A est vraie dans les entiers. En particulier on dira que deux énoncés A et B traitant des entiers sont équivalents s’ils sont équivalents dans les entiers.

Formules Δ, Σ et Π. Les formules Δ sont définies par récurrence :

— les formules atomiques sont Δ ;

— si A et B sont Δ alors ¬A, A ∧ B, A ∨ B sont Δ ;

— si A est Δ et si t est un terme ne contenant pas x alors ∀x(x < t → A) (que l’on notera ∀x < t. A) et ∃x(x < t ∧ A) (que l’on notera ∃x < t. A) sont Δ.

Remarque : Les quantificateurs ∀x < t. et ∃x < t. sont appelés quantificateurs bornés. Une formule Δ est donc une formule dans laquelle tous les quantificateurs sont bornés.

Les formules Σ sont données par :

— les formules atomiques et leurs négations sont Σ ;

— si A et B sont Σ alors A ∧ B et A ∨ B sont Σ ;

— si A est Σ et si t est un terme ne contenant pas x alors ∀x < t. A est Σ ;

— si A est Σ alors ∃xA est Σ.

Une formule Π est la négation d’une formule Σ.

Remarque : L’ensemble des formules Δ est inclus dans l’ensemble des formules Σ. L’inclusion est bien entendu stricte, mais il y a tout de même une « réciproque » au sens du lemme suivant.

Lemme 1.1.1. Si A est Σ alors il existe une formule A_{0} qui est Δ et telle que A est équivalente à ∃xA_{0}.

Ce lemme très utile, sera souvent utilisé sans référence dans la suite.

Démonstration. On choisit une variable x qui n’apparait pas dans A (ni libre, ni liée) et on remplace chaque quantificateur non borné ∃y de A par ∃y < x. On obtient ainsi une formule A_{0} qui est Δ et on voit facilement que A est équivalente à ∃x A_{0}.

Notations diverses. Soit A une formule. On écrira A[x_{1}, …, x_{k}] (ou A[x⃗]) pour dire que x_{1}, …, x_{k} sont des variables libres de A et dans ce cas on écrira A[t_{1}, …, t_{k}] (ou A[t⃗]) pour désigner la formule A dans laquelle chaque variable x_{i} est remplacée par le terme t_{i}, i.e., A[t⃗] = A[t_{1}/x_{1}, …, t_{k}/x_{k}]. A ce propos on rappelle que la notation A[t_{1}/x_{1}, …, t_{n}/x_{n}] désigne la substitution sans capture de variable. On se reportera au premier chapitre du Krivine [3] pour une définition rigoureuse d’ycelle.

Soit a un entier, on note \underline{a} le terme définie par récurrence par :

— si a = 0 alors \underline{a} est \underline{0} ;

— si a = b + 1 alors \underline{a} est \underline{S} \underline{b}.

Soit t un terme clos. On note |t| la valeur de t définie par récurrence par :

— si t est \underline{0} alors |t| = 0 ;

— si t est \underline{S} u alors |t| = |u| + 1 ;

— si t est u \underline{+} v alors |t| = |u| + |v|;

— si t est u \underline{.} v alors |t| = |u||v|.

On voit donc que |\underline{a}| = a pour tout entier a.

1.2 Fonctions (primitive) récursives

Notations. Soient x_{1}, …, x_{k} des objets. Lorsque le contexte est clair on écrira x⃗ en lieu et place de x_{1}, …, x_{k}; par exemple le l-uplet (a_{1}, …, a_{l}) s’écrira simplement (a⃗). On utilisera les lettres a, b, c, k, l, n, m pour désigner des entiers, t, u, v pour les termes, x, y, z pour les variables, F, G, H pour les fonctions, P, Q, R pour les prédicats.

Si e est une expression entière dépendant (ou pas) des variables x_{1}, …, x_{k} (par exemple e = x_{1} + x_{2}) on notera λx⃗. e la fonction qui à tout k-uplet d’entiers (a⃗) associe e(a⃗). En particulier si n est un entier, λx. n représente la fonction constante de valeur n.

Prédicats. On appelle prédicat d’arité k toute relation k-aire entre entiers où équivalemment, tout sousensemble de ℕ^{k}. Si P est un prédicat k-aire on notera indifféremment (a⃗) ∈ P ou P (a⃗). La fonction caractéristique de P est χ_{P} : ℕ^{k} → ℕ définie par χ_{P} (a⃗) = 0 si P (a⃗) (i.e., si a⃗ ∈ P), χ_{P} (a⃗) = 1 sinon. Remarquons que l’on prend ici une convention qui semble peu naturelle à savoir que 0 représente la valeur vraie et 1 la valeur faux ; ce choix s’explique pour des raisons techniques que l’on verra apparaître un peu plus bas.

Fonctions partielles. Une fonction partielle F (d’arité k) de ℕ^{k} → ℕ est donnée par une partie dom F de ℕ^{k} appelée le domaine de F et une fonction de dom F → ℕ. Si dom F = ℕ^{k} on dit que F est totale. On notera F (a⃗)↓ (resp. F (a⃗)↑) pour (a⃗) ∈ dom F (resp. (a⃗) ∉ dom F).

Si F est partielle d’arité k et G est partielle d’arité l, F (a⃗) = G(b⃗) signifie que soit F (a⃗)↑ et G(b⃗)↑, soit F (a⃗)↓ et G(b⃗)↓ et F (a⃗) = G(b⃗).

Fonctions récursives

Une fonction partielle d’arité k de ℕ^{k} → ℕ est récursive si on peut la définir en appliquant un nombre fini de fois les schémas suivant :

R1 les projections Π_{i}^{k} : (a⃗) → a_{i} sont récursives totales (d’arité k) ; l’addition, la multiplication et la

fonction caractéristique χ_{<} sont récursives totales (d’arité 2) ; R2 (schéma de composition) Si H est récursive (d’arité n) et G_{1}, …, G_{n} sont récursives (d’arité k)

alors la composée F :

F (a⃗) → H(G_{1}(a⃗), …, G_{n}(a⃗))

est récursive. Son domaine est défini par ;

F (a⃗)↓ ssi G_{i}(a⃗)↓ pour i = 1, …, n et H(G_{1}(a⃗), …, G_{n}(a⃗))↓

R3 (schéma de minimisation) Si G est récursive d’arité k + 1 alors la fonction F :

F (a⃗) = μx. (G(x, a⃗) = 0)

dont la valeur (si elle est définie) est le plus petit x tel que G(x, a⃗) = 0 et le domaine est donné par :

F (a⃗)↓ ssi \begin{cases}∀b < a, G(b, a⃗)↓ et G(b, a⃗) > 0 \\ G(a, a⃗)↓ et G(a, a⃗) = 0 \end{cases}

Remarque : Le schéma de minimisation est le seul qui peut produire des fonctions non totales. Par exemple la fonction F (a) = μx. (χ_{<}(x, 0) = 0) (F (a) est le premier entier strictement plus petit que 0) est nulle part définie ce qui ne l’empêche pas d’être récursive.

Prédicats récursifs, récursivement énumérables. Un prédicat est récursif si sa fonction caractéristique est récursive totale. Un prédicat P est récursivement énumérable s’il est le domaine d’une fonction récursive, c’est à dire s’il existe F récursive telle que P (a⃗) ssi F (a⃗)↓ pour tout k-uplet (a⃗). On utilise communément l’abbréviation r.e. pour « récursivement énumérable ».

Remarque : Un prédicat récursif est récursivement énumérable : soit F définie par F (a) = μx. (a = 0). Alors F est récursive (pourquoi ?) et on a F (a)↓ ssi a = 0. Par conséquent F (χ_{P} (a⃗))↓ ssi P (a⃗). Comme χ_{P} est récursive F ∘ χ_{P} l’est par schéma de composition et donc P est récursivement énumérable.

Définissabilité des fonctions récursives

Théorème 1.2.1 (Définissabilité). (i) Si F est une fonction récursive d’arité k alors il existe une formule A[x⃗, y] qui est Σ et qui définit F, c’est à dire que :

F (a⃗) = b ssi A[\underline{a}, \underline{b}]

(ii) Si P est un prédicat r.e. d’arité k alors il existe une formule A[x⃗] qui est Σ et qui définit P, c’est à dire que :

P (a⃗) ssi A[\underline{a}]

Démonstration. La deuxième partie du théorème se déduit de la première : si P est r.e. alors il y a une fonction récursive F telle que P (a⃗) ssi F (a⃗)↓, c’est à dire ssi ∃y y = F (a⃗). D’après (i) il y a une formule A[x⃗, y] qui définit F et qui est Σ ; mais alors B = ∃yA[x⃗, y] définit P et comme A est Σ, B l’est aussi.

La première partie se démontre par récurrence sur la construction de F. Si F est la projection Π_{i}^{k} alors F est définie par y = x_{i}; l’addition est définie par y = x_{1} \underline{+} x_{2} et la multiplication par y = x_{1} \underline{.} x_{2}. Enfin χ_{<} se définit par (x_{1} < x_{2} ∧ y = \underline{0}) ∨ (x_{1} ≮ x_{2} ∧ y = \underline{S} \underline{0}) (x_{1} ≮ x_{2} est une abbréviation pour ¬(x_{1} < x_{2})). Remarquons que pour l’instant toutes ces formules sont Δ.

Si F (a⃗) = H(G⃗(a⃗)) où les G_{i} et H sont récursives alors par hypothèse de récurrence il y a des formules B_{i}[x⃗, y_{i}] pour i = 1, …, n et C[y⃗, y] qui sont Σ et qui définissent respectivement les G_{i} et H. On pose

A = ∃y_{1} … ∃y_{n} B_{1}[x⃗, y_{1}] ∧ ⋯ ∧ B_{n}[x⃗, y_{n}] ∧ C[y⃗, y]

Clairement A est Σ et définit F.

Enfin si F (a⃗) = μx. (G(x, a⃗) = 0) où G est récursive alors par hypothèse de récurrence il y a une formule B[x, x⃗, y] qui est Σ et qui définit G. On pose

A = ∀y′ < y.∃z B[y′, x⃗, \underline{S} z] ∧ B[y, x⃗, \underline{0}]

(Question : pourquoi n’a-t-on pas défini A = ∀y′ < y. ¬B[y′, x⃗, 0] ∧ B[y, x⃗, \underline{0}] ?)

Fonctions primitives récursives

Il est bien clair que parmi les fonctions récursives on est plus intéressé par celles qui sont totales : du point de vue informatique la totalité correspond à la notion de correction de programme, c’est à dire que lorsqu’on écrit F (a⃗)↑ cela correspond à un programme qui « bugge » sur l’entrée a⃗ (typiquement en entrant dans une boucle infinie).

Toutefois l’ensemble des fonctions récursives totales n’a pas de bonnes propriétés, par exemple bien qu’il soit visiblement dénombrable, il n’est pas récursivement énumérable.^{1} C’est pourquoi on est amené à introduire des classes de fonctions récursives totales bénificiant de meilleures propriétés. On verra plus tard dans le cours les fonctions représentables par des lambda-termes typés mais tout de suite on va introduire les fonctions primitives récursives.

1. On le démontre par diagonalisation : on verra un peu plus loin qu’un ensemble X est r.e. ssi il existe une fonction récursive totale F qui énumère X, c’est à dire telle que X est l’image de F. Soit T_{1} l’ensemble des fonctions récursive totales unaires et φ une fonction de ℕ^{2} dans ℕ qui énumère T_{1}, c’est à dire telle que pour toute F dans T_{1} il existe un e_{F} tel que F (a) = φ(e_{F} , a)

pour tout a. On va voir que φ ne peut être récursive. Définissons G par G(a) = φ(a, a) + 1 ; alors G est clairement totale et unaire mais elle ne peut être récursive, sinon elle est dans T_{1} et il y a un e_{G} tel que G(a) = φ(e_{G}, a) pour tout a donc en particulier pour a = e_{G}, G(e_{G}) = φ(e_{G}, e_{G}) contredisant la définition de G. Donc φ n’est pas récursive, sinon G le serait également.

Une fonction de ℕ^{k} → ℕ est primitive récursive (p.r.) si on peut l’obtenir en appliquant un nombre fini de fois les schémas suivant :

PR1 Les projections Π_{i}^{k}, l’addition, la multiplication, la fonction caractéristique de < et les fonctions constantes λx⃗. n sont primitives récursives ;

PR2 (schéma de composition) idem que pour les fonctions récursives ;

PR3 (schéma de récurrence) si G est primitive récursive d’arité k et H est primitive récursive d’arité k + 2 alors F définie par :

F (a, a⃗) = \begin{cases}G(a⃗) & si a = 0 \\ H(F (a − 1, a⃗), a, a⃗) & si a > 0 \end{cases}

est primitive récursive d’arité k + 1.

Prédicat récursif primitif. Un prédicat est primitif récursif si sa fonction caractéristique l’est.

Théorème 1.2.2. Si F est une fonction primitive récursive alors F est récursive (totale). Si P est un prédicat primitif récursif alors P est récursif.

Démonstration. La démonstration qui suit est initialement due à Gödel ; c’est une variante de celles que l’on trouvera dans le Shoenfield [4] et/ou le Cori-Lascar [1]. Remarquons tout d’abord que la partie traitant des prédicats est conséquence immédiate de celle sur les fonctions.

On va montrer que chacun des schémas PR1, PR2 et PR3 peut se « programmer » à l’aide des schémas R1, R2 et R3. Pour PR1 il faut juste voir que les fonctions constantes sont programmables. La fonction C_{0} = λx⃗. 0 est donnée par C_{0}(a⃗) = μx. (Π)_{1}^{k+1}(x, a⃗) = 0 ; la fonction C_{1} = λx⃗. 1 par C_{1}(x⃗) = μx. (χ_{)} < (0, x) = 0. Remarquons que c’est cette définition qui justifie le choix technique et peu naturel de prendre 0 pour valeur vraie des fonctions caractéristiques. La fonction C_{2} = λx⃗. 2 est donnée par C_{2}(x⃗) = C_{1}(x⃗) + C_{1}(x⃗), et plus généralement on définit C_{n+1} par C_{n+1}(x⃗) = C_{n}(x⃗) + C_{1}(x⃗).

Le schéma PR2 est le même que le schéma R2 ; reste donc à voir le schéma de récurrence primitive PR3 et c’est là qu’il va falloir travailler un peu. On commence par dériver de R1, R2 et R3 des schémas supplémentaires pour programmer des fonctions récursives.

Soit P (x, x⃗) un prédicat récursif. Alors la fonction définie par F (a⃗) = μx. (P (x, a⃗)) est récursive ; en effet comme P est récursif χ_{P} est récursive (totale), et donc F est obtenue par R3 (ici aussi on se sert du choix χ_{P} (a, a⃗) = 0 ssi P (a, a⃗)). Si de plus pour tout a⃗ il y a un a tel que P (a, a⃗) alors F est totale.

La fonction λxy. x −^{·} y est récursive (totale) : on l’obtient par a −^{·} b = μx. (x + b + 1 > a).

Soient P et Q des prédicats récursifs ; alors ¬P, P ∨ Q, P ∧ Q sont récursifs. En effet leurs fonctions caractéristiques s’obtiennent au moyen de celles de P et Q par les opérations arithmétiques +, . et −^{·} qui sont tous récursifs totals. Remarquons que si on suppose P seulement r.e. alors ¬P n’est pas r.e. en général (pourquoi ?).

Soit P (x, x⃗) un prédicat récursif et F (x⃗) une fonction récursive totale ; alors la fonction G(x⃗) définie par G(a⃗) = μx < F (a⃗). (P)(x, a⃗) (le premier x < F (a⃗) tel que P (x, a⃗) s’il en existe, F (a⃗) sinon), est récursive totale. En effet G(a⃗) est égal à μx. ((x < F (a⃗) ∧ P (x, a⃗)) ∨ x = F (a⃗)). En particulier le prédicat ∃x < F (a⃗).P (x, a⃗) est récursif puisqu’il est équivalent à (μx < F (a⃗). (P (x, a⃗))) < F (a⃗). Par négation le prédicat ∀x < F (a⃗).P (x, a⃗) est également récursif.

Lemme 1.2.3. Il existe une fonction β récursive totale vérifiant : pour tout n et tous a_{0}, …, a_{n}, il existe c tel que pour i = 0, …, n on a β(i, c) = a_{i}.

On ne va pas démontrer ce lemme ici et l’on renvoie le lecteur aux références sus-citées ; Lascar-Cori le dérive du lemme chinois et Shoenfield le prouve in extenso au moyen de simples récurrences.

On note (c)_{i} = β(i, c). Muni du lemme on va pouvoir démontrer que le schéma de récurrence primitive PR3 est récursif.

Soit G(x⃗) et H(x, y, x⃗) des fonctions récursives totales. On définit F̄(x, x⃗) par :

F̄(a, a⃗) = μx. (((x)_{0} = G(a⃗) ∧ ∀y < a.((x)_{y+1} = H((x)_{y}, y + 1, a⃗)))).

La fonction F̄ est clairement récursive et on peut facilement se convaincre par récurrence sur n qu’elle est totale. Soit maintenant F donnée par F (a, a⃗) = (F̄(a, a⃗))_{a}; alors F est également récursive totale et on peut vérifier par récurrence sur a que l’on a F (0, a⃗) = G(a⃗) et F (a + 1, a⃗) = H(F (a, a⃗), a, a⃗) pour tout a, soit que F est définie par récurrence primitive à partir de G et H.

Programmation de fonctions primitives récursives.

On va maintenant se donner un certain nombre d’autres schémas pour définir des fonctions et prédicats p.r.

Itération. Si G est p.r. d’arité k + 1 alors la fonction F définie par :

F (a, b, a⃗) = G^{a}(b, a⃗)

est p.r. d’arité k + 2. En fait c’est une reformulation du schéma de récursion primitive. Clairement F est donnée par F (0, b, a⃗) = b et F (a + 1, b, a⃗) = G(F (a, b, a⃗), a⃗).

Soustraction. On définit a −^{·} 1 par : 0 −^{·} 1 = 0 et (a + 1) −^{·} 1 = a. On définit a −^{·} b par a −^{·} 0 = a et a −^{·} (b + 1) = (a −^{·} b) −^{·} 1. La fonction binaire −^{·} est clairement p.r.

Variante de la récursion primitive. Soient G_{0} une fonction p.r. d’arité k, H p.r. d’arité k + 2 et G_{1},…, G_{k} des fonctions p.r. d’arité k + 1 . Alors la fonction F définie par

F (0, a⃗) = G_{0}(a⃗)
F (a + 1, a⃗) = H(F (a, G⃗(a, a⃗)), a, a⃗)

est p.r. Remarquons qu’il s’agit presque du schéma de récurrence p.r. On va le montrer pour k = 1, le cas général s’en déduit immédiatement en utilisant des séquences.

Supposons donc que F est définie par

F (0, b) = G_{0}(b)
F (a + 1, b) = H(F (a, G_{1}(a, b)), a, b)

On se donne g :

g(0, b, a) = b
g(i + 1, b, a) = G_{1}(a −^{·} (i + 1), g(i, b, a))

et h :

h(0, b, a) = G_{0}(g(a, b, a))
h(i + 1, b, a) = H(h(i, b, a), i, g(a −^{·} (i + 1), b, a))

Il est clair que g et h sont toutes les deux p.r. On va montrer que pour tout b :

F (a, b) = h(a, b, a)  (1.1)

Comme h est p.r. on en déduira que F l’est.

On vérifie aisément par récurrence sur i que pour tout a ≥ i on a

g(i + 1, b, a + 1) = g(i, G_{1}(a, b), a)  (1.2)

puis que

h(i, b, a + 1) = h(i, G_{1}(a, b), a)  (1.3)

On montre (1.1) par récurrence sur a. Pour a = 0 on a h(0, b, 0) = G_{0}(g(0, b, 0)) = G_{0}(b) = F (0, b). Supposons que F (a, b) = h(a, b, a). Alors

h(a + 1, b, a + 1) = H(h(a, b, a + 1), a, g(0, b, a + 1)) par définition de h
= H(h(a, b, a + 1), a, b)  par définition de g
= H(h(a, G_{1}(a, b), a), a, b)  par l’équation (1.3)
= H(F (a, G_{1}(a, b)), a, b)  par hypothèse de récurrence
= F (a + 1, b)  par définition de F

Opérations booléennes. Si P et Q sont p.r. d’arité k alors ¬P, P ∨ Q, P ∧ Q sont p.r. : χ_{¬P} (a⃗) = 1 −^{·} χ_{P} (a⃗),

χ_{P ∨Q}(a⃗) = χ_{P} (a⃗)χ_{Q}(a⃗), χ_{P ∧Q}(a⃗) = 1 −^{·} (1 −^{·} χ_{P} (a⃗))(1 −^{·} χ_{Q}(a⃗)).

Définitions par cas. Si P est un prédicat p.r. d’arité k, G et H sont p.r. d’arité k alors F définie par :

F (a⃗) = \begin{cases}G(a⃗) & si P (a⃗) \\ H(a⃗) & sinon \end{cases}

est p.r. : on l’obtient par F (a⃗) = (1 −^{·} χ_{P} (a⃗))G(a⃗) + χ_{P} (a⃗)H(a⃗). Plus généralement si P_{1}, …, P_{n} sont p.r. et G_{1}, …, G_{n+1} sont p.r. alors

F (a⃗) = {G_{1}(a⃗)  si P_{1}(a⃗) ⋮ G_{n}(a⃗)  si ¬(P_{1}(a⃗) ∨ ⋯ ∨ P_{n−1}(a⃗)) ∧ P_{n}(a⃗) G_{n+1}(a⃗) sinon

est p.r.

Quelques prédicats p.r. Par définition < est p.r. C’est également le cas de ≮, =, ≠, ≤, ≰, >, ≯, ≥, ≱ : par

exemple χ_{≮}(a, b) = 1 −^{·} χ_{<}(a, b), χ_{=} = χ_{≮∧≯}, …

Minimisation bornée. Si P est p.r. alors F donnée par F (a, a⃗) = μx < a. (P (x, a⃗)) dont la valeur est le premier b < a tel que P (b, a⃗) s’il en existe, a sinon, est p.r. On la définit par F (a, a⃗) = G(a −^{·} 1, a, a⃗) où G est donnée par :

G(0, b, a⃗) = 0  si P (0, a⃗)
G(0, b, a⃗) = b  si ¬P (0, a⃗)
G(a + 1, b, a⃗) = G(a, a + 1, a⃗) si P (a + 1, a⃗)
G(a + 1, b, a⃗) = G(a, b, a⃗)  sinon

Quantificateurs bornés. Si P est un prédicat p.r. d’arité k + 1 alors ∀x < a. P (x, a⃗) et ∃x < a. P (x, a⃗) sont p.r. : le second est défini par : ∃x < a. P (x, a⃗) ssi μx < a. (P (x, a⃗)) < a (i.e., χ_{∃x < a. P} (a⃗) = χ_{<}(μx < a. (P (x, a⃗)), a)),

le premier par ∀x < a. P ssi ¬∃x < a. ¬P (x, a⃗) (i.e., χ_{∀x < a. P} = 1 −^{·} χ_{∃x < a. ¬P}).

Arithmétique. Les fonctions binaires λxy. x/y (quotient de x par y ) et λxy. x%y (reste de x modulo y) sont p.r. : la première est donnée par a/b = (μx < a + 1. (a < xb)) −^{·} 1 et la seconde par a%b = a −^{·} (a/b)b. Le prédicat a | b (a divise b) se définit par a%b = 0 et est donc p.r.

Suites d’entiers. On définit la fonction λxy. ⟨x, y⟩ par

⟨a, b⟩ = ((a + b)(a + b + 1))/2 + a

Il est clair qu’elle est p.r.

On définit π_{1} et π_{2} par :

π_{1}c = μx < c + 1. (∃y < c + 1. ⟨x, y⟩ = c)
π_{2}c = μy < c + 1. (∃x < c + 1. ⟨x, y⟩ = c)

π_{1} et π_{2} sont donc p.r. et, comme λxy. ⟨x, y⟩ est bijective on a ⟨π_{1}a, π_{2}a⟩ = a pour tout a.

Pour chaque k on pose :

⟨a_{1} …, a_{k}⟩_{k} = ⟨k, ⟨a_{1}, … ⟨a_{k−1}, a_{k}⟩ …⟩⟩

Plus précisément les fonction λx⃗. ⟨x⃗⟩_{k} sont définies par :

⟨⟩_{0} = 0
⟨a_{0}, a⃗⟩_{k+1} = ⟨k + 1, ⟨a_{0}, π_{2}⟨a⃗⟩_{k}⟩⟩

On voit donc (par récurrence sur k) que chacune d’elles est p.r.

— L’ensemble des (codes de) suites est caractérisé par le prédicat Seq : Seq(a) ssi π_{1}a ≠ 0 ∨ a = 0.

— La longueur d’une suite est Lg a = π_{1}a.

— Le i-ème élément de la suite a est (a)_{i} = π_{1}π_{2}^{i}a si i < Lg a, π_{2}^{Lg a}a sinon.

La concaténation a ∗ b des suites a et b est donnée par a ∗ b = ⟨Lg a + Lg b, F (Lg a, π_{2}a, π_{2}b)⟩ où F est définie par F (0, a, b) = b, F (1, a, b) = ⟨a, b⟩ et F (l + 1, a, b) = ⟨π_{1}a, F (l, π_{2}a, b)⟩.

— La suite d’une liste est donnée par Suite a = 0 si Lg a = 0, Suite a = μx < a. (⟨(a)_{1}⟩_{1} ∗ x = a) sinon.

Donc on a

Suite⟨a_{1}, …, a_{n}⟩_{n} = ⟨a_{2}, …, a_{n}⟩_{n−1}

En particulier si Lg a > 0 alors Suite a < a. Ceci nous permettra de définir des fonctions par récurrence sur des listes d’entiers.

Remarque : A cause de la bijectivité de λxy. ⟨x, y⟩, si a et b sont deux (codes de) suites telles que Lg a = Lg b et pour tout i ≤ Lg a, (a)_{i} = (b)_{i} alors a = b.

Toutes ces fonctions (et prédicats) sont clairement p.r.

Récurrence générale. Soit F une fonction p.r. d’arité k + 1. On note F̄ la fonction donnée par :

F̄(a, a⃗) = ⟨F (0, a⃗), …, F (a − 1, a⃗)⟩_{a}

Alors F̄ est p.r. En effet on l’obtient par : F̄(0, a⃗) = ⟨⟩_{0} et F̄(a + 1, a⃗) = F̄(a, a⃗) ∗ ⟨F (a)⟩_{1}.

Soit maintenant G une fonction p.r. d’arité k + 1. Alors la fonction F définie par (récurrence généralisée) :

F (a, a⃗) = G(F̄(a, a⃗), a⃗)

est p.r. Soit H donnée par H(0, a⃗) = ⟨⟩_{0} et H(a + 1, a⃗) = H(a, a⃗) ∗ ⟨G(H(a, a⃗), a⃗)⟩_{1} qui est donc p.r. On montre facilement par récurrence sur a que H(a, a⃗) = F̄(a, a⃗) d’où l’on déduit que F est p.r. en considérant que F (a, a⃗) = (F̄(a + 1, a⃗))_{a+1}.

Une autre récurrence. Soit G_{1}, …, G_{n} des fonctions p.r. d’arité k + 1 telles que G_{i}(a, a⃗) < a dès que a > 0, H_{0} une fonction p.r. d’arité k et H_{1} une fonction p.r. d’arité n + k + 2. Alors la fonction F donnée par :

F (a, a⃗) = \begin{cases}H_{0}(a⃗) & si a = 0 \\ H_{1}(F (G_{1}(a, a⃗), a⃗), …, F (G_{n}(a, a⃗), a⃗), a, a⃗) & sinon \end{cases}

est p.r. On définit H par

H(b, a, a⃗) = \begin{cases}H_{0}(a⃗) & si a = 0 \\ H_{1}((b)_{G_{1}(a,a⃗)}, …, (b)_{G_{n}(a,a⃗)}, a, a⃗) & sinon \end{cases}

La fonction H est clairement p.r., d’arité k + 2 et F est obtenue par récurrence généralisée sur H :

F (a, a⃗) = H(F̄(a, a⃗), a, a⃗)

1.3 Codage de Gödel

On va maintenant utiliser le petit « langage de programmation » des fonctions p.r. pour représenter le

formalisme du calcul des prédicats dans les entiers. A chaque objet X du formalisme (variable, terme, formule, démonstration) on va associer un entier unique ⌜X⌝ appelé son code de Gödel. On construit ensuite un ensemble de fonctions p.r. qui agissent sur les codes de Gödel et implémentent toutes les transformations syntaxiques standard, typiquement la substitution d’un ensemble de termes à un ensemble de variable dans une formule ou un terme.

Codage du formalisme

Soit L un langage, c’est à dire que L est déterminé par sa signature Σ_{L} = (F_{L}, P_{L}) où F_{L} est l’ensemble (au plus dénombrable) des symboles de fonctions de L et P_{L} est l’ensemble (au plus dénombrable) des symboles de prédicats. On suppose que L contient le langage de l’arithmétique c’est à dire que \underline{0}, \underline{S}, \underline{+} et \underline{.} sont dans F_{L} et que = et < sont dans P_{L}.

Représentation des symboles. Comme F_{L} et P_{L} sont au plus dénombrables on peut les énumérer par des suites (f_{i})_{i<σ_{L}} et (P_{i})_{i<τ_{L}} où σ_{L} et τ_{L} sont les cardinaux respectifs (possiblement infinis) de F_{L} et P_{L}. De même comme l’ensemble des (noms de) variables du calcul des prédicats est dénombrable on peut supposer que celui-ci est complètement énuméré par la suite (x_{i})_{i∈ℕ}. Si s est un symbole ou une variable, on définit alors

⌜s⌝ = \begin{cases}⟨0, 0, i, 0⟩_{4} & si s = x_{i} \\ ⟨0, 1, i, n⟩_{4} & si s = f_{i} et f_{i} est d’arité n \\ ⟨0, 2, i, n⟩_{4} & si s = P_{i} et P_{i} est d’arité n \end{cases}

Représentation des termes. Soit t un terme du langage L; on définit ⌜t⌝ par :

⌜t⌝ = \begin{cases}⟨1, 0, ⌜x⌝, 0⟩_{4} & si t est la variable x \\ ⟨1, 1, ⌜f⌝, ⟨⌜t_{1}⌝, …, ⌜t_{n}⌝⟩_{n}⟩_{4} & si t = f(t_{1}, …, t_{n}) \end{cases}

Représentation des formules. Soit A une formule du langage L. On définit ⌜A⌝ par :

⌜A⌝ = \begin{cases}⟨2, 0, ⌜P ⌝, ⟨⌜t_{1}⌝, …, ⌜t_{n}⌝⟩_{n}⟩_{4} & si A est la formule atomique P (t_{1}, …, t_{n}) \\ ⟨2, 1, ⌜A′⌝, 0⟩_{4} & si A = ¬A′ \\ ⟨2, 2, ⌜A′⌝, ⌜A′′⌝⟩_{4} & si A = A′ ∧ A′′ \\ ⟨2, 3, ⌜A′⌝, ⌜A′′⌝⟩_{4} & si A = A′ ∨ A′′ \\ ⟨2, 4, ⌜A′⌝, ⌜A′′⌝⟩_{4} & si A = A′ → A′′ \\ ⟨2, 5, ⌜x⌝, ⌜A′⌝⟩_{4} & si A = ∀xA′ \\ ⟨2, 6, ⌜x⌝, ⌜A′⌝⟩_{4} & si A = ∃xA′ \end{cases}

Lemme 1.3.1. Soit X un objet du langage (terme ou formule) et Y un sous-objet de X : par exemple X est la formule \underline{S} x < \underline{0} et Y est la variable x. Alors ⌜Y ⌝ < ⌜X⌝.

La preuve est immédiate par récurrence sur X et en considérant pour tout (a, b) ≠ (0, 0), (0, 1) on a a, b < ⟨a, b⟩. Ce lemme servira dans ce qui suit à définir des fonctions ou prédicats sur les (codes d’) objets du formalisme par récurrence sur leurs (codes) de sous-objets.

Prédicats de la signature. On définit les prédicats p.r. Var(a) : « a est le code d’une variable », Fun(a, n) : « a est le code d’un symbole de fonction d’arité n », Pred(a, n) : « a est le code d’un symbole de prédicat d’arité n » par :

Var(a) ssi Lg a = 4 ∧ (a)_{1} = 0 ∧ (a)_{2} = 0
Fun(a, n) ssi Lg a = 4 ∧ (a)_{1} = 0 ∧ (a)_{2} = 1 ∧ (a)_{4} = n
Pred(a, n) ssi Lg a = 4 ∧ (a)_{1} = 0 ∧ (a)_{2} = 2 ∧ (a)_{4} = n

Objets du langage. On définit Term(a) : « a est le code d’un terme », Atom(A) : « a est le code d’une formule atomique » et Form(a) : « a est le code d’une formule » par :

Term(a) ssi Lg a = 4 ∧ (a)_{1} = 1 ∧ \begin{cases}(a)_{2} = 0 ∧ Var((a)_{3}) ou \\ (a)_{2} = 1 ∧ Fun((a)_{3}, Lg(a)_{4}) ∧ ∀i < Lg(a)_{4}. Term(((a)_{4})_{i+1} \end{cases}
Atom(a) ssi Lg a = 4 ∧ (a)_{1} = 2 ∧ (a)_{2} = 0 ∧ Pred((a)_{3}, Lg(a)_{4}) ∧ ∀i < Lg(a)_{4}. Term(((a)_{4})_{i+1})

Form(a) ssi Lg a = 4 ∧ (a)_{1} = 2 ∧ \begin{cases}Atom(a) & ou \\ (a)_{2} = 1 ∧ (a)_{4} = 0 ∧ Form(a)_{3} & ou \\ (a)_{2} = 2 ∧ Form(a)_{3} ∧ Form(a)_{4} & ou \\ (a)_{2} = 3 ∧ Form(a)_{3} ∧ Form(a)_{4} & ou \\ (a)_{2} = 4 ∧ Form(a)_{3} ∧ Form(a)_{4} & ou \\ (a)_{2} = 5 ∧ Var(a)_{3} ∧ Form(a)_{4} & ou \\ (a)_{2} = 6 ∧ Var(a)_{3} ∧ Form(a)_{4} \end{cases}

Fonctions et prédicats manipulant le formalisme

On définit une fonction Num par

Num(0) = ⌜\underline{0}⌝
Num(a + 1) = ⟨1, 1, ⌜\underline{S}⌝, ⟨Num(a)⟩_{1}⟩_{4}

Num est clairement p.r. et vérifie :

Num(a) = ⌜\underline{a}⌝

pour tout entier a.

Variables libres. On définit le prédicat p.r. VarLibres(a, b) : « a est une séquence de variables contenant toutes les variables libres de l’objet codé par b », par :

VarLibres(a, b) ssi ∀i < Lg a. Var((a)_{i+1})∧

Term(b) ∧ (b)_{2} = 0 ∧ ∃i < Lg a. (b)_{3} = (a)_{i+1}  ou
Term(b) ∧ (b)_{2} = 1 ∧ ∀i < Lg(b)_{4}. VarLibres(a, ((b)_{4})_{i+1})  ou
Form(b) ∧ (b)_{2} = 0 ∧ ∀i < Lg(b)_{4}. VarLibres(a, ((b)_{4})_{i+1})  ou
Form(b) ∧ (b)_{2} = 1 ∧ VarLibres(a, (b)_{3})  ou
Form(b) ∧ (b)_{2} = 2, 3 ou 4 ∧ (VarLibres(a, (b)_{3}) ∧ VarLibres(a, (b)_{4})) ou
Form(b) ∧ (b)_{2} = 5 ou 6 ∧ VarLibres(a ∗ ⟨(b)_{3}⟩_{1}, (b)_{4})

Remarque : La dernière clause concerne une formule de la forme A = Qx B où Q est l’un des quantificateurs ; dans ce cas on dit que X est l’ensemble des variables libres de A si X ∪ {x} est l’ensemble des variables libres de B.

On définit la fonction p.r. VL(a) par :

VL(a) = \begin{cases}0 & si ¬ Term(a) ∨ ¬ Form(a) \\ μx <⟨a, …, a⟩_{a}. (VarLibres(x, a)) & sinon \end{cases}

On a donc pour tout objet X

VL(⌜X⌝) = ⟨⌜x_{1}⌝, …, ⌜x_{n}⌝⟩_{n}

où x_{1}, …, x_{n} sont toutes les variables libres de X.

On définit le prédicat p.r. Libre(a, b) (« a est le code d’une variable libre dans l’objet codé par b ») par :

Libre(a, b) ssi Var(a) ∧ \begin{cases}Term(b) ∧ (b)_{2} = 0 ∧ a = (b)_{3} & ou \\ Term(b) ∧ (b)_{2} = 1 ∧ ∃i < Lg(b)_{4}. Libre(a, ((b)_{4})_{i+1}) & ou \\ Form(b) ∧ (b)_{2} = 0 ∧ ∃i < Lg(b)_{4}. Libre(a, ((b)_{4})_{i+1}) & ou \\ Form(b) ∧ (b)_{2} = 1 ∧ Libre(a, (b)_{3}) & ou \\ Form(b) ∧ (b)_{2} = 2, 3 ou 4 ∧ (Libre(a, (b)_{3}) ∨ Libre(a, (b)_{4})) & ou \\ Form(b) ∧ (b)_{2} = 5 ou 6 ∧ a ≠ (b)_{3} ∧ Libre(a, (b)_{4}) \end{cases}

Objets clos. On définit Clos(a) (« a est le code d’un objet clos ») par

                                 Clos(a) ssi VarLibres(⟨⟩_{0}, a)

Clôture universelle d’une formule. Soit A une formule. La clôture universelle \overline{A} de A est la formule ∀x_{1} … ∀x_{n} A où x_{1}, …x_{n} sont toutes les variables libres de A. On définit Clot(a) = F (VL(a), a) où F est donnée par

F (l, a) = \begin{cases}a & si Lg l = 0 \\ ⟨2, 5, (l)_{1}, Clot(Suite l, a)⟩_{4} & sinon \end{cases}

Clairement Clot est p.r. vérifie

Clot(⌜A⌝) = ⌜\overline{A}⌝

pour toute formule A.

Substitution. On va maintenant définir la fonction p.r. Sub telle que :

Sub(⌜X⌝, ⌜x⌝, ⌜t⌝) = ⌜X[t/x]⌝

pour tout terme ou formule X, et toute variable x et terme t. Toutefois, pour résoudre le problème de « capture de variable », on va passer par une fonction légèrement plus générale ParSub qui prend en argument (le code d’) un objet X et (le code d’) une séquence de (code de) couples (x_{i}, t_{i}) et qui effectue la substitution en parallèle de chaque x_{i} par t_{i} dans X. L’idée est, dans le cas où l’on substitue la variable x par le terme t dans une formule quantifiée, par exemple Qy A, d’exploiter le fait que :

(Qy A)[t/x] ↔ Qz A[z/y, t/x]

où z est une variable qui n’est pas libre dans t.

On définit I par I(a, b) = μi < Lg b + 1. ((i > 0 ∧ π_{1}(b)_{i} = a)) ; donc si b = ⟨⟨a_{1}, b_{1}⟩, …, ⟨a_{n}, b_{n}⟩⟩_{n} alors I(a, b) est le premier i tel que a_{i} = a, ou n + 1 s’il n’existe aucun tel i.

On définit ParSub par :

       ParSub(a, b) =

0  si ¬((Term(a) ∨ Form(a)) ∧
∀i < Lg b. (Var(π_{1}(b)_{i}) ∧ Term(π_{2}(b)_{i})))
π_{2}(b)_{I(a,b)}  si Term(a) ∧ (a)_{2} = 0 ∧ I(a, b) ≤ Lg b
a  si Term(a) ∧ (a)_{2} = 0 ∧ I(a, b) > Lg b
⟨1, 1, (a)_{3}, ⟨a_{1}, …, a_{n}⟩_{n}⟩_{4}  si Term(a) ∧ (a)_{2} = 1 ∧ n = Lg(a)_{4} ∧
∀i < n + 1. (i = 0 ∨ a_{i} = ParSub(((a)_{4})_{i}, b))
⟨2, 0, (a)_{3}, ⟨a_{1}, …, a_{n}⟩_{n}⟩_{4}  si Form(a) ∧ (a)_{2} = 0 ∧ n = Lg(a)_{4} ∧
∀i < n + 1. (i = 0 ∨ a_{i} = ParSub(((a)_{4})_{i}, b))
⟨2, 1, ParSub((a)_{3}, b), 0⟩_{4}  si Form(a) ∧ (a)_{2} = 1
⟨2, (a)_{2}, ParSub((a)_{3}, b), ParSub((a)_{4}, b)⟩_{4}  si Form(a) ∧ (a)_{2} = 3, 4 ou 5
⟨2, (a)_{2}, V (a, b), ParSub((a)_{4}, ⟨⟨(a)_{3}, V (a, b)⟩⟩_{1} ∗ b)⟩_{4} si Form(a) ∧ (a)_{2} = 5 ou 6

où V (a, b) = ⟨0, 0, ab, 0⟩_{4} est le code de la variable de numéro ab. On s’assure ainsi que cette variable n’apparait ni dans la formule codée par a, ni dans aucun des termes dont les codes sont listés dans b. Remarquons que l’on a en particulier :

ParSub(⌜Qx A⌝, ⟨⟨⌜x⌝, ⌜t⌝⟩⟩_{1}) = ⌜Qv ParSub(⌜A⌝, ⟨⟨⌜x⌝, ⌜v⌝⟩, ⟨⌜x⌝, ⌜t⌝⟩⟩_{2})⌝

si bien que la variable x est substituée par la nouvelle variable v dans A, et non par t, ce qui est conforme à la définition de la substitution.

Remarque : Le prédicat ParSub est p.r. car il utilise essentiellement (dans la dernière clause) le schéma intitulé « variante de la récursion primitive ».

On définit finalement Sub par :

Sub(a, b, c) = ParSub(a, ⟨⟨b, c⟩⟩_{1})

Quantificateurs bornés. On définit le prédicat QuantBorn(a) (« a est le code d’une formule ∀x < t. A ou ∃x < t. A ») par :

QuantBorn(a) ssi Form(a) ∧ \begin{cases}(a)_{2} = 5 ∧ P ((a)_{4}, 4, (a)_{3}) ou \\ (a)_{2} = 6 ∧ P ((a)_{4}, 2, (a)_{3}) \end{cases}

où P (a, b, c) est le prédicat « a est le code d’une formule x < t α A′ où α = → si b = 4, α = ∧ si b = 2 et où x est la variable de code c et t est un terme ne contenant pas x » défini par :

P (a, b, c) ssi Form(a) ∧ (a)_{2} = b ∧ ((a)_{3})_{2} = 0 ∧ ((a)_{3})_{3} = ⌜<⌝ ∧ (((a)_{3})_{4})_{1} = c ∧ ¬ Libre(c, (((a)_{3})_{4})_{2})

Théorème 1.3.2. Il existe une fonction p.r. Val telle que pour tout terme clos t de l’arithmétique

Val(⌜t⌝) = |t|

Il existe un prédicat p.r. Vr telle que pour toute formule A de l’arithmétique, Δ et close

Vr(⌜A⌝) ssi A

Démonstration. La fonction Val est définie par :

Val(a) = \begin{cases}0 & si (a)_{3} = ⌜\underline{0}⌝ \\ Val(((a)_{4})_{1}) + 1 & si (a)_{3} = ⌜\underline{S}⌝ \\ Val(((a)_{4})_{1}) + Val(((a)_{4})_{2}) & si (a)_{3} = ⌜\underline{+}⌝ \\ Val(((a)_{4})_{1}) Val(((a)_{4})_{2}) & si (a)_{3} = ⌜\underline{.}⌝ \\ 0 & sinon \end{cases}

Le prédicat Vr est défini par :

Vr(a) ssi Form(a)∧Clos(a)∧\begin{cases}Val(((a)_{4})_{1}) = Val(((a)_{4})_{2}) & si (a)_{2} = 0 et (a)_{3} = ⌜=⌝ \\ Val(((a)_{4})_{1}) < Val(((a)_{4})_{2}) & si (a)_{2} = 0 et (a)_{3} = ⌜<⌝ \\ ¬ Vr((a)_{3}) & si (a)_{2} = 1 \\ Vr((a)_{3}) ∧ Vr((a)_{4}) & si (a)_{2} = 2 \\ Vr((a)_{3}) ∨ Vr((a)_{4}) & si (a)_{2} = 3 \\ ¬ Vr((a)_{3}) ∨ Vr((a)_{4}) & si (a)_{2} = 4 \\ ∀i < Val(((((a)_{4})_{3})_{4})_{2}). Vr(Sub(((a)_{4})_{4}, (a)_{3}, Num(i))) & si QuantBorn(a) ∧ (a)_{2} = 5 \\ ∃i < Val(((((a)_{4})_{3})_{4})_{2}). Vr(Sub(((a)_{4})_{4}, (a)_{3}, Num(i))) & si QuantBorn(a) ∧ (a)_{2} = 6 \end{cases}

La condition x n’est pas variable libre de t dans la définition des quantificateurs bornés nous assure d’une part que t est clos, si bien que l’on est fondé à appliquer Val à son code, et d’autre part que Sub(((a)_{4})_{4}, (a)_{3}, Num(i)) est bien le code d’une formule close.

Remarque : La définition de Vr n’entre pas exactement dans le cadre des schémas de définitions de prédicats p.r. vus dans la section précédente. Le problème est que dans les deux derniers cas (correspondant aux quantificateurs bornés), on définit Vr(⌜∀x < t. A⌝) en fonction de Vr(Sub(⌜A⌝, ⌜x⌝, Num(i)). Or pour que ceci soit vraiment p.r. il faudrait que Sub(⌜A⌝, ⌜x⌝, Num(i)) < ⌜∀x < t. A⌝ ce qui est en général faux. En fait il faut définit un prédicat V (a, b) à deux paramètres en utilisant la variante de la récursion primitive récursive : le paramètre a est le code de la formule sur laquelle on récurre, mais il ne s’agit pas d’une formule close ; le paramètre b est (le code d’) un ensemble de substitutions qui remplace toutes les variables libres de A par des termes clos. Par exemple, l’avant-dernière clause ci-dessus devient alors : V (⌜∀x < t. A⌝, b) ssi

∀i < Val ⌜t⌝. V (⌜A⌝, b :: [Num(i)/x])

où b :: [Num(i)/x] représente (le code de) la substitution b augmentée de la substitution Num(i)/x.

Résultats élémentaires sur les fonctions récursives

Les fonctions de codage vont nous permettre d’établir quelques résultats de base en théorie des fonctions récursives. L’idée fondamentale est d’associer un programme, c’est à dire un objet formel identifié par un entier, à une fonction récursive. Le programme d’une fonction récursive F sera ici une formule A de l’arithmétique définissant la fonction et le calcul de F (a⃗) revient à rechercher un b tel que A[\underline{a}, b].

Théorème 1.3.3 (Forme normale de Kleene). Pour tout k il existe un prédicat p.r. T_{k} d’arité k + 2 tel que si F est une fonction récursive d’arité k alors il existe un entier e appelé l’indice de F tel que

F (a⃗) = π_{1}μx. (T_{k}(e, a⃗, x))  (1.4)

Remarque : C’est un théorème de factorisation du schéma de minimisation.

Démonstration. Soit donc F une fonction récursive d’arité k. D’après le théorème 1.2.1 il y a une formule A[x⃗, y, z] de l’arithmétique qui est Δ et telle que :

b = F (a⃗) ssi ∃z A[\underline{a}, \underline{b}, z]

Mais d’après le théorème 1.3.2 de la partie précédente, pour tout entier c, comme A[\underline{a}, \underline{b}, \underline{c}] est une formule close, on a A[\underline{a}, \underline{b}, \underline{c}] ssi Vr(⌜A[\underline{a}, \underline{b}, \underline{c}]⌝). Par définition de la fonction ParSub on obtient donc

A[\underline{a}, \underline{b}, \underline{c}] ssi Vr(ParSub(⌜A⌝, ⟨⟨⌜x_{1}⌝, Num(a_{1})⟩, …, ⟨⌜x_{k}⌝, Num(a_{k})⟩, ⟨⌜y⌝, Num(b)⟩, ⟨⌜z⌝, Num(c)⟩⟩_{k+2}))

On définit

T_{k}(e, a⃗, a) ssi Vr(ParSub(e, ⟨⟨⌜x_{1}⌝, Num(a_{1})⟩, …, ⟨⌜x_{k}⌝, Num(a_{k})⟩, ⟨⌜y⌝, Num(π_{1}a)⟩, ⟨⌜z⌝, Num(π_{2}a)⟩⟩_{k+2}))

Le prédicat T_{k} est clairement p.r. et vérifie T_{k}(⌜A⌝, a⃗, a) ssi A[\underline{a}, \underline{π_{1}a}, \underline{π_{2}a}]. Supposons qu’il y a un b tel que b = F (a⃗). Donc par définition de A il y a un c tel que A[\underline{a}, \underline{b}, \underline{c}]. Si on prend a = ⟨b, c⟩ on a montré l’existence d’un a tel que T_{k}(⌜A⌝, a⃗, a). Réciproquement, si il existe un tel a, alors on a A[\underline{a}, \underline{π_{1}a}, \underline{π_{2}a}] et donc par définition de A on a π_{1}a = F (a⃗). Donc le théorème est démontré avec e = ⌜A⌝ où A est une formule qui définit F.

Théorème 1.3.4. Un prédicat P est récursif ssi P et ¬P sont tous deux récursivement énumérables.

Démonstration. On a déja vu que si P est récursif alors il est r.e. Si P est récursif alors ¬P est aussi récursif et donc ¬P est également r.e. Réciproquement supposons que P et ¬P sont tous deux r.e. Soient F_{1} et F_{2} deux fonctions récursives telles que P (a⃗) ssi F_{1}(a⃗)↓ et ¬P (a⃗) ssi F_{2}(a⃗)↓ et soient e_{1} et e_{2} des indices pour F_{1} et F_{2}. On a donc F_{i}(a⃗) = π_{1}μx. (T_{k}(e_{i}, a⃗, x)) et en particulier F_{i}(a⃗)↓ ssi il existe un a tel que T_{k}(e_{i}, a⃗, a). Donc

χ_{P} (a⃗) = π_{1}μx. ((T_{k}(e_{1}, a⃗, π_{2}x) ∧ π_{1}x = 0) ∨ (T_{k}(e_{2}, a⃗, π_{2}x) ∧ π_{1}x = 1))

Comme pour tout a⃗ on a F_{i}(a⃗)↓ pour exactement un i on déduit que la fonction χ_{P} est totale.

Théorème 1.3.5. Soit P (a⃗) un prédicat r.e. d’arité 1 et non vide (il y a un a ∈ ℕ tel que P (a)). Alors il existe une fonction récursive totale G telle que P est l’image de G, c’est à dire :

P (a) ssi ∃n, a = F (n)

Démonstration. Par définition de r.e. il y a une fonction récursive F dont P est le domaine c’est à dire : P (a) ssi F (a)↓. Soit e un indice de F. Par le théorème de Kleene on a donc :

P (a) ssi ∃x T_{1}(e, a, x)

Soit G la fonction définie par :

G(c) = \begin{cases}π_{1}c & si T_{1}(e, π_{1}c, π_{2}c) \\ π_{1}μx. (T_{1}(e, π_{1}x, π_{2}x)) & sinon \end{cases}

La fonction G est alors récursive et comme on a supposé P non vide elle est totale. De plus, par construction P est l’image de G.

Accolades de Kleene (Kleene’s brackets). Soit e un entier. On définit

{e}(a⃗) = π_{1}μx. (T_{k}(e, a⃗, x))

Remarque : La fonction λea⃗. {e}(a⃗) est donc récursive d’arité k + 1. Si F est k-récursive et e est un indice pour F alors

F (a⃗) = {e}(a⃗)

Théorème 1.3.6 (Théorème S_{m}^{n}). Pout tous entiers m et n, il existe une fonction p.r. S_{m}^{n} d’arité m + 1 telle que

{e}(a_{1}, …, a_{m+n}) = {S_{m}^{n}(e, a_{n+1}, …, a_{m+n})}(a_{1}, …, a_{n})

Démonstration. On ne traite que le cas m = 1, le reste s’en déduit par récurrence sur m. On définit S^{n} par :

S^{n}(e, a) = Sub(e, ⌜x_{n+1}⌝, Num(a))

On voit immédiatement par définition des accolades de Kleene et du prédicat T_{n} que l’on a le résultat attendu : {e}(a_{1}, …, a_{n+1}) = {S^{n}(e, a_{n+1})}(a_{1}, …, a_{n}).

Nous terminerons cette partie avec une conséquence importante du théorème S_{m}^{n}.

Théorème 1.3.7 (Théorème de récursivité de Kleene). Soit F une fonction récursive d’arité k + 1. Il existe un entier e tel que

{e}(a⃗) = F (a⃗, e)

C’est ce théorème qui permet de montrer que toute fonction définie par un système d’équations récursives (au sens informatique) est récursive. Un exemple notable est la fonction d’Ackermann définie par :

A(0, p) = p + 1
A(n + 1, 0) = A(n, 1)
A(n + 1, p + 1) = A(n, A(n + 1, p))

Pour montrer qu’elle est récursive on considère la fonction H définie par

H(n, p, a) = \begin{cases}p + 1 & si n = 0 \\ \{a\}(n −^{·} 1, 1) & si n > 0 et p = 0 \\ \{a\}(n −^{·} 1, \{a\}(n, p −^{·} 1)) & sinon \end{cases}

Alors H est récursive et en applicant le théorème de récursivité de Kleene, on déduit l’existence d’un a tel que {a}(n, p) = H(n, p, a). Un tel a est un indice pour la fonction A.

Démonstration. Soit G la fonction récursive définie par G(a⃗, a) = F (a⃗, S^{k}(a, a)) et soit f un indice pour G. Alors on a {f}(a⃗, a) = F (a⃗, S^{k}(a, a)) ; mais par le théorème S_{m}^{n} on en déduit que {S^{k}(f, a)}(a⃗) = F (a⃗, S^{k}(a, a)). Si on prend a = f on obtient le résultat souhaité avec e = S^{k}(f, f).

1.4 Le prédicat de prouvabilité

Codage des séquents On rappelle qu’un séquent n’est rien d’autre qu’un couple de deux suites finies de formules ; soit S = A_{1}, …, A_{m} ⊢ B_{1}, …, B_{n} un séquent. Le code de S est :

⌜S⌝ = ⟨3, 0, ⟨⌜A_{1}⌝, …, ⌜A_{m}⌝⟩_{m}, ⟨⌜B_{1}⌝, …, ⌜B_{n}⌝⟩_{n}⟩_{4}

Théorie. Une théorie T est un ensemble de formules closes appelées les axiomes de T, dans un langages L donné. Une formule A prouvable dans la théorie T si il existe un sous-ensemble fini T_{0} de T tel que le séquent T_{0} ⊢ A est prouvable. On dit alors que A est un théorème de T ce que l’on note T ⊢ A.

Une théorie est cohérente si le séquent vide n’y est pas démontrable, c’est à dire si pour tout sous-ensemble fini T_{0} de T le séquent T_{0} ⊢ n’est pas prouvable. Une théorie est primitive récursive si le prédicat

Ax_{T} (a) ssi a est le code d’un axiome de T

est primitif récursif.

On dit qu’une théorie T′ étend une théorie T si le langage L′ de T′ contient le langage L de T et si T′ contient T. On dit de plus que T′ est une extension primitive récursive de T si T et T′ sont primitive récursives

Codage des preuves. On se donne maintenant une numérotation des règles du calcul des séquents : 0 pour la règle axiome, 1 pour la règle de coupure, 2 et 3 pour les règles d’échanges gauche et droite, 4 et 5 pour les règles d’affaiblissement gauche et droite, … On définit le code d’une démonstration π du calcul des séquents dans la théorie p.r. T par :

⌜π⌝ = \begin{cases}⟨4, 0, ⌜A⌝, 0⟩_{4} & si π est la démonstration réduite au seul séquent A ⊢ A \\ ⟨4, i, ⌜π_{0}⌝, 0⟩_{4} & si π est obtenue en appliquant la règle unaire de numéro i à la preuve π_{0} \\ ⟨4, i, ⌜π_{1}⌝, ⌜π_{2}⌝⟩_{4} & si π est obtenue en appliquant la règle binaire de numéro i à π_{1} et π_{2} \end{cases}

Théorème 1.4.1. Soit T une théorie p.r. Il existe un prédicat p.r. Pr_{T} tel que :

Pr_{T} (a, p) ssi p = ⌜π⌝ et a = ⌜A⌝ où π est une démonstration de T_{0} ⊢ A pour un sous-ensemble fini T_{0} de T

Essentiellement le théorème établit que l’on peut vérifier de manière calculatoire (et même par une fonction primitive récursive ce qui est à peine plus fort) la correction d’une preuve. Il serait trop fastidieux de le démontrer ici. Il s’agit encore une fois de programmer tout un ensemble de fonctions et prédicats p.r.

Le prédicat de prouvabilité. On note Thm_{T} le prédicat de prouvabilité de la théorie T, c’est à dire que Thm_{T} est défini par :

Thm_{T} (a) ssi a est le code d’un théorème de T

Comme on a Thm_{T} (a) ssi ∃b Pr_{T} (a, b) on voit que Thm_{T} est r.e. (dès que T est p.r.).

Théories complètes, décidables. Une théorie T est complète si pour toute formule A close on a soit T ⊢ A, soit T ⊢ ¬A. Une théorie T est décidable si Thm_{T} est un prédicat récursif.

Théorème 1.4.2. Si T est une théorie p.r. cohérente et complète alors T est décidable.

Démonstration. Remarquons que pour toute formule A on a T ⊢ A ssi T ⊢ \overline{A}. Par conséquent si T est cohérente et complète alors T ⊬ A ssi T ⊢ ¬\overline{A}. Donc on a ¬ Thm_{T} (a) ssi soit a n’est pas le code d’une formule, soit Thm_{T} (Neg(Clot(a))). Comme la fonction λx. Neg(Clot(x)) est p.r. et comme Thm_{T} est r.e. on voit que ¬ Thm_{T} est r.e. d’où l’on déduit par le théorème 1.3.4 que Thm_{T} est récursif.

L’arithmétique élémentaire

L’arithmétique élémentaire (EA) est l’ensemble fini (des clôtures universelles) des axiomes suivants (dans le langage de l’arithmétique :

1. Axiomes d’égalité :

(a) x = x; ;

(b) x = x′ ∧ y = y′ ∧ x = y → x′ = y′;

(c) x = x′ → S(x) = S(x′) ;

(d) x = x′ ∧ y = y′ → x + x′ = y + y′ :

(e) x = x′ ∧ y = y′ → x · x′ = y · y′;

(f) x = x′ ∧ y = y′ ∧ x < y → x′ < y′;

2. Axiomes de définitions : (a) ¬S(x) = 0 ;

(b) S(x) = S(y) → x = y;

(c) x + 0 = x;

(d) x + S(y) = S(x + y) ;

(e) x · 0 = 0 ;

(f) x · S(y) = x · y + x;

(g) ¬x < 0 ;

(h) x < S(y) ↔ x < y ∨ x = y;

(i) x < y ∨ x = y ∨ y < x; Lemme 1.4.3. L’arithmétique élémentaire est une théorie primitive récursive.

On note Pr_{0} le prédicat Pr_{EA} et Thm_{0} le prédicat Thm_{EA}. Théorème 1.4.4. Si A est une formule de l’arithmétique qui est Δ et close alors :

A → EA ⊢ A
¬A → EA ⊢ ¬A

Si A est Σ et close alors :

A → EA ⊢ A

Démonstration. Le cas d’une formule Δ se déduit du lemme suivant : Lemme 1.4.5. Pour tous entiers n et m et tout terme t du langage de l’arithmétique on a

EA ⊢ \underline{n} \underline{+} \underline{m} = \underline{m + n}
EA ⊢ \underline{n} \underline{.} \underline{m} = \underline{mn}
|t| = n → EA ⊢ t = \underline{n}
n = m → EA ⊢ \underline{n} = \underline{m}
n ≠ m → EA ⊢ ¬(\underline{n} = \underline{m})
n < m → EA ⊢ \underline{n} < \underline{m}
n ≮ m → EA ⊢ ¬(\underline{n} < \underline{m})
EA ⊢ x < \underline{n} ↔ x = \underline{0} ∨ ⋯ ∨ x = \underline{n − 1}

Chaque clause du lemme se démontre par récurrence sur n et/ou m et/ou t. Pour fixer les idées on va montrer la dernière clause : EA ⊢ x < \underline{n} ↔ x = \underline{0} ∨ ⋯ ∨ x = \underline{n − 1}. Si n = 0 cette équivalence est conséquence de l’axiome x < 0 ⊢ de EA : en effet la disjonction est alors vide donc fausse donc équivalente à x < 0 puisque cette formule est supposée fausse dans EA. Supposons le résultat démontré pour n. On a EA ⊢ x < \underline{n + 1} ↔ x < \underline{n} ∨ x = \underline{n} comme conséquence des axiomes de EA et du fait que EA ⊢ \underline{S} \underline{n} = \underline{n + 1}. Or par récurrence sur n on a EA ⊢ x < \underline{n} ↔ x = \underline{0} ∨ ⋯ ∨ x = \underline{n − 1} ; on en déduit immédiatement le résultat, i.e., EA ⊢ x < \underline{n + 1} ↔ x = \underline{0} ∨ ⋯ ∨ x = \underline{n}.

Le théorème se déduit du lemme par induction sur la formule A. Le cas d’une formule atomique est traitée presqu’entièrement par le lemme. Le seul cas compliqué est est en fait celui des formules à quantificateur borné. Supposons donc que A = ∀x < t. B. Comme A est close, t est clos et B = B[x] a x pour seule variable libre.

Si A est vraie alors pour tout a inférieur à |t|, B[\underline{a}] est vraie. Par hypothèse d’induction on en déduit que EA ⊢ B[\underline{a}] pour tout a < |t|. Donc EA ⊢ x = \underline{a} → B pour tout a < |t|. Notons n = |t|. On a EA ⊢ x < \underline{n} ↔ x = \underline{0} ∨ ⋯ ∨ x = \underline{n − 1}. Donc EA ⊢ x < \underline{n} → B. Comme EA ⊢ t = \underline{n} (puisque n = |t|) on obtient finalement le résultat souhaité : EA ⊢ x < t → B.

Si A est fausse alors il y a un a < |t| tel que B[\underline{a}] est fausse. Par hypothèse d’induction on a EA ⊢ ¬B[\underline{a}], mais comme a < |t| on a également EA ⊢ \underline{a} < t d’où l’on déduit finalement EA ⊢ ∃x < t. ¬B. Mais cette dernière formule est logiquement équivalente à ¬A.

Le cas d’un ∃ borné se déduit de la remarque que EA ⊢ ¬∀x < t. B ↔ ∃x < t. ¬B (cette équivalence est d’ailleurs prouvable dans le calcul des séquents sans axiome) et du cas d’un ∀ borné.

Si maintenant A est une formule Σ close et que A est vraie on démontre que EA ⊢ A par induction sur A. Le seul cas intéressant de l’induction est A = ∃x B où B = B[x] a comme seule variable libre x. Comme A est vraie il existe un a tel que B[\underline{a}] est vraie, donc par induction EA ⊢ B[\underline{n}] d’où l’on déduit immédiatement que EA ⊢ A.

Fonctions et prédicats représentables dans EA. Soit F une fonction d’arité k. On dit que F est représentable si il existe une formule A[x⃗, y] de l’arithmétique et telle que :

b = F (a⃗) → EA ⊢ A[\underline{a}, y] ↔ y = \underline{b}

Soit P un prédicat d’arité k. On dit que P est représentable si il existe une formule A[x⃗] telle que :

P (a⃗) ssi EA ⊢ A[\underline{a}]
¬P (a⃗) ssi EA ⊢ ¬A[\underline{a}]

Théorème 1.4.6 (Représentabilité). Si F est est une fonction récursive alors F est représentable. Si P est un prédicat récursif alors P est représentable.

Démonstration. Le cas d’un prédicat récursif est conséquence de celui d’une fonction. Si P est récursif alors χ_{P} est récursive totale, donc il y a une formule A[x⃗, y] qui représente χ_{P}. Mais alors la formule B[x⃗] = A[x⃗, \underline{0}] représente P. Supposons que P (a⃗), c’est à dire que χ_{P} (a⃗) = 0. Alors on a EA ⊢ A[\underline{a}, y] ↔ y = \underline{0} d’où l’on déduit aisément en appliquant les axiomes d’égalité que EA ⊢ B[\underline{a}]. Si au contraire on a ¬P (a⃗) c’est à dire χ_{P} (a⃗) = 1 alors EA ⊢ A[\underline{a}, y] ↔ y = \underline{S} \underline{0}. En particulier EA ⊢ A[\underline{a}, \underline{0}] ↔ \underline{0} = \underline{S} \underline{0}. Comme EA ⊢ ¬(\underline{0} = \underline{S} \underline{0}) on voit que EA ⊢ ¬B[\underline{a}].

On montre maintenant le cas d’une fonction récursive. C’est une conséquence de : Lemme 1.4.7. Si F est récursive alors il existe une formule A[x⃗, y] qui est Σ, qui définit F et telle que

EA ⊢ A[x⃗, y] ∧ A[x⃗, y′] → y = y′

Commençons par finir le théorème. Supposons b = F (a⃗). Comme la formule A du lemme définit F on a A[\underline{a}, \underline{b}] ; comme elle est Σ, par le théorème 1.4.4 on déduit que EA ⊢ A[\underline{a}, \underline{b}]. En utilisant les axiomes d’égalité on voit immédiatement qu’alors EA ⊢ y = \underline{b} → A[\underline{a}, y]. Par ailleurs, d’après le lemme on a que EA ⊢ A[\underline{a}, y] ∧ A[\underline{a}, \underline{b}] → y = \underline{b}. Mais comme EA ⊢ A[\underline{a}, \underline{b}], on voit que EA ⊢ A[\underline{a}, y] → y = \underline{b}.

Démontrons maintenant le lemme. Soit A une formule Σ qui définit F. On va construire une formule D[x⃗, y] qui est Σ, équivalente à A (donc qui définit F) et telle que EA ⊢ D[x⃗, y] ∧ D[x⃗, y′] → y = y′. Comme A est Σ on sait qu’il existe une formule A_{0}[x⃗, y, z] qui est Δ et telle que

A ↔ ∃z A_{0}

On note x ≤ y pour x < \underline{S} y. On définit B_{0}[x⃗, y, z] = ∃w ≤ z (y ≤ z ∧ z = y \underline{+} w ∧ A_{0}[x⃗, y, w]). Clairement B_{0} est Δ et ∃z B_{0} est équivalente à A. Mais en plus on a

EA ⊢ B_{0}[x⃗, y, z] → y ≤ z

Soit maintenant C_{0} = B_{0} ∧ ∀z′ < z ∀y′ ≤ z′ ¬B_{0}[x⃗, y′, z′]. Alors C_{0} est Δ et on a encore ∃z C_{0} équivalente à A. Mais en plus on a

EA ⊢ C_{0}[x⃗, y, z] ∧ C_{0}[x⃗, y′, z′] → z = z′

On raisonne dans EA : soient z, z′ et y, y′ tels que C_{0}[x⃗, y, z] et C_{0}[x⃗, y′, z′]. Supposons que z < z′. Comme C_{0}[x⃗, y′, z′] on a ∀u < z′ ∀v ≤ u ¬B_{0}[x⃗, v, u] donc en particulier pour u = z, ∀v ≤ z ¬B_{0}[x⃗, v, z]. Mais comme C_{0}[x⃗, y, z] on a B_{0}[x⃗, y, z] et donc y ≤ z. En prenant v = y on obtient une contradiction. Donc ¬(z < z′). Similairement ¬(z′ < z) et les axiomes de EA entrainent alors que z = z′.

Soit finalement D_{0} = C_{0} ∧ ∀y′ < y ¬C_{0}[x⃗, y′, z]. Alors D = ∃z D_{0} a les propriétés requises par le lemme. En effet D_{0} est Δ et clairement D est équivalente à A donc définit F. Supposons que y et y′ sont tels que D[x⃗, y] et D[x⃗, y′]. On raisonne dans EA. Comme D[x⃗, y] il y a un z tel que D_{0}[x⃗, y, z] donc en particulier tel que C_{0}[x⃗, y, z]. De même, comme D[x⃗, y′], il y a un z′ tel que C_{0}[x⃗, y′, z′]. Mais alors z = z′ et donc D_{0}[x⃗, y, z] ∧ D_{0}[x⃗, y′, z]. Mais comme précédemment on voit que l’on ne peut alors avoir y < y′, ni y′ < y d’où y = y′ comme annoncé.

1.5 Théorèmes d’indécidabilité et d’incomplétude

Théorème 1.5.1 (Church). Soit T une extension p.r. de EA. Si T est cohérente alors T est indécidable.

Démonstration. On définit un prédicat Q par :

Q(a) ssi ¬ Thm_{T} (Sub(a, ⌜x⌝, Num(a))

Supposons que Q est récursif. Par le théorème de représentation il y a une formule A[x] qui représente Q. Posons a = ⌜A⌝.

Si Q(a) est vrai, alors EA ⊢ A[\underline{a}], donc comme T est une extension de EA, T ⊢ A[\underline{a}]. Mais alors Thm_{T} (⌜A[\underline{a}]⌝) est vrai, i.e., Thm_{T} (Sub(⌜A⌝, ⌜x⌝, Num(a))), i.e., ¬Q(a) puisque a = ⌜A⌝.

Donc Q(a) est faux, c’est à dire que Thm_{T} (Sub(a, ⌜x⌝, Num(a))) est vrai donc, comme a = ⌜A⌝, que T ⊢ A[\underline{a}]. Mais si Q(a) est faux, comme A représente Q on a EA ⊢ ¬A[\underline{a}], donc T ⊢ ¬A[\underline{a}] ce qui contredit la cohérence de T.

Par conséquent Q ne peut être récursif. Comme Sub et Num sont toutes les deux p.r., c’est que Thm_{T} n’est pas récursif.

Corollaire 1.5.2. Le calcul des prédicats est indécidable.

Démonstration. On note N la suite (finie) des formules de l’arithmétique suivantes :

Égalité x = x, x = y → \underline{S} x = \underline{S} y, x = x′ ∧ y = y′ → x \underline{+} y = x′ \underline{+} y′, x = x′ ∧ y = y′ → x \underline{.} y = x′ \underline{.} y′,

x = x′ ∧ y = y′ → x = y → x′ = y′, x = x′ ∧ y = y′ → x < y → x′ < y′; Arithmétique élémentaire x \underline{+} \underline{0} = x, x \underline{+} \underline{S} y = \underline{S}(x \underline{+} y), x \underline{.} \underline{0} = \underline{0}, x \underline{.} \underline{S} y = x \underline{.} y \underline{+} x, ¬(x < 0),

x < \underline{S} y ↔ x < y ∨ x = y, ¬(\underline{S} x = 0), \underline{S} x = \underline{S} y → x = y, x < y ∨ x = u ∨ y < x. On a alors

Lemme 1.5.3. Soit A une formule de l’arithmétique. Alors

EA ⊢ A ssi le séquent N ⊢ A est prouvable dans le calcul des séquents

La preuve de ce lemme est un (comme d’autres) trop fastidieuse pour être explicitée ici. On la laisse au lecteur.

Soit Thm_{LK} le prédicat de prouvabilité du calcul des séquents défini par Thm_{LK}(a) ssi a est le code d’un séquent S et S est prouvable dans LK. D’après le lemme pour toute formule A, Thm_{EA}(⌜A⌝) est équivalent à Thm_{LK}(⌜N ⊢ A⌝), donc d’après le théorème de Church, Thm_{LK} n’est pas récursif.

Corollaire 1.5.4 (Incomplétude). Soit T une extension p.r. de EA. Si T est cohérente alors T est incomplète.

Démonstration. On a vu qu’une théorie cohérente et complète est décidable.

1.6 Le second théorème de Gödel

Théorème 1.6.1. Soit T une extension primitive récursive cohérente de EA. Il existe une formule Π close G_{T} telle que : G_{T} est vraie mais G_{T} n’est pas prouvable dans T.

Démonstration. On va commencer par énoncer le lemme suivant Lemme 1.6.2. Soit Q un prédicat unaire. Si Q est r.e. (resp. si ¬Q est r.e.^{2}) alors il existe une formule close A de l’arithmétique qui est Σ (resp. Π) telle que :

Q(⌜A⌝) ssi A

2. On dit que Q est co-r.e.

Supposons le lemme démontré et prenons Q(a) ssi ¬ Thm_{T} (a). Alors Q est co-r.e. donc, d’après le lemme, il existe une formule close G_{T} qui est Π et telle que :

G_{T} ssi ¬ Thm_{T} (⌜G_{T} ⌝)

Si G_{T} est fausse on a donc Thm_{T} (⌜G⌝_{T}), donc T ⊢ G_{T}. Mais si G_{T} est fausse, ¬G_{T} est vraie et comme elle est (équivalente à une formule) Σ, on a EA ⊢ ¬G_{T} par le théorème 1.4.4. Comme T est une extension de EA on a également T ⊢ ¬G_{T}, ce qui contredit la cohérence de T. Par conséquent G_{T} est vraie et donc n’est pas prouvable dans T.

Démontrons maintenant le lemme. Supposons que Q est r.e. (resp. co-r.e.) et soit P le prédicat binaire défini par P (a, b) ssi Q(Sub(a, ⌜x⌝, Num(b))) (resp. ssi ¬Q(Sub(a, ⌜x⌝, Num(b))). Comme Sub et Num sont p.r. P est r.e. Donc il existe une formule de l’arithmétique B[x, y] qui est Σ et telle que

P (a, b) ssi B[\underline{a}, \underline{b}]

Posons A[x] = B[x, x] (resp. A[x] = ¬B[x, x]) et soit a = ⌜A⌝. Remarquons que A est Σ (resp. Π) et que A[\underline{a}] est close. On a : A[\underline{a}] est équivalente à P (a, a) (resp. à ¬P (a, a)), c’est à dire à Q(Sub(a, ⌜x⌝, Num(a))). Mais par définition de Sub on a Sub(a, ⌜x⌝, Num(a)) = ⌜A[\underline{a}]⌝, donc finalement A[\underline{a}] est équivalente à Q(⌜A[\underline{a}]⌝).

Remarque : Quand bien même G_{T} est vraie, il se pourrait que ¬G_{T} soit prouvable dans T. Il n’a jamais été dit, et c’est d’ailleurs faux, qu’une extension quelconque de EA ne démontre que des formules vraies. Typiquement si A est une formule qui exprime la cohérence de PA alors PA + ¬A est cohérente (en vertu du second théorème de Gödel ci-dessous) et démontre ¬A qui est visiblement fausse (nul ne doute que PA est cohérente !). On n’a donc pas démontré ici l’incomplètude de T mais un résultat un peu plus faible. C’est assez normal si on considère que l’on n’a utilisé ici que la définissabilité du prédicat Thm_{T} alors que pour démontrer l’incomplètude on s’est servi de la représentabilité de Thm_{T}.

Arithmétique de Peano. L’arithmétique de Peano PA est la théorie constituée des séquents de EA auxquels on ajoute le principe de récurrence, i.e., tous les séquents de la forme

A[\underline{0}], ∀x (A[x] → A[\underline{S} x]) ⊢ A[x]

où A[x] est une formule quelconque.

Lemme 1.6.3. PA est une théorie p.r.

Remarquons que toutes les preuves que nous avons faites jusqu’à maintenant (ainsi d’ailleurs que celles que nous n’avons pas faites) n’utilise comme principe le plus évolué que le principe de récurrence. C’est en particulier le cas du théorème ci-dessus ainsi que des deux faits que l’on a utilisés pour le montrer :

1. le fait que Thm_{T} est définissable par une formule Σ ;

2. le théorème 1.4.4 (une formule Σ vraie est prouvable dans EA).

Autrement dit on a le lemme suivant

Lemme 1.6.4. Le théorème 1.6.1 est entièrement formalisable dans PA, c’est à dire que, si T est une extension p.r. de EA alors :

PA ⊢ Coh(T) → G_{T} ∧ ¬ Thm_{T} (⌜G_{T} ⌝)

Encore une démonstration fastidieuse que l’on ommet ici.

Théorème 1.6.5 (Gödel). Soit T une extension p.r. de PA. Si T ⊢ Coh(T) alors T est incohérente.

Par contraposition : si T est cohérente alors T ne démontre pas Coh(T), ce que l’on résume souvent, et incorrectement, par le slogan : « T ne démontre pas sa propre cohérence ». C’est incorrect car T peut parfaitement démontrer Coh(T), il suffit que T soit incohérente !

Démonstration. Comme T étend PA on a T ⊢ Coh(T) → G_{T} ∧ ¬ Thm_{T} (⌜G_{T} ⌝) donc en particulier T ⊢ Coh(T) → G_{T}. Donc si T ⊢ Coh(T) alors T ⊢ G_{T} et d’après le théorème 1.6.1, T n’est pas cohérente.

22  Théorèmes de Gödel

Chapitre 2

Lambda-calcul

On va procéder ici à une rapide introduction au lambda-calcul. Pour plus ample information, le lecteur

est invité à se reporter au livre de Krivine [3] duquel sont empruntés les concepts et résultats exposés ici.

2.1 Le lambda-calcul pur

Le lambda-calcul peut être décrit comme une théorie générale des fonctions. Il fournit des notations pour les deux opérations sur les fonctions :

— application d’une fonction à un argument

— définition d’une fonction à partir d’un terme, comme lorsqu’on parle de la fonction qui à x associe x+3. Observer que cela nécessite aussi la présence de variables (comme « x » dans l’exemple précédent).

Ce qui peut sembler étrange au premier abord, c’est que la syntaxe du lambda-calcul ne possède que ces deux opérations : il n’y a pas d’objets « de base » (comme les entiers) sur lesquels calculer, ni d’opérations prédéfinies (addition, etc.). Il se trouve que ces objets peuvent être définis dans le lambda-calcul, comme on aura l’occasion de le voir.

On se donne un ensemble infini dénombrable V de variables. L’ensemble des lambda-termes Λ (ou Λ(V) lorsqu’il est nécessaire de préciser les variables) est donné par :

— Si x ∈ V, alors x ∈ Λ.

— Si t, u ∈ Λ, alors (t)u ∈ Λ (application de la « fonction » t à l’« argument » u).

— Si t ∈ Λ et x ∈ V, alors λx t ∈ Λ. Ce terme représente la fonction qui à x associe t (dans lequel x figure en général).

Il faut voir un (lambda-)terme comme un arbre possédant trois types de noeuds :

— Des feuilles, qui sont étiquetées par des variables.

— Des noeuds application, qui ont deux descendants (la fonction et l’argument).

— Des noeuds lambda ou abstraction, qui sont étiquetés par une variable et ont un descendant (le corps de la fonction).

Voici deux conventions typographiques très utiles et très répandues dans la littérature sur le sujet :

— Au lieu d’écrire (… (t)t_{1} …)t_{n}, on écrit (t)t_{1} … t_{n}.

— Au lieu d’écrire λx_{1} … λx_{n} t, on écrit λx_{1} … x_{n} t.

Sous-termes. Un sous-terme d’un terme t est un terme apparaissant sous un noeud de t. Un même sous-terme de t peut apparaître à plusieurs endroits différents de t : il a alors plusieurs occurrences dans t. Par exemple, le terme λx (y)x a deux occurrences différentes dans le terme suivant :

(λx (y)x)λz (z)λx (y)x

Variables libres, liées. Une variable apparaissant dans un terme est liée s’il y a au-dessus d’elle, dans l’arbre, un noeud lambda étiqueté par la même variable. Une variable qui n’est pas liée est libre. Par exemple, dans

t_{1} = λx (y)x,

la variable x est liée, et la variable y est libre.

Plus précisément, on peut définir par récurrence sur la taille des lambda-termes l’ensemble VL(t) des variables libres d’un terme t :

VL(t) = \begin{cases}\{x\} & si t = x \\ VL(u) ∪ VL(v) & si t = (u)v \\ VL(u) \ \{x\} & si t = λx u \end{cases}

Il est clair que le nom d’une variable liée n’a aucune importance : le terme t_{1} précédent doit être identifié au terme

λz (y)z

Toutefois, lorsqu’on renomme en y la variable liée x, dans une occurrence d’un sous-terme λx u d’un terme t, il faut prendre garde à ce que la nouvelle variable y que l’on veut utiliser ne soit pas déjà libre dans u : dans le terme t_{1}, on ne peut pas renommer x en y. On obtiendrait le terme λy (y)y, qui n’a pas la même signification que t.

Alpha-équivalence. Deux termes sont dits α-équivalents (ou simplement équivalents) si on peut obtenir le second à partir du premier en renommant des variables liées (en respectant bien sûr les précautions ci-dessus concernant la capture des variables libres). Il s’agit d’une relation d’équivalence.

A partir de maintenant, on considérera les lambda-termes à α-équivalence près, c’est à dire que l’on écrira t = u pour « t est α-équivalent à u », ou « t et u ne diffèrent que par les noms de leur variables liées ».

Substitution. Une opération très importante sur les lambda-termes est la substitution d’une suite de termes u_{1}, …, u_{n} à la suite de variables libres x_{1}, …, x_{n} d’un terme t, ce qu’on note t[u_{1}/x_{1}, …, u_{n}/x_{n}] (ou lorsque ce n’est pas ambigu t[u⃗/x⃗]), et qu’on définit par récurrence sur la taille de t :

t[u⃗/x⃗] = \begin{cases}t & si x_{i} ∉ VL(t) pour i = 1, …, n \\ u_{i} & si t = x_{i} \\ (t_{1}[u⃗/x⃗])t_{2}[u⃗/x⃗] & si t = (t_{1})t_{2} \\ λz s[z/y, u⃗/x⃗ \ y] & si t = λy s et z est une variable fraîche \end{cases}

Par « z est une variable fraîche » on entend : z ∉ VL(u_{i}) pour i = 1, …, n; par u⃗/x⃗ \ y on entend la suite u_{1}/x_{1}, …, u_{n}/x_{n} amputée de u_{i}/x_{i} si y = x_{i}.

Par exemple, si on veut substituer y à x et t à y dans le terme t = λy (y)x on obtient :

(λy (y)x)[y/x, t/y] = λz ((y)x)[z/y, y/x]
= λz (y[z/y, y/x])x[z/y, y/x]
= λz (z)y

Remarque : Quand on écrit t[t_{1}/x_{1}, …, t_{n}/x_{n}], les n substitutions sont faites simultanément, et non l’une après l’autre si bien que

t[t_{1}/x_{1}, …, t_{n}/x_{n}] = t[t_{σ1}/x_{σ1}, …, t_{σn}/x_{σn}]

pour toute permutation σ de {1, …, n}.

Lemme 2.1.1. Soit t, t_{1}, …, t_{n}, u_{1}, …, u_{m} des termes. On a

t[t⃗/x⃗][u⃗/y⃗] = t[t⃗[u⃗/y⃗]/x⃗, u⃗/y⃗]

La preuve de ce lemme est laissée en exercice (simple récurrence sur la taille de t).

Généralités sur les relations

Soit E un ensemble. Pour nous, une relation sur E est un sous-ensemble de E × E (on ne considère ici que des relations binaires). Soit R une relation sur E. On écrit souvent a R b au lieu de (a, b) ∈ R.

On dit que R est réflexive si

∀a ∈ E a R a .

On dit que R est symétrique si

∀a, b ∈ E a R b → b R a .

On dit que R est transitive si

∀a, b, c ∈ E a R b ∧ b R c → a R c .

On dit que R est une relation d’équivalence si elle a ces trois propriétés.

Clôtures symétrique et transitive. La clôture symétrique de R est la plus petite (pour l’inclusion) relation S sur E qui contient R et qui est symétrique. On vérifie facilement que

a S b ↔ a R b ∨ b R a .

La clôture transitive de R est la plus petite relation T sur E qui contient R et qui est réflexive et transitive. On vérifie facilement que a T b si et seulement s’il existe une suite a_{1}, … a_{n} telle que a_{1} = a, a_{n} = b et, pour chaque i = 1, …, n − 1, on a a_{i} R a_{i+1}.

La clôture symétrique transitive de R est la plus petite relation d’équivalence sur E qui contienne R. On vérifie facilement que c’est la clôture transitive de la clôture symétrique de R.^{1}

Confluence. La relation R est dite confluente si, pour tous a, a_{1}, a_{2} ∈ E tels que a R a_{1} et a R a_{2}, il existe b ∈ E tel que a_{1} R b et a_{2} R b. Lemme 2.1.2. La clôture transitive d’une relation confluente est confluente.

La preuve est laissée en exercice.

Congruences. Soit R une relation sur Λ. On dit que R est une congruence ou que R passe au contexte si R est réflexive et vérifie

— (u)v R (u′)v′ dès que u R u′ et v R v′;

— λx u R λx u′ dès que u R u′.

La β-réduction

Un rédex est un lambda-terme de la forme

(λx t)u

La β-réduction (la seule règle de calcul du lambda-calcul, pour nous du moins) exprime qu’un tel rédex, où qu’il se trouve dans un terme, peut être contracté en

t[u/x]

ce qui se justifie bien, si l’on a présent à l’esprit que l’expression (λx t)u représente l’application à u de la fonction qui à x associe t (dans lequel x figure libre en général).

Beta-réduction. Un terme t se β-réduit en une étape en un terme t′ si t′ s’obtient à partir de t en sélectionnant dans t exactement un rédex (c’est-à-dire une occurrence de sous-terme de t qui est un rédex) et en contractant ce rédex. Plus précisément, on définit la relation β_{0} par récurrence sur son premier argument :

— x β_{0} u n’est jamais vrai quand x ∈ V ;

— (λx u)v β_{0} u[v/x] ;

— (u)v β_{0} (u′)v si u β_{0} u′;

— (u)v β_{0} (u)v′ si v β_{0} v′;

— λx u β_{0} λx u′ si u β_{0} u′.

Forme normale. Un terme t est dit normal s’il ne contient aucun rédex, autrement dit, s’il n’existe aucun terme u tel que t β_{0} u. Par exemple, le terme

λf (f)λx (f)λd x

est normal.

On note β la clôture transitive de β_{0} et =_{β} la clôture symétrique et transitive de β_{0}. Deux termes qui sont reliés par cette relation d’équivalence sont dits β-équivalents. Lemme 2.1.3. Les relations β et =_{β} passent au contexte.

Remarque : En fait la relation β (resp. =_{β}) est la plus petite relation qui (i) passe au contexte, (ii) est transitive (resp. est une relation d’équivalence) et (iii) relate (λx u)v et u[v/x].

Termes (fortement) normalisables. Un terme t est normalisable s’il existe un terme normal u tel que t β u, et alors on dit que u est une forme normale de t. On dit que t est fortement normalisable s’il n’y a pas de suite infinie de terme (t_{i})_{i=1,2,...} telle que t_{1} = t et t_{i} β_{0} t_{i+1} pour tout i.

Clairement, tout terme fortement normalisable est normalisable.

Voici quelques exemples. Soit Δ = λx (x)x. Le terme (Δ)Δ n’est pas normalisable, puisqu’il se réduit en une étape en (Δ)Δ. Le terme

t = (λd z)(Δ)Δ

est normalisable, mais non fortement normalisable.

1. et non pas la clôture symétrique de la clôture transitive de R (cette dernière relation n’a d’ailleurs aucune raison d’être une relation d’équivalence).

Le théorème de Church-Rosser

Confluence. Un même terme peut contenir plusieurs rédex, et donc il y a plusieurs façons de le réduire en général. Par exemple, dans le terme t ci-dessus, la réduction du rédex le plus extérieur aboutit en une étape à une forme normale, alors que la réduction de l’autre rédex aboutit à un terme égal à t.

On peut donc se demander si, en réduisant un terme de deux façons différentes, on peut aboutir à deux formes normales distinctes. Ce n’est pas le cas, grâce au théorème de Church-Rosser :

Théorème 2.1.4 (Church-Rosser). La relation β sur Λ est confluente.

Admettons ce théorème pour un moment. Soient t un terme et t_{1}, t_{2} deux termes normaux tels que t β t_{1} et t β t_{2}. Par le théorème, il existe un terme t′ tel que t_{1} β t′ et t_{2} β t′. Comme t_{1} est normal, t_{1} = t′, et de même, t_{2} = t′. Donc t_{1} = t_{2} et on vient de montrer le

Corollaire 2.1.5. Un terme normalisable du lambda-calcul a une unique forme normale.

Une autre conséquence intéressante (et tout aussi immédiate) est

Corollaire 2.1.6. Soient t et u deux termes. On a t =_{β} u ssi il existe v tel que t β v et u β v.

En particulier deux termes normalisables sont β-équivalent ssi ils ont la même forme normale.

Le théorème 2.1.4 serait immédiat (grâce au lemme 2.1.2) si la relation β_{0} elle-même était confluente. Ce n’est malheureusement pas le cas, comme le montre l’exemple suivant.

Soit I = λx x (l’identité). Soit

t = (Δ)(I_{1})I_{2}

où l’on a indicé les deux occurrences de I pour les distinguer. Ce terme contient deux rédex. Selon que l’on réduit l’un ou l’autre on obtient :

t_{1} = ((I_{1})I_{2})(I_{1})I_{2} ou t_{2} = (Δ)I_{2}

Comme t_{2} n’a qu’un redex, il y a un unique t_{3} tel que t_{2} β_{0} t_{3}, à savoir :

t_{3} = (I_{2})I_{2}

Par contre t_{1} contient deux rédex, mais la réduction d’aucun de ces deux rédex ne permet (en une étape) d’obtenir t_{3} à partir de t_{1}. Donc la relation β_{0} n’est pas confluente.

Cet exemple explicite la raison pour laquelle β_{0} n’est pas confluente : le terme t contient deux rédex, et la réduction du rédex le plus extérieur (t lui-même) a pour effet de dupliquer l’autre rédex (le terme (I_{1})I_{2}). Du coup, il faut faire deux étapes de β_{0} pour passer de t_{1} à t_{3} et refermer le diagramme de confluence. Observer toutefois que, pour refermer ce diagramme, on ne réduit que des rédex qui étaient initialement présents dans t; le terme t_{3} est un rédex qui n’était pas initialement présent dans t, mais sa réduction n’est pas utile pour refermer le diagramme de confluence.

Création de redex. L’exemple illustre un autre phénomène très important en lambda-calcul, la création de redex. Comme I = λx x, le terme t_{3} contient un redex qui, comme on l’a déja dit, n’est pas initialement présent dans t, donc a été créé par la réduction. Le fait qu’une étape de réduction en général crée de nouveaux redex est la clef de la complexité calculatoire du lambda-calcul. C’est en particulier la raison pour laquelle il existe des termes non normalisables : par exemple si l’on fait une étape de réduction sur (Δ)Δ alors on crée un nouveau redex qui se trouve être le terme de départ. Pour se convaincre qu’il y a vraiment création de redex, indicer les deux occurrences de Δ, et faire la réduction.

Réduction parallèle. Nous allons montrer le théorème de Church-Rosser en définissant une relation ρ (appelé parfois réduction parallèle), qui contient β_{0}, est confluente, et dont la clôture transitive est β. L’idée est de supprimer la restriction de β_{0} (exactement un redex) qui est comme on vient de le voir, la raison pour laquelle β_{0} n’est pas confluente. Intuitivement on aura donc t ρ t′ si il existe un ensemble (possiblement vide) de redex de t tel que lorsqu’on les réduit tous (en parallèle), on obtient t′; ou encore si t se réduit en t′ sans qu’aucune des étapes de réductions ne choisisse un redex créé par les étapes précédentes.

On défini t ρ u pour tout u par récurrence sur la longueur de t :

— t ρ t pour tout t;

— (λx u)v ρ u′[v′/x] si u ρ u′ et v ρ b′;

— (u)v ρ (u′)v′ si u ρ u′ et v ρ b′;

— λx u ρ λx u′ si u ρ u′.

Lemme 2.1.7. La relation ρ est la plus petite relation qui passe au contexte et telle que si u ρ u′ et v ρ v′ alors (λx u)v ρ u′[v′/x].

La démonstration est immédiate.

Lemme 2.1.8.

β_{0} ⊆ ρ ⊆ β

Démonstration. Clairement ρ contient β_{0}. Et comme β est une (la plus petite en fait) relation transitive passant au contexte et vérifiant la condition de clôture de ρ, β contient ρ.

On en déduit le

Lemme 2.1.9. La clôture transitive de ρ est β.

Lemme 2.1.10. Soient t, t′, u, u′ ∈ Λ tels que t ρ t′ et u ρ u′, et soit x ∈ V. On a t[u/x] ρ t′[u′/x].

Démonstration. Par récurrence sur la taille de t.

Si t est une variable y, alors t′ = y et on conclut immédiatement, que y soit ou non égal à x.

Si t = (s)r et t′ = (s′)r′ avec s ρ s′ et r ρ r′, on a, par hypothèse de récurrence, s[u/x] ρ s′[u′/x] et r[u/x] ρ r′[u′/x], donc

(s[u/x])r[u/x] ρ (s′[u′/x])r′[u′/x]

c’est-à-dire (par définition de la substitution), t[u/x] ρ t′[u′/x].

Si t = (λy s)r et t′ = s′[r′/y], avec s ρ s′ et r ρ r′, observer d’abord qu’on peut supposer y ≠ x (quitte à renommer la variable liée y). Par hypothèse de récurrence, on a

s[u/x] ρ s′[u′/x] et r[u/x] ρ r′[u′/x]

et donc, par définition de ρ,

(λy s[u/x])r[u/x] ρ s′[u′/x][r′[u′/x]/y] ,

or par définition de la substitution (vu que y ≠ x, et qu’on peut supposer que y ∉ VL(u)), on a (λy s[u/x])r[u/x] = t[u/x], et par le lemme 2.1.1, on a

s′[r′/y][u′/x] = s′[u′/x, r′[u′/x]/y] ,

et comme on peut supposer que y ∉ VL(u′),

s′[u′/x, r′[u′/x]/y] = s′[u′/x][r′[u′/x]/y]

et on conclut que

(λy s[u/x])r[u/x] ρ s′[r′/y][u′/x] ,

ce qu’il fallait prouver.

Le cas où t = λy s et t′ = λy s′ (encore une fois, on peut supposer y ≠ x) est laissé au lecteur en exercice.

On conclut la preuve du théorème 2.1.4 au moyen du lemme suivant.

Lemme 2.1.11. La relation ρ est confluente sur Λ.

Démonstration. Soient t, t_{1}, t_{2} ∈ Λ tels que t ρ t_{1} et t ρ t_{2}. On prouve par induction sur la longueur de t qu’il existe u ∈ Λ tel que t_{i} ρ u pour i = 1, 2.

Si t = x ∈ V, alors t_{1} = t_{2} = x et on peut prendre u = x.

Si t = (u)v et t_{i} = (u_{i})v_{i} avec u ρ u_{i}, v ρ v_{i} alors par hypothèse de récurrence sur il existe des termes u′ et v′ tels que u_{i} ρ u′ et v_{i} ρ v′ pour i = 1, 2. Mais si on prend t′ = (u′)v′, comme ρ passe au contexte on voit que t_{i} ρ t′ pour i = 1, 2.

Si t = (λx u)v alors il y a deux cas à considérer :

— t_{1} = (λx u_{1})v_{1} et t_{2} = u_{2}[v_{2}/x] où u ρ u_{i} et v ρ v_{i} pour i = 1, 2. Par hypothése de récurrence on a alors u′ et v′ tels que u_{i} ρ u′ et v_{i} ρ v′ pour i = 1, 2. Par définition de ρ on a donc t_{1} ρ u′[v′/x] et par le lemme de substitution ci-dessus t_{2} ρ u′[v′/x], soit le résultat cherché avec t′ = u′[v′/x].

— t_{i} = u_{i}[v_{i}/x] où u ρ u_{i} et v ρ v_{i} pour i = 1, 2. On obtient à nouveau le résultat avec t′ = u′[v′/x] en appliquant deux fois le lemme de substitution.

Réduction de tête et réduction gauche

Le résultat suivant est une observation très simple, mais très importante, sur la forme générale d’un lambda-terme.

Lemme 2.1.12. Soit t ∈ Λ. Il existe une unique famille de variable x_{1}, …, x_{n} (avec n ≥ 0), une unique famille de termes u_{1}, …, u_{k} ∈ Λ (avec k ≥ 0), et un unique terme u ∈ Λ qui est soit une variable, soit un rédex, tels que

t = λx_{1} … x_{n} (u)u_{1} … u_{k} .

L’écriture du terme t fournie par ce résultat sera appelée écriture canonique de t.

Forme normale de tête, variable de tête. Avec les notations du lemme, si u est un rédex, on dit que c’est le rédex de tête de t. Si u est une variable, on dit que c’est la variable de tête de t, et que t est en forme normale de tête ou est une forme normale de tête.

Un terme en forme normale est évidemment aussi en forme normale de tête, mais la réciproque est fausse. Par exemple, le terme

λx (x)(Δ)Δ

est en forme normale de tête, mais il n’est pas en forme normale.

Réduction de tête. Soient t et t′ deux termes et λx⃗ (t_{0})t⃗ l’écriture canonique de t. On dit que t se réduit de tête en t′ en une étape, et on écrit t β_{0}^{t} t′ si t_{0} est un rédex (λx u)v et

t′ = λx⃗ (u[v/x])t⃗.

La réduction de tête est la clôture transitive de la réduction de tête en une étape. Elle sera notée β^{t}. Il est clair que β_{0}^{t} ⊆ β_{0} et que β^{t} ⊆ β (exercice : montrer par des contre-exemples que ces inclusions sont strictes).

Remarquer que dans un terme, il y a au plus un rédex de tête, donc contrairement à la β-réduction, la β-réduction de tête est une stratégie de réduction (à chaque étape, on n’a qu’une seule possibilité pour continuer).

Sur un terme en forme normale de tête, il est bien sûr impossible d’exécuter une réduction de tête.

Formes normales de tête et beta-équivalence. Observer qu’un terme peut avoir plusieurs formes normales de tête. Toutefois, si deux termes t et t′, tous deux en forme normale de tête, sont β-équivalents, disons :

t = λx_{1} … x_{n} (y)u_{1} … u_{k} et t′ = λx′_{1} … x′_{n′} (y′)u′_{1} … u′_{k′} ,

il faut qu’on ait n′ = n, k′ = k et (au renommage près des variables liées), x′_{1} = x_{1},…, x′_{n} = x_{n}, y′ = y et u′_{1} =_{β} u_{1},…u_{k} =_{β} u′_{k}, comme le montre le corollaire 2.1.6. En effet, les seules β-réductions que l’on peut effectuer sur t sont à l’intérieur des u_{i}, et elle ne peuvent pas affecter l’ossature de t (les λ extérieurs λx_{1} … x_{n}, la variable de tête et le nombre de ses arguments).

Normalisation de tête On dira qu’un terme t est normalisable de tête si sa réduction de tête termine, autrement dit s’il n’y a pas de suite infinie de terme t_{1}, t_{2}, … telle que t_{i} β_{0}^{t} t_{i+1} pour tout i. Dans ce cas, le dernier élément de la suite des réduits de tête de t est évidemment une forme normale de tête.

Voici un petit lemme utile sur la normalisabilité de tête.

Lemme 2.1.13. Soient t, u_{1},…, u_{n}, v_{1}, …, v_{m} des termes. Si (t[u⃗/x⃗])v⃗ est normalisable de tête alors t l’est.

Démonstration. Par récurrence sur la longueur de la réduction de tête de t′ = (t[u⃗/z⃗])v⃗. Si t′ est en forme normale de tête alors t l’est ; sinon on a

t = λy⃗. ((λy. t_{0})t_{1})w⃗

d’où

t′ = (λy⃗. ((λy. t_{0}[u⃗/x⃗])t_{1}[u⃗/x⃗])w⃗[u⃗/x⃗])v⃗

et t′ n’est clairement pas en forme normale de tête.

Si t′ n’est pas en forme normale de tête on raisonne par cas sur t. Si t est en forme normale de tête il n’y a rien à dire. Si t = (r)w⃗ où r est un redex alors t′ = (r[u⃗/x⃗])w⃗[u⃗/x⃗]v⃗ donc t′ β_{0}^{t} t′′ = (r′[u⃗/x⃗])w⃗[u⃗/x⃗]v⃗ où r′ est le contracté de r. Mais t β_{0}^{t} t′′′ = (r′)w⃗ et (t′′′[u⃗/x⃗])v⃗ = t′′; par récurrence sur la longueur de la réduction de tête de t′′ on a que la réduction de tête de t′′′ termine et donc celle de t puisque t′′′ est son réduit de tête à une étape.

Enfin si t = λx. t_{0} alors t′ = (λx. t_{0}[u⃗/x⃗])v⃗ donc t′ β_{0}^{t} t′′ = (t_{0}[u⃗/x⃗, v_{1}/x])v_{2} … v_{n}. Par récurrence sur la longueur de la réduction de tête de t′′ on a que la réduction de tête de t_{0} termine, et donc celle de t par définition de la réduction de tête.

Le théorème de normalisation de tête. Il s’agit de l’un des résultats de base de la théorie du lambda-calcul, au même titre que le théorème de Church-Rosser. On l’énonce ici mais on le démontrera en 2.3.

Théorème 2.1.14. Un terme est normalisable de tête si et seulement s’il est β-équivalent à un terme en forme normale de tête.

Autrement dit, la réduction de tête est une stratégie qui aboutit toujours à une forme normale de tête, dès lors qu’on l’applique à un terme β-équivalent à un terme en forme normale de tête.

Réduction gauche. Soient t et t′ deux termes. On dit que t se réduit à gauche en t′ en une étape, et on écrit t β_{0}^{g} t′ si, soit t a un redex de tête et t′ est obtenu par contraction d’ycelui, soit t = λx⃗. (x)t_{1} … t_{n} est en forme normale de tête et t′ = λx⃗. (x)t_{1} … t_{i−1}t′_{i}t_{i+1} … t_{n} où t′_{i} est un réduit gauche à une étape de t_{i} pour un i. Autrement dit la réduction gauche est l’extension de la réduction de tête aux arguments de la variable de tête. On note β^{g} la clôture transitive de β_{0}^{g}.

Remarquons que la réduction gauche, contrairement à la réduction de tête, n’est pas une stratégie car elle ne détermine pas un unique redex dans le cas où t n’est pas en forme normale de tête. On pourrait et c’est d’ailleurs souvent ainsi qu’elle est présentée dans la littérature, la déterminiser complètement en demandant que l’on ne réduit dans t_{i} que si t_{1},…, t_{i−1} sont normaux. On peut aussi considérer que les redex de chaque t_{i} sont indépendants et que la réduction gauche les réduit tous en parallèle.

La réduction gauche admet une propriété du même genre que la réduction de tête :

Théorème 2.1.15. Un terme est normalisable si et seulement si l’une des ses réductions gauche termine.

Remarque : Il est relativement facile de voir que si l’une des réductions gauche termine alors toutes terminent.

On ne démontrera pas ce théorème dans ces notes. Le lecteur pourra exercer sa compréhension de la méthode de réductibilité exposée en 2.3 en tâchant d’adapter la preuve du théorème précédent. Une autre méthode consiste à utiliser le théorème précédent et le fait que la réduction gauche est une itération de la réduction de tête.

2.2 Représentation des fonctions récursives

Entiers de Church. Soit n un entier. On note \underline{n} le lambda-terme

\underline{n} = λf. λx. \underbrace{(f) … (f)}_{n ×} x

Les lambda-termes de la forme \underline{n} sont appelés les entiers de Church. Remarquons qu’ils ont une interprétation fonctionnelle très simple : ce sont des itérateurs.

Représentation des fonctions. Soit F : ℕ^{k} → ℕ une fonction partielle. On dira que le lambda-terme \underline{F} représente F si pour tous entiers n_{1}, …, n_{k} on a :

— si F (n⃗)↑ alors le terme (\underline{F})\underline{n⃗} n’a pas de forme normale de tête ;

— si F (n⃗) = m alors (\underline{F})\underline{n⃗} =_{β} \underline{m}

Remarque : D’après le théorème 2.1.14, la première condition est équivalente à : si F (n⃗)↑ alors la réduction de tête de (\underline{F})\underline{n⃗} ne termine pas.

Fonctions de base sur les entiers. On a en particulier \underline{0} = λf. λx. x. On voit facilement que le terme

\underline{S} = λn. λf. λx. (f)((n)f)x

représente la fonction successeur au sens où (\underline{S})\underline{n} =_{β} \underline{n + 1}. De même les termes

Add = λn. λm. λf. λx. ((n)f)((m)f)x

et

Mult = λn. λm. λf. λx. ((n)(m)f)x

représente respectivement l’addition et la multiplication

Enfin le terme

Inf = λn. λm. ((((\underline{S})n)φ)λd. \underline{0})((m)φ)λd. \underline{1}

où φ = λf. λg. (g)f représente la fonction caractéristique de <.

Un terme de mise en mémoire. On note T le terme

T = λf. λn. (((n)λh. λx. (h)(\underline{S})x)f)\underline{0}

Lemme 2.2.1. Soit t et u deux termes.

— Si il existe un entier n tel que u =_{β} \underline{n} alors (T)tu =_{β} (t)\underline{n};

— Si u n’a pas de forme normale de tête alors (T)tu non plus.

Démonstration. Commençons à effectuer la réduction de tête de (T)tu. Pour alléger le calcul on note φ le terme λh. λx. (h)(\underline{S})x.

(T)tu β_{0}^{t} λn. (((n)φ)t)\underline{0}
β_{0}^{t} (((u)φ)t)\underline{0}

Si u n’a pas de forme normale de tête alors sa réduction de tête est infinie et, par le lemme 2.1.13, celle de (((u)φ)t)\underline{0} aussi. Par le théorème 2.1.14 on en déduit que (T)tu n’a pas de forme normale de tête.

Si u =_{β} \underline{n} alors on voit facilement qu’il existe des termes u′, u_{0}, u_{1}, …, u_{n} tels que :

u β^{t} λf. u′
u′ β^{t} λx. u_{0}
u_{0} β^{t} (f)u_{1}
⋮
u_{n−1} β^{t} (f)u_{n}
u_{n} β^{t} x

Alors la réduction de tête de (T)tu se continue ainsi :

(((u)φ)t)\underline{0} β^{t} (((λf. u′)φ)t)\underline{0}
β_{0}^{t} ((u′[φ/f])t)\underline{0}
β^{t} ((λx. u′_{0})t)\underline{0}
β_{0}^{t} (u′′_{0})\underline{0}
β^{t} ((φ)u′′_{1})\underline{0}
β_{0}^{t} (λx. (u′′_{1})(\underline{S})x)\underline{0}
β_{0}^{t} (u′′_{1})(\underline{S})\underline{0}
⋮
β^{t} (u′′_{n})(\underline{S}) … (\underline{S})\underline{0}
β^{t} (t)(\underline{S}) … (\underline{S})\underline{0}

où u′_{0} = u_{0}[φ/f] et u′′_{i} = u_{i}[φ/f, t/x]. Mais comme (\underline{S}) … (\underline{S})\underline{0} =_{β} \underline{n}, le dernier terme est clairement betaéquivalent à (t)\underline{n}, comme annoncé.

Remarque : Le terme T fait partie de la classe des termes de mise en mémoire. Ce sont des termes qui ont la propriété que l’on vient de voir, à savoir que pour tout n, il existe un terme θ_{n} (ici θ_{n} = (\underline{S}) … (\underline{S})\underline{0}) tel que (T)tu β^{t} (t)θ_{n} dès que u =_{β} \underline{n}. Le terme T applique donc t à u mais après avoir effectué la normalisation complète de u et donc calculé sa valeur θ_{n}. Si on pense que la réduction de tête est une stratégie paresseuse, selon la terminologie des langages fonctionnels, c’est à dire une stratégie qui ne calcule la valeur des arguments que lorsque c’est strictement nécessaire, alors le terme T permet de faire de l’appel par valeur, c’est à dire de calculer l’argument avant de le passer à la fonction.

Le schéma de composition. Soit F la fonction définie par :

F (a) = μx. (x = 0)

Clairement F est représentée par \underline{F} = λd. \underline{0}. Soit maintenant G donnée par

G(a) = μx. (x + 1 = 0)

Tout aussi clairement G est représentée par \underline{G} = λd. (Δ)Δ. Finalement soit H définie par

H(a) = F (G(a))

Alors par définition du schéma de composition, H est, comme G, la fonction nulle part définie. On voit donc que l’on ne peut pas représenter H par le terme h = λx. (\underline{F})(\underline{G})a. En effet pour tout n on a

(h)\underline{n} =_{β} \underline{0}

est donc normalisable, en contradiction avec la définition de représentation d’une fonction. Par contre, grâce au lemme de mise en mémoire, on voit que

\underline{H} = λa. ((T)\underline{F})(\underline{G})a

représente H correctement. On va maintenant généraliser un peu cette idée de manière à coder le schéma de composition complet en utilisant T.

Soient t, u_{1}, …, u_{n} des termes. On note ⟨t, u_{1}, …, u_{n}⟩ ou ⟨t, u⃗⟩ le terme défini par récurrence sur n :

⟨t, u_{1}⟩ = ((T)t)u_{1}
⟨t, u_{1}, …, u_{n+1}⟩ = ((T)⟨t, u_{1}, …, u_{n}⟩)u_{n+1}

On voit immédiatement par récurrence sur n que

— si l’un des u_{i} n’a pas de forme normale de tête alors (t)u⃗ non plus ;

— si il existe m_{1}, …, m_{n} tels que u_{i} = \underline{m}_{i} pour i = 1, …, n alors ⟨t, u⃗⟩ =_{β} (t)\underline{m}_{1}, …, \underline{m}_{n}. D’où l’on déduit le Lemme 2.2.2 (Composition). Soient F une fonction partielle d’arité n et G_{1}, …, G_{k} des fonctions partielles d’arité k telles qu’il existe des termes \underline{F}, \underline{G}_{1}, …, \underline{G}_{n} les représentant. Alors le terme

λx_{1}…. λx_{k}. ⟨\underline{F} , (\underline{G}_{1})a⃗, …, (\underline{G}_{n})a⃗⟩

représente la fonction composée F (G_{1}(a⃗), …, G_{n}(a⃗)).

Schéma de minimisation. On note Y le terme

Y = (λx. λf. (f)((x)x)f)λx. λf. (f)((x)x)f

Lemme 2.2.3 (Point fixe). Pour tout terme t on a

(Y)t β^{t} (t)(Y)t

Soit maintenant φ et U les termes

φ = λu. λn. (((f)n)λd. (u)(\underline{S})n)n
U = λf. ((Y)φ)\underline{0}

Lemme 2.2.4. Soit t un terme et n un entier tel que pour tout i < n, il existe m_{i} > 0 tel que (t)\underline{i} =_{β} \underline{m}_{i}. Alors on a

— si (t)\underline{n} n’a pas de forme normale de tête alors (U)t non plus ;

— si (t)\underline{n} =_{β} \underline{0} alors (U)t =_{β} \underline{n}.

Démonstration. On note φ′ le terme φ[t/f] et U_{n} le terme ((Y)φ′)(\underline{S}) … (\underline{S})\underline{0} où \underline{S} occure n fois. On a alors

(U)t β_{0}^{t} U_{0}
β^{t} ((φ′)(Y)φ′)\underline{0}
β^{t} (((t)\underline{0})λd. ((Y)φ′)(\underline{S})\underline{0})\underline{0} = (((t)\underline{0})λd. U_{1})\underline{0}
β ((\underline{m}_{0})λd. U_{1})\underline{0}
β^{t} U_{1}
⋮
β^{t} U_{n}
β (((t)\underline{n})λd. U_{n+1})\underline{n}

Si (t)\underline{n} n’a pas de forme normale de tête alors par le lemme 2.1.13 et le théorème 2.1.14, (U)t non plus. Si (t)\underline{n} =_{β} \underline{0} alors (U)t =_{β} ((\underline{0})λd. U_{n+1})\underline{n} β^{t} \underline{n} comme annoncé.

Avec ce dernier lemme on a achevé de démontrer le

Théorème 2.2.5. Si F est une fonction récursive alors il existe un terme \underline{F} qui représente F.

Récursion primitive. Puisque le lambda-calcul représente les fonctions récursives, d’après le théorème 1.2.2 il représente également les fonctions primitive récursives. On va donner une preuve directe de ce fait.

Si u_{1} et u_{2} sont des termes on note ⟨u_{1}, u_{2}⟩ le terme

⟨u_{1}, u_{2}⟩ = λx. (x)u_{1}u_{2}

Si c est un terme et i = 1 ou 2, on note π_{i}c le terme

π_{i}c = (c)λx._{1}λx._{2}x_{i}

On vérifie immédiatement que l’on a

π_{i}⟨u_{1}, u_{2}⟩ β^{t} u_{i}

On note φ et R les termes

φ = λc. ⟨(\underline{S})π_{1}c, ((f)π_{1}c)π_{2}c⟩
R = λf. λb. λn. π_{2}((n)φ)⟨\underline{0}, b⟩

Lemme 2.2.6. Pour tous termes t et u on a :

(R)tu\underline{0} =_{β} u
(R)tu \underline{n + 1} =_{β} ((t)\underline{n})(R)tu \underline{n}

pour tout entier n.

La preuve est laissé en exercice au lecteur. Soient maintenant G une fonction d’arité k et H une fonction d’arité k + 2 représentées respectivement par les termes \underline{G} et \underline{H}. On vérifie facilement que si on définit

φ = λa. λv. (\underline{H})vaa⃗
ψ = (\underline{G})a⃗
\underline{F} = λa. λa⃗. (((R)φ)ψ)a

alors le terme \underline{F} représente la fonction F définie par récursion primitive à partir de G et H.

2.3 Le modèle de Engeler

Le modèle E(A) de Engeler est un cas particulier de domaine de Scott tel qu’il existe deux fonctions :

E(A) \overrightarrow{⟵}_{ψ}^{ϕ} E(A) → E(A)

vérifiant ϕ ∘ ψ = Id. Toutefois nous allons en donner ici une présentation plus concrète que nous utiliserons ensuite pour démontrer le théorème 2.1.14 selon la méthode classique de réductibilité.

Fonctions continues

Notations et conventions. Soit X un ensemble. On note P(X) l’ensemble des parties de X. On utilisera a, b et c pour dénoter les éléments de X, x et y pour dénoter les parties de X (les éléments de P(X)) et A, B pour dénoter les parties de P(X) (les ensembles de parties de X). Si A est un ensemble de parties de X on note ⋃ A la réunion des éléments de A. Si f est une fonction de I → P(X), on note ⋃_{i∈I} f(i) la réunion des f(i).

Familles filtrantes. Soit A un ensemble d’ensembles. On note ⋃ A ou ⋃_{x∈A} x la réunion des éléments de A. On dira que A est filtrant si A est non vide et pour tous x_{1}, x_{2} dans A, il existe un y tel que x_{i} ⊂ y pour i = 1, 2. L’exemple typique de famille filtrante est l’ensemble des parties finies d’un ensemble X, que l’on notera P_{fin}(X). Si x est un ensemble, on écrira x_{0} ⊂_{fin} x pour « x_{0} est une partie finie de x ».

Fonctions continues. Soient X et Y deux ensembles. Une fonction F : P(X) → P(Y) est dite continue si elle est croissante (pour l’inclusion) et pour tout ensemble filtrant A ⊂ P(X) on a :

F (⋃ A) = ⋃_{x∈A} F (x)

Remarque : L’une des inclusions est réalisée dès que F est croissante, à savoir ⋃_{x∈A} F (x) ⊂ F (⋃ A).

Lemme 2.3.1 (Finitude). Soit F : P(X) → P(Y) une fonction croissante. Alors F est continue ssi pour tout b ∈ Y et tout x ⊂ X on a la condition de finitude :

si b ∈ F (x) alors ∃x_{0} ⊂_{fin} x tel que b ∈ F (x_{0})

Cette condition exprime une propriété fondamentale des programmes : pour pouvoir donner un résultat fini, même partiel, tel le b qui appartient à F (x), la fonction F qui représente un programme n’a besoin que d’utiliser un nombre fini d’informations sur son entrée. Clairement un programme qui utiliserait x en entier pour pouvoir répondre que b est un élément du résultat, calculerait en temps infini dès que x l’est. C’est l’un des buts de la sémantique dénotationnelle que de trouver des propriétés abstraites des programmes, telles que la condition de finitude, qui permettent de définir des classes de fonctions représentant les programmes.

Démonstration. Supposons pour commencer que F est continue et soit b ∈ F (x). On considère la famille P_{fin}(x) qui est filtrante ; comme x = ⋃ P_{fin}(x) on a par continuité de F

F (x) = ⋃_{x_{0}∈P_{fin}(x)} F (x_{0})

Comme b ∈ F (x) on voit qu’il y a un x_{0} ⊂_{fin} x tel que b ∈ F (x_{0}).

Réciproquement supposons que F est croissante et vérifie la condition de finitude. Soit A un ensemble filtrant inclus dans P(X). On sait déja, par croissance de F que ⋃_{x∈A} F (x) ⊂ F (⋃ A). Soit b ∈ F (⋃ A). Par condition de finitude, on sait qu’il existe un x_{0} ⊂_{fin} ⋃ A tel que b ∈ F (x_{0}) ; notons a_{1}, …, a_{n} les éléments de x_{0}. Comme les a_{i} sont des éléments de ⋃ A, il existe x_{1}, …, x_{n} appartenant à A tels que a ∈ x_{i} pour i = 1, …, n. Mais comme A est filtrant, on voit facilement (par récurrence sur n) qu’il existe un x appartenant à A et tel que x_{i} ⊂ x pour i = 1, …, n. Donc x_{0} ⊂ x et par croissance de F on obtient b ∈ F (x) ⊂ ⋃_{x∈A} F (x).

Trace d’une fonction continue. Soit F une fonction continue de P(X) dans P(Y). On appelle trace de F et on note Tr F l’ensemble inclus dans P_{fin}(X) × Y des couples :

Tr F = {(x_{0}, b), x_{0} ⊂_{fin} X et b ∈ F (x_{0})}

Le lemme de finitude nous assure que Tr F contient toute l’information nécessaire pour calculer F (x). Plus précisément, si f est une partie de P_{fin}(X) × Y, notons Fun f la fonction de P(X) → P(Y) définie par :

Fun f(x) = {b ∈ Y, ∃x_{0} ⊂_{fin} x tel que (x_{0}, b) ∈ f}

Alors on a

Lemme 2.3.2. La fonction Fun f est continue de P(X) dans P(Y). Réciproquement, si F est une fonction continue de P(X) dans P(Y) alors

Fun Tr F = F

Tout le propos de la théorie des domaines est de généraliser les définitions ci-dessus de façon à les appliquer à une classe d’ordre plus générale que les simples P(X) que l’on considère ici. On parvient alors à munir l’ensemble des fonctions continues d’une structure de domaine et on obtient que les fonctions Tr et Fun sont elles même continues. Mais c’est une autre histoire…

Fonctions à plusieurs variables. Soient X_{1}, …, X_{n} et Y des ensembles. Une fonction F : P(X_{1})×⋯×P(X_{n}) → P(Y) est continue si elle l’est séparément sur chacun de ses paramètres. Cette définition est cohérente avec la remarque que P(X_{1})×⋯×P(X_{n}) est isomorphe à P(X_{1} +⋯+X_{n}) (où X_{1} +X_{2} représente l’union disjointe de X_{1} et X_{2}).

Soit maintenant F : P(X_{1}) × ⋯ × P(X_{n+1}) → P(Y) une fonction continue. On note Tr_{n} F la fonction de P(X_{1}) × ⋯ × P(X_{n}) → P(P_{fin}(X_{n+1}) × Y) définie par :

Tr_{n} F (x_{1}, …, x_{n}) = Tr F_{x_{1},...,x_{n}}

où F_{x_{1},...,x_{n}} : P(X_{n+1}) → P(Y) est la fonction : F_{x_{1},...,x_{n}}(x) = F (x_{1}, …, x_{n}, x) (Exercice : montrer que Tr_{n} F est continue).

Réciproquement si F : P(X_{1}) × ⋯ × P(X_{n}) → P(P_{fin}(X_{n+1}) × Y) est continue, on note Fun_{n} F : P(X_{1}) × ⋯ × P(X_{n+1}) → P(Y) la fonction définie par :

Fun_{n} F (x_{1}, …, x_{n+1}) = Fun(F (x_{1}, …, x_{n}))(x_{n+1})

(Exercice : montrer que Fun_{n} F est continue). Comme pour le lemme 2.3.2 on a pour F : P(X_{1}) × ⋯ × P(X_{n+1}) → P(Y)

Fun_{n} Tr_{n} F = F

Modèle de Engeler

Construction du modèle. Soit A un ensemble dénombrables dont les éléments seront appelés les atomes. On se donne une suite d’ensembles (D_{n}) définie par récurrence par :

D_{0} = A
D_{n+1} = D_{n} ∪ {(x_{0}, a), x_{0} ⊂_{fin} D_{n} et a ∈ D_{n}}

On note D(A) la réunion de tous les D_{n}. Par construction D(A) est le plus petit ensemble D tel que A ⊂ D et P_{fin}(D) × D ⊂ D.

On note E(A) l’ensemble P(D(A)). Si F : E(A) → E(A) est continue alors comme Tr F ⊂ P_{fin}(D(A)) × D(A) on a Tr F ∈ E(A). Réciproquement si f ∈ E(A) on écrira Fun f pour Fun(f/A) qui est donc une fonction continue de E(A) → E(A). Comme Fun Tr F = F pour toute fonction continue F sur D(A) on voit que, en notant D(A) → D(A) l’espace des fonctions continues sur D(A), on a :

E(A) \overrightarrow{⟵}_{Tr}^{Fun} E(A) → E(A)

si bien que Fun et Tr réalisent le programme annoncé dans l’introduction (p. 32).

Interprétation des termes. Dans toute cette partie, afin d’éviter les confusions on n’utilisera que la lettre z pour dénoter les variables du lambda-calcul. Soient ℓ = (z_{1}, …, z_{n}) une suite finie de variables et t un terme dont les variables libres sont parmi les éléments de ℓ. On va associer à t une fonction continue ⟦t⟧_{ℓ} : E(A) × ⋯ × E(A) → E(A) d’arité n définie par récurrence sur t :

— si t = z_{i} alors ⟦t⟧_{ℓ}(x⃗) = x_{i};

— si t = (u)v alors ⟦t⟧_{ℓ}(x⃗) = Fun_{n}⟦u⟧_{ℓ}(x⃗, ⟦v⟧_{ℓ}(x⃗)) ;

— si t = λz. u alors ⟦t⟧_{ℓ}(x⃗) = Tr_{n}⟦u⟧_{ℓ.z}(x⃗) où ℓ.z est la suite (z_{1}, …, z_{n}, z).

Le modèle de Engeler vu comme système de typage. Si on applique les définitions de Fun et Tr on a que — si t = (u)v alors ⟦t⟧_{ℓ}(x⃗) = {a, ∃x_{0} ⊂_{fin} ⟦v⟧_{ℓ}(x⃗) tel que (x_{0}, a) ∈ ⟦u⟧_{ℓ}(x⃗)}.

— si t = λz. u alors ⟦t⟧_{ℓ}(x⃗) = {(x_{0}, a), x_{0} ⊂_{fin} D(A) et a ∈ ⟦u⟧_{ℓ.z}(x⃗, x_{0})}

Notons z_{1} : x_{1}, …, z_{n} : x_{n} ⊢ t : a le fait que a ∈ ⟦t⟧_{ℓ}(x⃗) et notons x_{0} → a le couple (x_{0}, a). Alors les clauses ci-dessus deviennent :

— z⃗ : x⃗ ⊢ z_{i} : a_{i} si a_{i} ∈ x_{i};

— z⃗ : x⃗ ⊢ (u)v : a si il existe x_{0} fini tel que pour tout b dans x_{0} on ait z⃗ : x⃗ ⊢ v : b et tel que z⃗ : x⃗ ⊢ u : x_{0} → a;

— z⃗ : x⃗ ⊢ t : x_{0} → a si z⃗ : x⃗, z : x_{0} ⊢ u : a.

En fait cette façon de représenter le modèle de Engeler comme système de typage existe sous le nom de types avec intersections ou système D (voir [3]).

Théorème 2.3.3 (Correction du modèle de Engeler). L’interprétation ⟦t⟧_{ℓ} est dénotationnelle c’est à dire que si t et t′ sont deux termes et ℓ est une suite de variables contenant toutes les variables libres de t et t′ alors

si t =_{β} t′ alors ⟦t⟧_{ℓ} = ⟦t′⟧_{ℓ}

Démonstration. Il suffit de démontrer le théorème dans le cas où t β_{0} t′. On raisonne par récurrence sur t. On suppose que ℓ = (z_{1}, …, z_{n}) contient toutes les variables libres de t. Les cas t = z_{i}, t = (u)v et t′ = (u′)v, t = (u)v et t′ = (u)v′, t = λz. u et t′ = λz. u′ sont immédiats par hypothèse de récurrence. Ce qui nous amène au seul cas intéressant : t = (λz. u)v et t′ = u[v/z]. Il résulte du lemme suivant Lemme 2.3.4 (Substitution). Pour tous termes u et v et toute suite ℓ = (z_{1}, …, z_{n}) contenant toutes les variables libres de t et u distinctes de z on a

⟦u[v/z]⟧_{ℓ}(x⃗) = ⟦u⟧_{ℓ.z}(x⃗, ⟦v⟧_{ℓ}(x⃗))

Supposons le lemme de substitution démontré. On a

⟦t⟧_{ℓ}(x⃗) = Fun_{n} Tr_{n}⟦u⟧_{ℓ.z}(x⃗, ⟦v⟧_{ℓ}(x⃗)) par définition de l’interprétation
= ⟦u⟧_{ℓ.z}(x⃗, ⟦v⟧_{ℓ}(x⃗))  par le lemme 2.3.2
= ⟦u[v/z]⟧_{ℓ}(x⃗)  par le lemme de substitution
= ⟦t′⟧_{ℓ}(x⃗)

On démontre le lemme de substitution par… récurrence sur u. Si u = z_{i} alors u[v/z] = u et le résultat est immédiat. Si u = z alors u[v/z] = v; par définition ⟦u⟧_{ℓ.z}(x⃗, x) = x d’où l’on déduit le résultat en prenant x = ⟦v⟧_{ℓ}(x⃗).

Si u = (u_{1})u_{2} alors u[v/z] = (u_{1}[v/z])u_{2}[v/z] et l’on a

⟦u[v/z]⟧_{ℓ}(x⃗) = Fun_{n}⟦u_{1}[v/z]⟧_{ℓ}(x⃗, ⟦u_{2}[v/z]⟧_{ℓ}(x⃗))  par définition de l’interprétation
= Fun(⟦u_{1}[v/z]⟧_{ℓ}(x⃗))(⟦u_{2}[v/z]⟧_{ℓ}(x⃗))  par définition de Fun_{n}
= Fun(⟦u_{1}⟧_{ℓ.z}(x⃗, ⟦v⟧_{ℓ}(x⃗)))(⟦u_{2}⟧_{ℓ.z}(x⃗, ⟦v⟧_{ℓ}(x⃗))) par récurrence sur u_{1} et u_{2}
= Fun_{n+1}⟦u_{1}⟧_{ℓ.z}(x⃗, ⟦v⟧_{ℓ}(x⃗), ⟦u_{2}⟧_{ℓ.z}(x⃗, ⟦v⟧_{ℓ}(x⃗))) par définition de Fun_{n+1}
= ⟦u⟧_{ℓ.z}(x⃗, ⟦v⟧_{ℓ}(x⃗))  par définition de l’interprétation

Si u = λz. u_{0} alors u[v/z] = u et le résultat est immédiat. Si u = λz_{n+1}. u_{0} où z_{n+1} ≠ z et z_{n+1} n’apparaît pas dans v (ce que l’on peut toujours supposer à α-conversion près) alors u[v/z] = λz_{n+1}. u_{0}[v/z] et le résultat vient par un raisonnement analogue au cas de l’application.

Une application du modèle de Engeler

On va maintenant utiliser le résultat précédent pour démontrer le théorème de réduction de tête 2.1.14. Pour ce faire on va associer à chaque élément a de E(A) un ensemble |a| de lambda-termes inclus dans l’ensemble des lambda-termes dont la réduction de tête termine. Puis on démontrera le lemme d’appartenance qui stipule que si a ∈ ⟦t⟧_{ℓ} alors t ∈ |a|. On conclut en montrant que si t est en forme normale de tête alors ⟦t⟧_{ℓ} est non vide. Donc si t =_{β} t_{0} et t_{0} est en forme normale de tête alors par le théorème de correction du modèle de Engeler on a que ⟦t⟧_{ℓ} est non vide donc par le lemme d’appartenance que sa réduction de tête termine.

Réalisabilité. Soit X et Y deux ensembles de lambda-termes. On note X → Y l’ensemble

X → Y = {u tel que ∀v ∈ X, (u)v ∈ Y }

Remarquons que dans le cas particulier où X est vide, alors X → Y = Λ, l’ensemble de tous les lambda-termes (à α-conversion près).

Saturation. On dit qu’une partie X de Λ est saturée si pour tous u, v, v_{1}, …, v_{n} on a

si (u[v/z])v⃗ ∈ X alors (λz. u)vv⃗ ∈ X

Lemme 2.3.5. Soient X et Y deux parties de Λ. Si Y est saturée alors X → Y est saturée. Si de plus X est saturée alors X ∩ Y est saturée.

Démonstration. Supposons que (u[v/z])v⃗ est un élément de X → Y et soit w ∈ X. Par définition de X → Y on a (u[v/z])v⃗w ∈ Y et comme Y est saturée, (λz. u)vv⃗w ∈ Y. Comme w est quelconque on vient de montrer que (λz. u)vv⃗ appartient à X → Y.

Le cas de l’intersection est immédiat.

Termes normalisables de têtes. On note N l’ensemble des termes dont la réduction de tête termine et N_{0} l’ensemble des termes de la forme (z)v⃗ où z est une variable et v_{1}, …, v_{n} des termes quelconques. En particulier N_{0} contient toutes les variables.

Lemme 2.3.6. Soient X et Y deux parties de Λ.

— si N_{0} ⊂ Y alors N_{0} ⊂ X → Y ;

— si N_{0} ⊂ X et Y ⊂ N alors X → Y ⊂ N :

— si X et Y contiennent N_{0} et/ou sont contenues dans N alors il en de même de X ∩ Y.

En particulier, et c’est sous cette forme que l’on utilisera le lemme, si X et Y contiennent tous deux N_{0} et sont tous deux contenus dans N alors il en de même de X ∩ Y et X → Y.

Démonstration. Le cas de l’intersection est immédiat. Supposons que N_{0} ⊂ Y et soit u = (z)v⃗ une élément de N_{0} et v un élément de X. Alors (u)v = (z)v⃗v ∈ N_{0} dont (u)v ∈ Y. Comme v est un élément quelconque de X on vient de montrer que u ∈ X → Y, donc que N_{0} ⊂ X → Y.

Supposons maintenant que N_{0} ⊂ X et Y ⊂ N et soit u ∈ X → Y. Prenons un v dans X; alors (u)v ∈ Y et comme Y ⊂ N la réduction de tête de (u)v termine. Par le lemme 2.1.13 on a que la réduction de tête de u termine, c’est à dire que u ∈ N.

Interprétation par réalisabilité. On va maintenant associer à chaque point de D(A) une partie saturée contenant N_{0} et contenue dans N. L’intuition est que les points de D(A) sont des types (un point de la forme (x_{0}, a) représente le type x_{0} → a), c’est à dire des spécifications formelles de programmes, et que l’on associe à un point l’ensemble des termes qui réalisent ce type, c’est à dire qui respectent la spécification.

On appelle valuation une fonction ρ : A → P(Λ) qui associe à tout atome α un ensemble ρ(α) saturé, contenant N_{0} et contenu dans N. Étant donnée une valuation ρ, on définit l’ensemble |a|_{ρ} des réalisateurs d’un élément a de D(A) par récurrence sur a (ou plus précisément par récurrence sur le plus petit n tel que a ∈ D_{n}) :

— si a ∈ A alors |a|_{ρ} = ρ(a) ;

— si a = (x_{0}, b) alors

|a|_{ρ} = |x_{0}|_{ρ} → |b|_{ρ}

où |x_{0}|_{ρ} est ⋂_{c∈x_{0}} |c|_{ρ}. En particulier si x_{0} est vide alors |x_{0}|_{ρ} est Λ. Grâce aux lemmes 2.3.5 et 2.3.6 on a bien que pour tout a ∈ D(A) et toute valuation ρ, |a|_{ρ} est une partie

de Λ saturée contenant N_{0} et contenue dans N.

Le lemme d’appartenance. C’est le lemme fondamental de toute interprétation par réalisabilité. On le retrouve dans la preuve de forte normalisation du système F mais aussi dans d’autres contexte comme la définition du collapse extensionnel d’un modèle dénotationnel…

Lemme 2.3.7 (Appartenance). Soient t un terme dont toutes les variables libres appartiennent à la liste ℓ = (z_{1}, …, z_{n}), x_{1}, …, x_{n} des éléments de E(A) (des parties de D(A)) et ρ une valuation. Alors pour tout a ∈ D(A) et tous termes u_{1}, …, u_{n} on a

si \begin{cases}a ∈ ⟦t⟧_{ℓ}(x⃗) et \\ u_{i} ∈ |x_{i}|_{ρ} pour i = 1, …, n \end{cases} alors t[u⃗/z⃗] ∈ |a|_{ρ}

où |x_{i}|_{ρ} est ⋂_{b∈x_{i}} |b|_{ρ}.

Démonstration. Le lemme d’appartenance se démontre par récurrence sur t. Si t = z_{i} alors ⟦t⟧_{ℓ}(x⃗) = x_{i}, donc a ∈ x_{i} et |x_{i}|_{ρ} ⊂ |a|_{ρ}. Comme u_{i} ∈ |x_{i}|_{ρ} on a u_{i} ∈ |a|_{ρ}. Mais u_{i} = t[u⃗/z⃗] puisque t = z_{i}.

Si t = (u)v alors ⟦t⟧_{ℓ}(x⃗) = Fun_{n}⟦u⟧_{ℓ}(x⃗, ⟦v⟧_{ℓ}(x⃗)), et a ∈ ⟦t⟧_{ℓ}(x⃗) entraîne qu’il existe un x_{0} ⊂_{fin} ⟦v⟧_{ℓ}(x⃗) tel que (x_{0}, a) ∈ ⟦u⟧_{ℓ}(x⃗). Par hypothèse de récurrence on a donc u[u⃗/z⃗] ∈ |(x_{0}, a)|_{ρ} = |x_{0}|_{ρ} → |a|_{ρ}. Mais, comme x_{0} ⊂ ⟦v⟧_{ℓ}(x⃗), par récurrence sur v on a v[u⃗/z⃗] ∈ |x_{0}|_{ρ} = ⋂_{b∈x_{0}} |b|_{ρ}. Par définition de → on a donc que (u[u⃗/z⃗])v[u⃗/z⃗] = t[u⃗/z⃗] ∈ |a|_{ρ}.

Si t = λz. v alors ⟦t⟧_{ℓ}(x⃗) = Tr_{n}⟦v⟧_{ℓ.z}(x⃗) et a ∈ ⟦t⟧_{ℓ}(x⃗) entraîne que a est de la forme (x_{0}, b) où b ∈ ⟦v⟧_{ℓ.z}(x⃗, x_{0}). Par hypothèse de récurrence, pour tout u ∈ |x_{0}|_{ρ} on a v[u⃗/z⃗, u/z] ∈ |b|_{ρ}; mais par saturation de |b|_{ρ} ceci entraîne que (λz. v[u⃗/z⃗])u ∈ |b|_{ρ} pour tout u ∈ |x_{0}|_{ρ}. Donc λz. v[u⃗/z⃗] = t[u⃗/z⃗] ∈ |x_{0}|_{ρ} → |b|_{ρ} = |a|_{ρ}.

Corollaire 2.3.8. Soient x_{1}, …, x_{n} dans E(A). Si ⟦t⟧_{ℓ}(x⃗) est non vide alors la réduction de tête de t termine.

Démonstration. Comme N_{0} contient toutes les variables et est contenu dans tous les |x_{i}|_{ρ}, on a z_{i} ∈ |x_{i}|_{ρ} pour i = 1, …, n, donc par le lemme d’appartenance t[z⃗/z⃗] = t ∈ |a|_{ρ}. Mais |a|_{ρ} ⊂ N, donc par définition de N la réduction de tête de t termine.

On termine la preuve du théorème 2.1.14 en montrant le lemme suivant :

Lemme 2.3.9. Si t est beta-équivalent à une forme nomale de tête t_{0} alors pour toute liste ℓ = (z_{1}, …, z_{n}) contenant les variables libres de t et de t_{0}, il existe x_{1}, …, x_{n} dans E(A) tels que ⟦t⟧_{ℓ}(x⃗) est non vide.

Le théorème se déduit alors du corollaire au lemme d’appartenance.

Démonstration. En vertu du théorème de correction du modèle de Engeler, l’interprétation de t est égale à celle de la forme normale de tête t_{0}. Donc il suffit de montrer le lemme dans le cas où t est en forme normale de tête.

Soit a ∈ D(A). On définit a^{m} par récurrence sur m : a^{0} = a et a^{m+1} = (∅, a^{m}). Autrement dit, en utilisant l’analogie avec les types :

a^{m} = \underbrace{∅ → ⋯ → ∅}_{m ×} → a

Si t est en forme normale de tête alors on a soit t = (z_{i})u_{1} … u_{m}, soit t = λz. u où u est en forme normale de tête. Dans le premier cas, par définition de l’interprétation on a :

⟦t⟧_{ℓ}(x⃗) = {a, ∃y_{1} ⊂_{fin} ⟦u_{1}⟧(x⃗), …, ∃y_{m} ⊂_{fin} ⟦u_{m}⟧(x⃗), (y_{m}, …, (y_{1}, a) …) ∈ x_{i}}

Si on choisit x_{i} tel que a^{m} ∈ x_{i}, comme y_{j} = ∅ ⊂_{fin} ⟦u_{j}⟧(x⃗) pour tout x⃗ et tout j on a a ∈ ⟦t⟧_{ℓ}(x⃗) et donc ⟦t⟧_{ℓ}(x⃗) est non vide.

Si maintenant t = λz. u alors

⟦t⟧_{ℓ}(x⃗) = {(x_{0}, a) ∈ P_{fin}(D(A)) × D(A), a ∈ ⟦u⟧_{ℓ.z}(x⃗, x_{0})}

Par récurrence sur u il existe x⃗ et x_{0} tel que ⟦u⟧_{ℓ.z}(x⃗, x_{0}) est non vide d’où l’on déduit immédiatement que ⟦t⟧_{ℓ}(x⃗) est non vide.

38  Lambda-calcul

Bibliographie

[1] René Cori and Daniel Lascar. Logique mathématique. Axiomes. Masson, 1993.

[2] Jean-Yves Girard. Proof Theory and Logical Complexity. Bibliopolis, edizioni di filosofia e scienze, Napoli (Italy), 1987.

[3] Jean-Louis Krivine. Lambda-Calcul : Types et Modèles. Études et Recherches en Informatique. Masson, 1990.

[4] Joseph R. Shoenfield. Mathematical Logic. Addison Wesley, 1967.