Interpretation des symboles de predicat constants

Télécharger le fichier original (Mémoire de fin d’études)

Historique

Ce sous-chapitre n’a pas la pretention de fournir un apercu historique absolument rigoureux. Nous souhaitons seulement rappeler les concepts de base sur lesquels repose notre travail (types, -calcul, etc.) et montrer comment celui-ci s’inscrit dans la continuation de travaux visant a introduire toujours plus de calcul dans la logique ou, dualement, a introduire toujours plus de logique dans la programmation. Nous prendrons donc certaines libertes avec le formalisme utilise.
Le lecteur rompu a ces notions (en particulier le Calcul des Constructions et le Calcul des Constructions Inductives) peut aller directement au Sous-chapitre 1.2 suivant ou nous presentons nos motivations pour l’ajout dans le Calcul des Construc-tions de recriture aussi bien au niveau des objets qu’au niveau des predicats.
La Theorie des ensembles
Un des premiers systemes formels qui permettent de decrire l’ensemble des mathematiques est la theorie des ensembles de E. Zermelo (1908) etendue plus tard par A. Fraenkel (1922). Il a et suivi par la theorie des types de A. Whitehead et B. Russell (1911) [119], aussi appelee logique d’ordre superieur . Ces deux systemes formels ont et introduits pour repondre a l’incoherence de la theorie des ensembles de G. Cantor (1878).
En logique du premier ordre, dans laquelle est generalement exprimee la theorie des ensembles de E. Zermelo et A. Fraenkel, les objets du discours sont de nis a partir de constantes et de symboles de fonctions (0; +; : : :). Ensuite, des symboles de predicats (2, . . . ), les connecteurs logiques (_; ^; ), : : 🙂 et les quanti cateurs universels et existentiels (8; 9) permettent d’exprimer des propositions sur ces objets.
Un des axiomes de la theorie des ensembles de G. Cantor est l’axiome de compre-hension qui dit que toute proposition de nit un ensemble :
(9x)(8y) y 2 x , P (y)
A partir de cet axiome, on peut exprimer le paradoxe de Russell (1902). En prenant P (x) = x 2= x, on peut de nir l’ensemble R des x qui n’appartiennent pas a eux-m^emes. Alors, R 2 R , R 2= R et on peut deduire que toute proposition est vraie. Pour remedier a ce probleme, E. Zermelo a propose de restreindre l’axiome de comprehension de la maniere suivante :
(8z)(9x)(8y) y 2 x , y 2 z ^ P (y)
c’est-a-dire que, desormais, on ne pourra de nir par comprehension que des sous-ensembles d’ensembles precedemment de nis.
La Theorie des types
En theorie des types, l’idee n’est pas de restreindre l’axiome de comprehension mais d’interdire des expressions comme x 2= x ou x 2 x, en restreignant l’application d’un predicat a un objet. Pour cela, on associe a chaque symbole de fonction et a chaque symbole de predicat (sauf le symbole d’appartenance) un type de la maniere suivante :
{ a une constante, on associe le type ,
{ a une fonction prenant un argument, on associe le type ! ,
{ a une fonction prenant deux arguments, on associe le type ! ! , { …
{ a une proposition, on associe le type o,
{ a un predicat prenant un argument, on associe le type ! o,
{ a un predicat prenant deux arguments, on associe le type ! ! o, { …
Alors, on peut appliquer une fonction f prenant n arguments a des objets t1; : : : ; tn si le type de f est ! : : : ! ! et chacun des ti est de type . Et on peut ecrire que des objets t1; : : : ; tn veri ent un predicat P a n arguments si le type de P est ! : : : ! ! o et chacun des ti est de type .
En n, on considere qu’un ensemble n’est plus un objet (une expression de type ) mais un predicat (une expression de type ! o). Et, pour representer x 2 E, qui signi e que x veri e E, on ecrira Ex (application de E a x). Ainsi, on veri e aisement qu’il n’est pas possible d’exprimer le paradoxe de Russell : on ne peut pas ecrire xx pour representer x 2 x car il faudrait que x soit a la fois de type ! o et de type . Par la suite, on ecrira t : pour signi er que t est de type .
Maintenant, pour representer les entiers naturels, il y a plusieurs possibilites. Mais il est toujours necessaire de poser un axiome d’in nite pour et de pouvoir exprimer l’ensemble des entiers naturels comme le plus petit ensemble contenant zero et stable par incrementation. Pour cela, il faut pouvoir quanti er sur des en-sembles, c’est-a-dire sur des expressions de type ! o et non plus seulement sur des expressions de type .
C’est la que le terme de logique d’ordre superieur prend tout son sens. Desormais, on ne va plus se restreindre aux expressions d’objets et de predicats decrites prec – demment, on va considerer l’ensemble des expressions que l’on peut former par application en respectant les types, quels que soient ceux-ci :
{ On de nit l’ensemble des types simples comme le plus petit ensemble T contenant , o et ! des lors que et appartiennent a T .
{ On de nit l’ensemble des termes de type comme le plus petit ensemble contenant les constantes de type et les applications tu des lors que t est un terme de type ! et u un terme de type .
En n, on introduit une notation explicite pour designer les fonctions et les en-sembles, la -abstraction , et on inclut dans les constantes les connecteurs et quan-ti cateurs en leur assignant les types suivants : _ : o ! o ! o, ^ : o ! o ! o, 8 : ( ! o) ! o, . . . Par exemple, si designe l’ensemble des entiers natu-rels, on peut designer le predicat \est pair » (de type ! o) par l’expression pair = x : :9 ( y : 😡 = 2 y) qu’on abregera par x : :9y : 😡 = 2 y. Le langage des termes ainsi obtenu s’appelle le -calcul simplement type , note !.
10 CHAPITRE 1. INTRODUCTION
Mais que dire de pair 2 et 9y : :2 = 2 y ? La seconde expression s’obtient en substituant x par 2 dans le corps de pair. Cette operation de substitution s’appelle la -reduction . De maniere generale, x : : t applique a u se -reduit en le terme t ou x est substitue par u : x: : t u ! tfx 7!ug.
Il est assez naturel de considerer ces deux expressions comme denotant la m^eme proposition. C’est pourquoi on rajoute l’axiome de conversion suivant :
P , Q si P ! Q
On aboutit alors a la theorie des types de A. Church (1940) [28].
Dans une telle theorie, il est possible de quanti er sur l’univers des propositions lui-m^eme : 8P : o:P ) P . Autrement dit, une proposition peut ^etre de nie en quanti ant sur l’ensemble des propositions, y compris elle-m^eme. Si on autorise de telles quanti cations, on dit que la theorie est impredicative , sinon on dit qu’elle est predicative .
Les mathematiques comme langage de programmation
La -reduction correspond au processus d’evaluation d’une fonction. Lorsqu’on a une fonction f de nie par une expression f(x) et qu’on veut sa valeur en 5 par exemple, on va substituer x par 5 dans f(x) et simpli er l’expression obtenue jusqu’a obtenir la valeur de f(5).
On peut alors se demander quelles fonctions on peut ainsi de nir dans la theorie des types de A. Church. En fait, bien peu. Sur les entiers de Peano (i.e. en pre-nant 0 : pour zero et s : ! pour la fonction successeur), on ne peut exprimer que des fonctions constantes et des fonctions qui ajoutent une constante a l’un de leurs arguments. Sur les entiers de A. Church, ou n est represent par le terme x : : f : ! :f : : : f x avec n occurrences de f, H. Schwichtenberg [105] montra qu’on ne peut exprimer que des polyn^omes etendus (plus petit ensemble de fonctions clos par composition et contenant la fonction nulle, la fonction successeur, les pro-jections, l’addition, la multiplication, la fonction caracteristique de f0g et la fonction caracteristique de N n f0g).
Bien s^ur, il est possible de montrer l’existence de nombreuses fonctions, c’est-a-dire de prouver une proposition de la forme (8x)(9y) P xy ou le predicat P represente le graphe de la fonction. Dans la theorie des types intuitionniste par exemple (i.e. sans l’axiome du tiers-exclu P _ 😛 ), il est possible de montrer l’existence de toutes les fonctions primitives recursives. Mais on ne dispose pas de terme f : ! qui nous permette de calculer les puissances de 2 par exemple, c’est-a-dire, tel que f n ! : : : ! 2n.

Table des matières

1 Introduction
1.1 Historique
1.2 Motivations
1.3 Travaux anterieurs
1.4 Contributions
1.5 Plan de la these
2 Preliminaires
3 Systemes de Types Modulo (TSM)
3.1 Denition
3.2 Proprietes
3.3 TSM stables par substitution
3.4 TSM logiques
4 Systemes de Types a Reduction (RTS)
4.1 Denition
4.2 RTS logiques et fonctionnels
4.3 RTS logiques et injectifs
4.4 RTS con
uents
5 Systemes de Types Algebriques (ATS)
6 Conditions de Normalisation Forte
6.1 Classication des termes
6.2 Types inductifs et constructeurs
6.3 Schema General
6.3.1 Recriture d’ordre superieur
6.3.2 Denition du schema
6.4 Conditions de normalisation forte
7.1 Calcul des Constructions Inductives
7.2 Calcul des Constructions Inductives + Recriture
7.3 Deduction Naturelle Modulo
8 Correction des conditions de normalisation forte
8.1 Espace des termes interpretes
8.2 Candidats de reductibilite
8.3 Schema d’interpretation des types
8.4 Interpretation des symboles de predicat constants
8.5 Ordre de reductibilite
8.6 Interpretation des symboles de predicat denis
8.6.1 Systemes primitifs
8.6.2 Systemes positifs, petits et simples
8.6.3 Systemes recursifs, petits et simples
8.7 Correction des conditions de normalisation forte
9 Futures directions de recherche
Bibliographie