Cours Preuves et Types

Description

Notes de cours « Preuves et Types», DEAMDFI Version préliminaire 27 janvier2006 2Table des matières1 Théorèmes de Gödel 51.1 Lelangage de l’arithmétique. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51.2 Fonctions (primitive)récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . 6Fonctions récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7Définissabilité desfonctionsrécursives . . . . . . . . . . . . . . . . . . . . . . . 8Fonctions primitivesrécursives . . . . . . . . . . . . . . . . . . . . . . . . . . . 8Programmationdefonctionsprimitivesrécursives.. . . . . . . . . . . . . . . . 101.3 CodagedeGödel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13Codageduformalisme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13Fonctions etprédicatsmanipulantleformalisme . . . . . . . . . . . . . . . . . 15Résultatsélémentairessurlesfonctionsrécursives . . . . . . . . . . . . . . . . 181.4 Leprédicatdeprouvabilité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21L’arithmétiqueélémentaire. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221.5 Théorèmesd’indécidabilitéetd’incomplètude . . . . . . . . . . . . . . . . . . 251.6 LesecondthéorèmedeGödel . . . . . . . . . . . . . . . . . . . . . . . . . . . . 262 Lambda-calcul 292.1 Lelambda-calculpur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29Généralitéssurlesrelations . . . . . . . . . . . . . . . . . ...

Informations

• Publié par: Aprea
• Nombre de lectures: 31
• Langue: Français

Extrait

Notes

de

cours

«

Preuves et Types Version préliminaire

27

janvier

2006

»,

DEA

MDFI

2

Table des matières

1 Théorèmes de Gödel 1.1 Le langage de l’arithmétique. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Fonctions (primitive) récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . Fonctions récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Définissabilité des fonctions récursives . . . . . . . . . . . . . . . . . . . . . . . Fonctions primitives récursives . . . . . . . . . . . . . . . . . . . . . . . . . . . Programmation de fonctions primitives récursives. . . . . . . . . . . . . . . . . 1.3 Codage de Gödel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Codage du formalisme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Fonctions et prédicats manipulant le formalisme . . . . . . . . . . . . . . . . . Résultats élémentaires sur les fonctions récursives . . . . . . . . . . . . . . . . 1.4 Le prédicat de prouvabilité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . L’arithmétique élémentaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.5 Théorèmes d’indécidabilité et d’incomplètude . . . . . . . . . . . . . . . . . . 1.6 Le second théorème de Gödel . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Lambda-calcul 2.1 Le lambda-calcul pur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Généralités sur les relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Laβ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .-réduction . Le théorème de Church-Rosser . . . . . . . . . . . . . . . . . . . . . . . . . . . Réduction de tête et réduction gauche . . . . . . . . . . . . . . . . . . . . . . . 2.2 Représentation des fonctions récursives . . . . . . . . . . . . . . . . . . . . . . 2.3 Le modèle de Engeler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Fonctions continues . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Modèle de Engeler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Une application du modèle de Engeler . . . . . . . . . . . . . . . . . . . . . . .

3

5 5 6 7 8 8 10 13 13 15 18 21 22 25 26 29 29 31 32 33 36 38 42 42 44 46

4

TABLE

DES

MATIÈRES

EHCPATI porterauShoenfielpruorraasuiseserepoln.laleLeeuctsli t gtiussordomo Girarede]donrd[2ahipeicrluvirtdetienss’eemprleeldorper ER lruoptiu d[4]pour

C é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 0 (symbole de constante,i.e., fonction d’arité 0),S(symbole de fonction unaire),+et ;(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 notationpolonaise préfixéeà dire que la formule qui exprime que(c’est xest égale àys’é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 formulesAetBsontlogiquement équiva- lentessi le séquent⊢A↔Best prouvable dansLK(le calcul des séquents). On dira qu’une formuleAde l’arithmétique est vraie, ou simplement que l’on aAsiAest vraie dans les entiers. En particulier on dira que deux énoncésAetBtraitant des entiers sont équivalents s’ils sont équivalents dans les entiers. FormulesD,SetP.Les formulesDsont définies par récurrence : – les formules atomiques sontD; – siAetBsontDalors¬A,A∧B,A∨BsontD; – siAestDet sitest un terme ne contenant pasxalors∀x(x<t→A) (que l’on notera ∀x<tA) et∃x(x<t∧A) (que l’on notera∃x<tA) sontD. R EMARQUE : Les quantificateurs∀x<tet∃x<tsont appelésquantificateurs bornés. Une formuleDest donc une formule dans laquelle tous les quantificateurs sont bornés. Les formulesSsont données par : – les formules atomiques et leurs négations sontS; – siAetBsontSalorsA∧BetA∨BsontS; – siAestSet sitest un terme ne contenant pasxalors∀x<tAestS; – siAestSalors∃xAestS. Une formulePest la négation d’une formuleS. R EMARQUE : L’ensemble des formulesDest inclus dans l’ensemble des formulesS. L’inclu- sion est bien entendu stricte, mais il y a tout de même une « réciproque » au sens du lemme suivant.

Chapitre 1

Théorèmes de Gödel

5

6

ThéorèmesdeGödel

Lemme 1.1.1SiAestSalors il existe une formuleA 0 qui estDet telle queAest équivalente à∃xA 0 . Ce lemme très utile, sera souvent utilisé sans référence dans la suite. Preuve :On choisit une variablexqui n’apparait pas dansA(ni libre, ni liée) et on remplace chaque quantificateur non borné∃ydeApar∃y<x. On obtient ainsi une formuleA 0 qui estDet on voit facilement queAest équivalente à∃x A 0 . Notations diverses.SoitAune formule. On écriraA[x 1     x k ] (ouA[x~]) pour dire quex 1 , . . .,x k sont des variables libres deAet dans ce cas on écriraA[t 1     t k ] (ouA[t ~ ]) pour désigner la formuleAdans laquelle chaque variablex i est remplacée par le termet i ,i.e., A[t ~ ]=A[t 1 x 1     t k x k ]. A ce propos on rappelle que la notationA[t 1 x 1     t n x n ] dé- signe la substitutionsans capture de variable. On se reportera au premier chapitre du Kri- vine [3] pour une définition rigoureuse d’ycelle. Soitaun entier, on noteale terme définie par récurrence par : – sia=0 alorsaest 0 ; – sia=b+1 alorsaestS b. Soittun terme clos. On note|t|lavaleurdetdéfinie par récurrence par : – sitest 0 alors|t|=0 ; – sitestS ualors|t|=|u|+1 ; – sitestu+valors|t|=|u|+|v|; sitestuvalors|t|=|u||v|. – On voit donc que|a|=apour tout entiera.

1.2 Fonctions (primitive) récursives Notations.Soientx 1  . .,, .x k des objets. Lorsque le contexte est clair on écrirax~en lieu et place dex 1     x k ; par exemple lel-uplet (a 1     a l ) s’écrira simplement (a~). On utilisera les lettresa,b,c,k,l,n,mpour désigner des entiers,t,u,vpour les termes,x,y,zpour les variables,F,G,Hpour les fonctions,P,Q,Rpour les prédicats. Sieest une expression entière dépendant (ou pas) des variablesx 1  . .,, .x k (par exemple e=x 1 +x 2 ) on noteraλx~ela fonction qui à toutk-uplet d’entiers (~a) associee(a~). En parti- culier sinest un entier,λxnreprésente la fonction constante de valeurn. Prédicats.On appelleprédicatd’aritéktoute relationk-aire entre entiers où équivalemment, tout sous-ensemble deN k . SiPest un prédicatk-aire on notera indifféremment (~a)∈Pou P(a~). Lafonction caractéristiquedePestχ P :N k →Ndéfinie parχ P (a~)=0 siP(~a) (i.e., sia~∈P), χ P (~a)=prend ici une convention qui semble peu naturelle1 sinon. Remarquons que l’on à 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 fonctionpartielle F(d’ariték) deN k →Nest donnée par une partie domFdeN k appelée ledomainedeFet une fonction de domF→N. Si domF=N k on dit queFesttotale. On noteraF(~a)↓(resp.F(~a)↑) pour (a~)∈domF(resp. (a~)6∈domF). ~ SiFest partielle d’aritéketGest partielle d’aritél,F(a~)=G(b) signifie que soitF(a~)↑et ~ ~ ~ G(b)↑, soitF(~a)↓etG(b)↓etF(~a)=G(b). F ONCTIONS RÉCURSIVES Une fonction partielle d’aritékdeN k →Nestrécursivesi on peut la définir en appliquant un nombre fini de fois les schémas suivant :

1.2.Fonctions(primitive)récursives

7

R1les projectionsP k i : (~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)SiHest récursive (d’aritén) etG 1  . .,, .G n sont récursives (d’ariték) alors lacomposée F: F(~a)→H(G 1 (a~)    G n (a~)) est récursive. Son domaine est défini par ; F(~a)↓ssiG i (~a)↓pouri=1, . . .,netH(G 1 (~a)    G n (~a))↓ R3 (schéma de minimisation)SiGest récursive d’ariték+1 alors la fonctionF: F(~a)=x(G(xa)=0) ~ dont la valeur (si elle est définie) est le plus petitxtel queG(xa)=0 et le domaine est ~ donné par : F(~a)↓ ( G(a ~a)↓etG(a ~a)=0 ssi ∀b<aG(ba~)↓etG(ba~)>0 R EMARQUE : Le schéma de minimisation est le seul qui peut produire des fonctions non to- tales. Par exemple la fonctionF(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édicatPestrécursivement énumérables’il est le domaine d’une fonction récursive, c’est à dire s’il existeFrécursive telle queP(a~) ssiF(a~)↓pour tout k-uplet (~a). On utilise communément l’abbréviationr.e.pour « récursivement énumérable ». R EMARQUE : Un prédicat récursif est récursivement énumérable : soitFdéfinie parF(a)= x(a=0). AlorsFest récursive (pourquoi ?) et on aF(a)↓ssia=0. Par conséquentF(χ P (a~))↓ ssiP(a~). Commeχ P est récursiveF◦χ P l’est par schéma de composition et doncPest récur- sivement é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 estSet quidéfinitF, c’est à dire que : F(a~)=b ssi A[~ab] (ii)Si P est un prédicat r.e. d’arité k alors il existe une formule A[x~]qui estSet quidéfinitP, c’est à dire que : P(~a)ssi A[~a] Preuve :La deuxième partie du théorème se déduit de la première : siPest r.e. alors il y a une fonction récursiveFtelle queP(~a) ssiF(~a)↓, c’est à dire ssi∃y y=F(a~). D’après(i)il y a une formuleA[x~y] qui définitFet qui estS; mais alorsB=∃yA[x~y] définitPet comme AestS,Bl’est aussi. La première partie se démontre par récurrence sur la construction deF. SiFest la projec- tionP k i alorsFest définie pary=x i ; l’addition est définie pary=x 1 +x 2 et la multiplication pary=x 1 x 2 . Enfinχ < se définit par (x 1 <x 2 ∧y=0)∨(x 1 6<x 2 ∧y=S0) (x 1 6<x 2 est une abbréviation pour¬(x 1 <x 2 pour l’instant toutes ces formules sont)). Remarquons que D. ~ SiF(a~)=H(G(a~)) où lesG i etHsont récursives alors par hypothèse de récurrence il y a des formulesB i [~xy i ] pouri=1    netC[y~y] qui sontSet qui définissent respectivement lesG i etH. On pose A=∃y 1   ∃y n B 1 [x~y 1 ]∧    ∧B n [~xy n ]∧C[~yy]

8

ThéorèmesdeGödel

ClairementAestSet définitF. Enfin siF(~a)=x(G(xa~)=0) oùGest récursive alors par hypothèse de récurrence il y a une formuleB[x ~xy] qui estSet qui définitG. On pose A=∀y ′ <y∃z B[y ′ x~S z]∧B[y ~x0]  (Question : pourquoi n’a-t-on pas définiA=∀y ′ <y¬B[y ′  ~x0]∧B[yx~0] ?) F ONCTIONS 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 decorrection de programme, c’est à dire que lorsqu’on écritF(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énifi- ciant 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 lesfonctions primitives ré- cursives. Une fonction deN k →Nrécursive (p.r.) si on peut l’obtenir en appliquantest primitive un nombre fini de fois les schémas suivant : PR1Les projectionsP 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)siGest primitive récursive d’aritéketHest primitive récur- sive d’ariték+2 alorsFdéfinie par : a~)= ( H(F(a−1a~)aa~) sia>0 F(a G(a~) sia=0 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.2F est récursive (totale). Si P est unSi F est une fonction primitive récursive alors prédicat primitif récursif alors P est récursif. Preuve :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émasPR1,PR2etPR3peut se « programmer » à l’aide des schémasR1,R2etR3. PourPR1il faut juste voir que les fonctions constantes sont pro- grammables. La fonctionC 0 =λx~0 est donnée parC 0 (a~)=x(P) 1 k+1 (xa~)= la fonction0 ; C 1 =λ~x1 parC 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éris- tiques. La fonctionC 2 =λx~2 est donnée parC 2 (x~)=C 1 (x~)+C 1 (~x), et plus généralement on définitC n+1 parC n+1 (x~)=C n (~x)+C 1 (x). ~ 1 On le démontre pardiagonalisation: on verra un peu plus loin qu’un ensembleXest r.e. ssi il existe une fonction récursive totaleFquiénumère X, c’est à dire telle queXest l’image deF. SoitT 1 l’ensemble des fonctions récursive totales unaires etϕune fonction deN 2 dansNqui énumèreT 1 , c’est à dire telle que pour touteFdansT 1 il existe un e F tel queF(a)=ϕ(e F a) pour touta. On va voir queϕne peut être récursive. DéfinissonsGparG(a)=ϕ(aa)+1 ; alorsGne peut être récursive, sinon elle est dansest clairement totale et unaire mais elle T 1 et il y a une G tel que G(a)=ϕ(e G a) pour toutadonc en particulier poura=e G ,G(e G )=ϕ(e G e G ) contredisant la définition deG. Donc ϕn’est pas récursive, sinonGle serait également.

1.2.Fonctions(primitive)récursives9 Le schémaPR2est le même que le schémaR2; reste donc à voir le schéma de récurrence primitivePR3et c’est là qu’il va falloir travailler un peu. On commence par dériver deR1, R2etR3des schémas supplémentaires pour programmer des fonctions récursives. SoitP(x ~xrécursif. Alors la fonction définie par) un prédicat F(a~)=x(P(x ~a)) est ré- cursive ; en effet commePest récursifχ P est récursive (totale), et doncFest obtenue parR3 (ici aussi on se sert du choixχ P (aa~)=0 ssiP(a~a)). Si de plus pour tout~ail y a unatel que  P(aa~) alorsFest totale. La fonctionλxyx−  yest récursive (totale) : on l’obtient para−  b=x(x+b+1>a). SoientPetQdes prédicats récursifs alors ;¬P,P∨Q,P∧Qsont récursifs. En effet leurs fonctions caractéristiques s’obtiennent au moyen de celles dePetQpar les opérations arithmétiques+,et−  qui sont tous récursifs totals. Remarquons que si on supposeP seulement r.e. alors¬Pn’est pas r.e. en général (pourquoi ?). SoitP(xx~) un prédicat récursif etF(x~) une fonction récursive totale ; alors la fonction G(~x) définie parG(a~)=x<F(~a)(P)(xa~) (le premierx<F(~a) tel queP(xa~) s’il en existe, F(~a) sinon), est récursive totale. En effetG(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.3Il existe une fonctionβrécursive totale vérifiant : pour toutnet tousa 0 , . . .,a n , il existectel que pouri=0    non 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écur- rence primitivePR3est récursif. ¯ SoitG(~x) etH(xy ~x) des fonctions récursives totales. On définitF(xx~) par : ¯  (x a  (x) y+1 =H((x) y y+1a~)  ) F(aa)=x( ) 0 =G(~a)∧ ∀y< ~ ¯ La fonctionFest clairement récursive et on peut facilement se convaincre par récurrence sur ¯ nqu’elle est totale. Soit maintenantFdonnée parF(aa~)=(F(a ~a)) a ; alorsFest également récursive totale et on peut vérifier par récurrence suraque l’on aF(0a~)=G(a~) etF(a+ 1a~)=H(F(a ~a)a ~a) pour touta, soit queFest définie par récurrence primitive à partir de GetH. P ROGRAMMATION DE FONCTIONS PRIMITIVES RÉCURSIVES . On va maintenant se donner un certain nombre d’autres schémas pour définir des fonc- tions et prédicats p.r. Itération.SiGest p.r. d’ariték+1 alors la fonctionFdéfinie par : F(aba~)=G a (ba) ~ est p.r. d’ariték+une reformulation du schéma de récursion primitive. Clai-2. En fait c’est rementFest donnée parF(0ba~)=betF(a+1b ~a)=G(F(aba~) ~a). Soustraction.On définita  −1 par : 0  −1=0 et (a+1)−  1=a. On définita  −bpara  −0=a eta−  (b+1)=(a  −b)  −1. La fonction binaire−  est clairement p.r. Variante de la récursion primitive.SoientG 0 une fonction p.r. d’ariték,Hp.r. d’ariték+2 et G 1 ,. . .,G k des fonctions p.r. d’ariték+1 . Alors la fonctionFdéfinie par F(0a)=G 0 (a~) ~ ~ F(a+1a)=H(F(aG(a ~a))aa~) ~

10

ThéorèmesdeGödel

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 queFest définie par F(0b)=G 0 (b) F(a+1b)=H(F(aG 1 (ab))ab) On se donneg: g(0ba)=b g(i+1ba)=G 1 (a  −(i+1)g(iba))

eth:

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 quegethsont toutes les deux p.r. On va montrer que pour toutb: F(ab)=h(aba) (1.1) Commehest p.r. on en déduira queFl’est. On vérifie aisément par récurrence surique pour touta≥ion 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 sura. Poura=0 on ah(0b0)=G 0 (g(0b0))=G 0 (b)= F(0b). Supposons queF(ab)=h(aba). Alors h(a+1ba+1)=H(h(aba+1)ag(0ba+ définition de1)) parh =H(h(aba+1)ab définition de) parg =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 définition de) parF

Opérations booléennes.SiPetQsont p.r. d’aritékalors¬P,P∨Q,P∧Qsont 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.SiPest un prédicat p.r. d’ariték,GetHsont p.r. d’aritékalorsFdéfinie par : F(a~)= ( G H ( ( ~ a a ~n s ) i is )P on (~a) est p.r. : on l’obtient parF(~a)=(1−  χ P (a~))G(~a)+χ P (~a)H(~a). Plus généralement siP 1  . .,, .P n sont p.r. etG 1 , . . .,G n+1 sont p.r. alors  G 1 (~a) siP 1 (~a) F(a~)=   n . (~a) si¬(P 1 (~a)∨    ∨P n−1 (a~))∧P G n (a~)   G n+1 (a~) sinon

est p.r.