Ce mémoire est une introduction à un dossier d'habilitation composé d'articles écrits entre 1994 et 1998 et référencés ci-dessous [a, b, c, d, e, f, g, h, i, j]. Par ailleurs, une annexe contient deux articles d'exposition référencés [x, y] destinés essentiellement à des chercheurs de disciplines connexes 1 .

On trouvera peu d'arguments techniques dans ce mémoire. J'ai tenté, en revanche, de donner les motivations de ce travail, de mettre les différents articles en perspective, de donner des exemples et de montrer quelle pourrait être une suite de ces recherches.

Les articles [a, b, c, d, e, f, h, i] ont été publiés dans des journaux ou des actes de conférences. L'article [g] n'est, en revanche, que soumis à publication. L'article [j] est un article invité au symposium First order theorem proving qui s'est tenu à Vienne en Novembre 1998. Les articles publiés dans des journaux apparaissent dans ce dossier dans leur forme définitive. Ceux qui sont publiés dans des actes de conférences ou soumis à publication apparaissent en version longue.

Chapitre 1

La déduction modulo

Les règles

Les notions de langage, de terme et de proposition de la déduction modulo sont les mêmes que celles de la logique du premier ordre. En revanche, dans ce formalisme, une théorie est composée non seulement d'un ensemble d'axiomes, mais aussi d'une congruence ≡ définie sur les termes et les propositions. On identifie les propositions congruentes. La règle de modus ponens, par exemple, ne s'exprime plus de la manière traditionnelle A ⇒ B A B mais, pour prendre en compte le cas où les deux occurrences de A ne sont pas identiques, mais seulement congruentes, on formule cette règle de la manière suivante

Une formulation plus générale sera, en fait, utile dans la suite C A si C ≡ A ⇒ B B Les règles de déduction naturelle modulo sont données figure 1.1 et celles du calcul des séquents modulo figure 1.2. Nous avons proposé le calcul des séquents modulo dans [g], puis la déduction naturelle modulo dans [h].

À titre d'exemple, donnons une démonstration, en arithmétique, en déduction naturelle modulo de la proposition "4 est pair", ∃x (2 × x = 4) ∀x x = x (x, x = x, 4) ∀-élim

Je tiens, avant toute chose, à remercier Monsieur Guy Cousineau de l'honneur qu'il me fait en présidant ce jury. Enseigner dans le DEA Programmation qu'il dirige a été pour moi une source constante de questions et de remise en question.

Je tiens, ensuite, à remercier Messieurs Henk Barendregt, Pierre-Louis Curien et Jean-Pierre Jouannaud qui ont lu ces pages avec une grande patience. Je dois, entres autres choses, à Henk Barendregt de m'avoir signalé le passage dans lequel Poincaré oppose démonstration et vérification et plusieurs discussions "informelles" sur les rapports entre déduction et calcul lors des symposiums Types. Je suis reconnaissant à Pierre-Louis Curien de l'intérêt qu'il a porté très tôt à l'utilisation que nous avons faite des substitutions explicites, qui est assez éloignée -en apparence -de ce pour quoi il les avait inventées. Jean-Pierre Jouannaud m'a invité à plusieurs reprises au séminaire qu'il anime à Orsay. J'ai toujours trouvé, lors de ces exposés, une stimulante exigence.

Je suis également très reconnaissant à Messieurs Paul Gochet, Gilles Kahn et Per Martin-Löf de l'intérêt qu'ils portent à ce travail en formant le jury qui le sanctionne. La clarté de Paul Gochet, qui a beaucoup contribué à faire connaître Quine aux informaticiens et la démonstration automatique aux philosophes, est pour moi un exemple. L'encyclopédisme de Gilles Kahn est un modèle difficile à imiter. De nombreuses conversations avec Per Martin-Löf m'ont appris un certain sens de la synthèse, et aussi de la prudence.

Toute ma gratitude va à Gérard Huet qui a accepté le rôle de directeur de recherche pour cette habilitation. L'influence de ses recherches sur ce travail qui touche à la résolution d'ordre supérieur, à la réécriture et à l'interprétation fonctionnelle des démonstrations est immense.

Ce travail, qui est largement collectif, n'aurait jamais pu voir le jour si je n'avais pas rencontré Thérèse Hardin, Claude Kirchner, Frank Pfenning et Benjamin Werner avec qui nombre des articles qui constituent ce dossier sont signés. Je suis conscient de la chance que j'ai eu de pouvoir travailler avec chacun d'eux et de ce qu'ils m'ont appris.

Enfin, ce travail n'aurait pas non plus pu se faire, si je n'avais pas eu la chance de travailler dans le projet Coq de l'INRIA que dirige Christine Paulin. La richesse intellectuelle et la liberté que procure cet exceptionnel environnement de travail méritent d'être préservées.

Je crois que deux et deux sont quatre, Sganarelle, et que quatre et quatre sont huit.

Molière -Dom Juan

Comme toute proposition mathématique, la proposition 2 + 2 = 4 est susceptible d'être démontrée. La figure 1 donne une démonstration possible. Certains, pourtant, comme H. Poincaré, contestent le fait qu'un tel raisonnement soit véritablement une démonstration : "On ne saurait nier que ce raisonnement soit purement analytique. Mais interrogez un mathématicien quelconque : 'Ce n'est pas une démonstration proprement dite, vous répondra-t-il, c'est une vérification' " [81].

Le problème de savoir si deux et deux font quatre, ou plus généralement de trouver la somme de deux nombres, leur produit ou leur plus grand diviseur commun, est en effet d'une nature très différente de celui de savoir si, par exemple, un carré peut être le double d'un autre ou la somme de deux puissances n ème , une puissance n ème . Résoudre le premier problème demande uniquement d'effectuer un calcul, alors que résoudre le second demande de construire un raisonnement, car la quantification sur une quantité infinie d'objets rend la vérification impossible.

Les mathématiques assyrio-babyloniennes et égyptiennes étaient essentiellement constituées de méthodes de calcul : méthodes pour effectuer des opérations comptables ou calculer des aires agricoles, ... Puis la géométrie grecque introduisit la notion d'espace indéfini, elle cessa alors de parler de telle ou telle parcelle agricole, pour parler d'objets abstraits : les triangles, les cercles, ... De même, l'arithmétique cessa de parler de telle ou telle quantité, pour parler, elle aussi, d'objets abstraits : les nombres. Avec ces objets abstraits arrivèrent de nouveaux problèmes que le calcul ne suffisait pas à résoudre. On introduisit alors un nouvel outil : le raisonnement. Les Éléments d'Euclide restèrent longtemps le prototype de la méthode mathématique : la solution de problèmes par le raisonnement. C'est encore ce point de vue qui domine, au début du vingtième siècle dans les travaux de G. Peano, G. Frege, D. Hilbert, E. Zermelo, A.N. Whitehead, B. Russell ou N. Bourbaki. Dans l'arithmétique de Peano, par exemple, il n'y a pas de règle de calcul qui permette de vérifier que 2 + 2 = 4, mais il y a des axiomes qui permettent de démontrer cette proposition. La spécificité de ce problème, qui peut se résoudre par un simple calcul, est gommée, au profit d'une méthode uniforme : le raisonnement. Il en est de même dans la Begriffschrift de Frege, la géométrie de Hilbert, la théorie des ensembles de Zermelo, les Principia mathematica de Whitehead et Russell ou les Éléments de mathématique de Bourbaki.

Si le raisonnement domine dans ces travaux qui concernent tous la formalisation des mathématiques ou de l'une de ses branches, on peut noter que dans les mathématiques informelles, en revanche, une place importante a toujours été accordée à la construction de méthodes de calcul, comme en témoignent les algorithmes de multiplication des nombres en notation décimale (al-Uqlidisi, ...), de résolution d'équation algébriques du Ce paradoxe se retrouve au sein de la logique. La notion de calcul est, par exemple, centrale dans le programme de Hilbert (trouver un algorithme qui décide si une proposition mathématique est un théorème ou non) et dans la théorie de la calculabilité qui permet d'y répondre négativement. Cette notion est également centrale dans l'étude des démonstrations intuitionnistes, par exemple dans la démonstration de terminaison de l'algorithme d'élimination des coupures qui transforme chaque démonstration d'existence en un témoin de cette existence. Pourtant, si les logiciens s'intéressent au calcul, la notion de démonstration qu'ils utilisent, qui est celle de la logique du premier ordre, se fonde, quant à elle, uniquement sur le raisonnement.

Depuis l'apparition des ordinateurs, la notion de calcul connaît un certain renouveau. Par delà l'effet de mode, ce regain d'intérêt s'explique, très concrètement, par le fait que la solution de certains problèmes en informatique demande d'utiliser une formalisation des mathématiques qui accorde une place au calcul, contrairement à la formulation traditionnelle de la théorie des ensembles.

Le premier de ces problèmes est celui de la démonstration automatique, c'est-à-dire de la construction de programmes qui recherchent des démonstrations pour des propositions mathématiques. L'utilisation de formalisations des mathématiques reposant uniquement sur le raisonnement aboutit au paradoxe suivant : quand on demande à un tel programme de résoudre le problème "Est-ce que 2 + 2 = 4 ?", il ne voit pas que ce problème peut se résoudre par un simple calcul et il cherche à démontrer la proposition 2 + 2 = 4 en utilisant potentiellement tous les axiomes des mathématiques. Chercher une telle démonstration est naturellement une opération beaucoup plus coûteuse qu'effectuer une simple addition.

Un autre problème est celui de la vérification de correction des démonstrations. Quand on vérifie la correction d'une démonstration qui utilise le fait que 2 + 2 est égal à 4, on peut penser qu'il est paradoxal de devoir vérifier une démonstration de ce fait, alors qu'on peut directement effectuer le calcul et vérifier le fait lui-même.

Un autre exemple de problème est celui de la programmation en langage mathématique [64, 79, y]. Il est devenu banal de remarquer qu'un programme qui associe une valeur (la valeur de sortie) à une ou plusieurs autres valeurs (les valeurs d'entrée) n'est rien d'autre qu'une fonction, au sens mathématique du terme. Par exemple, le programme qui calcule le montant des mensualités d'un prêt en fonction de la somme empruntée, du nombre de mensualités et du taux d'intérêt n'est rien d'autre que la fonction f = e, n, t -→ e t 1 -1 (1+t) n Le langage mathématique étant bien adapté à l'expression de fonctions, certains proposent de l'utiliser comme langage de programmation. Si on emprunte 5000 € sur 24 mois au taux mensuel de 0.64% (ce qui correspond à un taux annuel de 8%), les mensualités seront de f (5000, 24, 0.0064) €. Hélas, ce n'est pas cette information qui est utile, mais celle que les mensualités seront de 225 €. Exécuter les programmes écrits en langage mathématique demande donc une formalisation des mathématiques qui distingue un terme quelconque, comme f (5000, 24, 0.0064) d'une valeur, comme 225, et qui permette de calculer le terme f (5000, 24, 0.0064) en la valeur 225.

Un dernier exemple est le calcul formel. Ici encore, il ne suffit pas de savoir que la dérivée de la fonction x -→ sin 2 x est la fonction x -→ 2 sinx cosx mais il faut que le terme (D (x -→ sin 2 x)) se calcule sur le terme x -→ 2 sinx cosx.

Des systèmes formels qui intègrent raisonnement et calcul ont été développés pour répondre à ces problèmes : G. Plotkin [START_REF] Plotkin | Building-in equational theories[END_REF] et P.B. Andrews [3] proposent, dans le cadre de la démonstration automatique, de mêler certains axiomes à l'unification, ce qui permet de les supprimer de l'ensemble des axiomes avec lesquels on raisonne, après le langage du système Automath [START_REF] De Bruijn ; To | A Survey of the project Automath[END_REF], la théorie des types de P. Martin-Löf [START_REF] Martin-Löf | Intuitionistic type theory[END_REF], le Calcul des constructions [START_REF] Th | The calculus of constructions[END_REF] et le Calcul des constructions inductives [START_REF] Ch | Inductive definitions in the system COQ, Rules and properties, Typed Lambda Calculi and Applications[END_REF][START_REF] Werner | Une théorie des constructions inductives[END_REF] ont une règle de conversion qui permet d'effectuer des calculs dans une proposition sans changer sa démonstration, l'Arithmétique fonctionnelle du second ordre [START_REF] Krivine | Programming with proofs[END_REF][START_REF] Krivine | Lambda-calcul, types et modèles[END_REF]] permet d'utiliser des axiomes équationnels sans que cela apparaisse dans les démonstrations. H. Barendregt et E. Barendsen [START_REF] Barendregt | Autarkic computations in formal proofs[END_REF] ont proposé d'appeler "principe de Poincaré" ce principe -qu'on retrouve ici et là -qui consiste à calculer dans une proposition sans en changer la démonstration.

L'objectif de l'ensemble d'articles réunis dans ce dossier est de proposer, et d'étudier les propriétés, d'un ensemble de règles de déduction, la déduction modulo, qui intègre le calcul et le raisonnement de la manière la plus générale qui soit, indépendamment d'une formalisation particulière des mathématiques (la théorie des ensembles, l'Arithmétique fonctionnelle du second ordre, la théorie des types simples, la théorie des types de Martin-Löf, le Calcul des constructions, le Calcul des constructions inductives, ...) ou d'une application particulière (la démonstration automatique, la vérification de correction des démonstrations, la programmation en langage mathématique, le calcul formel, ...). Pour que la correction des démonstrations reste décidable, il faut que l'information supprimée des démonstrations puisse être reconstruite. Il faut donc que la congruence ≡ soit décidable. De plus, il faut indiquer le témoin lors de l'application des règles d'élimination du quantificateur universel et d'introduction du quantificateur existentiel. En effet, en l'absence de ces témoins, la décidabilité de la correction des démonstrations demanderait non seulement la décidabilité de la congruence ≡ elle-même, mais aussi celle du filtrage modulo cette congruence, puisqu'il faudrait pouvoir décider si une proposition est une instance d'une autre modulo ≡ ou non.

Γ ⊢≡ C Γ, A ⊢≡ B (x, A) ∃-élim si C ≡ (∃x A) et x ̸ ∈ F V (ΓB) Γ ⊢≡ B B tiers exclu si A ≡ (B ∨ ¬B) Γ ⊢≡ A Figure 1.1 -La déduction naturelle modulo 1.1. LES RÈGLES Γ, A ⊢≡ ∆ (x, A) ∃-gauche si B ≡ (∃x A) et x ̸ ∈ F V (Γ∆) Γ, B ⊢≡ ∆ Γ ⊢≡ [t/x]A, ∆ (x, A, t) ∃-droite si B ≡ (∃x A) Γ ⊢≡ B, ∆
Proposition 1.1.1 Si la congruence ≡ est décidable, il existe un algorithme qui prend en argument une proposition et une dérivation (en déduction naturelle modulo ou en calcul des séquents modulo) et indique si la dérivation est une démonstration correcte de la proposition ou non.

Cependant, rien n'empêche de considérer abstraitement des "démonstrations" modulo une congruence indécidable ou dont la décidabilité est un problème ouvert, et d'étudier certaines de leur propriétés. C'est par exemple le cas de la théorie des ensembles que nous discuterons au chapitre 3. Si ce système de réécriture termine et est confluent, la congruence est décidable.

Les congruences

Les équations entre termes

Quand on utilise une opération commutative, on veut parfois pouvoir identifier les propositions P (x+y) et P (y+x), c'est-à-dire considérer que la permutation des termes est du ressort du calcul et non du raisonnement, bien que la règle

x + y → y + x ne termine pas. On considère donc des congruences définies par des règles de réécriture et des équations entre termes.

La réécriture des propositions

Ces différentes congruences sont définies par des règles de réécriture et des équations sur les termes du langage. La congruence sur les propositions est induite par la congruence sur les termes : c'est parce que les termes 2 + 2 et 4 sont congruents que les propositions 2 + 2 = 4 et 4 = 4 le sont également. Dans de nombreux cas, on veut pouvoir définir des congruences directement sur les propositions. On est amené à poser des règles de réécriture sur les propositions elles-mêmes, par exemple la règle Remarquons que le langage des propositions contenant des symboles lieurs (les quantificateurs) ces systèmes de réécriture sont des systèmes de réduction combinatoires (combinatory reduction systems) ou CRS [START_REF] Klop | Combinatory reduction systems : introduction and survey[END_REF].

Succ(x) = Succ(y) → x = y
La forme des propositions atomiques joue un rôle très mineur dans les démonstrations (seule la règle axiome y est sensible). La possibilité d'appliquer ou non une règle logique dépend essentiellement des connecteurs et quantificateurs de la proposition. De ce fait, les congruences qui n'affectent que les termes influent peu sur la possibilité d'appliquer une règle logique ou non. La situation est tout à fait différente avec les règles comme celle ci-dessus : le fait que la proposition x×y = 0 soit congruente à la proposition x = 0∨y = 0 permet de la démontrer en utilisant une règle d'introduction de la disjonction. Ces règles permettent donc une véritable interaction entre le calcul et le raisonnement.

Dans les articles réunis dans ce dossier, nous nous sommes restreints à des règles qui réécrivent des propositions atomiques en des propositions quelconques. Cela nous prive de la possibilité d'appliquer les règles de simplification propositionnelle proposées par J. Hsiang [START_REF] Hsiang | Refutational theorem proving using term-rewriting systems[END_REF]. L'avantage de se placer dans une telle restriction est que, pour pouvoir appliquer une règle de déduction, il suffit de réduire la proposition considérée. Ce ne serait pas le cas si on avait, par exemple, une règle de la forme

A ∧ B → C
dans ce cas, la proposition C étant congruente à la proposition A ∧ B, on pourrait la démontrer à l'aide de la règle d'introduction de la conjonction, mais pour mettre cette proposition C sous la forme d'une conjonction, il faudrait appliquer la règle "à l'envers", ce qui est contraire à l'intuition de la réécriture.

Les congruences que nous considérons sont donc définies par -un ensemble E de règles de réécriture et d'équations entre termes ou entre propositions atomiques, -un ensemble R de règles de réécriture qui réécrivent des propositions atomiques sur des proposition quelconques.

Le lemme d'équivalence

La première propriété de ces systèmes de déduction modulo est le lemme d'équivalence démontré dans [g]. Ce lemme établit que du point de vue de la démontrabilité, une théorie modulo est toujours équivalente à une théorie du premier ordre. Du point de vue de la démontrabilité, la déduction modulo n'est donc pas une nouvelle logique, c'est simplement une nouvelle formulation de la logique du premier ordre.

La notion de modèle pour la déduction modulo

Le lemme d'équivalence nous permet de définir simplement la notion de modèle pour la déduction modulo : on définit les modèles d'une théorie modulo (≡, Γ) comme les modèles de T Γ où T est la théorie ci-dessus. Cette définition peut également se formuler de la manière suivante. Définition 1.4.1 Un modèle de (≡, Γ) est un modèle de Γ tel que si P ≡ Q alors P et Q ont même dénotation.

Du théorème de correction et du théorème de complétude de K. Gödel pour la logique du premier ordre, on déduit les propositions suivantes. Proposition 1.4.1 (Correction) Si Γ ⊢ ≡ P alors P est valide dans tous les modèles de (≡, Γ). Proposition 1.4.2 (Complétude) Si P est valide dans tous les modèles de (≡, Γ) alors Γ ⊢ ≡ P .

Avec cette notion de modèle, deux propositions congruentes ont nécessairement la même dénotation, mais pas nécessairement deux termes congruents. Cependant, les dénotations de deux termes congruents ne peuvent être discernée par aucun prédicat. Comme dans le cas de la théorie de l'égalité, on peut renforcer le lemme de complétude en se restreignant à une classe plus petite de modèles. Définition 1.4.2 Un modèle égalitaire de (≡, Γ) est un modèle de Γ tel que si P ≡ Q alors P et Q ont même dénotation et si t ≡ u alors t et u ont même dénotation.

Clairement, tous les modèles égalitaires d'une théorie (≡, Γ) sont des modèles de cette théorie. On montre que pour tout modèle de (≡, Γ), il existe un modèle égalitaire qui valide les mêmes propositions. On en déduit les lemmes de correction et de complétude.

Proposition 1.4.4 (Correction) Si Γ ⊢ ≡ P alors P est valide dans tous les modèles égalitaires de (≡, Γ).

Proposition 1.4.5 (Complétude) Si P est valide dans tous les modèles égalitaires de (≡, Γ) alors Γ ⊢ ≡ P .

Le cas des congruences présentées par un système de réécriture

Quand la congruence est présentée par un système de réécriture RE, on peut prendre une théorie T plus petite dans le lemme d'équivalence : pour chaque règle de réécriture l → r ou équation l = r de RE, on prend la clôture universelle de la proposition t = u ou t ⇔ u selon que t et u sont des termes ou des propositions.

Cela demande de disposer d'un prédicat d'égalité et des axiomes correspondants. Si la théorie ne contient pas un tel prédicat, on peut l'ajouter de manière conservatrice, comme le montre le lemme suivant.

On obtient également une caractérisation plus simple des modèles égalitaires comme les modèles égalitaires (c'est-à-dire dans lesquels l'égalité dénote l'égalité) de la théorie ci-dessus. De manière équivalente, on peut les caractériser comme les modèles tels que pour toute règle de réécriture l → r ou équation l = r de RE, l et r ont même dénotation.

Chapitre 2

La théorie des types simples

Deux exemples de théories modulo méritent une attention particulière : la théorie des types simples, aussi appelée logique d'ordre supérieur et la théorie des ensembles. Ce chapitre est consacré à la théorie des types simples. L'intérêt de cette théorie est que beaucoup des propriétés et des algorithmes de la théorie des types simples (en particulier la normalisation des démonstrations et la résolution d'ordre supérieur) seront des cas particuliers de propriétés et d'algorithmes de la déduction modulo.

La théorie naïve des ensembles

La théorie naïve, incohérente, des ensembles, pose un schéma d'axiome, le schéma de compréhension, qui énonce l'existence de tous les ensembles définissables par une proposition P : ∀x 1 ... ∀x n ∃y ∀w (w ∈ y ⇔ P ) où x 1 , ..., x n sont les variables libres de P sauf w.

Pour obtenir un langage de termes on peut skolémiser ce schéma. On obtient alors une infinité de symboles de fonction f

v ∈ R → ¬v ∈ v et donc en notant A la proposition R ∈ R A → ¬A
ce qui permet de construire une suite infinie de réductions

A → ¬A → ¬¬A → ...

De plus cette théorie est incohérente car on peut démontrer la proposition

⊥ 19 axiome A ⊢ ≡ ¬A axiome A ⊢ ≡ A ¬-élim A ⊢ ≡ ⊥ ¬-intro ⊢ ≡ ¬A axiome A ⊢ ≡ ¬A axiome A ⊢ ≡ A ¬-élim A ⊢ ≡ ⊥ ¬-intro ⊢ ≡ A ¬-élim ⊢ ≡ ⊥

La théorie des types simples

La théorie des types simples résout le paradoxe de Russell en classant les objets en fonction du nombre et de la nature de leurs arguments : la théorie des types simples est une théorie multisortée.

Comme la théorie naïve des ensembles, la théorie des types simples comporte des termes qui expriment des ensembles, mais elle comporte aussi des termes qui expriment des relations, et également des fonctions. Les ensembles s'identifient alors simplement avec les relations à un argument unique.

Si R est un terme de relation portant sur des objets de sorte T 1 , ..., T n et t 1 , ..., t n sont des termes de sorte T 1 , ..., T n , la proposition exprimant le fait que les termes t 1 , ..., t n sont liés par la relation R s'écrit en général R(t 1 , ..., t n ). Comme en théorie naïve des ensembles, si on veut rester dans un langage du premier ordre, il faut introduire un symbole ∈ T1,...,Tn et noter cette proposition ∈ T1,...,Tn (R, t 1 , ..., t n ). De même si f est un terme de fonction qui s'applique à des objets de sorte T 1 , ..., T n pour donner un objet de sorte U et t 1 , ..., t n sont des termes de sorte T 1 , ..., T n , le terme exprimant le résultat de l'application de f à t 1 , ..., t n s'écrit en général f (t 1 , ..., t n ). Ici encore, si on veut rester dans un langage du premier ordre, il faut introduire un symbole α T1,...,Tn,U et noter ce terme α T1,...,Tn,U (f, t 1 , ..., t n ).

Quand n = 0 le symbole α U n'a pas grand intérêt, car le terme α U (t) est redondant avec le terme t. En revanche, le symbole ∈ ϕ , qu'on note aussi ε, est beaucoup plus intéressant, car il permet de distinguer le terme t de la proposition ε(t). Le terme t véhicule la même information que la proposition ε(t), mais sous forme d'un terme. On l'appelle contenu de la proposition ε(t). Ce symbole ε et corrélativement la distinction entre les propositions et leur contenu est la principale différence entre cette présentation de la théorie des types et les présentations plus traditionnelles [START_REF] Church | A formulation of the simple theory of types[END_REF]6], qui insistent moins sur la possibilité d'exprimer cette théorie comme une théorie du premier ordre ou une théorie modulo. Nous reviendrons sur ce symbole au paragraphe 2.3.

En théorie des types, il est d'usage d'identifier la relation R avec la fonction qui à n objets t 1 , ..., t n associe le contenu de la proposition R(t 1 , ..., t n ). Il est également d'usage de curryfier les fonctions, c'est-à-dire d'identifier la fonction f avec la fonction qui à x 1 associe la fonction qui à x 2 , ..., x n associe f (x 1 , x 2 , ..., x n ). On peut, de cette manière, considérer toutes les fonctions comme des fonctions d'un argument unique. Ainsi, les sortes qui permettent de classer les objets peuvent simplement être définies inductivement comme le plus petit ensemble qui contient ι (sorte des objets de base) et o (sorte des contenus propositionnels) et qui est clos par la flèche → qui forme la sorte des fonctions d'une sorte vers une autre. Ces sortes sont appelées types simples. Suivant l'usage on notera

T 1 → ... → T n → U le type T 1 → (T 2 → ... → (T n → U )...).
Dans cette présentation de la théorie des types, seuls les symboles de fonction α T,U , et le symbole de prédicat ε sont utiles. Le terme α T1,...,Tn,U (f, t 1 , ..., t n ) se note α Tn,U (...α T1,T2→...→Tn→U (f, t 1 ), ..., t n ). De même, la proposition ∈ T1,...,Tn (R, t 1 , ..., t n ) se note ε(α Tn,o (...α T1,T2→...→Tn→o (R, t 1 ), ..., t n )). Suivant l'usage, dans les exemples, on note

(t u) le terme α T,U (t, u) et (t u 1 ... u n ) le terme (...(t u 1 ) ... u n ).
Comme en théorie naïve des ensembles on pose un schéma d'axiome de compréhension

∃R ∀x 1 ... ∀x n (ε(R x 1 ... x n ) ⇔ P )
où toutes les variables libres de la proposition P sont parmi

| P } x 1 ... x n ) ⇔ P ) ∀x 1 ... ∀x n ((x 1 , ..., x n -→ t) x 1 ... x n ) = t
On peut ensuite transformer ces axiomes en règles de réécriture

ε({x 1 , ..., x n | P } y 1 ... y n ) → [y 1 /x 1 , ..., y n /x n ]P ((x 1 , ..., x n -→ t) y 1 ... y n ) → [x 1 → y 1 , ..., x n → y n ]t 1
On peut démontrer qu'on garde une théorie équivalente en se restreignant à certaines instances de ces schémas, ou ce qui est équivalent à certains symboles de Skolem :

- -S T,U,V de sorte

S T,U,V = x, y, z -→ ((x z) (y z)), où x est de sorte T → U → V , y de sorte T → U et z de sorte T , -K T,U = x, y -→ x où x est de sorte T et y de sorte U , -⇒ = {x, y | ε(x) ⇒ ε(y)}, -∧ = {x, y | ε(x) ∧ ε(y)}, -∨ = {x, y | ε(x) ∨ ε(y)}, -¬ = {x | ¬ε(x)}, -⊥ = {| ⊥}, -∀T = {x | ∀y ε(x y)}, -∃T = {x |
(T → U → V ) → (T → U ) → T → V , -K T,U de sorte T → U → T , -⇒, ∧ et ∨ de sorte o → o → o, -¬ de sorte o → o, -⊥ de sorte o, -∀T et ∃T de sorte (T → o)
→ o, les symboles de fonction α T,U de rang (T → U, T, U ), et le symbole de prédicat ε de rang (o). Les règles de réécriture de la théorie des types simples sont celles de la figure 2.1.

(S x y z) → ((x z) (y z)) (K x y) → x ε( ⇒ x y) → ε(x) ⇒ ε(y) ε( ∧ x y) → ε(x) ∧ ε(y) ε( ∨ x y) → ε(x) ∨ ε(y) ε( ¬ x) → ¬ε(x) ε( ⊥) → ⊥ ε( ∀ x) → ∀y ε(x y) ε( ∃ x) → ∃y ε(x y)
Figure 2.1 -Les règles de réécriture de la théorie des types simples Ce système de réécriture est confluent car il est orthogonal. On montre dans [e] qu'il termine fortement en exhibant un plongement dans le langage des combinateurs simplement typés qui termine fortement par le théorème de W. Tait [START_REF] Tait | Intensional interpretation of functionals of finite type I[END_REF]. La congruence est donc décidable.

Dans cette théorie, on utilise deux notions de fonction qu'il ne faut pas confondre. Le symbole d'individu S, par exemple, est un terme et il a, de ce fait, une sorte. Ce terme exprime un objet de la théorie qui se révèle être une fonction. De ce fait, sa sorte est un type fonctionnel. Le symbole de fonction α T,U , en revanche n'est pas un terme et n'exprime pas un objet de la théorie mais une fonction associant un objet de la théorie à des objets de la théorie. La sorte des objets antécédents et images de cette fonction est définie par le rang de ce symbole. Cette situation est similaire à celle de la théorie des ensembles où il est d'usage de distinguer les ensembles, en tant qu'objets de la théorie des ensembles d'objets de la théorie.

On peut ensuite étendre cette théorie en ajoutant d'autres axiomes : l'axiome de l'infini, l'axiome de descriptions, l'axiome du choix et les axiomes d'extensionnalité. Les axiomes d'extensionnalité peuvent se formuler ainsi :

∀f ∀g ((∀x (f x) = (g x)) ⇒ f = g) ∀x ∀y ((ε(x) ⇔ ε(y)) ⇒ x = y)
2.3 Le symbole ε

Les contenus propositionnels

La principale différence entre cette présentation de la théorie des types et les présentations plus traditionnelles, qui insistent moins sur la possibilité d'exprimer cette théorie comme une théorie du premier ordre ou une théorie modulo, est l'introduction du symbole ε et corrélativement la distinction entre les propositions et leur contenu et entre les connecteurs et les quantificateurs (par exemple, ⇒) et leur contenu (par exemple, ⇒).

Cette distinction est essentielle pour exprimer la théorie des types comme une théorie du premier ordre ou une théorie modulo, puisqu'on ne peut, dans une telle théorie, quantifier que sur des objets, et il faut donc, pour pouvoir quantifier sur les propositions, réifier ces propositions, comme on réifie les prédicats unaires en théorie naïve des ensembles.

On montre dans [b] On pourrait objecter que puisqu'il y a, en théorie des types, une correspondance parfaite entre les propositions et certains termes, on pourrait se passer des propositions, c'est-à-dire considérer les propositions comme des termes comme les autres et n'utiliser que deux sortes d'expressions : le terme t et la métaproposition ⊢ t affirmant que t est démontrable. C'est, par exemple, le point de vue de A. Church [START_REF] Church | A formulation of the simple theory of types[END_REF] et de Andrews [6]. L'inconvénient de ce point de vue est que le fait de considérer les propositions comme des termes, c'est-à-dire les faits comme des objets, n'est pas "ontologiquement neutre". En effet, s'il est facile, et "relativement" neutre, de remplacer les symboles de prédicat et les connecteurs par des symboles de fonction et donc de transformer les propositions sans quantificateurs en termes, exprimer les propositions formées avec des quantificateurs comme des termes suppose, en revanche, des choix ontologiques lourds. En effet, les symboles ∀ et ∃ doivent être appliqués à des fonctions ou des ensembles, il faut donc faire relever la définition de ces notions de la logique et non de la théorie.

La logique du premier ordre (et la déduction modulo), en distinguant les termes (sans lieurs) des propositions (avec quantificateurs) parvient à expliquer la signification des quantificateurs (c'est-à-dire à formuler des règles de déduction) sans utiliser de fonctions ni d'ensembles. La notion de déduction se définit de manière semblable que la théorie contienne des fonctions et des ensembles ou non. Cela permet de séparer clairement la logique, ontologiquement neutre, de la théorie qui exprime les choix concernant les objets du discours. Un autre avantage est que beaucoup de propriétés (complétude, élimination des coupures, ...) et d'algorithmes (démonstration automatique, ...) peuvent être étudiés génériquement indépendamment de la théorie considérée.

Le fait que la théorie considérée, comme la théorie des types simple, permette d'exprimer des fonctions et des ensembles et donc des contenus propositionnels n'impose en rien de se priver de la notion de proposition introduite par la logique du premier ordre et des résultats et algorithmes généraux. Cela demande simplement de distinguer les propositions des contenus propositionnels.

Le langage des termes et l'intentionnalité

Nous l'avons rapidement dit plus haut : en théorie des types, skolémiser les schéma de compréhension donne un langage pour les objets de la théorie des types dans lequel on peut noter x -→ x la fonction identité et {x | ∃y x = 2 × y} l'ensemble des nombres pairs. Cependant, ce langage ne comporte pas de symboles lieurs x -→ ... et {x | ...} dans toute leur généralité. On propose ici une variante plus souple de ce langage.

La substitution des variables de fonction et de prédicat

Certaines formulations anciennes (par exemple, [START_REF] Church | Introduction to mathematical logic[END_REF]) de la théorie des types comprennent des variables de fonction et de prédicat, mais pas, à proprement parler, de termes de fonction ou de prédicat. Par exemple, le schéma d'axiome de récurrence s'écrit ∀P ((P (0) ∧ ∀x (P (x) ⇒ P (Succ(x)))) ⇒ ∀x P (x)) mais il n'y a pas de terme {y | y + 0 = y} qu'on puisse substituer à P . On utilise, en revanche, une nouvelle opération de substitution : substituer P (y 1 , ..., y n ) par une proposition A consiste à substituer chaque proposition de la forme P (t 1 , ..., t n ) par la proposition [t 1 /y 1 , ..., t n /y n ]A.

Par exemple, en substituant la proposition P (y) par la proposition y +0 = y dans le schéma de récurrence, on obtient la proposition

(0 + 0 = 0 ∧ ∀x (x + 0 = x ⇒ Succ(x) + 0 = Succ(x))) ⇒ ∀x (x + 0) = x
Cette notion de substitution est notoirement difficile à définir correctement, surtout quand on sort du cadre de la logique du second ordre. De plus, on introduit ici une nouvelle opération, qui complique le formalisme et rend difficile l'application de résultats ou d'algorithmes généraux.

Le schéma de compréhension

Dans [START_REF] Henkin | Banishing the rule of substitution for functional variables[END_REF], L. Henkin propose de bannir la règle de substitution des variables de fonction et de prédicat dans la logique du second ordre en ajoutant le schéma d'axiome de compréhension. Il montre l'équivalence de son système avec la formulation "traditionnelle" de la logique du second ordre qui utilise cette règle de substitution.

Henkin démontre cette équivalence sans passer par une théorie intermédiaire, dans laquelle le schéma de compréhension est skolémisé. Il n'introduit donc pas réellement de notation pour les fonctions et les prédicats, mais uniquement des axiomes exprimant l'existence de ces objets.

Les combinateurs

Le schéma de compréhension de Henkin peut se généraliser à la théorie des types. Quand on skolémise ce schéma de compréhension, on introduit pour chaque terme purement applicatif t dont les variables libres sont parmi On distingue alors la proposition y + 0 = y et l'ensemble P y,y+0=y ou {y | y + 0 = y}, et de même le nombre y + 0 de la fonction f y,y+0 ou y -→ y + 0 et on peut utiliser la substitution ordinaire pour les variables de fonction et de prédicat. Ainsi, on introduit une nouvelle proposition

({y | y + 0 = y}(0) ∧ ∀x ({y | y + 0 = y}(x) ⇒ {y | y + 0 = y}(Succ(x)))) ⇒ ∀x {y | y + 0 = y}(x)
qui est équivalente à la proposition

(0 + 0 = 0 ∧ ∀x (x + 0 = x ⇒ Succ(x) + 0 = Succ(x))) ⇒ ∀x (x + 0) = x
Mais, contrairement à la présentation avec une substitution particulière pour les variables de prédicat, il est désormais nécessaire d'introduire des axiomes de compréhension skolémisés ou de conversion qui expriment la signification des notations {y 1 , ..., y n | P } et y 1 , ..., y n -→ t et qui permettent de montrer l'équivalence des deux propositions ci-dessus.

A cause de leur ressemblance avec les supercombinateurs de R.M.J. Hughes [START_REF] Hughes | Super-combinators, a new implementation method for applicative languages[END_REF] nous avons dans [a] appelé ces symboles hypercombinateurs. Cette terminologie est, en fait, assez mal choisie, car ces symboles sont précisément ceux que H.B. Curry appelle combinateurs dans [START_REF] Curry | The combinatory foundations of mathematical logic[END_REF][START_REF] Curry | Combinatory logic[END_REF] (avant que ce terme ne serve à désigner des choses assez disparates, comme les termes clos du λ-calcul, ou les symboles de n'importe quel langage du premier ordre servant à exprimer des fonctions).

Dans une présentation utilisant la déduction modulo, les axiomes de conversion peuvent être transformés en règles de réécriture. Substituer une variable de fonction ou de prédicat par un combinateur puis normaliser la proposition obtenue donne le même résultat que la substitution définie au paragraphe 2.4.1. On montre ainsi, au moins pour la logique du second ordre, que la formulation avec des combinateurs est une extension conservatrice de la formulation du paragraphe 2.4.1. Mais c'est précisément cette décomposition entre substitution et réduction qui simplifie le formalisme.

L'équivalence de la présentation de la théorie des types avec le schéma de compréhension et avec des combinateurs est une simple conséquence du théorème de Skolem (de plus, seuls les quantificateurs existentiels les plus extérieurs à la formule sont skolémisés, ce qui permet une démonstration d'équivalence particulièrement simple).

On peut noter x 1 , ..., x n -→ t le combinateur f x1,...,xn,t . Mais l'impression d'avoir un symbole lieur dans le langage est trompeuse. D'une part toutes les variables de t doivent être liées dans x 1 , ..., x n -→ t, on n'a donc pas le terme x -→ y, d'autre part le terme t ne doit pas, lui-même, contenir de symboles de Skolem. On n'a donc pas le terme x -→ (y -→ y), ni a fortiori le terme x -→ (y -→ x) qui viole les deux conditions à la fois.

Pour construire un langage un peu plus libéral on peut tenter d'utiliser un schéma de compréhension plus général. Le schéma de compréhension fermé

∃R ∀x 1 ... ∀x n (ε(R x 1 ... x n ) ⇔ A) ∃f ∀x 1 ... ∀x n (f x 1 ... x n ) = t
dans lequel toutes les variables libres de A (resp. t) sont parmi x 1 , ..., x n est équivalent au schéma de compréhension ouvert dans lequel cette condition est relâchée. Mais, on montre dans [a] que le langage obtenu en skolémisant ces deux schémas est très différent. En skolémisant l'instance du schéma de compréhension ouvert ∀y ∃f ∀x (f x) = y on introduit un symbole de fonction unaire f et l'axiome ∀y ∀x (f (y) x) = y. On peut noter x -→ y, le terme f (y) dans lequel la variable y est libre et qui est la fonction constante identiquement égale à y. On peut donc ainsi avoir des variables libres dans les abstractions. Il faut, cela dit, éviter de noter x -→ x le terme f (x) qui est la fonction constante identiquement égale à x. Ce terme doit se noter x ′ -→ x dans lequel on a renommé la variable liée pour éviter la confusion avec la variable libre. On peut aussi appliquer le symbole f à un terme contenant une abstraction, par exemple au terme y -→ y ce qui donne le terme f (y -→ y) qu'on peut noter x -→ (y -→ y). En revanche, il faut éviter de noter

x -→ (y -→ x) le terme f (y -→ x), mais il faut le noter x ′ -→ (y -→ x). La variable libre dans y -→ x ne peut donc plus être abstraite. Il semble donc impossible de construire une fonction qui à x et y associe x en abstrayant les deux variables l'une après l'autre.

On montre dans [a] qu'il est nécessaire, pour construire cette fonction, d'utiliser une instance du schéma de compréhension binaire ∃f ∀x ∀y (f x y) = x

En effet, cette instance du schéma de compréhension est indépendante du schéma de compréhension unaire, car on peut construire un modèle du schéma de compréhension unaire dans lequel cette proposition n'est pas valide. Le schéma de compréhension unaire est donc plus faible que le schéma de compréhension général.

En revanche le schéma de compréhension ternaire est équivalent au schéma général puisque les instances correspondant aux combinateurs S et K suffisent. Nous laissons ouvert le problème de l'équivalence du schéma de compréhension binaire et du schéma de compréhension général.

Le λ-calcul

La λ-calcul introduit par Church [START_REF] Church | The calculi of lambda-conversion[END_REF] et utilisé, également par Church, en théorie des types [START_REF] Church | A formulation of the simple theory of types[END_REF] consiste à généraliser l'utilisation des lieurs de manière à pouvoir former le terme x -→ (y -→ x) qu'on note alors λx λy x. Par rapport aux langages de combinateurs, le λ-calcul introduit une plus grande homogénéité puisqu'il devient possible de lier n'importe quelle variable, y compris celles qui apparaissent libres dans les abstractions.

On pose alors l'axiome (β)

(λx t) u = [u/x]t
qui peut se transformer en une règle de réécriture, la règle de β-réduction

(λx t) u → [u/x]t
Cependant, le λ-calcul introduit une nouvelle difficulté qui est la nécessité de substituer sous les abstractions. Les formulations de la théorie des types qui utilisent des combinateurs peuvent facilement s'exprimer comme des théories du premier ordre (en introduisant des symboles d'application α T,U et un symbole ε). La substitution dans les termes est donc la substitution simple (le remplacement) de la logique du premier ordre. Ce n'est plus le cas avec la formulation de la théorie des types utilisant le λ-calcul qui demande à nouveau une substitution particulière : quand on substitue la variable x par le terme u dans le terme λy x, il faut substituer x par u sous le λ, et quand on substitue la variable x par le terme y dans le terme λy x, il faut, en outre, renommer la variable liée y de manière à éviter les captures.

L'objectif de bannir la règle de substitution des variables de fonction et de prédicat, qui nous avait amené au langage des combinateurs, est donc partiellement abandonné puisqu'il faut à nouveau introduire une substitution particulière. Cette substitution est à l'origine de bien des bizarreries de la formulation de la théorie des types utilisant le λ-calcul, par exemple du traitement assez subtil de la portée des variables dans l'algorithme d'unification d'ordre supérieur de G. Huet [START_REF] Huet | A unification algorithm for typed lambda calculus[END_REF][START_REF] Huet | Résolution d'équations dans les Langages d[END_REF][START_REF] Snyder | Higher-order unification revisited : complete sets of transformations[END_REF]. Ce point est discuté dans [c]. Cependant, la simplicité et l'uniformité du λ-calcul font que cette formulation de la théorie des types est souvent préférée à celle utilisant des combinateurs.

L'équivalence entre les formulations utilisant la règle de substitution des variables de prédicats et de fonctions, le schéma de compréhension et des combinateurs est simple à établir. En revanche, l'équivalence de ces formulations avec celles utilisant le λ-calcul est un peu plus difficile. L'idée est de traduire les termes du λ-calcul dans le langage des combinateurs. Cette traduction s'appelle l'ascension des variables (λ-lifting) [54, a]. Le seul cas intéressant est celui des abstractions. Pour traduire un terme de la forme λx 1 ... λx n t, on commence par traduire le terme t. On obtient un terme t ′ qui contient, outre les variables x 1 , ..., x n , des variables y 1 , ..., y p et des combinateurs c 1 , ..., c q . On remplace ces combinateurs par des variables z 1 , ..., z q , ce qui donne un terme t ′′ et on définit la traduction du terme λx 1 ... λx n t comme ((y 1 , ..., y p , z 1 , ..., z q , x 1 , ..., x n -→ t ′′ ) y 1 ... y p c 1 ... c q ). Le problème est que pour montrer l'équivalence de ces deux formulations de la théorie des types, on a besoin de l'axiome d'extensionnalité dans les deux formulations de la théorie. Par exemple, dans la formulation utilisant le λ-calcul, la proposition ((λx λy λz x) w w) = ((λx λy λz y) w w) est démontrable car elle se réduit sur λz w = λz w

En revanche sa traduction

((x, y, z -→ x) w w) = ((x, y, z -→ y) w w)
demande l'axiome d'extensionnalité pour être démontrée. On montre dans [a], en construisant un modèle très simple, qu'en l'absence de cet axiome, cette proposition est indépendante de la théorie des types. En fait, on peut dire que l'axiome β contient un soupçon d'extensionnalité car il permet la substitution sous les abstractions et identifie donc les termes ((λx λy λz x) w w) et λz w, qui en toute rigueur ne sont pas intentionnellement identiques. Ce point sera discuté au paragraphe 2.4.7.

De plus, diverses variantes de la traduction du λ-calcul dans le langage des combinateurs donnent des résultats un peu différents. Par exemple, si on traduit les abstractions en bloc, comme ci-dessus, dans la proposition ((λx λy λz x) w w) = ((λy λx λz x) w w)

on obtient une proposition qui ne peut pas se démontrer sans l'axiome d'extensionnalité. En revanche, si on traduit les abstractions une par une, on obtient la proposition

((d, e, x -→ (d e x)) (x, c, y -→ (c y)) (x, z -→ x) w w) = ((d, e, y -→ (d e)) (c, x -→ (c x)) (x, z -→ x) w w)
qui est démontrable sans l'axiome d'extensionnalité, car elle se réduit sur

((x, z -→ x) w) = ((x, z -→ x) w)
Une autre traduction, qui n'utilise que les combinateurs S et K [START_REF] Barendregt | The lambda-calculus, its syntax and semantics[END_REF][START_REF] Hindley | Introduction to combinators and λ-calculus[END_REF][START_REF] Krivine | Lambda-calcul, types et modèles[END_REF], utilise l'extensionnalité moins souvent encore, mais ne peut pas non plus s'en passer totalement.

On peut alors se demander si le problème n'est pas davantage dans la traduction que dans le λ-calcul luimême. En faisant l'hypothèse que toutes les traductions conservent les termes purement applicatifs (c'est-àdire sans abstractions) du λ-calcul, cette question est formulée dans [a] comme le problème, que nous laissons ouvert, de trouver une proposition sans abstractions qui soit démontrable dans la présentation utilisant le λ-calcul, mais pas dans celle utilisant les combinateurs.

Le calcul des substitutions explicites

Si on prend la formulation de la théorie des types utilisant le λ-calcul comme référence, les combinateurs permettent de donner une présentation au premier ordre qui est extensionnellement équivalente, c'est-à-dire que les deux formulations sont équivalentes quand l'axiome d'extensionnalité est posé dans les deux cas. Si on ne pose pas l'axiome d'extensionnalité, les deux théories ne sont plus équivalentes, et on doit poser des axiomes d'extensionnalité faible (les axiomes de Curry [START_REF] Barendregt | The lambda-calculus, its syntax and semantics[END_REF][START_REF] Hindley | Introduction to combinators and λ-calculus[END_REF][START_REF] Krivine | Lambda-calcul, types et modèles[END_REF]) dans la formulation utilisant les combinateurs de manière à obtenir l'équivalence. Ces axiomes sont notoirement compliqués et on ne sait pas bien les transformer en règles de réécriture dans une théorie modulo.

Parallèlement au langage des combinateurs, les indices de N.G. De Bruijn [START_REF] De Bruijn | Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem[END_REF], puis les combinateurs catégoriques [START_REF] Curien | Categorical combinators, sequential algorithms and functional programming, second edition[END_REF] et le calcul des substitutions explicites ou λσ-calcul [1,[START_REF] Curien | Confluence properties of weak and strong calculi of explicit substitutions[END_REF] ont fourni d'autres langages du premier ordre pour noter les fonctions et, comme nous allons le voir, d'autres formulations au premier ordre de la théorie des types qui sont intentionnellement équivalentes à la formulation utilisant le λ-calcul.

Les indices de De Bruijn sont, au départ, une notation alternative pour le λ-calcul. S'appuyant sur l'idée que les noms des variables liées servent uniquement à relier une occurrence d'une telle variable à son lieur, De Bruijn a proposé de remplacer chaque occurrence de variable liée par un nombre entier, qui peut s'assimiler à l'adresse relative du lieur et qui est le nombre de lieurs qu'il faut traverser pour arriver à celui qui correspond à cette variable.

Ainsi, le terme λx λy (x y λz (z y)), par exemple, s'écrit λλ(2 1 λ(1 2)). Ce terme peut, à son tour, se lire comme un terme d'un langage du premier ordre contenant une infinité de symboles d'individu 1, 2, 3, ..., un symbole de fonction unaire λ et un symbole de fonction binaire α pour l'application.

On peut remarquer que ce langage contient bien davantage que le λ-calcul. Si le terme λ1 est naturellement l'expression du terme λx x, son sous-terme, le terme 1, ne représente aucun λ-terme, à moins de le lire dans un contexte de variables, par exemple, x, y, z, auquel cas, il exprime le terme ouvert x. Les termes ouverts du λ-calcul peuvent donc à la fois s'exprimer comme des termes clos dans un contexte de variables ou comme des termes ouverts du λ-calcul avec des indices de De Bruijn. Par exemple, le terme x peut ou bien s'exprimer comme le terme 1 dans un contexte x, y, z ou bien comme le terme x.

Dans le λ-calcul avec des indices de De Bruijn, l'axiome de β-conversion s'exprime ainsi

((λt) u) = [u/1]t
Cet axiome peut se transformer en une règle de réécriture, la β-reduction

((λt) u) → [u/1]t
La substitution du [u/n]t désigne maintenant la substitution de l'indice de De Bruijn n par le terme u dans t, il ne s'agit donc pas de l'opération de substitution simple (de remplacement) mais d'une autre opération qui se définit ainsi par récurrence sur la structure de t

-[u/n]x = x, -[u/n](t 1 t 2 ) = ([u/n]t 1 [u/n]t 2 ), -[u/n]λt = λ[lft(u, 0)/n + 1]t, -[u/n]m = m -1 si m > n, -[u/n]m = u si m = n, -[u/n]m = m si m < n.
où le terme lft(u, i) (qui se lit "incrémentation (lift) de u à partir de i") est défini par récurrence sur la structure de u

-lft(x, i) = x, -lft((u 1 u 2 ), i) = (lft(u 1 , i) lft(u 2 , i)), -lft(λu, i) = λ(lft(u, i + 1)), -lft(m, i) = m + 1 si m > i, -lft(m, i) = m si m ≤ i.
Par exemple le terme λx λy ((λz λw (x z)) y), qui se réduit λx λy λw (x y), s'exprime avec des indices de De Bruijn par le terme λλ((λλ(4 2)) 1). Ce terme se réduit sur λλ( 32) qui qui est bien la traduction du terme λx λy λw (x y).

[1/1]λ(4 2)) = λλλ([lft(1, 0)/2](4 2)) = λλλ([2/2](4 2)) = λλλ(
Cette notion de substitution est assez délicate à définir car elle doit prendre en compte deux phénomènes : d'une part la nécessité de décrémenter les indices libres (c'est-à-dire désignant une variable liée au dessus du radical) dans t (par exemple la variable x exprimée par l'indice 4 dans le terme initial est décrémentée et exprimée par l'indice 3 dans le terme final), d'autre part la nécessité d'incrémenter les indices libres dans u quand on traverse une abstraction (par exemple, la variable y représentée par l'indice 1 dans le terme initial est représentée par l'indice 2 dans le terme final).

Ce calcul présente deux inconvénients. D'une part, comme c'était déjà le cas pour le λ-calcul, un algorithme de substitution extérieur aux règles de réécriture est nécessaire à la définition de la réduction. Ce système de réécriture contient, de ce fait, un nombre infini de règles. D'autre part, les variables libres ne sont pas affectées par ces opérations de substitution et d'incrémentation. De ce fait, l'opération de réduction sur les termes ouverts ne commute pas avec la substitution simple (le remplacement) d'une telle variable. Par exemple le terme (λ(x 1) y) se réduit sur (x y), mais si on substitue la variable x par le terme (z 1) on obtient le terme (λ(z 1 1) y) qui se réduit sur (z y y) alors que si on substitue la variable x par le terme (z 1) dans le terme (x y), on obtient le terme (z 1 y).

En revanche la réduction commute avec une autre forme de substitution des variables qui correspond à la substitution du λ-calcul et qui demande d'incrémenter les indices libres du terme substitué quand on passe sous un λ. Ainsi, le terme (λ(x 1) y) se réduit sur (x y), et si on substitue la variable x par le terme (z 1) on obtient le terme (λ(z 2 1) y) qui se réduit sur (z 1 y) qui est bien le terme obtenu en substituant la variable x par le terme (z 1) dans le terme (x y).

Le calcul des combinateurs catégoriques et le calcul des substitutions explicites pallient ces inconvénients du λ-calcul avec des indices de De Bruijn. D'une part, il permettent de ne plus recourir à une opération externe de substitution et ils ont un nombre fini de règles. En corollaire de cela, la substitution des variables libres et la réduction commutent, comme dans tout système de réécriture du premier ordre.

L'idée de ce calcul est d'internaliser la notion de substitution comme un symbole du langage au même titre que λ ou α. On note t[s] le terme t auquel est appliquée la substitution s. Les termes sont à présent de cinq formes : indices de De Bruijn, variables, applications d'un terme à un autre, abstractions et applications d'une substitution à un terme.

Cet opérateur prend en argument un terme et une substitution explicite qui est une liste u 1 , ..., u n de termes. Des règles de réécriture permettent ensuite de réduire le terme t[u 1 , ..., u n ] en substituant dans t l'indice 1 par u 1 , l'indice 2 par u 2 , ..., l'indice n par u n et en décrémentant de n tous les autres indices libres. Pour construire ces listes, on a besoin de la liste vide, notée id car c'est la substitution identité, et du symbole "cons" noté ".". Deux autres symboles sont encore nécessaires : la substitution ↑ qui incrémente les indices libres d'un terme et le symbole • qui permet de composer les substitutions.

Les règles de réécriture du λσ-calcul sont les suivantes

(λa)b → a[b.id] (a b)[s] → (a[s] b[s]) 1[a.s] → a a[id] → a (λa)[s] → λ(a[1.(s • ↑)]) (a[s])[t] → a[s • t] id • s → s ↑ • (a.s) → s (s 1 • s 2 ) • s 3 → s 1 • (s 2 • s 3 ) (a.s) • t → a[t].(s • t) s • id → s 1. ↑→ id 1[s].(↑ • s) → s
La première règle est la β-réduction, les autres, appelées règles de σ-réduction, permettent de propager une substitution explicite dans un terme.

Dans ce calcul, comme dans tout système de réécriture du premier ordre, la réduction commute avec la substitution simple (le remplacement) des variables. Ainsi, le terme (λ(x 1) y) se réduit sur (x[y.id] y), et si on substitue la variable x par le terme (z 1) on obtient le terme (λ(z 1 1) y) qui se réduit sur (z[y.id] y y) qui est le terme obtenu, après normalisation de la substitution, en substituant la variable x par le terme (z 1) dans le terme (x[y.id] y).

Quand on étend le λ-calcul avec des indices de De Bruijn en ajoutant des substitutions explicites, on peut envisager une autre traduction du λ-calcul dans ce formalisme. Dans la traduction présentée plus haut, quand on traduisait le terme λx (y x) en conservant y comme une variable libre on obtenait le terme λ(y 1).

Dans le λ-calcul, si on substitue la variable y par le terme t, il faut éventuellement renommer la variable liée x de manière à éviter les captures. Dans le λ-calcul avec des indices de De Bruijn, il faut de même, comme nous l'avons vu, incrémenter les indices libres de t. Donc, bien que le λ-calcul avec des substitutions explicites soit un langage du premier ordre, la substitution des variables de ce langage du premier ordre qui correspond à celle du λ-calcul n'est pas la substitution simple (le remplacement). Cette opération de substitution peut se décomposer d'une part en une opération d'incrémentation et d'autre part en une substitution simple (un remplacement). Comme le λσ-calcul contient des opérateurs explicites d'incrémentation, on peut préparer cette incrémentation en appliquant cet opérateur à la variable y, on obtient alors le terme λ(y[↑] 1) comme traduction de λx (y x). À présent, si on substitue simplement (on remplace) la variable y par le terme 1 on obtient le terme λ(1[↑] 1) c'est-à-dire λ(2 1).

Dans [c], puis dans [i], nous avons appelé "précuisson" ("pre-cooking") cette traduction qui anticipe l'incrémentation du terme substitué. Si on note t F la précuisson du λ-terme t, nous avons montré, dans [c], le résultat clé

([u/x]t) F = [x → u F ]t F
où t/x la substitution du λ-calcul et x → t est la substitution simple (le remplacement). Autrement dit, la précuisson est un homomorphisme du λ-calcul dans le λσ-calcul qui transforme la substitution d'un calcul en la substitution de l'autre.

Pour utiliser le calcul des substitutions explicites comme langage des fonctions de la théorie des types simples, il faut pouvoir associer un type à chaque terme du calcul. Ici, un nouveau problème surgit. Si on sait donner le type ι → ι au terme λ1, qui exprime le λ-terme λx x, il est plus difficile, en revanche, de donner un type au terme 1 qui n'exprime un λ-terme que dans un contexte de variable. On doit donc connaître le type des variables de ce contexte pour pouvoir associer un type à ce terme [1,[START_REF] Curien | Un résultat de complétude pour les substitutions explicites[END_REF]. Si on considère un contexte de trois variables x, y, z de types respectifs A, B, C alors le terme 1 a le type A, le terme 2 le type B, le terme

1 Γ A de sorte AΓ ⊢ A α Γ A,B de rang (Γ ⊢ A → B, Γ ⊢ A, Γ ⊢ B) λ Γ A,B de rang (AΓ ⊢ B, Γ ⊢ A → B) [] Γ,Γ ′ A de rang (Γ ′ ⊢ A, Γ ⊢ Γ ′ , Γ ⊢ A) id Γ de sorte Γ ⊢ Γ ↑ Γ A de sorte AΓ ⊢ Γ . Γ,Γ ′ A de rang (Γ ⊢ A, Γ ⊢ Γ ′ , Γ ⊢ AΓ ′ ) • Γ,Γ ′ ,Γ ′′ de rang (Γ ⊢ Γ ′′ , Γ ′′ ⊢ Γ ′ , Γ ⊢ Γ ′ )
Le λσ-calcul typé avec des variables de termes est confluent [START_REF] Ríos | Contributions à l'étude des λ-calculs avec des substitutions explicites[END_REF] et il termine faiblement [START_REF] Muñoz-Hurtado | Un calcul de substitutions pour la représentation des preuves partielles en théorie des types[END_REF][START_REF] Muñoz-Hurtado | A calculus of substitutions for incomplete-proof representation in type theory[END_REF][START_REF] Muñoz-Hurtado | A left-linear variant of λσ[END_REF][START_REF] Goubault-Larrecq | A proof of weak termination of the simply typed λσ-calculus[END_REF] mais P.-A. Melliès [START_REF] Melliès | Typed λ-calculi with explicit substitutions may not terminate[END_REF] a montré qu'il ne termine pas fortement.

À ces symboles, nous avons ajouté dans [i] les symboles

⇒ de sorte ⊢ o → o → o ∧ de sorte ⊢ o → o → o ∨ de sorte ⊢ o → o → o ¬ de sorte ⊢ o → o ⊥ de sorte ⊢ o ∀T de sorte ⊢ (T → o) → o ∃T de sorte ⊢ (T → o) → o et le symbole de prédicat ε de rang (⊢ o)
Les variables libres dans ce langage ont une sorte de la forme Γ ⊢ T , c'est-à-dire qu'à chaque variable est associé non seulement un type, mais aussi un contexte qui est celui dans lequel les termes qu'on substitue à cette variable doivent être typés. On peut montrer que si un λ-terme t contenant des variables libres x 1 , ..., x n de type T 1 , ..., T n est bien typé alors sa précuisson est un λσ-terme bien typé contenant les variables libres x 1 , ..., x n de sorte ⊢ T 1 , ..., ⊢ T n .

Sur ce langage, on définit ensuite le système de réécriture de la figure 2.2. La première règle est la règle de β-réduction, le groupe suivant est constitué des règles de σ-réduction, le dernier groupe est constitué des règles de réduction associées aux symboles ⇒, ∧, ... On peut également ajouter une règle de réduction correspondant à la η-réduction du λ-calcul, qui permet d'incorporer dans la réduction une partie plus importante de l'axiome d'extensionnalité :

λ(a 1) → b si a = σ b[↑]
On montre dans [i] que ce système de réécriture est confluent. On montre également qu'il est faiblement normalisable en le plongeant dans le λσ-calcul typé.

On montre dans [i] que la théorie modulo constituée de ce système de réécriture et de l'ensemble vide d'axiomes est intentionnellement équivalente à la formulation de la théorie des types utilisant le λ-calcul. En effet, une proposition t est démontrable dans la théorie des types utilisant le λ-calcul si et seulement si la proposition ε(t F ) est démontrable dans cette présentation de la théorie des types. De plus, la structure des démonstrations est conservée : les étapes de calcul correspondent aux étapes de calcul, les étapes de déduction aux étapes de déduction. Contrairement à la formulation de la théorie des types avec des combinateurs, il n'est jamais nécessaire de faire appel aux axiomes d'extensionnalité ou aux axiomes de Curry pour démontrer une proposition qui se démontre sans ces axiomes dans la théorie des types utilisant le λ-calcul.

Cette formulation de la théorie des types est celle que nous utiliserons dans les chapitres suivants. Nous allons, cependant, conclure ce paragraphe consacré aux langages des termes en théorie des types par la présentation de deux autres langages qui sont plus prospectifs.

Les combinateurs, à nouveau

On construit, dans [i], un modèle de la théorie des types simples utilisant les substitutions explicites. Les sortes de cette théorie étant de la forme

Γ ⊢ T et Γ ⊢ ∆,
(M U1 × ... × M Up ) M Tn ... M T 1 .
Cette double notion de fonctionnalité (puisque la flèche → et le symbole ⊢ dans les sortes Γ ⊢ ∆ sont interprétés, l'une comme l'autre comme des constructeurs d'espaces fonctionnels) rappelle l'origine catégorique du calcul des substitutions explicites, puisque les catégories cartésiennes closes comportent deux flèches : celle des morphismes, ici ⊢, et l'exponentielle, ici →. Une substitution, en revanche, se traduit par une suite finie de termes. L'application d'une substitution à un terme se traduit également par le combinateur app.

(λa)b → a[b.id] (a b)[s] → (a[s] b[s]) 1[a.s] → a a[id] → a (λa)[s] → λ(a[1.(s • ↑)]) (a[s])[t] → a[s • t] id • s → s ↑ • (a.s) → s (s1 • s2) • s3 → s1 • (s2 • s3) (a.s) • t → a[t].(s • t) s • id → s 1. ↑→ id 1[s].(↑ • s) → s ε( ⇒ x y) → ε(x) ⇒ ε(y) ε( ∧ x y) → ε(x) ∧ ε(y) ε( ∨ x y) → ε(x) ∨ ε(y) ε( ¬ x) → ¬ε(x) ε( ⊥) → ⊥ ε( ∀T x) → ∀y ε(x y) ε( ∃T x) → ∃y ε(x y)
(app n (app p a b) c) → (app p-1 (app n a c) (app n b c)) si n < p (1) (app n 1 p c) → c si p = n + 1 (2) (app n 1 p c) → 1 p-1 si n + 1 < p (3) (app n (↑ p a) b) → a si p = n (4) (app n (↑ p a) b) → (↑ p-1 (app n a b)) si n < p (5) (↑ n (app p a b)) → (app p+1 (↑ n a) (↑ n b)) si n ≤ p (6) (↑ n 1 p ) → 1 p+1 si n < p (7) (↑ n (↑ p a)) → (↑ p+1 (↑ n a)) si n ≤ p (8)
Ces symboles sont donc des combinateurs au sens du paragraphe 2.4.3 et les premières règles de réécriture qu'on voudrait poser sont

(1 n x 1 ... x n ) → x n (↑ n a x 1 ... x n y ) → (a x 1 ... x n ) (app n a b x 1 ... x n ) → (a x 1 ... x n (b x 1 ... x n ))
On traduit un λ-terme t exprimé avec des indices de De Bruijn dans un contexte de longueur n comme le terme |t| n .

-

|k| n = (↑ n-1 (...(↑ n-k+1 1 n-k+1 )...)) -|(a b)| n = (app n |a| n |b| n ) -|λa| n = |a| n+1 .
Il est facile de voir que ce système de réécriture ne simule pas la β-réduction. Un β-radical de la forme ((λa) b) se traduit par le terme (app n |a| n+1 |b| n ) qui n'est pas, en général, un radical. Un tel β-radical est caractérisé par le fait que l'argument du symbole app n est traduit dans un contexte plus long que n. Il faut ici distinguer les différents cas en fonction de la forme de a. On peut montrer, quoi que cela soit fastidieux, que si a → β b alors |a| n → |b| n . La réciproque de ce résultat, en revanche, est fausse car le terme ((λ(1 y)) z) se traduit par (app 2 (app

3 1 3 (↑ 2 1 2 )) (↑ 1 1 1 )) qui se réduit sur (app 2 (app 2 1 3 (↑ 1 1 1 )) (app 2 (↑ 2 1 2 ) (↑ 1 1 1 )
)) qui est la traduction de (((λ1) z) ((λy) z)). On paie ici le prix de la confusion entre application d'un terme à un autre et d'une substitution à un terme. Une solution est peut-être d'introduire deux variantes du combinateur app.

On peut remarquer que si la règle (app n 1 n+1 b) → b n'est pas une conséquence du système de réécriture naïf ci-dessus, c'est une conséquence de ce système de réécriture et de l'axiome d'extensionnalité. En effet le terme (app n 1 n+1 b x 1 ... x n ) se réduit sur (1 n+1 x 1 ... x n (b x 1 ... x n )) puis sur (b x 1 ... x n ). On peut montrer qu'il en est de même des autres règles. On retrouve ici cette idée que le λ-calcul contient une forme faible d'extensionnalité qui est absente du langage des combinateurs. La solution traditionnelle à ce problème est d'ajouter les axiomes de Curry à la théorie des combinateurs, mais à la différence des axiomes de Curry, l'extension proposée ici s'exprime sous forme d'un ensemble de règles de réécriture et non d'axiomes équationnels.

Alors que je travaillais sur ce système de réécriture, j'ai appris qu'il avait été proposé indépendamment, à quelques variations près par H. Goguen et J. Goubault-Larrecq [START_REF] Goguen | Sequent combinators : a Hilbert system for the lambda calculus[END_REF]. Goguen et Goubault sont allés beaucoup plus loin que moi dans l'étude de ce système. En particulier, ils ont démontré sa confluence, alors que je n'avais montré que la confluence locale, et ils ont montré que le calcul simplement typé n'avait que la propriété de terminaison faible. Il est remarquable aussi que le contre-exemple à la terminaison forte qu'ils proposent ait été découvert par un programme de recherche aléatoire et n'ait qu'un lointain rapport avec le contre-exemple proposé par Melliès à la forte normalisation du λσ-calcul typé.

Le calcul faible des substitutions explicites

On l'a dit plusieurs fois, le λ-calcul contient une forme d'extensionnalité faible qui n'est pas présente dans le calcul des combinateurs. Cette forme d'extensionnalité est la possibilité de substituer sous un λ, ce qui permet de transformer le terme ((λx λy λz x) w w) ou le terme en ((λx λy λz y) w w) en λz w alors que dans le calcul des combinateurs le terme ((x, y, z -→ t) w w) ne peut pas se réduire. Cela est dû au fait qu'en λ-calcul, la possibilité de substituer sous les abstractions permet de n'avoir que des fonctions unaires et d'itérer la construction de fonctions unaires pour construire les fonctions n-aires, alors que cela est impossible dans le calcul des combinateurs qui est essentiellement n-aire.

Le calcul des substitutions explicites, permet d'avoir la même forme d'extensionnalité que le λ-calcul tout en restant un langage de premier ordre. La possibilité de substituer sous les abstractions dans ce calcul s'exprime par la règle

(λa)[s] → λ(a[1.s• ↑])
On peut vouloir garder la notation du λ-calcul qui permet d'abstraire une variable libre dans un terme, où que soit l'occurrence de cette variable, mais rejeter la β-réduction et l'extensionnalité qu'elle contient. En effet, on peut argumenter que du point de vue intentionnel les termes ((λx λy λz x) w w) et λz w n'expriment pas le même algorithme et que c'est une erreur du λ-calcul que d'identifier ces termes (argumentation, qui demande, cela dit, d'avoir résolu l'épineux problème de l'égalité intentionnelle de deux fonctions).

J.R. Hindley propose dans [START_REF] Hindley | Combinatory reductions and lambda reductions compared[END_REF] une notion de réduction dans le λ-calcul sans substitution sous les abstractions et montre son équivalence avec celle du calcul des combinateurs. Dans le λσ-calcul, interdire la propagation des substitutions sous les abstractions est particulièrement simple, puisqu'il suffit de supprimer la règle ci-dessus. On aboutit alors au λσ-calcul faible [START_REF] Curien | Confluence properties of weak and strong calculi of explicit substitutions[END_REF][START_REF] Martin-Löf | [END_REF][START_REF] Maranget | Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems[END_REF][START_REF] Th | Functional back-ends within the lambda-sigma calculus[END_REF].

Il devient alors naturel de se poser la question de l'équivalence entre le λσ-calcul faible et le calcul des combinateurs, puisque l'un comme l'autre revendiquent la pureté intentionnelle. Hélas, l'ascension des variables, traduction du λσ-calcul faible dans le langage des combinateurs, ne respecte pas la réduction. Par exemple, les termes λy x et ((λx λy x) x) ne sont pas convertibles dans le λσ-calcul faible, mais leur traduction est la même : ((x, y -→ x) x). Ici, le problème semble venir de l'ascension des variables elle-même, qui n'est pas intentionnellement neutre.

Cependant, un premier pas vers un théorème d'équivalence entre λσ-calcul faible et combinateurs a été effectué par T. Strahm [START_REF] Strahm | Partial applicative theories and explicit substitutions[END_REF] qui a montré qu'on pouvait, en revanche, traduire les combinateurs dans le λσ-calcul faible en conservant la convertibilité.

En conclusion : quel langage ?

En conclusion de ce long paragraphe consacré aux langage des termes en théorie des types simples, on peut dire qu'on a le choix entre deux langages du premier ordre : celui des combinateurs et celui du calcul des substitutions explicites. Ce dernier est équivalent au λ-calcul ce qui signifie qu'une partie de l'extensionnalité est incluse dans les règles de réduction. On peut voir cela comme un point positif (davantage est transféré du raisonnement vers le calcul) ou comme un point négatif si on cherche la pureté intentionnelle. Le langage des combinateurs, en revanche, est plus intentionnel.

Le langage des substitutions explicites est plus complexe à définir que celui des combinateurs, mais les exemples sont plus simples à écrire du fait de la présence d'un opérateur d'abstraction.

Nous avons également présenté deux autres langages, les combinateurs étendus et le λσ-calcul faible, qui sont plus prospectifs et demandent à être davantage étudiés.

La complétude

Formuler la théorie des types comme une théorie du premier ordre (ou une théorie modulo) permet de lui appliquer des théorèmes et des algorithmes généraux valables pour toutes les théories du premier ordre. Le premier exemple auquel on pense est le théorème de complétude.

C'est un résultat du folklore qu'on peut déduire le théorème de complétude de Henkin [START_REF] Henkin | Completeness in the theory of types[END_REF] de celui de Gödel en utilisant une formulation au premier ordre de la théorie des types. Nous avons détaillé la démonstration de ce résultat dans [b].

En appliquant le théorème de complétude de Gödel à une formulation de la théorie des types comme une théorie du premier ordre, on montre qu'une proposition P est démontrable en théorie des types si et seulement si elle est valide dans tous les modèles de cette théorie. La classe des modèles de la théorie des types est, cela dit, plus vaste que la classe des modèles de Henkin. Les modèles de Henkin sont les modèles égalitaires et fonctionnels de la théorie des types. Un premier lemme montre que la classe des modèles égalitaires valide les même propositions que la classe de tous les modèles des axiomes de l'égalité. Un second lemme, homologue du théorème de l'effondrement d'A. Mostovski, montre que la classe des modèles fonctionnels égalitaires valide les même propositions que la classe de tous les modèles égalitaires de l'axiome d'extensionnalité. Ce deuxième lemme n'est vrai que pour les modèles égalitaires et donc cette condition doit être incluse dans la définition des modèles de Henkin (ce que Henkin n'avait pas fait explicitement) comme l'avait déjà remarqué Andrews [5].

Ce théorème de complétude peut aussi s'appliquer à la théorie des types intentionnelle, c'est-à-dire privée de l'axiome d'extensionnalité, et on sait que les modèles de Henkin sont insuffisants pour cela, car ils valident toujours l'axiome d'extensionnalité.

La skolémisation

Un deuxième exemple de théorème général qui peut s'appliquer aux formulations de la théorie des types comme une théorie du premier ordre est le théorème de Skolem.

Le problème de la skolémisation en théorie des types

Dans la présentation de la théorie des types utilisant le λ-calcul, la règle de skolémisation est relativement complexe. La règle naïve qui consiste à skolémiser l'axiome ∀x ∃y (P x y) en introduisant un symbole f de type T → U où T est le type de x et U celui de y est incorrecte, puisque de la proposition ∀x (P x (f x))

on peut déduire ∃f ∀x (P x (f x))

qui n'est pas démontrable à partir de la proposition ∀x ∃y (P x y) car l'axiome du choix est indépendant de la théorie des types [4].

Une solution naturelle consiste à proposer que pour chaque terme t, on puisse construire un terme (f t) tel que (P t (f t)) mais sans pour autant disposer de la fonction f dans sa totalité. Cela a amené D.A. Miller [START_REF] Miller | Proofs in higher order logic[END_REF][START_REF] Miller | A compact representation of proofs[END_REF] à proposer une extension du λ-calcul dans laquelle chaque symbole a un indice, son indice de Skolem qui indique le nombre d'arguments auxquels il faut obligatoirement l'appliquer pour former un terme. Ainsi, on skolémise la proposition ∀x ∃y (P x y)

en introduisant un symbole f 1 d'indice de Skolem 1. Le terme (f 1 x) est bien formé, mais pas le symbole f 1 tout seul. Hélas, cette restriction n'est pas suffisante, car si le symbole f 1 tout seul n'est pas un terme bien formé, le terme λx (f 1 x), en revanche, l'est et de la proposition

∀x (P x (f 1 x)) on peut donc déduire ∀x (P x ((λx (f 1 x)) x)) puis ∃f ∀x (P x (f x))
Miller a donc introduit une seconde restriction qui interdit la liaison par un λ des variables libres dans les arguments obligatoires d'un symbole de Skolem. Ainsi, le terme λx (f 1 x) n'est pas non plus bien formé. Miller a montré que si on pose ces deux conditions on retrouve un théorème analogue au théorème de Skolem, c'est-à-dire que les propositions sans occurrences de symboles de Skolem sont conséquences d'une proposition si et seulement si elles sont conséquences de sa forme skolémisée.

Il faut noter, cela dit, que si on considère, comme c'est l'habitude en théorie des types que le λ-terme ∀x P est une notation pour le terme ∀ (λx P ) où ∀ est une constante de type (T → o) → o alors la proposition skolémisée elle-même ∀x (P x (f 1 x))

n'est pas bien formée : en effet la seconde condition de Miller interdit de lier par un λ la variable x libre dans un argument obligatoire de f 1 .

On doit donc ou bien introduire les quantificateurs comme des symboles lieurs supplémentaires ou bien donner une forme plus restreinte de la règle de skolémisation. Par exemple, si on utilise la skolémisation lors de la mise en forme clausale d'une proposition à réfuter par la méthode de résolution [START_REF] Robinson | A Machine-oriented logic based on the resolution principle[END_REF], comme le quantificateur universel est lui-même appelé à être supprimé, on peut définir la forme clausale de la proposition ∀x ∃y (P x y)

comme la proposition (bien formée)

(P X (f 1 X))
et le théorème de Skolem prend la forme de la complétude et correction de cette transformation (c'est-àdire la forme clausale de la négation d'une proposition P est réfutable par résolution si et seulement si la proposition P est démontrable au sens ordinaire du terme). Dans [START_REF] Miller | Proofs in higher order logic[END_REF][START_REF] Miller | A compact representation of proofs[END_REF] Miller formule son théorème comme la correction de cette transformation pour la méthode des connections.

La skolémisation dans la présentation de la théorie des types utilisant les combinateurs

La présentation de la théorie des types utilisant des combinateurs étant une théorie du premier ordre, on peut lui appliquer le théorème de Skolem.

L'axiome ∀x ∃y ε(α(α(P, x), y))

se skolémise en introduisant un symbole de fonction f de rang (T, U ) où T est le type de On peut donner une intuition de la seconde condition de Miller en remarquant qu'on peut étendre l'ascension des variables aux termes qui vérifient cette condition mais pas aux autres.

Pour traduire un terme de la forme λx 1 ... λx n t, où t n'est pas une abstraction, on commence par traduire le terme t. On obtient un terme t ′ qui contient outre les variables x 1 , ..., x n des variables y 1 , ..., y p et des combinateurs c 1 , ..., c q et des sous-termes u 1 , ..., u r de la forme (f k v 1 ... v k ) dans lesquels les variables x 1 , ..., x n n'apparaissent pas. On remplace ces combinateurs par des variables z 1 , ..., z q , et ces termes par des variables z ′ 1 , ..., z ′ r , ce qui donne un terme t ′′ . On définit ensuite la traduction du terme λx 1 ... λx n t comme ((y 1 , ..., y p , z 1 , ..., z q , z ′ 1 , ..., z ′ r , x 1 , ..., x n -→ t ′′ ) y 1 ... y p c 1 ... c q u 1 ... u r ). Naturellement, si les variables x 1 , ..., x n apparaissaient dans u 1 , ..., u r , leur liaison serait perdue.

La skolémisation dans la présentation de la théorie des types utilisant des substitutions explicites

La présentation de la théorie des types utilisant des substitutions explicites étant une théorie du premier ordre, on peut lui appliquer le théorème de Skolem. Ici, le résultat est beaucoup plus intéressant car, comme on le montre dans [i], on retrouve exactement les deux conditions de Miller.

Comme ci-dessus, l'axiome ∀x ∃y ε(α(α(P, x), y))

se skolémise en introduisant un symbole de fonction f de rang

(Γ ⊢ T, ∆ ⊢ U ) où Γ ⊢ T est la sorte de x et ∆ ⊢ U la sorte de y et l'axiome ∀x ε(α(α(P, x), f (x)))
Ici encore, le symbole f tout seul n'est pas un terme, car c'est un symbole de fonction et non un symbole d'individu. On retrouve donc la première condition de Miller. Mais on retrouve aussi la seconde : si la proposition ∀x ∃y ε(α(α(P, x), y))

est obtenue par précuisson puis réduction à partir d'un terme de type o du λ-calcul, la variable x a la sorte ⊢ T où le contexte est nécessairement vide. L'argument de f doit donc être de sorte ⊢ T ce qui lui interdit de contenir des indices de De Bruijn qui désigneraient des lieurs hors du terme lui-même. Le fait que ce contexte soit vide est donc exactement la seconde condition de Miller.

Enfin, ici encore, on dispose de quantificateurs indépendamment des symboles ∀ et ∃ de ce langage particulier. Il n'y a donc pas de problème de formulation de la proposition skolémisée ∀x ε(α(α(P, x), f (x))) et on peut formuler le théorème Proposition 2.6.2 Les propositions sans occurrences de symboles de Skolem sont conséquences d'une proposition si et seulement si elles sont conséquences de sa forme skolémisée.

Chapitre 3

La théorie des ensembles

Le second exemple de théorie modulo que nous détaillons est la théorie des ensembles. L'intérêt de cet exemple est dû au fait que c'est un contre-exemple à de nombreuses propriétés des systèmes modulo (terminaison du système de réécriture, normalisation des démonstrations, complétude de la résolution, ...).

Comme le montre la faible longueur de ce chapitre, le travail sur cette théorie modulo est beaucoup moins avancé que celui sur la théorie des types. En particulier, nous n'avons pas encore de langage des termes du premier ordre intentionnellement équivalent au langage avec un lieur.

La théorie des ensembles de Zermelo

La théorie des ensembles de Zermelo résout le paradoxe de Russell en remplaçant le schéma de compréhension par trois axiomes et un schéma d'axiome : les axiomes de la paire, de l'union, des parties et le schéma du sous-ensemble (ou de compréhension restreint). Ces axiomes s'énoncent ainsi ∀x ∀y ∃z ∀w (w ∈ z ⇔ (w = x ∨ w = y))

∀x ∃y ∀w (w ∈ y ⇔ ∃z (w ∈ z ∧ z ∈ x)) ∀x ∃y ∀w (w ∈ y ⇔ ∀z (z ∈ w ⇒ z ∈ x)) ∀x 1 ...∀x n ∀y ∃z ∀w (w ∈ z ⇔ (w ∈ y ∧ P ))
où x 1 , ..., x n sont les variables libres de P sauf w.

À ces axiomes s'ajoutent éventuellement l'axiome d'extensionnalité, l'axiome de fondation, et d'autres axiomes d'existence : l'axiome de l'infini, divers axiomes de grands cardinaux, le schéma de remplacement et l'axiome du choix.

Pour obtenir un langage de termes, on peut skolémiser ces axiomes. On obtient alors les axiomes

∀x ∀y ∀w (w ∈ {}(x, y) ⇔ (w = x ∨ w = y)) ∀x ∀w (w ∈ (x) ⇔ ∃z (w ∈ z ∧ z ∈ x)) ∀x ∀w (w ∈ P(x) ⇔ ∀z (z ∈ w ⇒ z ∈ x))
∀x 1 ...∀x n ∀y ∀w (w ∈ f x1,...,xn,w,P (x 1 , ..., x n , y) ⇔ (w ∈ y ∧ P ))

Ici encore, il est naturel de transformer ces axiomes en règles de réécriture. On aboutit aux règles de la figure 3.1. De ce fait, la décidabilité de la congruence engendrée par les règles de réécriture de la théorie des ensembles ne peut pas s'établir comme une conséquence de la confluence et de la terminaison. Nous laissons ici ouvert le problème de la décidabilité de cette congruence.

w ∈ {}(x, y) → w = x ∨ w = y w ∈ (x) → ∃z (w ∈ z ∧ z ∈ x) w ∈ P(x) → ∀z (z ∈ w ⇒ z ∈ x) v ∈ fx 1 ,...,

Le langage des termes

Le dernier paragraphe de [a] traite du problème du langage des termes pour la théorie des ensembles. La skolémisation des axiomes de la paire, de la réunion et des parties donne les symboles {}, et P attendus. Le cas du schéma du sous-ensemble (schéma de compréhension restreint) est plus compliqué. D'une part, comme on ne considère en théorie des ensembles que des ensembles et non des relations, le schéma de compréhension n'est pas trivialement équivalent au schéma de compréhension fermé comme c'était le cas en théorie des types. On doit donc skolémiser le schéma ouvert ∀x 1 ...∀x n ∀y ∃z ∀w (w ∈ z ⇔ (w ∈ y ∧ P )) où x 1 , ..., x n sont les variables libres de P sauf w.

La skolémisation de ce schéma introduit des symboles de fonction f x1,...,xn,w,P , et en notant {x ∈ z | P } le terme f x1,...,xn,w,P (x 1 , ..., x n , z) on obtient l'axiome

∀x 1 ... ∀x n ∀z (w ∈ {x ∈ z | P } ⇔ (w ∈ z ∧ P ))
Comme dans le langage des combinateurs on semble disposer d'un symbole d'abstraction { | }, mais avec la restriction que dans le terme {x ∈ A | P } la proposition P doit être sans abstractions. On peut introduire certaines abstractions dans P en appliquant le symbole f à des termes qui contiennent des abstractions, mais on n'obtient pas pour autant un symbole d'abstraction général, car, comme en théorie des types, la variable x liée dans {x ∈ A | P } ne peut pas être libre dans les abstractions apparaissant dans P .

Par ailleurs ce langage comporte un nombre infini de symboles de fonction produits par la skolémisation du schéma de compréhension, ce qui le rend difficilement utilisable en pratique. Des présentations finies de la théorie des ensembles, comme celle de Von Neumann-Bernays-Gödel [START_REF] Mendelson | Introduction to mathematical logic[END_REF] seraient donc sans doute utiles ici.

On peut également introduire un symbole d'abstraction général et on obtient alors une présentation de la théorie des ensembles homologue à la présentation de la théorie des types avec le λ-calcul. On montre dans [a] que cette présentation de la théorie des ensembles est équivalente à la présentation avec les symboles de Skolem, mais, ici encore, l'axiome d'extensionnalité est nécessaire pour montrer cette équivalence.

On ne donne pas de présentation au premier ordre de la théorie des ensembles, intentionnellement équivalente à la présentation avec un opérateur lieur général, mais il est probable qu'on puisse construire un tel langage en utilisant des substitutions explicites.

Chapitre 4

L'élimination des coupures

En déduction modulo, comme dans d'autres cadres, l'élimination des coupures s'étudie d'abord pour la logique intuitionniste, puis se généralise ensuite à la logique classique. En déduction modulo, comme en logique du premier ordre, la déduction naturelle intuitionniste est obtenue en supprimant la règle du tiers exclu et le calcul des séquents intuitionniste en restreignant le calcul à des séquents qui ont une conclusion au plus.

Les coupures en déduction modulo

A ⊢ ≡ ¬A axiome A ⊢ ≡ A ¬-élim A ⊢ ≡ ⊥ ¬-intro ⊢ ≡ ¬A axiome A ⊢ ≡ ¬A axiome A ⊢ ≡ A ¬-élim A ⊢ ≡ ⊥ ¬-intro ⊢ ≡ A ¬-élim ⊢ ≡ ⊥
contient une coupure unique, et l'élimination de cette coupure donne la même démonstration. Elle n'a donc pas de forme normale.

Un cas similaire, mais plus intéressant utilise la règle

A → B ∧ ¬A. La démonstration axiome BA ⊢ ≡ B ∧ ¬A ∧-élim BA ⊢ ≡ ¬A axiome BA ⊢ ≡ A ¬-élim BA ⊢ ≡ ⊥ ¬-intro B ⊢ ≡ ¬A axiome B ⊢ ≡ B axiome BA ⊢ ≡ B ∧ ¬A ∧-élim BA ⊢ ≡ ¬A axiome BA ⊢ ≡ A ¬-élim BA ⊢ ≡ ⊥ ¬-intro B ⊢ ≡ ¬A ∧-intro B ⊢ ≡ A ¬-élim B ⊢ ≡ ⊥ réduit successivement sur 43 axiome B ⊢ ≡ B axiome BA ⊢ ≡ B ∧ ¬A ∧-élim BA ⊢ ≡ ¬A axiome BA ⊢ ≡ A ¬-élim BA ⊢ ≡ ⊥ ¬-intro B ⊢ ≡ ¬A ∧-intro B ⊢ ≡ B ∧ ¬A ∧-élim B ⊢ ≡ ¬A axiome B ⊢ ≡ B axiome BA ⊢ ≡ B ∧ ¬A ∧-élim BA ⊢ ≡ ¬A axiome BA ⊢ ≡ A ¬-élim BA ⊢ ≡ ⊥ ¬-intro B ⊢ ≡ ¬A ∧-intro B ⊢ ≡ A ¬-élim B ⊢ ≡ ⊥ puis sur axiome BA ⊢ ≡ B ∧ ¬A ∧-élim BA ⊢ ≡ ¬A axiome BA ⊢ ≡ A ¬-élim BA ⊢ ≡ ⊥ ¬-intro B ⊢ ≡ ¬A axiome B ⊢ ≡ B axiome BA ⊢ ≡ B ∧ ¬A ∧-élim BA ⊢ ≡ ¬A axiome BA ⊢ ≡ A ¬-élim BA ⊢ ≡ ⊥ ¬-intro B ⊢ ≡ ¬A ∧-intro B ⊢ ≡ A ¬-élim B ⊢ ≡ ⊥ qui est la démonstration initiale.
L'intérêt de ce contre-exemple est que, comme on l'a vu, en théorie des ensembles, la proposition de Crabbé A se réécrit sur une proposition de la forme B ∧ ¬A. La théorie des ensembles ne vérifie donc pas la propriété d'élimination des coupures. Ce contre-exemple dû à Crabbé est discuté par L. Hallnäs [START_REF] Hallnäs | On normalization of proofs in set theory[END_REF] et J. Ekman [START_REF] Ekman | Normal proofs in set theory[END_REF] dans une présentation de la théorie des ensembles avec des axiomes de conversion.

On conjecture dans [h] que l'élimination des coupures termine modulo toutes les congruences définies par un système de réécriture confluent et qui termine. On montre certains cas particuliers de cette conjecture.

La notation fonctionnelle des démonstrations

Pour cela, on utilise une notation fonctionnelle pour les démonstrations en suivant la sémantique de Brouwer-Heyting-Kolmogorov et l'isomorphisme de Curry-De Bruijn-Howard. On propose donc un λ-calcul typé dont les types sont des propositions de la déduction modulo. Ici, notre objectif est simplement de disposer d'une notation pour les démonstrations de déduction modulo, pas de proposer une théorie dans laquelle les démonstrations sont des objets (ce sera l'objet du paragraphe 4.6). Autrement dit, les termes de la théorie considérée et les termes de démonstration appartiennent à deux langages distincts. On utilisera des lettres latines x, y, ... pour les variables d'objet et des lettres grecques (α, β, ...) pour les variables de démonstrations.

Les termes de ce λ-calcul sont

π ::= α | λα π | (π π ′ ) | (π, π ′ ) | fst(π) | snd(π) | i(π) | j(π) | (δ π απ ′ βπ ′′ ) | (botélim π) | λx π | (π t) | (t, π) | (exélim π xαπ ′ )
La figure 4.1 donne les règles de typage de ce calcul.

Il est trivial qu'une proposition est un type habité de ce calcul si et seulement si elle est démontrable en déduction naturelle modulo intuitionniste.

La démonstration de Crabbé ci-dessus, par exemple, s'exprime par le terme λα (snd(α) α) (β, λα (snd(α) α))

On définit ensuite les règles de réduction des démonstrations qui correspondent à l'élimination des coupures.

Γ ⊢≡ π : C (x, A, t) ∃-intro si B ≡ (∃x A), C ≡ [t/x]A Γ ⊢≡ (t, π) : B Γ ⊢≡ π : C Γ, α : A ⊢≡ π ′ : B (x, A) ∃-élim si C ≡ (∃x A), x ̸ ∈ F V (ΓB) Γ ⊢≡ (exélim π xαπ ′ ) : B
(λα π 1 π 2 ) → [π 2 /α]π 1 fst(π 1 , π 2 ) → π 1 snd(π 1 , π 2 ) → π 2 δ(i(π 1 ), απ 2 , βπ 3 ) → [π 1 /α]π 2 δ(j(π 1 ), απ 2 , βπ 3 ) → [π 1 /β]π 3 (λx π t) → [t/x]π (exélim (t, π 1 ) αxπ 2 ) → [t/x, π 1 /α]π 2
On veut maintenant montrer la terminaison du processus d'élimination des coupures, c'est-à-dire la normalisation de ce calcul.

La réductibilité

La première tentative pour démontrer la normalisation des démonstrations, au moins modulo certaines congruences, est de s'inspirer de la démonstration de la normalisation des démonstrations en logique du premier ordre et d'utiliser la méthode de Tait.

L'élimination des coupures en logique du premier ordre

En logique du premier ordre, on ne peut pas montrer que toutes les démonstrations sont normalisables par une simple récurrence sur la structure des démonstrations. En effet, le fait que π et π ′ soient normalisables ne permet pas de déduire que (π π ′ ) l'est, car ce terme peut être lui-même un radical.

On renforce donc l'hypothèse de récurrence en montrant par récurrence que toutes les démonstrations sont réductibles. Une démonstration réductible de la proposition A ⇒ B est une démonstration fortement normalisable, telle que quand elle se réduit sur une démonstration de la forme λα π 1 alors, pour toute démonstration réductible π ′ de A, [π ′ /α]π 1 est une démonstration réductible de B. Le cas où le terme est un radical est ainsi anticipé. On définit de même l'ensemble des démonstrations réductibles d'une proposition de la forme A ∧ B, A ∨ B, ¬A, ⊥, ∀x P , ∃x P . Les démonstrations réductibles d'une proposition atomique sont, quant à elles, simplement les démonstrations fortement normalisables. L'ensemble des démonstrations réductibles d'une proposition P se construit donc par récurrence sur la taille de P . En utilisant le vocabulaire du λ-calcul, l'ensemble des termes réductibles de type T se construit par récurrence sur la taille de T .

On montre ensuite, par récurrence sur la structure des démonstrations, que toute démonstration d'une proposition A est réductible et donc fortement normalisable.

Pour cela, on note R A l'ensemble des démonstrations réductibles de A et on commence par montrer les lemmes suivants.

-si π ∈ R A , alors π est fortement normalisable, [START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types[END_REF][START_REF] Girard | Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF][START_REF] Girard | Proofs and types[END_REF][START_REF] Krivine | Lambda-calcul, types et modèles[END_REF][START_REF] Gallier | On Girard's candidats de réductibilité[END_REF], on appelle candidat de réductibilité un ensemble qui vérifie ces conditions.

-si π ∈ R A et π → π ′ alors π ′ ∈ R A , -si π est neutre (c'est-à-dire une variable ou une élimination) et pour tout π ′ telle que π → 1 π ′ , π ′ ∈ R A alors π ∈ R A . Après

L'élimination des coupures en déduction modulo

En déduction modulo, si deux propositions P et Q sont congruentes, toute démonstration de l'une est une démonstration de l'autre. De ce fait, on doit avoir R P = R Q . On ne peut donc plus définir l'ensemble des démonstrations réductibles d'une proposition atomique A comme l'ensemble de toutes les démonstrations fortement normalisables, car cette proposition peut se réduire, par exemple, sur une proposition de la forme B ⇒ C et dans ce cas, pour être réductible, une démonstration doit, en outre, vérifier la propriété que si elle se réduit sur une démonstration de la forme λα π 1 , alors pour toute démonstration réductible π ′ , [π ′ /α]π 1 est réductible. De ce fait, la construction de la famille R P ne peut plus se faire simplement par récurrence sur la taille de P .

Une tentative consiste à définir les ensembles R P par récurrence sur la taille de P pour P normal, puis de définir l'ensemble R P pour P quelconque comme R P ↓ où P ↓ est la forme normale de P . Hélas, cette tentative échoue, car cela nous amène à définir les démonstrations réductibles de la proposition normale ∀x A comme l'ensemble des démonstrations π de ∀x A qui vérifient les propriétés suivantes π est fortement normalisable, -si π se réduit sur une démonstration de la forme λx π Cette remarque n'est pas nouvelle : en théorie des types simples la substitution d'une variable de prédicat modifie, similairement, la complexité des propositions. L'élimination des coupures en théorie des types est d'ailleurs un corollaire de cette conjecture. Le contre-exemple traditionnel [START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types[END_REF][START_REF] Girard | Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF][START_REF] Girard | Proofs and types[END_REF][START_REF] Krivine | Lambda-calcul, types et modèles[END_REF][START_REF] Gallier | On Girard's candidats de réductibilité[END_REF] qui montre qu'on ne peut pas donner une telle définition de la réductibilité en théorie des types, s'adapte ici. On serait amené à poser qu'une démonstration π de la proposition ∀x ε(x) est réductible si elle est fortement normalisable et si quand elle se réduit sur une démonstration de la forme λx π 1 , alors pour tout terme t, [t/x]π 1 est une démonstration réductible de ε(t) ↓. Cela demande d'avoir au préalable défini l'ensemble des démonstrations réductibles pour toutes les propositions ε(t) ↓ en particulier pour ε( ∀ (λ1)) ↓= ∀x ε(x).

Cependant, cet argument est correct pour tous les systèmes de réécriture qui ne comportent pas de quantificateurs dans leurs membres droits. Dans ce cas, la définition ci-dessus est une définition correcte par récurrence pour l'ordre lexicographique sur le couple (q(A), c(A)) où q(A) est le nombre de quantificateurs dans la proposition A et c le nombre de connecteurs.

On en déduit donc la proposition suivante.

Proposition 4.3.1 Les démonstrations modulo une congruence définie par un système de réécriture qui est confluent, qui termine et qui n'a pas d'occurrences de quantificateurs dans les membres droits de ses règles sont fortement normalisables.

Les prémodèles

Dans les autres cas, montrer l'élimination des coupures demande de construire une famille d'ensembles R A indexée par les propositions qui vérifie les conditions suivantes.

-Les ensembles R A sont des candidats de réductibilité.

-Conditions sur les propositions composées : -R A⇒B est l'ensemble des démonstrations π telles que π est fortement normalisable et si π se réduit sur une démonstration de la forme λα π 1 , alors pour toute démonstration

π ′ de R A , [π ′ /α]π 1 est un élément de R B .
- L'avantage de ce choix est que la famille des ensembles R A est entièrement définie par les ensembles R A où A est atomique. Autrement dit, pour définir une famille R A , il suffit de se donner les ensembles R P (t1,...,tn) , c'est-à-dire pour chaque symbole de prédicat P une fonction P qui à chaque n-uplet de termes associe un candidat de réductibilité. On voit apparaître ici une similarité avec la notion de modèle. Pour se donner un modèle, il faut également, se donner pour chaque symbole de prédicat P une fonction P qui à chaque n-uplet de termes associe une valeur de vérité. La comparaison peut se poursuivre. Si deux termes t 1 et t On montre également que des variantes de la notion de prémodèle permettent d'obtenir des résultats similaires pour le calcul des séquents intuitionniste et classique. Dans ce cas, il n'y a pas ici de processus d'élimination des coupures dont on montre la terminaison, puisqu'en calcul des séquents, le processus d'élimination d'une coupure n'est pas local. On montre donc que si une congruence a un prémodèle (dans un sens légèrement différent) alors la règle de coupure est redondante dans le calcul des séquents modulo cette congruence.

R
On montre facilement que pour les systèmes de réécriture qui ne comportent pas de quantificateurs dans leurs membres droits, on peut construire un prémodèle très simple qui rappelle, par certains aspects, le modèle syntaxique construit dans le théorème de complétude.

On montre aussi dans [h] que la démonstration de normalisation pour la théorie des types exprimée avec des combinateurs peut s'exprimer comme la construction d'un prémodèle. Cette construction de prémodèle ressemble par bien des aspects à la construction du modèle fonctionnel de la théorie des types : dans un cas comme dans l'autre l'ensemble M ι est un singleton et l'ensemble M T →U est l'ensemble des fonctions de M T dans M U . On retrouve aussi plusieurs aspects de la démonstration traditionnelle de normalisation des démonstrations en exprimant ces démonstrations dans le λ-calcul polymorphe avec constructeurs de types F ω [START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types[END_REF][START_REF] Girard | Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF] : le fait que tous les termes d'un même type construit sans le type o dénotent le même objet correspond à l'élimination des termes du premier ordre dans la démonstration traditionnelle, et la fonctionnalité du modèle fait qu'un symbole de type o → o, par exemple, est interprété comme une fonction des candidats dans les candidats. Dans [i] on montre la normalisation des démonstrations dans la formulation de la théorie des types utilisant des substitutions explicites, encore une fois en construisant un prémodèle.

On montre enfin dans [h] que si un système de réécriture n'a pas d'occurrence négative de proposition atomique dans les membres droits de ses règles, alors on peut construire un prémodèle comme plus petit point fixe.

La de normalisation

Notre conjecture est que pour tous les systèmes de réécriture confluents et qui terminent, on peut construire un prémodèle et donc les démonstrations normalisent fortement modulo ce système de réécriture. Nous croyons cette conjecture vraie car nous n'avons pas réussi à trouver de contre-exemple.

Même si cette conjecture est vraie, on peut s'interroger sur les outils nécessaires pour la démontrer. Puisqu'elle implique la cohérence de la théorie des types, on sait par le second théorème d'incomplétude de Gödel, qu'on ne peut pas la démontrer dans la théorie des types elle-même. Une question importante, du point de vue méthodologique, est de savoir si cette conjecture implique la cohérence de la théorie des ensembles ou non. Le système de réécriture que nous avons proposé pour la théorie des ensembles ne termine pas, mais on peut le modifier ainsi : On peut montrer que ce système termine. Hélas, l'élimination des coupures modulo ce système n'implique pas trivialement la cohérence de la théorie des ensembles car, dans ce système, les axiomes de l'égalité sont nécessaires pour exprimer les démonstrations de la théorie des ensembles. Mais, on peut imaginer qu'il y a là une piste pour montrer que notre conjecture implique la cohérence de la théorie des ensembles et donc qu'elle ne peut se démontrer sans faire appel à des axiomes au delà de la théorie des ensembles, comme par exemple, des axiomes de grands cardinaux. Plus modestement, on peut voir que le système de réécriture de la figure 3.1 termine pour de grands fragments de la théorie des ensembles (par exemple, vraisemblablement, pour le fragment où on restreint le schéma du sous-ensemble aux propositions stratifiables au sens de W.V.O. Quine) et donc que pour démontrer cette conjecture, il est nécessaire de sortir de ce fragment.

w ∈ {}(x, y) → ∀a (w = a ⇒ (a = x ∨ a = y)) w ∈ (x) → ∃z (w ∈ z ∧ z ∈ x) w ∈ P(x) → ∀z (z ∈ w ⇒ z ∈ x) v ∈ f x1,...,

Des prémodèles aux modèles

Si une théorie (≡, Γ) a un prémodèle, alors le calcul des séquents classiques modulo la congruence ≡ a la propriété d'élimination des coupures. Si, en outre, le candidat de réductibilité dénotation de ⊥ ne contient pas de démonstration close (c'est, par exemple, toujours le cas quand Γ est vide car il n'y a pas de démonstration sans coupure et sans axiome de la proposition ⊥), alors la théorie est cohérente et, d'après le théorème de complétude de Gödel, elle a un modèle.

On peut s'interroger sur les relations entre les prémodèles et les modèles de cette théorie, en particulier on peut vouloir transformer les prémodèles en modèles (ce qui justifierait notre terminologie de "prémodèle").

Un prémodèle est un modèle multivalué dont les valeurs de vérité sont des candidats de réductibilité. Une piste est donc de considérer un candidat qui contient une démonstration close comme une valeur de vérité positive et un candidat qui ne contient que des démonstrations ouvertes comme une valeur de vérité négative. Hélas cette idée est trop naïve car une proposition indéterminée de la théorie dénoterait une valeur de vérité négative, ainsi que sa négation. Il faut donc vraisemblablement, comme dans la démonstration du théorème de complétude, commencer par compléter et saturer le prémodèle.

Nous laissons ce projet pour un travail futur.

Les coupures de conversion

Nous l'avons vu, une théorie en déduction modulo est toujours équivalente à une théorie du premier ordre. La notion de coupure modulo se traduit donc en logique du premier ordre en une notion de coupure relative à certains axiomes (comme les notions de coupure en logique du premier ordre avec égalité, ou dans l'arithmétique sont relatives aux axiomes de l'égalité ou à l'axiome de récurrence).

On a caractérisé dans [e] ces coupures que nous avons appelées coupures de conversion. Une coupure de conversion est une séquence formée d'une règle d'introduction et d'une règle d'élimination séparées par une étape de conversion, c'est-à-dire une séquence d'utilisation des axiomes équationnels ou d'équivalence de la théorie.

Cela permet, par exemple, de formuler le théorème d'élimination des coupures pour la théorie des types en restant intégralement au premier ordre, sans même utiliser la déduction modulo.

La normalisation des démonstrations du théorème de Cantor

À titre d'exemple, on présente dans ce paragraphe plusieurs démonstrations du théorème de Cantor dans différentes théories modulo et leur forme normale. Le théorème de Cantor montre qu'il n'y a pas de surjection d'un ensemble dans l'ensemble de ses parties.

En théorie des types avec une fonction

En théorie des types, un ensemble est un objet de type T → o. Ici, nous faisons le choix de nous intéresser uniquement à l'ensemble de tous les objets de type ι. L'ensemble des parties de cet ensemble est l'ensemble de tous les objets de type ι → o. Cela revient à montrer qu'il n'y a pas de surjection du type ι dans le type ι → o.

La première possibilité est de représenter cette surjection potentielle par une fonction f de type ι → ι → o. La surjectivité de cette fonction peut s'exprimer par l'existence d'une fonction g inverse à droite de f , c'està-dire d'une fonction de type (ι → o) → ι telle que pour tout x, (f (g x)) = x. En utilisant la définition de G.W. Leibniz de l'égalité, cette hypothèse se traduit par la proposition

H : ∀x ∀p (ε(p (f (g x))) ⇔ ε(p x))
On considère alors l'ensemble λx ¬((f x) x) des objets x de type ι qui n'appartiennent pas à (f x).

C = λ ¬[↑](f [↑] 1 1)
L'ensemble C est l'image par f de l'objet (g C) de type ι. Par définition de C, (g C) appartient à C si et seulement si il n'appartient pas à (f (g C)), mais cet ensemble n'est autre que C lui-même donc (g C) appartient à C si et seulement si il ne lui appartient pas, ce qui est contradictoire.

On construit le λ-terme démonstration du théorème de Cantor ainsi. La proposition A "(g

C) appartient à C" s'écrit ε(λ ¬[↑](f [↑] 1 1) (g λ ¬[↑](f [↑] 1 1))) Sa forme normale est ¬ε((f (g λ ¬[↑](f [↑] 1 1)) (g λ ¬[↑](f [↑] 1 1))))
En appliquant l'hypothèse H au terme C et au prédicat

P = λ(1 (g[↑] λ ¬[↑ 2 ](f [↑ 2 ] 1 1)
)) on obtient une démonstration de (H C P ) de la proposition

ε(f (g λ ¬[↑](f [↑] 1 1)) (g λ ¬[↑](f [↑] 1 1))) ⇔ ε(λ ¬[↑](f [↑] 1 1) (g λ ¬[↑](f [↑] 1 1)))
qui se réduit sur

ε(f (g λ ¬[↑](f [↑] 1 1)) (g λ ¬[↑](f [↑] 1 1))) ⇔ ¬ε(f (g λ ¬[↑](f [↑] 1 1)) (g λ ¬[↑](f [↑] 1 1)))
c'est-à-dire sur A ⇔ ¬A. De cette proposition on peut déduire une démonstration de la proposition ¬A λα (f st(H C P ) α α)

puis une démonstration de ⊥ λα (f st(H C P ) α α) (snd(H C P ) λα (f st(H C P ) α α))
Comme toute démonstration en théorie des types, cette démonstration est fortement normalisable, sa forme normale est

(f st(H C P ) (snd(H C P ) λα (f st(H C P ) α α)) (snd(H C P ) λα (f st(H C P ) α α)))
À partir de cette démonstration de ⊥ sous l'hypothèse H, on peut facilement construire une démonstration de la proposition ¬∃f ∃g ∀x ∀p (

))) ⇔ ε(p x)) ε(p (f (g x

En théorie des types avec une relation

Au lieu d'utiliser la notion primitive de fonction de la théorie des types, on peut coder les fonctions comme des relations fonctionnelles. On pose alors un symbole R de type ι → (ι → o) → o et deux hypothèses qui expriment que R est surjective E : ∀y ∃x ε(R x y)

et fonctionnelle ∀x ∀y ∀z (ε(R x y) ⇒ ε(R x z) ⇒ y = z)
Encore une fois, on utilise la définition de Leibniz de l'égalité

F : ∀x ∀y ∀z (ε(R x y) ⇒ ε(R x z) ⇒ ∀p (ε(p y) ⇔ ε(p z)))
Pour dire que x n'appartient pas à son image, on est obligé de dire qu'il n'appartient à aucune de ses images car on ne dispose plus d'un terme pour désigner cette image. L'ensemble

C est donc λx ∀λy ((R x y) ⇒ ¬(y x)), c'est-à-dire C = λ ∀λ((R 2 1) ⇒ ¬(1 2))
On commence par démontrer ⊥ sous l'hypothèse h : (R a C). Soit A la proposition ε(C a), cette proposition se réduit sur ∀y (ε(R a y) ⇒ ¬ε(y a))

Le terme π = λα (α C h)
est une démonstration de A ⇒ ¬A et le terme

π ′ = λα λy λβ (f st(F a C y h β (λ ¬[↑](1 a[↑]))) α)
une démonstration de ¬A ⇒ A. On peut comme ci-dessus, en déduire une démonstration de ⊥

(π (π ′ (λγ (π γ γ))) (π ′ (λγ (π γ γ))))
Comme toute démonstration en théorie des types, cette démonstration a une forme normale

π 0 = (f st(F a C C h h (λ ¬[↑](1 a[↑]))) (λγ (γ C h γ))))(λy λβ (f st(F a C y h β (λ ¬[↑](1 a[↑]))) (λγ (γ C h γ))))
On peut ensuite se passer de l'hypothèse h pour obtenir une démonstration normale de ⊥ sous les hypothèses

E et F (exélim (E C) ahπ 0 )
À partir de cette démonstration de ⊥ sous les hypothèses E et F , on peut facilement construire une démonstration de la proposition

¬∃R ((∀y ∃x ε(R x y)) ∧ (∀x ∀y ∀z (ε(R x y) ⇒ ε(R x z) ⇒ ∀p (ε(p y) ⇔ ε(p z)))))

En théorie des ensembles

La démonstration du théorème de Cantor en théorie des ensembles ressemble beaucoup à celle en théorie des types avec une relation. La démonstration que nous donnons ici est, cela dit, un peu plus générale puisque nous considérons un ensemble B quelconque, alors que dans la démonstration en théorie des types ci-dessus, nous avions fait le choix de nous restreindre à l'ensembles des objets de type ι.

On note < x, y > l'ensemble {{x}, {x, y}} c'est-à-dire {}({}(

On pose un ensemble R et deux axiomes qui expriment que R est une relation surjective

E : ∀y (y ∈ P(B) ⇒ ∃x (x ∈ B∧ < x, y >∈ R)) et fonctionnelle F : ∀x ∀y ∀z (< x, y >∈ R ⇒< x, z >∈ R ⇒ y = z)
On utilise aussi l'axiome de l'égalité

L : ∀z ∀x ∀y (x = y ⇒ ¬z ∈ x ⇒ ¬z ∈ y)
Pour dire que x n'appartient pas à son image, on dit qu'il n'appartient à aucune de ses images

C = {x ∈ B | ∀y (< x, y >∈ R ⇒ ¬x ∈ y)}
On a donc une règle de réécriture

x ∈ C → x ∈ B ∧ ∀y (< x, y >∈ R ⇒ ¬x ∈ y) 1
1. La skolémisation du schéma du sous-ensemble ne nous donne pas un tel terme puisque la proposition

∀r ∀b ∃e ∀x (x ∈ e ⇔ ((x ∈ b) ∧ ∀y (< x, y >∈ r ⇒ ¬x ∈ y)))
qui contient des symboles de Skolem, n'est pas une instance du schéma du sous-ensemble. On peut remplacer la proposition < x, y >∈ r par ∀u ((∀v

(v ∈ u ⇔ (∀w (w ∈ v ⇔ (w = x ∨ w = y)) ∨ ∀w (w ∈ v ⇔ w = x)))) ⇒ u ∈ r)
mais on obtient une démonstration beaucoup plus compliquée. En revanche, on a un tel terme C dans le système avec lieurs présenté dans [a]. On aurait également un tel terme dans une présentation au premier ordre de ce système. En attendant, on se place dans un système dans lequel le terme C est une constante et où on pose la règle de réécriture ci-dessus.

On commence par démontrer la proposition ⊥ sous l'hypothèse h : a ∈ B∧ < a, C >∈ R. Soit A la proposition a ∈ C, cette proposition se réduit sur

a ∈ B ∧ ∀y (< a, y >∈ R ⇒ ¬a ∈ y) Le terme π = λα (snd(α) C snd(h))
est une démonstration de A ⇒ ¬A et le terme

π ′ = λα < f st(h), λy λβ (L a C y (F a C y snd(h) β) α) >
une démonstration de ¬A ⇒ A. On peut, comme ci-dessus, en déduire une démonstration de ⊥

(π (π ′ (λγ (π γ γ))) (π ′ (λγ (π γ γ))))
Cette démonstration a une forme normale

π 0 = (L a C C (F a C C snd(h) snd(h)) (λγ (snd(γ) C snd(h) γ)) < f st(h), λy λβ (L a C y (F a C y snd(h) β) (λγ (snd(γ) C snd(h) γ))) >)
On peut ensuite se passer de l'hypothèses h pour obtenir une démonstration normale de ⊥ sous les hypothèses

E et F . La proposition C ∈ P(B) se réduit sur ∀x ((x ∈ B ∧ ∀y (< x, y >∈ R ⇒ ¬x ∈ y)) ⇒ x ∈ B)).
Le terme ρ = λx λα f st(α) en est donc une démonstration. On construit alors la démonstration suivante de ⊥ sous les hypothèses E et F (exélim (E C ρ) ahπ 0 )

À partir de cette démonstration de ⊥ sous les hypothèses E et F , on peut facilement construire une démonstration de la proposition

∀B ¬∃R ((∀y (y ∈ P(B) ⇒ ∃x (x ∈ B∧ < x, y >∈ R))) ∧ (∀x ∀y ∀z (< x, y >∈ R ⇒< x, z >∈ R ⇒ y = z)

Dans les théories étendues

Dans la formulation du théorème de Cantor en théorie des types avec une fonction, on peut étendre le système de réécriture avec la règle (f (g x)) → x de manière à faire entrer dans la congruence l'égalité entre (f (g x)) et x. L'hypothèse H peut être remplacée par la démonstration λx λp (λβ β, λβ β) et la démonstration ci-dessus se réduit sur

(λα (α α) λα (α α))
qui n'a pas de forme normale. Remarquons que, dans ce cas, le système de réécriture lui-même ne termine pas car la proposition A se réduit sur sa négation. Dans les formulations en théorie des types avec une relation et dans la formulation en théorie des ensembles, on utilise l'axiome F pour montrer la proposition C = C puis on applique l'axiome de Leibniz de manière à remplacer C par C dans la proposition ¬A. Dans [START_REF] Ekman | Normal proofs in set theory[END_REF], Ekman propose d'étendre la notion de coupure en théorie des ensembles en considérant comme une coupure une application de l'axiome de Leibniz à une égalité de la forme a = b si a et b sont liées par une certaine relation d'équivalence. En suivant cette idée, on peut considérer comme une coupure une application de l'axiome de Leibniz à une égalité de la forme a = a que cette proposition soit démontrée par l'axiome d'identité ou de n'importe quel autre manière. Une telle coupure s'élimine naturellement en supprimant la démonstration de la proposition a = a et l'application de l'axiome de Leibniz.

Cela amène à ajouter une règle de réduction des démonstrations liée à l'axiome F (f st(F x y y α α ′ P ) β) → β universel. Le type produit cartésien sert à exprimer les propositions formées avec la conjonction et le quantificateur existentiel, l'union disjointe sert à former les propositions formées avec la disjonction, et le type vide les propositions formées avec la négation et la contradiction.

Pour que les propositions atomiques aient le type T ype il est nécessaire de plonger les symboles de prédicat de rang (s 1 , ..., s n ) comme des symboles de type s 1 → ... → s n → T ype. Cela demande de pouvoir former des termes tels que s 1 → ... → s n → T ype. On introduit pour cela une nouvelle constante Kind et on donne le type Kind à ces termes. On aboutit au calcul de la figure 4.2. Remarquons que contrairement aux présentations traditionnelles du λ-calcul avec des types dépendants [START_REF] Harper | A framework for defining logics[END_REF][START_REF] Barendregt | Lambda calculi with types[END_REF], ce calcul ne comporte ni règle de conversion, ni règle d'abstraction pour former des objets dont le type est de type Kind :

Γ ⊢ T : T ype Γ, x : T ⊢ T ′ : Kind Γ, x : T ⊢ t : T ′ Γ ⊢ λx : T t : Πx : T T ′
Suivant l'usage, on note T → U le terme Πx : T U et T × U le terme Σx : T U quand la variable x n'apparaît pas dans U . On pose, pour chaque sorte s de la théorie, une variable s ′ de type T ype, pour chaque variable x de sorte s une variable x ′ de type s ′ , pour chaque symbole de fonction f de rang (s 1 , ..., s n , t) une variable f ′ de type s ′ 1 → ... → s ′ n → t ′ , pour chaque symbole de prédicat P de rang (s 1 , ..., s n ) une variable P ′ de type s ′ 1 → ... → s ′ n → T ype. Les propositions se plongent alors comme des termes de type T ype dans ce contexte :

-(f (t 1 , ..., t n )) ′ = (f ′ t ′ 1 ... t ′ n ), -(P (t 1 , ..., t n )) ′ = (P ′ t ′ 1 ... t ′ n ), -(A ⇒ B) ′ = A ′ → B ′ , -(A ∧ B) ′ = A ′ × B ′ , -(A ∨ B) ′ = A ′ + B ′ , -(¬A) ′ = A ′ → ∅, -⊥ ′ = ∅, -(∀x A) ′ = Πx : T A ′ , -(∃x A) ′ = Σx : T A ′ .
Pour chaque axiome A, on pose une variable x A de type A ′ . Les démonstrations d'une proposition A peuvent alors s'exprimer comme des termes de type A ′ .

Le plongement des théories modulo dans le λ-calcul

On peut, de même, plonger une théorie modulo, en transformant les règles de ce calcul de manière à autoriser une conversion à chaque étape de déduction (on remplace alors le symbole ⊢ par le symbole ⊢ ≡ ). De manière équivalente, on peut ajouter une règle de conversion :

Γ ⊢ ≡ t : T Γ ⊢ ≡ T : T ype Γ ⊢ ≡ T ′ : T ype T ≡ T ′ Γ ⊢ ≡ t : T ′
Dans ce cas, cela dit, les étapes de conversions apparaissent explicitement dans la dérivation bien qu'elles n'apparaissent pas dans le λ-terme.

Le cas de la théorie des types simples

Comme toute théorie modulo, la théorie des types simples avec des combinateurs peut se plonger dans le λ-calcul avec des types dépendants. Il y a, malgré tout, une petite difficulté due au fait que cette théorie a un nombre infini de sortes : ι, o, ι → o, ... Pour ne pas avoir à introduire un nombre infini de variables de type T ype, on peut introduire deux variables ι et o, un nouveau symbole Arrow et une nouvelle règle

Γ ⊢ ≡ A : T ype Γ ⊢ ≡ B : T ype Γ ⊢ ≡ Arrow(A, B) : T ype Γ ⊢ a : T + T ′ Γ ⊢ U : T ype Γ, x : T ⊢ b : U Γ, y : T ′ ⊢ c : U Γ ⊢ (δ T,T ′ ,U a xb yc) : U
Utilisation des éléments du type vide : Mais ce plongement n'est pas satisfaisant. En effet, la théorie des types simples comportant déjà une notion de fonction le calcul obtenu comporte deux notions, redondantes, de fonction : celle propre au λcalcul et celle importée de la théorie des types. Au type A → B que permet de former le λ-calcul avec des types dépendants, s'ajoute le type Arrow(A, B) qui est une sorte de la théorie des types simples. De même, au terme λx λy x s'ajoute le terme K de la théorie des types simples.

Γ ⊢ t : ∅ Γ ⊢ (R T t) : T
Autrement dit, dans le cas de la théorie des types simples, parce que cette théorie comporte déjà une notion de fonction, on peut optimiser le plongement naïf ci-dessus : on ne pose que deux variables ι et o de type T ype, et on plonge la sorte T → U (flèche de la théorie des types simples) comme le type T → U (flèche du λ-calcul). On plonge le combinateur K comme le terme λx λy x, et on plonge de manière similaire les autres combinateurs et les termes formés par application. Il faut alors ajouter la β-conversion des termes du λ-calcul avec des types dépendants dans la congruence ≡ utilisée dans la règle de conversion pour remplacer les règles de réduction des combinateurs.

On peut s'étonner du fait que nous parvenions ici à exprimer les démonstrations de la théorie des types simples dans le λ-calcul avec des types dépendants (non polymorphe) alors que le polymorphisme a précisément été inventé pour exprimer les démonstrations de cette théorie [START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types[END_REF][START_REF] Girard | Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF][START_REF] Girard | Proofs and types[END_REF][START_REF] Krivine | Lambda-calcul, types et modèles[END_REF][START_REF] Gallier | On Girard's candidats de réductibilité[END_REF]. Cela est dû au fait que, si nous avons identifié l'implication ⇒ avec la flèche → du λ-calcul typé, et également la flèche → de construction des sortes de la théorie des types simples avec la flèche → du λ-calcul typé, nous avons, en revanche, gardé la distinction entre l'implication ⇒ et son contenu ⇒ qui a été introduite dans la présentation au premier ordre de la théorie des types simples.

Certes, nous ne pouvons pas typer le terme λX : T ype λx : X x de type ΠX : T ype (X → X), mais nous pouvons typer le terme λX : o λx : ε(X) x de type ΠX : o (ε(X) → ε(X)). Certes, nous ne pouvons pas appliquer le terme λX : T ype λx : X x au type T → T pour obtenir le terme λx : T → T x de type (T → T ) → (T → T ), mais nous pouvons appliquer le terme λX : o λx : ε(X) x au terme t ⇒t et obtenir le terme λx : ε(t ⇒t) x de type ε(t ⇒t) → ε(t ⇒t) qui est identique, modulo la congruence, au terme λx :

ε(t) → ε(t) x de type (ε(t) → ε(t)) → (ε(t) → ε(t)).
Cet exemple nous montre que le polymorphisme peut être obtenu en λ-calcul avec des types dépendants modulo, non seulement par l'ajout de règles de typage, comme c'est l'usage, mais aussi par l'ajout de règles de réécriture. On obtient ainsi une présentation du Calcul des constructions qui si elle n'est pas la plus courante, n'est pas, pour autant, nouvelle. Elle a, par exemple, été étudiée en détails par T. Altenkirch [2] qui note pr notre symbole ε et qui distingue le terme P de type o du type pr(P ) des démonstrations de P .

On retombe sur la présentation traditionnelle du Calcul des constructions en optimisant encore le plongement : au lieu de poser deux variables ι et o on ne pose que la variable ι et on plonge la sorte o comme le symbole T ype. De même, on plonge le symbole ⇒ comme la flèche du λ-calcul, et on donne un plongement similaire pour les symboles ∧, ∨, ... Il est alors nécessaire d'ajouter la règle des types polymorphes pour exprimer la quantification sur les objets de type o qui sont désormais de type T ype, la règle des constructeurs de types pour exprimer la sorte o → o, et la règle de construction d'abstractions dont le type est de type Kind pour former le terme λx : o λy : ι x qui est désormais de type T ype → ι → T ype.

Ces différentes présentations ne sont pas nécessairement équivalentes. En particulier, il reste à déterminer celles dans lesquelles on peut exprimer une démonstration de l'axiome du choix ou le paradoxe de la somme forte.

Il y a, cela dit, un avantage à garder la distinction entre les connecteurs et leur contenus. En effet, les extensions du λ-calcul avec des types dépendants sont traditionnellement classées en deux familles : celles obtenues par l'ajout de règles de typage (qui sont élégamment présentées dans le cube de H. Barendregt [START_REF] Barendregt | Lambda calculi with types[END_REF]) : le polymorphisme et les constructeurs de types, et celles qui sont obtenues par l'ajout de règles de réécriture : les types inductifs. Dans le λ-calcul avec des types dépendants modulo, toutes ces extensions sont obtenues de manière uniforme par l'ajout de règles de réécriture.

Notons enfin qu'on peut aussi plonger la théorie des types simples présentée avec des substitutions explicites dans le λ-calcul avec des types dépendants. Mais, pour optimiser le plongement comme ci-dessus, il est nécessaire de présenter le λ-calcul avec des types dépendants lui-même avec des substitutions explicites, comme l'ont proposé P. Martin-Löf [START_REF] Martin-Löf | [END_REF], L. Magnusson [START_REF] Magnusson | The implementation of ALF, a proof editor based on Martin-Löf monomorphic type theory with explicit substitution[END_REF] et C. Muñoz [START_REF] Muñoz-Hurtado | Dependent types with explicit substitutions : a meta-theoretical development[END_REF][START_REF] Muñoz-Hurtado | Un calcul de substitutions pour la représentation des preuves partielles en théorie des types[END_REF][START_REF] Muñoz-Hurtado | A calculus of substitutions for incomplete-proof representation in type theory[END_REF].

Chapitre 5

La démonstration automatique

La résolution équationnelle

Dans une théorie modulo dont la congruence est définie par des règles de réécriture et des équations portant sur les termes uniquement, les méthodes de démonstration automatique sont assez similaires à celles pour la logique du premier ordre. On peut utiliser la résolution, ou la méthode des tableaux, en remplaçant simplement l'algorithme d'unification du premier ordre par un algorithme d'unification équationnelle modulo cette congruence. Cette idée n'est pas nouvelle, Plotkin propose dans [START_REF] Plotkin | Building-in equational theories[END_REF] d'abandonner l'axiome d'associativité en remplaçant l'unification par l'unification associative (ce qui revient, dans notre cadre, à raisonner modulo l'associativité) et M. Stickel [START_REF] Stickel | Automated deduction by theory resolution[END_REF] donne un cadre général à la résolution équationnelle qu'il appelle theory resolution.

Un problème d'unification équationnelle est une équation a = b (ou un ensemble d'équations) et une solution en est une substitution σ telle que les termes σa et σb soient congruents (et non plus nécessairement identiques).

L'algorithme général d'unification équationnelle est appelé la surréduction [START_REF] Fay | First-order unification in an equational theory[END_REF][START_REF] Hullot | Canonical forms and unification[END_REF][START_REF] Gallier | Complete set of transformations for general E-unification[END_REF][START_REF] Jouannaud | Solving equations in abstract algebras : a rule-based survey of unification[END_REF]. L'idée de base est d'ajouter aux règles de l'unification du premier ordre, une règle qui permet de surréduire (c'est-à-dire d'instancier puis de réduire) un sous-terme d'une équation qui n'est pas réductible mais dont une instance l'est.

Par exemple, le problème d'unification

z + 5 = 7
n'a pas de solution pour l'unification du premier ordre, mais il a une solution z → 2, modulo les règles de réécriture

0 + y → y Succ(x) + y → Succ(x + y)
En effet, le terme z + 5 n'est pas réductible, c'est-à-dire que ce n'est pas une instance d'un membre gauche d'une des règles, ou encore qu'il n'est pas filtré (au sens du filtrage du premier ordre) par le membre gauche de l'une des règles, mais il est surréductible c'est-à-dire qu'une de ses instance est réductible ou encore qu'il est unifiable (au sens de l'unification du premier ordre) avec le membre gauche de l'une des règles. En unifiant, au sens ordinaire, le terme z + 5 avec le terme Succ(x) + y on instancie z en Succ(z ′ ). Le terme Succ(z ′ ) + 5 se réduit alors en Succ(z ′ + 5). En procédant de même on instancie z ′ en Succ(z ′′ ), puis z ′′ en 0 ce qui donne la solution z → 2. est démontrable car la proposition ε(A ∨ ¬A) l'est, mais on ne peut rien déduire de la forme clausale de sa négation ¬ε(X).

En résolution d'ordre supérieur, cela a amené à proposer une nouvelle règle de déduction, la règle de scission (splitting), qui consiste à instancier arbitrairement les littéraux dont le symbole de tête est une variable en des propositions formées avec des connecteurs et des quantificateurs. Par exemple, en partant de la clause ¬X, on instancie la variable X par le terme Y ∨ Z ce qui donne après mise en forme clausale de

}/E 1 ∪ E 2 ∪ {A 1 = E . . . A n = E C 1 = E . . . C p } C/E si l → r ∈ R Surréd. étendue cl(C[r] p )/(E ∪ {C |p = E l})

Les contraintes

Comme d'habitude, quand les problèmes d'unification ne sont pas décidables et unitaires, la bonne formulation de la résolution est celle de la résolution contrainte [START_REF] Huet | Constrained resolution : a complete method for higher order logic[END_REF][START_REF] Huet | A mechanization of type theory[END_REF]. Les problèmes d'unification ne sont pas toujours immédiatement résolus au moment de l'application des règles, mais leur résolution peut être retardée. On les garde alors comme des contraintes. Nous aboutissons alors au système de la figure 5.1 appelé Résolution et surréduction étendues ou, plus simplement, Résolution modulo.

La complétude

La complétude de cette méthode s'exprime comme le fait que si une proposition A est démontrable en déduction modulo, alors de la forme clausale de sa négation, on peut déduire par les règles ci-dessus une clause contrainte vide, c'est-à-dire une clause de la forme 2/E où E est un ensemble unifiable de contraintes.

Dans [g], on montre que cette complétude est atteinte pour toutes les théories modulo qui ont la propriété d'élimination des coupures, faute de quoi il faut se restreindre aux propositions A qui ont une démonstration sans coupures.

Un exemple simple

Pour comprendre pourquoi il est plus efficace de transformer un axiome A ⇔ B en une règle de réécriture de l'ensemble R et d'utiliser la règle de surréduction étendue plutôt que de garder cet axiome tel quel, on peut considérer l'exemple suivant.

Si on veut réfuter la théorie

P 1 ⇔ (Q 2 ∨ P 2 ), P 1 , Q 2 ⇔ ⊥, P 2 ⇔ ⊥,

¬P n+1

En revanche, si on transforme les propositions P i ⇔ (Q i+1 ∨ P i+1 ) en des règles de réécriture Certes, réduire la proposition P 1 a un certain coût, mais ce coût est sans comparaison avec celui de la recherche non déterministe d'une réfutation par résolution de l'ensemble de clauses ci-dessus. Ce processus de réduction est, en effet, déterministe car le système de réécriture est confluent.

P i → Q i+1 ∨ P i+1 les propositions Q i ⇔ ⊥ en des règles de réécriture Q i → ⊥

La démonstration automatique en théorie des types simples

La surréduction et la scission

Dans le cas de la théorie des types simples, on partitionne les règles de réécriture en deux ensembles. Les règles de l'ensemble E qui sont exactement les règles du λσ-calcul (avec η-réduction)

(λa)b → a[b.id] λ(a 1) → b si a = σ b[↑] (a b)[s] → (a[s] b[s]) 1[a.s] → a a[id] → a (λa)[s] → λ(a[1.(s • ↑)]) (a[s])[t] → a[s • t] id • s → s ↑ • (a.s) → s (s 1 • s 2 ) • s 3 → s 1 • (s 2 • s 3 ) (a.s) • t → a[t].(s • t) s • id → s 1. ↑→ id 1[s].(↑ • s) → s
et les règles de l'ensemble R qui sont les autres règles

ε( ∧ x y) → ε(x) ∧ ε(y) ε( ∨ x y) → ε(x) ∨ ε(y) ε( ⇒ x y) → ε(x) ⇒ ε(y) ε( ¬ x) → ¬ε(x) ε( ⊥) → ⊥ ε( ∀T x) → ∀y ε(x y) ε( ∃T x) → ∃y ε(x y)
Remarquons qu'en logique classique, on peut se restreindre à n'utiliser que les connecteurs ∨ et ¬ et le quantificateur ∀, les autres pouvant se définir à l'aide des règles de De Morgan. De même, on peut se restreindre à n'utiliser que les symboles ∨, ¬ et ∀. Dans ce cas le système R se réduit aux règles

ε( ∨ x y) → ε(x) ∨ ε(y) ε( ¬ x) → ¬ε(x) ε( ∀T x) → ∀y ε(x y)
La règle de surréduction étendue se spécialise alors exactement en la règle de scission de [START_REF] Huet | Constrained resolution : a complete method for higher order logic[END_REF][START_REF] Huet | A mechanization of type theory[END_REF]. En effet, un littéral réduit est surréductible s'il n'a pas la forme ε( ∨ x y), ε( ¬ x), ε( ∀ x), mais s'il peut s'unifier avec une telle proposition. Il est facile de montrer que cette condition est équivalente au fait que le symbole de tête d'un tel littéral est une variable. La règle de surréduction étendue consiste à remplacer un tel littéral L, ou bien par ε(x) ∨ ε(y) en ajoutant la contrainte L = ε( ∨ x y), ou bien par ¬ε(x) en ajoutant la contrainte L = ε( ¬ x), ou bien par ∀y ε(x y) en ajoutant la contrainte L = ε( ∀ x). C'est exactement la règle de scission.

La règle de scission n'est donc pas propre à la théorie des types. La nécessité d'utiliser une telle règle s'explique par le fait que la théorie des types contient des règles qui réécrivent des propositions atomiques en des propositions non atomiques. La forme de la règle de scission se déduit simplement de la forme de ces règles de réécriture.

L'unification équationnelle et l'unification d'ordre supérieur

L'unification équationnelle qui est utilisée dans cette méthode est l'unification équationnelle modulo le système E ci-dessus, c'est-à-dire modulo le λσ-calcul avec η-réduction.

Nous avons donné dans [c] un algorithme d'unification équationnelle dans le λσ-calcul qui peut être vu comme un algorithme optimisé de surréduction. Les optimisations portent sur trois points. D'une part, on utilise le théorème de terminaison de la réduction pour ne considérer que des équations en forme normale [START_REF] Werner | Normalizing narrowing for weakly terminating and confluent systems[END_REF] et pour réduire l'espace de recherche en spéculant sur la forme normale des solutions (en particulier sur leur symbole de tête). Ensuite, on reconnaît certaines équations qui n'ont pas de solution et on en simplifie d'autres en gardant le même ensemble de solutions. Enfin, on reconnaît certaines équations (entre termes flexibles) qui ont toujours des solutions et qu'il n'est donc pas nécessaire de résoudre puisque l'utilisation des contraintes permet de se limiter au test d'unifiabilité et ne demande jamais l'énumération des solutions [START_REF] Huet | Constrained resolution : a complete method for higher order logic[END_REF][START_REF] Huet | A mechanization of type theory[END_REF].

Nous avons établi dans [c] un théorème d'équivalence entre l'unification équationnelle modulo la théorie λσ et l'unification d'ordre supérieur [START_REF] Huet | A unification algorithm for typed lambda calculus[END_REF][START_REF] Huet | Résolution d'équations dans les Langages d[END_REF][START_REF] Snyder | Higher-order unification revisited : complete sets of transformations[END_REF] Nous avons enfin montré dans [c] que l'algorithme d'unification dans le λσ-calcul était plus simple, par certains aspects que l'algorithme d'unification d'ordre supérieur. En particulier l'utilisation de la substitution simple (du remplacement), et non de la substitution particulière du λ-calcul qui demande un renommage des variables, évite le codage fonctionnel de la portée des variables et permet une expression plus atomique des règles. Par exemple, une équation de la forme λa = λb se simplifie en a = b dans le λσ-calcul alors que dans le λ-calcul une telle simplification est incorrecte puisque la variable liée par le λ ne peut pas être substituée aux variables libres de a et b dans la première équation, mais le peut dans la seconde. Autre exemple, une variable X de sorte Γ ⊢ T → U peut être instanciée par un terme de la forme λY où Y est une variable de sorte T Γ ⊢ U alors qu'une telle instanciation est incomplète dans le λ-calcul, car il n'est plus possible ensuite d'instancier la variable Y par la variable liée par le symbole λ. Cette simplicité est due au fait que les contraintes de portée des variables sont incorporées dans les termes eux-mêmes par la précuisson.

Nous avons enfin montré dans [d] que la restriction de l'unification d'ordre supérieur aux patterns de Miller [START_REF] Miller | Unification under a mixed prefix[END_REF][START_REF] Miller | A logic programming language with lambda-abstraction, function variables, and simple unification[END_REF] pouvait également se définir dans le λσ-calcul. La décidabilité et le caractère unitaire de l'unification est alors une conséquence de l'inversibilité de certaines substitutions explicites.

De la résolution d'ordre supérieur à la résolution modulo

Par rapport à la résolution du premier ordre, la résolution d'ordre supérieur apporte trois nouveautés : l'unification d'ordre supérieur, la règle de scission et la skolémisation d'ordre supérieur (qui n'a, en fait, été formulée correctement que dix ans après l'apparition de la résolution d'ordre supérieur dans [START_REF] Miller | Proofs in higher order logic[END_REF][START_REF] Miller | A compact representation of proofs[END_REF]).

Plusieurs auteurs, en particulier M. Davis [24], ont insisté assez tôt sur le fait que la théorie des types n'était qu'une théorie du premier ordre comme les autres. On pouvait en tirer l'intuition que les outils introduits pour la résolution d'ordre supérieur avaient une portée plus générale et pouvaient s'appliquer à d'autres théories, en particulier à la théorie des ensembles. Cela suggérait le programme de définir une méthode de démonstration automatique pour la logique du premier ordre qui se spécialise exactement en la résolution d'ordre supérieur quand on l'applique à la formulation au premier ordre de la théorie des types.

Ce programme présentait deux difficultés : d'une part les présentations traditionnelles de la théorie des types comme une théorie du premier ordre utilisaient le schéma de compréhension ou des combinateurs, alors que l'unification d'ordre supérieur utilisait la notation plus élégante et plus compacte du λ-calcul. D'autre part, il semblait bien que la séparation entre calcul (β-réduction) et déduction que permettait la théorie des types était un élément essentiel pour le fonctionnement de l'unification d'ordre supérieur et de la scission.

Cette première difficulté a été surmontée par l'introduction des combinateurs catégoriques puis du calcul des substitutions explicites que nous avons utilisé dans [c] pour réduire l'unification d'ordre supérieur à l'unification équationnelle du premier ordre, puis dans [i] pour donner une formulation au premier ordre de la théorie des types intentionnellement équivalente à la formulation utilisant le λ-calcul. La seconde difficulté a été surmontée par l'introduction dans [g] d'un cadre général, la déduction modulo, qui permet de séparer calcul et déduction. Cela nous a permis de formuler une méthode de démonstration automatique pour la déduction modulo qui s'instancie exactement en la résolution d'ordre supérieur quand on l'applique à la formulation de la théorie des types donnée dans [i] et de réaliser ce programme.

Les particularités de la skolémisation d'ordre supérieur sont donc avant tout une conséquence du système de sortes du λσ-calcul. L'unification d'ordre supérieur en revanche est une forme particulière d'unification équationnelle et la scission une forme particulière de surréduction étendue.

La démonstration automatique en théorie des ensembles

En théorie des ensembles, toutes les règles de réécriture transforment des propositions atomiques en des propositions composées, l'ensemble E est donc vide et l'ensemble R contient toutes les règles de la figure 3.1. L'unification est donc simplement l'unification du premier ordre. La résolution modulo est incomplète car elle ne permet de démontrer que les propositions qui ont une démonstration sans coupures. Elle permet de démontrer le théorème de Cantor, mais pas le théorème de Crabbé Ici, il faudrait que la méthode de démonstration automatique devine la coupure qui se trouve dans la démonstration de Crabbé.

Les différences entre la résolution modulo en théorie des types et en théorie des ensembles sont discutées dans [j]. Cette discussion est illustrée par la recherche de démonstrations du théorème de Cantor dans les différentes formulations présentées au paragraphe 4.5.

Chapitre 6

Les types et la terminaison

Les types et les ensembles

Dans les chapitres précédents nous avons donné deux exemples de théories modulo, la théorie des types simples et la théorie des ensembles, qui se présentent, l'une et l'autre, comme des axiomatisations possibles des mathématiques. L'une et l'autre peuvent être vues comme des restrictions de la théorie naïve (incohérente) des ensembles. La théorie des ensembles restreint le schéma de compréhension à quatre instances et la théorie des types le restreint en le plaçant dans un langage multisorté.

La déduction modulo permet de jeter un regard nouveau sur les différences entre ces deux théories. Le système de réécriture associé à la théorie des ensembles ne termine pas, de ce fait la théorie des ensembles n'a pas la propriété d'élimination des coupures et la résolution modulo n'est pas complète. En revanche, le système de réduction de la théorie des types simples termine, cette théorie a la propriété d'élimination des coupures et la résolution modulo est complète.

Par ailleurs, la théorie des types dispose d'une notion primitive de fonction et de la possibilité de former un terme α(f, x) pour désigner l'image de l'objet x par la fonction f . Cela permet de définir des objets comme l'ensemble de Cantor plus simplement (en particulier avec moins de quantificateurs et de connecteurs) qu'en théorie des ensembles et la recherche de démonstrations fait moins souvent appel à la règle de surréduction qu'en théorie des ensembles.

Cependant, on ne peut pas ignorer certaines critiques souvent opposées à la théorie des types. D'abord, en utilisant un langage multisorté, c'est-à-dire restreint syntaxiquement, la théorie des types élude, plus qu'elle ne résout, le paradoxe de Russell. En caricaturant, on peut dire que la théorie des types résout le paradoxe du menteur en interdisant aux Crétois de prononcer la phrase "Tous les crétois sont menteurs". D'autre part il semble y avoir, dans cette théorie, une certaine redondance entre la notion de type et la notion d'ensemble, par exemple entre le type ι et l'ensemble λx ⊤ de type ι → o de tous les objets de type ι. Plus concrètement, on peut se demander comment choisir les ensembles qui sont destinés à être des types de base. Certains choisissent par exemple un type de base pour les entiers, alors que pour d'autres, les entiers ne sont que des objets de type (ι → o) → o qui se révèlent être des cardinaux finis. Autrement dit, la théorie des types renouvelle l'épineuse distinction entre propriété essentielle et propriété accidentelle.

Dans [START_REF] Quine | Set theory and its logic[END_REF], Quine a résolu le premier problème en donnant une formulation de la théorie des types comme une théorie du premier ordre ordinaire (c'est-à-dire monosortée). Pour cela, il suffit de relativiser [START_REF] Enderton | A mathematical introduction to logic[END_REF][START_REF] Gallier | Logic in computer science[END_REF] la présentation de la théorie des types comme une théorie du premier ordre multisortée. On peut, en effet, toujours traduire une théorie du premier ordre multisortée en une théorie monosortée en introduisant pour chaque symbole de fonction ou de prédicat un symbole de même arité et pour chaque sorte s un prédicat unaire T s et en traduisant les propositions comme suit :

-

x ′ = x, (f (t 1 , ..., t n )) ′ = f ′ (t ′ 1 , ..., t ′ n ), -(P (t 1 , ..., t n )) ′ = P ′ (t ′ 1 , ..., t ′ n ), -(A ⇒ B) ′ = A ′ ⇒ B ′ , (A ∧ B) ′ = A ′ ∧ B ′ , (A ∨ B) ′ = A ′ ∨ B ′ , (¬A) ′ = ¬A ′ , ⊥ ′ = ⊥, -(∀x A) ′ = ∀x (T s (x) ⇒ A ′ ), (∃x A) ′ = ∃x (T s (x) ∧ A ′ ).
La traduction d'une théorie Γ s'effectue en traduisant chacune des propositions et en ajoutant pour chaque symbole de fonction f de rang (s 1 , ..., s n , t) un axiome

∀x 1 ... ∀x n ((T s1 (x 1 ) ∧ ... ∧ T sn (x n )) ⇒ T t (f (x 1 , ..., x n )))
et pour chaque sorte s un axiome ∃x T s (x)

On peut alors démontrer que Γ ⊢ P dans la théorie initiale si et seulement si Γ ′ ⊢ P ′ dans la théorie monosortée.

En exprimant ainsi la théorie des types comme une théorie du premier ordre monosortée, on résout le premier problème puisqu'on n'utilise plus d'artifice syntaxique pour éviter le paradoxe de Russell.

Comme la théorie des ensembles, la théorie des types apparaît comme une restriction du schéma de compréhension à certaines instances : celles qui sont stratifiables et dont les quantificateurs sont bornés. L'instance du schéma de compréhension utilisée dans le paradoxe de Russell

∃R ∀x (R x) ⇔ ¬(x x)
n'est pas un axiome de la théorie car la proposition ¬(x x) n'est la relativisation d'aucune proposition du langage multisorté. La question soulevée par Quine de savoir si on peut relâcher la condition des quantifications bornées et accepter toutes les instances stratifiables du schéma de compréhension, c'est-à-dire la cohérence de ses Fondations nouvelles (New foundations ou NF) est, à notre connaissance, toujours ouverte.

Si cette formulation de la théorie des types résout le premier problème, le second demeure car les types sont remplacés par les prédicats T ι , T o , T ι→o , ... qui sont toujours redondants avec certains ensembles. Dans [b], nous avons proposé une formulation de la théorie des types dans laquelle les types ne sont que des ensembles particuliers. Pour cela, on introduit dans le langage lui-même des symboles I, O et →, on supprime les symboles T s et on traduit les propositions de la forme T s (t) par ε(s ′ t), où s ′ est défini comme suit :

-

ι ′ = I, o ′ = O, -(T → U ) ′ = T ′ → U ′ .
L'expression I → I, à la différence du type ι → ι, est un terme du langage.

Nous montrons dans [b], en utilisant des techniques de construction de modèles, qu'une proposition est démontrable en théorie des types si et seulement si sa traduction l'est dans cette théorie.

La réduction dans un cadre monosorté

On peut, à présent, s'interroger sur la possibilité de présenter cette théorie comme une théorie modulo. Dans cette théorie, les axiomes de conversion sont des axiomes gardés. Par exemple, l'un de ces axiomes se formule Autrement dit, rien dans ce langage n'interdit de former une proposition comme ε(λx ¬(x x) λx ¬(x x)), mais cette proposition n'est pas prouvablement équivalente à sa négation et a fortiori ne se réduit pas sur elle, car l'argument auquel la fonction est appliquée n'est pas dans son domaine de définition et donc l'image obtenue n'est pas spécifiée par la théorie.

Dans ce cadre restreint où les ensembles de définition des fonctions ne sont que quelques ensembles particuliers (les types, c'est-à-dire les ensembles formés à partir des ensembles I et O avec le constructeur d'espace fonctionnel →), on peut espérer que ces gardes soient décidables. Mais nous proposons dans le dernier paragraphe de [b] une extension de cette théorie dans laquelle, comme dans les mathématiques informelles, n'importe quel ensemble peut être ensemble de définition d'une fonction. Il est alors illusoire d'espérer décider les gardes des règles de réécriture.

Pour avoir à la fois un système de réécriture dont les gardes sont décidables et la possibilité de prendre n'importe quel ensemble comme ensemble de définition d'une fonction, il faut demander, à chaque fois qu'on applique une fonction à un objet, une démonstration que cet objet est dans l'ensemble de définition de cette fonction. Cela demande de faire des démonstrations des objets à part entière de la théorie.

6.3 Les démonstrations objets de la théorie

Les motivations

Si on demande, à chaque fois qu'on applique une fonction à un objet, une démonstration que cet objet est dans l'ensemble de définition de cette fonction, l'application n'est plus une opération binaire qui s'applique à une fonction et son argument, mais une opération ternaire qui s'applique à une fonction, son argument et une démonstration que cet argument est dans l'ensemble de définition de la fonction. Cette méthode est la manière traditionnelle de traiter des "fonctions partielles" (c'est-à-dire les fonctions dont le domaine de définition est une partie d'un type et non un type entier) en théorie des types de Martin-Löf, dans le Calcul des constructions ou dans le Calcul des constructions inductives.

Ici, puisque nous sommes dans un cadre non typé, rien n'empêche de former le terme α(f, a, p) où a est un objet qui n'est pas dans le domaine de définition de f et p est un terme quelconque. Mais dans ce cas, la vérification que p est une démonstration que a est dans l'ensemble de définition de f échoue et les règles de réduction ne s'appliquent pas.

Une seconde motivation pour construire une théorie où les démonstrations sont des objets à part entière est, comme nous l'avons déjà évoqué au paragraphe 4.6, de donner des règles de calcul pour l'opérateur de descriptions.

Une formulation sans types des mathématiques où les démonstrations sont des objets

Plusieurs formalisations des mathématiques dans lesquelles les démonstrations sont des objets ont été proposées, parmi lesquelles la théorie des types de Martin-Löf, le Calcul des constructions et le Calcul des constructions inductives. Toutes ces théories sont des théories typées. Cela s'explique par le fait que leurs auteurs ont toujours cherché un formalisme dans lequel la β-réduction termine et par le fait que l'isomorphisme de Curry-De Bruijn-Howard entre propositions et types demande un langage typé.

Nous défendons le point de vue qu'il n'est pas nécessaire d'interdire l'application d'une fonction à un argument qui est hors de son domaine de définition par des règles syntaxiques, mais qu'il est suffisant d'interdire la β-réduction quand l'argument d'une fonction n'est pas dans cet ensemble. (Simplement parce que la règle de β-réduction est fausse dans ce cas, si f est la fonction identité définie sur l'ensemble des nombres pairs f = x ∈ P -→ x, alors f (1) n'est pas nécessairement égal à 1. La valeur de ce terme n'est pas spécifiée par les axiomes.) En suivant ce point de vue, seule la terminaison de la β-réduction gardée importe.

Par ailleurs, l'isomorphisme de Curry-De Bruijn-Howard nous paraît un outil utile en théorie de la démonstration (c'est-à-dire quand on cherche à construire un langage L ′ pour exprimer les démonstrations d'une théorie fondée sur un langage L, sans confusion entre ces langages (voir, par exemple, le chapitre 4)) mais pas nécessairement quand on cherche à construire une théorie fondée sur un langage L telle que les démonstrations de cette théorie soient exprimables dans ce même langage L.

Dans [f] nous avons proposé une première tentative de langage non typé dans lequel les démonstrations sont des objets. Pour cela, nous avons introduit un symbole pr tel que si P est un contenu propositionnel, alors pr(P ) est l'ensemble des démonstrations de la proposition ε(P ). La sémantique de Brouwer-Heyting-Kolmogorov s'exprime alors par certains axiomes de la théorie, par exemple ε(pr(P ⇒Q) = pr(P ) → pr(Q))

On retrouve ici plusieurs outils que nous avons introduits dans les versions multisortée et monosortée de la théorie des types simples : la distinction entre proposition et contenus propositionnels, la notion primitive de fonction, le constructeur d'espace fonctionnel →, ... Les propositions p ∈ pr(P ) ne sont pas toujours décidables, mais on donne dans [f] un algorithme qui permet d'en décider certaines : on montre qu'à chaque fois que la proposition ε(P ) est démontrable, il existe un terme p tel que la proposition p ∈ pr(P ) soit non seulement démontrable, mais de plus reconnue par l'algorithme. On appelle ces démonstrations reconnues par l'algorithme démonstrations directes. On montre aussi que si p une démonstration indirecte de P , et que q est une démonstration directe de p ∈ pr(P ), alors on peut construire à partir de p et q une démonstration directe de P .

Le paradoxe de Tarski

On montre enfin qu'on peut poser l'axiome "vérité = démontrabilité" ε(P ⇔ ∃x ∈ pr(P )) sans qu'on puisse pour autant appliquer le paradoxe de Tarski pour montrer l'incohérence de cette théorie. En effet, réfléchir les propositions comme des termes (c'est-à-dire avoir une fonction "." qui associe un terme à chaque proposition), un prédicat de vérité T et un schéma P ⇔ T ("P ") n'est pas contradictoire en soi. Si Γ est une théorie qui a un modèle M de plus de deux éléments, on peut montrer facilement qu'ajouter ce schéma à Γ n'est pas contradictoire, il suffit d'appeler 0 et 1 deux éléments distincts de M, de prendre 1 comme dénotation de "P " si la proposition P est valide dans M et 0 sinon, et d'interpréter T par l'ensemble {1}.

La contradiction, dans le paradoxe de Tarski, vient de l'existence d'un prédicat de substitution, c'est-àdire d'un prédicat R tel qu'on puisse démontrer la proposition ∀x ∀y ∃z R(x, y, z) et pour toute proposition P et terme t, la proposition (schéma de substitution) R("P ", t, q) ⇔ q = "P [t/x]" Le théorème de Tarski montre que dès qu'on a un prédicat de vérité, ce schéma de substitution est une forme du schéma de compréhension de la théorie naïve des ensembles. En effet, en skolémisant la proposition ∀x ∀y ∃z R(x, y, z) on obtient ∀x ∀y R(x, y, α(x, y))

et donc pour toute proposition P et terme t, on a R("P ", t, α("P ", t)) soit α("P ", t) = "P [t/x]"

En utilisant les axiomes de l'égalité, on obtient T (α("P ", t)) ⇔ T ("P [t/x]") et comme T est un prédicat de vérité T (α("P ", t)) ⇔ P [t/x] On peut s'interroger sur l'existence de restrictions de la théorie des ensembles pour lesquelles le système de réécriture termine et la propriété d'élimination des coupures est vérifiée. Une solution est sans doute de restreindre le schéma de compréhension aux propositions P stratifiables au sens de Quine. On aurait alors un système intermédiaire entre N F et Z. On peut remarquer que ce système n'est pas typé, comme d'usage en théorie des ensembles, il restreint la formation des objets en agissant sur les axiomes et non sur la syntaxe du langage, et il est sans doute suffisant pour exprimer une bonne partie des mathématiques informelles. Un résultat qui semble indiquer que ce programme est réalisable est la démonstration par S.C. Bailin [START_REF] Bailin | A normalization theorem for set theory[END_REF] de l'élimination des coupures pour une variante de la théorie des ensembles dans laquelle une règle de déduction t ∈ t ⊥ est ajoutée, ainsi qu'un mécanisme de priorité qui interdit d'appliquer une règle autre que celle-ci à une proposition de cette forme.

Conclusion

La principale contribution de ce dossier d'habilitation est d'avoir proposé un ensemble de règles de déduction qui permet d'intégrer le calcul et le raisonnement. Certes, cette idée n'est pas nouvelle : Plotkin et Andrews l'avaient déjà implicitement proposé dans le cadre de la démonstration automatique, le langage du système Automath, la théorie des types de Martin-Löf, le Calcul des constructions et le Calcul des constructions inductives comportaient déjà une règle de conversion, l'Arithmétique fonctionnelle du second ordre permettait déjà d'utiliser les axiomes équationnels sans laisser de trace dans la démonstration. Mais nous soutenons que cette distinction qui est centrale en mathématique doit être étudiée dans le cadre le plus général possible : la logique du premier ordre. Les applications en démonstration automatique et en λ-calcul s'en déduisent alors naturellement.

Par ailleurs, nous avons insisté sur la possibilité d'utiliser des règles de calcul qui transforment des propositions atomiques en des propositions non atomiques. C'est dans ce cadre qu'on peut exprimer des systèmes puissants comme la théorie des types simples et la théorie des ensembles. Ce sont ces règles de calcul qui sont responsables de la difficulté de démontrer l'élimination des coupures et ce sont elles qui, en démonstration automatique, rendent nécessaire la règle de surréduction étendue.

Cette habilitation propose deux autres contributions plus techniques qui consistent à replacer le théorème d'élimination des coupures et les algorithmes de démonstration automatique développés pour la théorie des types simples dans le cadre plus général de la déduction modulo. Nous défendons le point de vue que les outils qui ont été développés dans ces deux cas ne sont en rien propres à cette théorie, et qu'ils ont une portée beaucoup plus générale.

Contrairement à ce que nous avions fait dans les articles qui constituent ce dossier, nous avons accordé une large place, dans ce mémoire, à des conjectures et à la discussion de problèmes encore mal dégrossis. On peut donc à présent tracer un programme de travail pour les années à venir : en premier lieu, nous avons conjecturé qu'on pouvait toujours construire un prémodèle pour une congruence présentée par un système de réécriture confluent et qui termine. Si nous croyons cette conjecture vraie, parce que nous n'avons pas réussi à construire de contre-exemple, nous pouvons cependant nous demander si elle peut être démontrée en théorie des ensembles, ou si, au contraire, elle implique la cohérence de cette théorie. Nous avons également uniquement esquissé les applications de la notion de déduction modulo dans le cadre du λ-calcul typé avec des types dépendants. Nous laissons également ouvert le problème de trouver une axiomatisation des mathématiques non typée dont le système de réécriture termine et dans laquelle les fonctions sont des objets primitifs. Si la notion de β-réduction gardée nous semble ici essentielle, il est probable que cela demande de développer une théorie non typée dans laquelle les démonstrations sont des objets, et nous avons évoqué les difficultés, notamment de cohérence, que cela pose.

Enfin, nous voudrions conclure par une perspective qui concerne la déduction modulo elle-même. Dans le système de déduction naturelle modulo que nous avons présenté au chapitre 1, les règles de déduction peuvent modifier les axiomes de la théorie (c'est, par exemple, le cas de la règle d'introduction de l'implication) mais jamais la congruence. De ce fait, la congruence est fixée une fois pour toutes au début de la démonstration et ne peut pas s'enrichir. On peut imaginer un cadre plus général où il serait possible de transformer dynamiquement un théorème en une règle de réécriture. Il faudrait alors donner à ce moment un métaargument qui assurerait que le système de réécriture reste confluent et qu'il continue à terminer. Éventuellement, cela peut demander d'utiliser un algorithme de complétion pour compléter le système de réécriture enrichi.

Cela nous semble particulièrement important pour les démonstrations par récurrence où on veut souvent transformer l'hypothèse de récurrence en une règle de réécriture pour résoudre la conclusion.

Une telle possibilité correspondrait également davantage à la pratique mathématique : au sein des mathématiques, nous développons des algorithmes, nous montrons leur terminaison puis nous les incorporons peu à peu à nos automatismes de calcul qui, ainsi, s'enrichissent sans cesse.

Index

7 2 4 Figure 1 -

 741 Figure 1 -Deux et deux font quatre

Figure 1 . 2 -

 12 Figure 1.2 -Le calcul des séquents modulo

1. 2 . 1

 21 La réécriture des termesUne congruence peut se définir par un ensemble de règles de réécriture sur les termes du langage. En arithmétique, par exemple, on pose les règles0 + y → y Succ(x) + y → Succ(x + y) 0 × y → 0 Succ(x) × y → x × y + yDe même, quand on utilise une opération associative, on pose la règle (x + y) + z → x + (y + z)

1. 3 .

 3 LE LEMME D'ÉQUIVALENCE Dans cet exemple, on réécrit une proposition atomique sur une autre proposition atomique. Dans d'autres exemples, on veut pouvoir effectuer des calculs qui introduisent des connecteurs ou des quantificateurs. Par exemple, dans les anneaux intègres, la règle x × y = 0 → x = 0 ∨ y = 0 transforme une proposition atomique en une disjonction.

Proposition 1 . 3 . 1 (

 131 Équivalence) Soit une congruence ≡, et T la théorie formée de toutes les clôtures universelles des propositions de la forme A ⇔ B où A ≡ B. On a Γ ⊢ ≡ P si et seulement si T Γ ⊢ P Naturellement, si les propositions démontrées sont les mêmes, les démonstrations sont très différentes. En particulier elles sont beaucoup plus courtes car les étapes calculatoires ont été supprimées.

Proposition 1 . 4 . 3

 143 Pour tout modèle M de (≡, Γ), il existe un modèle égalitaire M ′ qui valide les mêmes propositions.Soit M un modèle de (≡, Γ). On appelle E la plus petite relation d'équivalence définie sur sur les éléments de M , l'ensemble de base de M, telle que a et b sont mis en relation s'il existe des termes t et u tels que t ≡ u, où t dénote a et u dénote b. On pose M ′ = M/E. La relation ≡ étant une congruence, les dénotations des symboles de fonction et de prédicat de M passent au quotient, ce qui définit un modèle M ′ . On montre par récurrence structurelle que la dénotation d'un terme dans M ′ est la classe de sa dénotation dans M et la dénotation d'une proposition dans M ′ est sa dénotation dans M.

1 .

 1 on doit donner un ensemble D Γ⊢T ou D Γ⊢∆ pour chacune de ces sortes. Cette construction se fait en deux étapes. On construit, dans un premier temps, une famille d'ensembles M T en partant de deux ensembles M ι et M o et en définissant M T →U comme l'ensemble des fonctions de M T dans M U , puis dans un second temps les ensembles D Γ⊢T et D Γ⊢∆ , encore une fois comme des ensembles de fonctions. L'ensemble D T1,...,Tn⊢U est défini comme M U M T 1 ×...×M Tn ou mieux, en curryfiant, comme l'ensemble M U M Tn ... M T De même, l'ensemble D T1,...,Tn⊢U1,...,Up est défini comme

Figure 2 . 2 -

 22 Figure 2.2 -Les règles de réécriture de la théorie des types simples avec des substitutions explicites

Figure 2 . 3 - 1 .

 231 Figure 2.3 -Règles étendues pour les combinateurs

  Si a est par exemple l'indice de De Bruijn 1 on obtient le terme (app n 1 n+1 |b| n ). Ce terme n'est pas réductible par le système ci-dessus et la règle du λσ-calcul ((λa) b) → a[b.id] suggère la règle (app n 1 n+1 b) → b. L'étude des différents cas amène au système de réécriture de la figure 2.3.

Figure 3 . 1 -

 31 Figure 3.1 -Les règles de réécriture de la théorie des ensembles

  En déduction naturelle modulo, comme en déduction naturelle du premier ordre, une coupure est simplement une règle d'introduction d'un connecteur ou d'un quantificateur suivie d'une règle d'élimination de ce même symbole. Le processus d'élimination des coupures se définit comme en déduction naturelle du premier ordre. En revanche, sa terminaison pose davantage de problèmes. Si on n'impose pas de restriction sur la congruence, il n'est pas difficile d'exhiber une démonstration qui n'a pas de forme normale. Par exemple, avec la règle A → ¬A, la démonstration axiome

Figure 4 . 1 -

 41 Figure 4.1 -Les règles de typage des démonstrations

  xn,w,P (y 1 , ..., y n , z) → ∀a ∀b 1 ... ∀b n (a = v ∧ b 1 = y 1 ∧ ... ∧ b n = y n ) ⇒ a ∈ z ∧ [b 1 /x 1 , ..., b n /x n , a/w]P

Figure 4 . 2 -

 42 Figure 4.2 -Le λ-calcul avec des types dépendants

59

 59

5. 2

 2 La résolution modulo 5.2.1 La règle de surréduction étendue Dans le cas général, où on a des règles de réécriture qui réécrivent des propositions atomiques en des propositions non atomiques, la résolution équationnelle et la méthode des tableaux équationnelle, ne sont plus complètes. Par exemple, modulo la règle x × y = 0 → x = 0 ∨ y = 0 on peut démontrer la proposition a × a = 0 ⇒ a = 0 et donc ∃y (a × a = y ⇒ a = y) Pourtant, la mise en forme clausale de la négation de cette proposition donne les deux clauses a × a = Y ¬a = Y et les propositions a × a = Y et a = Y n'étant pas unifiables, on ne peut pas appliquer la règle de résolution avec succès. Ce problème a déjà été rencontré dans le cadre de la méthode de résolution d'ordre supérieur de Huet [50, 51]. En logique d'ordre supérieur, en effet, la la proposition ∃x x est démontrable car la proposition A ∨ ¬A l'est, mais on ne peut rien déduire de la forme clausale de sa négation. Dans notre présentation, cela s'exprime par le fait que la proposition ∃x ε(x)

Figure 5 . 1 -

 51 Figure 5.1 -La résolution modulo

  et la proposition P n ⇔ ⊥ en une règle de réécriture P n → ⊥ il ne reste plus que la proposition P 1 a mettre en forme clausale. Cette proposition se réduit sur ⊥ ∨ ... ∨ ⊥ et sa forme clausale est la clause vide.

  . Ce théorème exprime qu'un problème d'unification d'ordre supérieur a = b a une solution si et seulement si c'est également le cas du problème d'unification équationnelle dans λσ a F = b F où . F est l'injection du λ-calcul dans le λσ-calcul appelée précuisson (pre-cooking) et décrite au paragraphe 2.4.5 (mais qui a été introduite pour la première fois dans le cadre de cet algorithme d'unification [c]). Le sens direct du théorème est facile : si le premier problème a une solution c 1 /x 1 , ..., c n /x n alors le second a la solution x 1 → c 1F , ..., x n → c nF . Pour montrer la réciproque, on doit montrer que si le problème d'unification a F = b F a une solution alors il a aussi une solution dans l'image de la précuisson. Nous avons montré dans [c] que l'algorithme d'unification dans le λσ-calcul reproduisait fidèlement l'algorithme d'unification d'ordre supérieur, c'est-à-dire que chaque étape de cet algorithme pouvait être simulée par un nombre fini d'étapes de l'algorithme d'unification dans le λσ-calcul.

  ¬{x ∈ A | ¬x ∈ x} ∈ A en effet notons f le symbole de Skolem introduit par la skolémisation de l'axiome ∀A ∃B ∀x ((x ∈ B) ⇔ (x ∈ A ∧ ¬x ∈ x)) on a la règle de réécriture x ∈ f (y) → x ∈ y ∧ ¬x ∈ x la proposition de Crabbé s'écrit ¬f (a) ∈ a la forme clausale de sa négation est formée de l'unique clause f (a) ∈ a Avec cette clause on ne peut pas appliquer la règle de résolution, on ne peut pas non plus appliquer la règle de surréduction étendue car on devrait alors unifier la proposition f (a) ∈ a avec une proposition de la forme w ∈ {}(x, y), w ∈ P(x), w ∈ (x) ou w ∈ g(x 1 , ..., x n ). La contrainte se simplifierait en une contrainte de la forme a = {}(x, y) a = P(x) a = (x) ou a = g(x 1 , ..., x n ) et aucune de ces équations n'a de solution puisque a est une constante.

  (ε((I → I → I) a) ∧ ε((I → I) b) ∧ ε(I c)) ⇒ (S I,I,I a b c) = (a c (b c)) Les règles de réécriture correspondantes doivent donc également être gardées. Pour réduire (S I,I,I a b c) en (a c (b c)), il faut au préalable "vérifier" que a appartient à l'ensemble I → I → I, b à l'ensemble I → I et c à l'ensemble I.

  x1,...,xn,w,P et un axiome ∀x 1 ... ∀x n ∀w (w ∈ f x1,...,xn,w,P (x 1 , ..., x n ) ⇔ P ) On peut, si on veut, noter {w | P } le terme f x1,...,xn,w,P (x 1 , ..., x n ) (ce point sera discuté en détail aux paragraphes 2.4 et 3.2). On peut remarquer que ce système de réécriture est trivialement confluent car il est orthogonal, mais qu'il ne termine pas. Un contre-exemple à la terminaison est le paradoxe de Russell : en notant R le terme {w | ¬w ∈ w} c'est-à-dire le symbole d'individu f w,¬w∈w , on a la règle de réécriture

Il est ensuite naturel de transformer ces axiomes en règles de réécriture v ∈ f x1,...,xn,w,P (y 1 , ..., y n ) → [y 1 /x 1 , ..., y n /x n , v/w]P

  Dans ce dernier schéma, on utilise un symbole d'égalité. On se place donc en logique du premier ordre avec égalité.Skolémiser ces axiomes amène à introduire un nombre infinis de symboles d'individu, qu'on peut noter {x 1 , ..., x n | P } et x 1 , ..., x n -→ t et les axiomes de conversion ∀x 1 ... ∀x n (ε({x 1 , ..., x n

x 1 , ..., x n . Et on pose également un schéma d'axiome de compréhension fonctionnelle ∃f ∀x 1 ... ∀x n (f x 1 ... x n ) = t où toutes les variables libres de t sont parmi x 1 , ..., x n .

  Deux et deux sont quatre." assertion, énoncé ou jugement. Hélas, cette terminologie introduit une confusion. D'une part, l'acte d'asserter, d'énoncer ou de juger n'est pas plus présent dans ε(t) que dans t, d'autre part, la terminologie de la logique du premier ordre oppose les termes qui sont les expressions désignant des objets et les propositions qui sont les expressions désignant des faits et il serait maladroit d'appeler le terme t proposition et la proposition ε(t) énoncé. Nous préférons donc appeler le terme t contenu propositionnel ou information et la proposition ε(t) proposition.Une autre remarque terminologique est que le symbole ε pourrait être noté comme le symbole de Frege "⊢", en suivant, par exemple, Whitehead et Russell qui distinguent la lexis p de l'assertion ⊢ p. Cela n'est pas possible, car dans le métalangage (c'est-à-dire dans le langage que nous utilisons pour parler des théories logiques) nous utilisons le symbole ⊢ pour affirmer qu'une proposition est démontrable. Nous devons donc distinguer : le terme p, la proposition ε(p) et la métaproposition ⊢ ε(p) affirmant que la proposition ε(p) est démontrable. En théorie des ensembles, on distingue, de même, l'ensemble P des nombres pairs, la proposition 4 ∈ P et la métaproposition ⊢ 4 ∈ P affirmant que cette proposition est démontrable.

	des propriétés différentes peuvent avoir des contenus différents même s'ils sont démontrables l'un et l'autre.
	On vera toutefois au paragraphe 6.3.3 que certains traits syntaxiques de la proposition doivent être gommés
	de son contenu, faute de quoi, le symbole ε peut se voir comme le prédicat de vérité d'A. Tarski et la théorie
	obtenue est contradictoire.
	2.3.2 Les termes, les propositions et les assertions
	Cette distinction entre une proposition ε(t) et son contenu t, ou lexis [61], est traditionnelle en grammaire
	où on distingue la proposition "Deux et deux sont quatre." du groupe nominal "que deux et deux sont quatre"
	qui remplit les fonctions d'un groupe nominal, par exemple la fonction d'objet dans la phrase "Je crois que
	deux et deux sont quatre." Elle permet donc d'utiliser les prédicats d'attitude propositionnelle comme des
	prédicats ordinaires.
	Une terminologie possible pour distinguer ces deux expressions est de nommer l'expression "que deux et
	deux sont quatre" proposition et l'expression "
	que quand on pose l'axiome d'extensionnalité
	∀x ∀y ((ε(x) ⇔ ε(y)) ⇒ x = y)
	le contenu d'une proposition se réduit à sa valeur de vérité. Mais en l'absence d'un tel axiome, le contenu
	d'une proposition peut véhiculer beaucoup plus sur la proposition elle-même. Deux théorèmes qui expriment

  x 1 , ..., x n un symbole f x1,...,xn,t et un axiome ∀x 1 ... ∀x n (f x1,...,xn,t x 1 ... x n ) = t De même, on introduit pour chaque proposition A dont les variables libres sont parmi x 1 , ..., x n un symbole P x1,...,xn,A et un axiome ∀x 1 ... ∀x n ((P x1,...,xn,A x 1 ... x

	Par exemple, on introduit un symbole S et l'axiome
	∀x ∀y ∀z (S x y z) = ((x z) (y z))

n ) ⇔ A)

  x et U le type de y et l'axiome ∀x ε(α(α(P, x), f (x))) Le symbole f est un symbole de fonction de rang (T, U ) et non un symbole d'individu de type T → U et on écrit donc f (x) et non α(f, x). De ce fait, il va de soi que le symbole f tout seul n'est pas un terme, car dans un langage du premier ordre, les symboles de fonction d'arité non nulle ne sont pas des termes. On retrouve ainsi la première condition de Miller. La seconde condition n'a pas lieu d'être, puisque dans le langage des combinateurs, il n'y a pas d'opérateur d'abstraction. Enfin, comme dans tout langage du premier ordre on dispose de quantificateurs indépendamment des symboles ∀ et ∃ de ce langage particulier. Il n'y a donc pas de problème de formulation de la proposition skolémisée

∀x ε(α(α(P, x), f (x))) et on peut formuler le théorème Proposition 2.6.1 Les propositions sans occurrences de symboles de Skolem sont conséquences d'une proposition si et seulement si elles sont conséquences de sa forme skolémisée.

  Cette définition est incorrecte, car la proposition [t/x]A peut très bien ne pas être normale. On peut alors tenter de remplacer cette seconde condition par -si π se réduit sur une démonstration de la forme λx π 1 alors pour terme t, [t/x]π 1 est une démonstration réductible de ([t/x]A) ↓. où ([t/x]A) ↓ est la forme normale de la proposition [t/x]A. Cette tentative échoue également, car la proposition ([t/x]A) ↓ n'est pas nécessairement plus petite que la proposition ∀x P .

1 alors pour tout terme t, [t/x]π 1 est une démonstration réductible de [t/x]A.

  A∧B est l'ensemble des démonstrations π telles que π est fortement normalisable et si π se réduit sur une démonstration de la forme (π 1 , π 2 ), alors π 1 est un élément de R A et π 2 est un élément de R B . -R A∨B est l'ensemble des démonstrations π telles que π est fortement normalisable et si π se réduit sur une démonstration de la forme i(π 1 ) (resp. j(π 2 )) alors π 1 est un élément de R A (resp. π 2 est un élément de R B ). -R ¬A est l'ensemble des démonstrations π telles que π est fortement normalisable et si π se réduit sur une démonstration de la forme λαπ 1 , alors pour toute démonstration π ′ de R A , [π ′ /α]π 1 est fortement normalisable. -R ⊥ est l'ensemble des démonstrations fortement normalisables. -R ∀x A est l'ensemble des démonstrations π telles que π est fortement normalisable et si π se réduit sur une démonstration de la forme λx π 1 alors pour tout terme t [t/x]π 1 est un élément de R [t/x]A . -R ∃x A est l'ensemble des démonstrations π telles que π est fortement normalisable et si π se réduit sur une démonstration de la forme (t, π 1 ) alors [t/x]π 1 est un élément de R [t/x]A . -Si P ≡ Q alors R P = R Q . Dans cette définition, nous avons fait le choix de ne pas normaliser les propositions dans l'expression des conditions sur les ensembles R ∀x P et R ∃x P . Cela nous impose d'ajouter la dernière condition : les propositions congruentes doivent avoir le même ensemble de démonstrations réductibles.

  (ou d'une famille d'ensembles dans le cas multisorté) de fonctions f et P est appelée prémodèle, et l'ensemble R A est appelé dénotation de A. La définition d'un prémodèle est la même que celle d'un modèle, sauf que les valeurs de vérité sont remplacées par des candidats de réductibilité et la dénotation des propositions composées est définie comme ci-dessus. Un prémodèle et donc un modèle multivalué dont les valeurs de vérités sont des candidats de réductibilité. Un prémodèle est un prémodèle d'un système de réécriture si deux propositions congruentes ont même dénotation.

′ 1 sont congruents, les ensembles P (t 1 , ..., t n ) et P (t ′ 1 , ..., t n ) doivent être identiques. La fonction P peut donc se définir comme une fonction d'un objet abstrait (par exemple, la classe de t 1 et t ′ 1 ) que t 1 et t ′ 1 dénotent. Enfin, la condition selon laquelle deux propositions congruentes doivent avoir le même ensemble de démonstrations réductibles est la même que celle que nous avons vue dans la définition des modèles d'une théorie modulo au paragraphe 1.4. Dans [h], nous avons donc utilisé le vocabulaire de la théorie des modèles : la donnée d'un ensemble M Dans [h] on a montré la proposition suivante Proposition 4.3.2 Si une congruence a un prémodèle, alors les démonstrations en déduction naturelle modulo cette congruence normalisent fortement.

  on applique ensuite la règle de résolution pour obtenir la clause vide. La règle de scission et la règle de résolution d'ordre supérieur forment ensemble un système complet pour la logique d'ordre supérieur[START_REF] Huet | Constrained resolution : a complete method for higher order logic[END_REF][START_REF] Huet | A mechanization of type theory[END_REF].Dans le cadre de la déduction modulo, il faut ajouter à la règle de résolution une règle qui anticipe l'instanciation d'un littéral, permettant de le réduire sur une proposition composée. Par exemple, le littéral {A 1 , . . . , A n , B 1 , . . . , B m }/E 1 {¬C 1 , . . . , ¬C p , D 1 , . . . , D q }/E 2 Rés. étendue {B 1 , . . . , B m , D 1 , . . . , D q

	la
	proposition ¬(Y ∨ Z) les deux clauses
	¬Y
	¬Z
	on instancie ensuite la variable Z par le terme ¬Z ′ ce qui donne les deux clauses
	¬Y
	Z ′

  la solution naïve donne les clauses ¬P 1 , Q 2 , P 2 En revanche, si on transforme la proposition P 1 ⇔ (Q 2 ∨ P 2 ) en une règle de réécritureP 1 → Q 2 ∨ P 2 et les propositions Q 2 ⇔ ⊥ et P 2 ⇔ ⊥, en les règles Q 2 → ⊥ P 2 → ⊥il ne reste plus que la proposition P 1 a mettre en forme clausale. Cette proposition se réduit sur ⊥ ∨ ⊥. Sa forme clausale est la clause vide.Plus généralement, si on veut réfuter la théorieP 1 ⇔ (Q 2 ∨ P 2 ), ..., P i ⇔ (Q i+1 ∨ P i+1 ), ..., P n ⇔ (Q n+1 ∨ P n+1 ), P 1 , Q 2 ⇔ ⊥, ..., Q n+1 ⇔ ⊥, P n+1 ⇔ ⊥,la solution naïve donne les 4n + 2 clauses ¬P 1 , Q 2 , P 2

	¬Q 2 , P 1
	¬P 2 , P 1
	P 1
	¬Q 2
	¬P 2
	¬Q 2 , P 1
	¬P 2 , P 1
	...
	¬P i , Q i+1 , P i+1
	¬Q i+1 , P i
	¬P i+1 , P i
	...
	¬P n , Q n+1 , P n+1
	¬Q n+1 , P n+1
	¬P n+1 , P n+1
	P 1
	¬Q 2
	...
	¬Q n+1

× 2 = 4 (x, 2 × x = 4, 2) ∃-intro ∃x (2 × x = 4)Substituer la variable x par le terme 2 dans la proposition 2 × x = 4 donne la proposition 2 × 2 = 4, qui est congruente à 4 = 4. Le passage d'une proposition à l'autre, qui requiert plusieurs fastidieuses étapes de démonstration dans la formulation traditionnelle de l'arithmétique de Peano, est ici gommée de la démonstration, c'est un simple calcul qui n'a pas besoin d'être écrit, puisque chacun peut le refaire.On peut remarquer que, dans cette démonstration, on n'utilise pas les axiomes de l'addition et de la multiplication. Cela s'explique par le fait que raisonner modulo une congruence permet de supprimer ces axiomes. En effet, si on pose que les termes 0 + x et x sont congruents, alors l'axiome ∀x 0 + x = x est congruent à l'axiome de l'égalité ∀x x = x, il est donc redondant et on peut le supprimer. 11

CHAPITRE 1. LA DÉDUCTION MODULOaxiome si A ∈ Γ et A ≡ B Γ ⊢≡ B Γ, A ⊢≡ B ⇒-intro si C ≡ (A ⇒ B) Γ ⊢≡ C Γ ⊢≡ C Γ ⊢≡ A ⇒-élim si C ≡ (A ⇒ B) Γ ⊢≡ B Γ ⊢≡ A Γ ⊢≡ B ∧-intro si C ≡ (A ∧ B) Γ ⊢≡ C Γ ⊢≡ C ∧-élim si C ≡ (A ∧ B) Γ ⊢≡ A Γ ⊢≡ C ∧-élim si C ≡ (A ∧ B) Γ ⊢≡ B Γ ⊢≡ A ∨-intro si C ≡ (A ∨ B) Γ ⊢≡ C Γ ⊢≡ B ∨-intro si C ≡ (A ∨ B) Γ ⊢≡ C Γ ⊢≡ D Γ, A ⊢≡ C Γ, B ⊢≡ C ∨-élim si D ≡ (A ∨ B) Γ ⊢≡ C Γ, A ⊢≡ ⊥ ¬-intro si B ≡ (¬A) Γ ⊢≡ B Γ ⊢≡ B Γ ⊢≡ A ¬-élim si B ≡ (¬A) Γ ⊢≡ ⊥ Γ ⊢≡ B ⊥-élim si B ≡ ⊥ Γ ⊢≡ A Γ ⊢≡ A (x, A) ∀-intro si B ≡ (∀x A) et x ̸ ∈ F V (Γ) Γ ⊢≡ B Γ ⊢≡ B (x, A, t) ∀-élim si B ≡ (∀x A) et C ≡ [t/x]A Γ ⊢≡ C Γ ⊢≡ C (x, A, t) ∃-intro si B ≡ (∃x A) et C ≡ [t/x]A Γ ⊢≡ B

axiome si A ≡ B A ⊢≡ B Γ, A ⊢≡ ∆ Γ ⊢≡ B, ∆ coupure si A ≡ B Γ ⊢≡ ∆ Γ, B1, B2 ⊢≡ ∆ contr-gauche si A ≡ B1 ≡ B2 Γ, A ⊢≡ ∆ Γ ⊢≡ B1, B2, ∆ contr-droite si A ≡ B1 ≡ B2 Γ ⊢≡ A, ∆ Γ ⊢≡ ∆ aff-gauche Γ, A ⊢≡ ∆ Γ ⊢≡ ∆ aff-droite Γ ⊢≡ A, ∆ Γ ⊢≡ A, ∆ Γ, B ⊢≡ ∆ ⇒-gauche si C ≡ (A ⇒ B) Γ, C ⊢≡ ∆ AΓ ⊢≡ B, ∆ ⇒-droite si C ≡ (A ⇒ B) Γ ⊢≡ C, ∆ Γ, A, B ⊢≡ ∆ ∧-gauche si C ≡ (A ∧ B) Γ, C ⊢≡ ∆ Γ ⊢≡ A, ∆ Γ ⊢≡ B, ∆ ∧-droite si C ≡ (A ∧ B) Γ ⊢≡ C, ∆ Γ, A ⊢≡ ∆ Γ, B ⊢≡ ∆ ∨-gauche si C ≡ (A ∨ B) Γ, C ⊢≡ ∆ Γ ⊢≡ A, B, ∆ ∨-droite si C ≡ (A ∨ B) Γ ⊢≡ C, ∆ Γ ⊢≡ A, ∆ ¬-gauche si B ≡ (¬A) Γ, B ⊢≡ ∆ Γ, A ⊢≡ ∆ ¬-droite si B ≡ (¬A) Γ ⊢≡ B, ∆ ⊥-gauche si A ≡ ⊥ Γ, A ⊢≡ ∆ Γ, [t/x]A ⊢≡ ∆ (x, A, t) ∀-gauche si B ≡ (∀x A) Γ, B ⊢≡ ∆ Γ ⊢≡ A, ∆ (x, A) ∀-droite si B ≡ (∀x A) et x ̸ ∈ F V (Γ∆) Γ ⊢≡ B, ∆

Proposition 1.5.1 (Conservativité) Soit (≡, Γ) une théorie modulo sur un langage L, on obtient une extension conservatrice de cette théorie en ajoutant un symbole d'égalité et les axiomes de l'égalité Eq correspondants.On montre que tout modèle égalitaire de la théorie (≡, Γ) sur le langage L s'étend en un modèle égalitaire de (≡, ΓEq) sur le langage L ∪ {=}, en interprétant l'égalité par l'égalité.On peut remarquer que cette démonstration ne marche pas si on ne se restreint pas aux modèles égalitaires. En effet, comme la congruence est définie sur les termes, quand on ajoute un nouveau prédicat elle s'étend automatiquement aux propositions atomiques formées avec ce prédicat. Ainsi, si t et u sont deux termes congruents la proposition t = u est congruente à t = t et elle est donc démontrable.

On note x 1 → t 1 , ..., xn → tn la substitution simple, ou le remplacement, des variables x 1 , ..., xn par les termes t 1 , ..., tn par opposition à la notation t 1 /x 1 , ..., tn/xn qui désigne la substitution "avec renommage" utilisée dans les langages avec lieurs.Cette notation x 1 → t 1 , ..., xn → tn avec une flèche courte → ne doit pas être confondue avec la notation x 1 , ..., xn -→ t avec une flèche longue.

le type C et le terme

n'est pas bien typé.Les jugements de typage sont donc de la forme Γ ⊢ t : T où Γ est un contexte de typage, c'est-à-dire une liste de types. Pour exprimer le λσ-calcul typé comme un langage du premier ordre multisorté, nous avons proposé dans[c] puis dans[i], de considérer des sortes de la forme Γ ⊢ T où T est un type simple et Γ une liste de types simples. Les substitutions qui sont des listes de termes ont naturellement des types qui sont des listes de types simples. Comme les termes, elles doivent être typées dans un contexte. Elles ont donc des sortes de la forme Γ ⊢ ∆ où Γ et ∆ sont des listes de types simples.On doit ensuite, comme c'était déjà le cas avec les combinateurs, distinguer divers symboles en fonction de leur sorte. Par exemple, on a un nombre infini de constantes de 1 Γ A , la constante 1 Γ A étant de sorte AΓ ⊢ A. On aboutit au langage suivant.

axiome si α : A ∈ Γ, A ≡ B Γ ⊢≡ α : B Γ, α : A ⊢≡ π : B ⇒-intro si C ≡ (A ⇒ B) Γ ⊢≡ λα π : C Γ ⊢≡ π : C Γ ⊢≡ π ′ : A ⇒-élim si C ≡ (A ⇒ B) Γ ⊢≡ (π π ′ ) : B Γ ⊢≡ π : A Γ ⊢≡ π ′ : B ∧-intro si C ≡ (A ∧ B) Γ ⊢≡ (π, π ′ ) : C Γ ⊢≡ π : C ∧-élim si C ≡ (A ∧ B) Γ ⊢≡ fst(π) : A Γ ⊢≡ π : C ∧-élim si C ≡ (A ∧ B) Γ ⊢≡ snd(π) : B Γ ⊢≡ π : A ∨-intro si C ≡ (A ∨ B) Γ ⊢≡ i(π) : C Γ ⊢≡ π : B ∨-intro si C ≡ (A ∨ B) Γ ⊢≡ j(π) : C Γ ⊢≡ π : D Γ, α : A ⊢≡ π ′ : C Γ, β : B ⊢≡ π ′′ : C ∨-élim si D ≡ (A ∨ B) Γ ⊢≡ (δ π απ ′ βπ ′′ ) : C Γ, α : A ⊢≡ π : ⊥ ¬-intro si B ≡ (¬A) Γ ⊢≡ λα π : B Γ ⊢≡ π : B Γ ⊢≡ π ′ : A ¬-élim si B ≡ (¬A) Γ ⊢≡ (π π ′ ) : ⊥ Γ ⊢≡ π : B ⊥-élim si B ≡ ⊥ Γ ⊢≡ (botélim π) : A Γ ⊢≡ π : A (x, A) ∀-intro si B ≡ (∀x A), x ̸ ∈ F V (Γ) Γ ⊢≡λx π : B Γ ⊢≡ π : B (x, A, t) ∀-élim si B ≡ (∀x A), C ≡ [t/x]A Γ ⊢≡ (π t) : C

CHAPITRE 4. L'ÉLIMINATION DES COUPURES Déclaration et utilisation des variables : [ ] bien formé Γ ⊢ T : Kind Γ, x : T bien formé Γ ⊢ T : T ype Γ, x : T bien formé Γ bien formé x : T ∈ Γ Γ ⊢ x : T Construction des objets de type Kind : Γ bien formé Γ ⊢ T ype : Kind Γ ⊢ T : T ype Γ, x : T ⊢ T ′ : Kind Γ ⊢ Πx : T T ′ : KindConstruction des objets de type T ype :Γ ⊢ T : T ype Γ, x : T ⊢ T ′ : T ype Γ ⊢ Πx : T T ′ : T ype Γ ⊢ T : T ype Γ, x : T ⊢ T ′ : T ype Γ ⊢ Σx : T T ′ : T ype Γ ⊢ T : T ype Γ ⊢ T ′ : T ype Γ ⊢ T + T ′ : T ype Γ bien formé Γ ⊢ ∅ : T ypeConstruction et utilisation des fonctions :Γ ⊢ T : T ype Γ, x : T ⊢ T ′ : T ype Γ, x : T ⊢ t : T ′ Γ ⊢ λx : T t : Πx : T T ′ Γ ⊢ t : Πx : T T ′ Γ ⊢ t ′ : T Γ ⊢ (t t ′ ) : [t ′ /x]T ′ Construction et utilisation des couples : Γ ⊢ T : T ype Γ, x : T ⊢ T ′ : T ype Γ ⊢ a : T Γ ⊢ b : [a/x]T ′ Γ ⊢ (p Σx:T T ′ a b) : Σx : T T ′ Γ ⊢ U : T ype Γ ⊢ a : Σx : T T ′ Γ, x : T, y : T ′ ⊢ b : U Γ ⊢ (E a xyb) : U Construction et utilisation des éléments des unions disjointes : Γ ⊢ T : T ype Γ ⊢ T ′ : T ype Γ ⊢ a : T Γ ⊢ (i T,T ′ a) : T + T ′ Γ ⊢ T : T ype Γ ⊢ T ′ : T ype Γ ⊢ b : T ′ Γ ⊢ (j T,T ′ b) : T + T ′

λ-calcul, 26 avec des constructeurs de types, 49, 57 avec des substitutions explicites, 27 avec des types dépendants, 54 avec des types dépendants modulo, 54 avec des types inductifs, 57 faible avec des substitutions explicites, 34 polymorphe, 49, 57 λσ-calcul, 27 lemme d'équivalence, 15 de conservativité, 16 lexis, 23 méthode de Tait, 46 modèle, 15, 49 opérateur de descriptions, 54, 69 paradoxe de Russell, 19 de Tarski, 23, 70 plongement d'une théorie dans le λ-calcul, 54 d'une théorie modulo dans le λ-calcul, 55 précuisson (pre-cooking), 30, 64 prémodèle, 48 programmation en langage mathématique, 8, 54 proposition de Crabbé, 40, 44, 65 raisonnement, 7 réductible, 46 règle de réduction des démonstrations, 44 de réécriture, 14 de la théorie des ensembles, 40 de la théorie des types simples, 22 de typage des démonstrations, 45 résolution équationnelle, 59 modulo, 60 schéma de compréhension, 19, 24 fermé, 25 ouvert, 25 scission, 60