<figure><img src="image_1.png" /></figure>

HAL
open science

# Démonstration Automatique dans le Calcul des Constructions

Gilles Dowek

<figure><img src="image_2.png" /></figure>

## To cite this version:

Gilles Dowek. Démonstration Automatique dans le Calcul des Constructions. Informatique [cs]. Université de Paris 7 - Denis Diderot, 1991. Français. NNT: tel-04201468

HAL Id: tel-04201468

https://inria.hal.science/tel-04201468

Submitted on 10 Sep 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
THESE DE DOCTORAT

présentée

A L'UNIVERSITE PARIS 7

Spécialité : Informatique Fondamentale

par

Gilles DOWEK

Sujet de la thèse :

Démonstration Automatique
dans le
Calcul des Constructions

Soutenue le 16 décembre 1991 devant la Commission d'examen composée de :

MM.

Dominique Perrin
Thierry Coquand
Michel Parigot
Hassan Aït-Kaci
Gérard Huet
Gordon Plotkin
Christian Queinnec
Président
Rapporteurs
Examinateurs
Je tiens, avant toute chose, à remercier Monsieur le Professeur Dominique Perrin de l'honneur qu'il me fait en présidant le jury de cette thèse. Je voudrais également remercier Messieurs Thierry Coquand et Michel Parigot qui ont lu ces pages avec une grande patience et Messieurs Hassan Aït-Kaci, Gordon Plotkin et Christian Queinnec de l'intérêt qu'ils portent à ce travail en formant le jury qui le sanctionne.

Gérard Huet m'a tout d'abord proposé ce sujet de recherche, il en a ensuite constamment suivi le déroulement, modérant de sa lucidité mes excès d'enthousiasme et de découragement. J'aimerais qu'il sache combien je l'en remercie.

Nombre des idées présentées ici m'ont été suggérées par des membres du projet Formel de l'INRIA, qui m'a accueilli pour ce travail. En particulier, l'idée d'utiliser des termes marqués pour prouver le résultat du chapitre 2 m'a été donnée par Gérard Huet et celle d'utiliser un codage à la Harper-Honsel-Plotkin pour prouver la normalisation de la réduction sur ces termes par Christine Paulin-Mohring. Il va sans dire que l'influence de cet exceptionnel environnement de travail a été déterminante.
# Table des matières

<table><tbody><tr><td>1</td><td>Trois Formalismes Logiques</td><td>13</td></tr><tr><td>1.1</td><td>Logique du Premier Ordre</td><td>13</td></tr><tr><td>1.1.1</td><td>Termes</td><td>13</td></tr><tr><td>1.1.2</td><td>Propositions</td><td>13</td></tr><tr><td>1.1.3</td><td>Déduction Naturelle</td><td>14</td></tr><tr><td>1.2</td><td>Logique d'Ordre Supérieur</td><td>16</td></tr><tr><td>1.2.1</td><td>λ-calcul</td><td>16</td></tr><tr><td>1.2.2</td><td>Logique d'Ordre Supérieur</td><td>19</td></tr><tr><td>1.2.3</td><td>Limites de la Logique d'Ordre Supérieur</td><td>21</td></tr><tr><td>1.3</td><td>Systèmes de Types</td><td>23</td></tr><tr><td>1.3.1</td><td>Quelques Systèmes de Types</td><td>23</td></tr><tr><td>1.3.2</td><td>Classification des Systèmes de Types</td><td>27</td></tr><tr><td>1.3.3</td><td>Propriétés des Systèmes de Types Purs</td><td>30</td></tr><tr><td>1.3.4</td><td>Une Extension de la Logique d'Ordre Supérieur : Le Calcul des Constructions</td><td>33</td></tr><tr><td>2</td><td>Bonne Fondation de la Récursion Simultanée sur le Type et les Sous-Termes Stricts d'un Terme</td><td>37</td></tr><tr><td>2.1</td><td>Termes Marqués</td><td>38</td></tr><tr><td>2.2</td><td>Normalisation des Termes Marqués</td><td>39</td></tr><tr><td>2.3</td><td>Terme Marqué Associé à un Terme non Marqué</td><td>41</td></tr><tr><td>2.4</td><td>Forme η-longue d'un Terme Marqué</td><td>43</td></tr><tr><td>2.5</td><td>Bonne Fondation de la Relation &lt;</td><td>44</td></tr><tr><td>3</td><td>Contextes Quantifiés Contraints, Substitution</td><td>47</td></tr><tr><td>3.1</td><td>Preuves Incomplètes</td><td>47</td></tr><tr><td>3.2</td><td>Contextes Quantifiés Contraints</td><td>49</td></tr><tr><td>3.3</td><td>Substitution</td><td>51</td></tr><tr><td>4</td><td>Une Méthode Complète de Synthèse de Preuves</td><td>55</td></tr><tr><td>4.1</td><td>Approches</td><td>55</td></tr><tr><td>4.1.1</td><td>Résolution et Unification</td><td>55</td></tr><tr><td>4.1.2</td><td>Unification à l'Ordre Supérieur</td><td>56</td></tr><tr><td>4.1.3</td><td>Résolution à l'Ordre Supérieur</td><td>56</td></tr><tr><td>4.1.4</td><td>Introduction-Résolution dans les Systèmes de Types</td><td>57</td></tr><tr><td>4.1.5</td><td>Une Méthode d'Enumeration des Termes d'un Type Donné</td><td>58</td></tr></tbody></table>
<table><tr><td>4.1.6</td><td>Nombre d'Applications</td><td>59</td></tr><tr><td>4.1.7</td><td>Variables dans la Proposition à Prouver</td><td>59</td></tr><tr><td>4.2</td><td>Une Méthode Complète</td><td>59</td></tr><tr><td>4.3</td><td>Exemples</td><td>62</td></tr><tr><td>4.3.1</td><td>Un Exemple au Premier Ordre</td><td>62</td></tr><tr><td>4.3.2</td><td>Un Exemple avec Scission</td><td>62</td></tr><tr><td>4.4</td><td>Propriétés</td><td>64</td></tr><tr><td>4.4.1</td><td>Typage</td><td>64</td></tr><tr><td>4.4.2</td><td>Correction</td><td>66</td></tr><tr><td>4.4.3</td><td>Complétude</td><td>67</td></tr><tr><td>4.5</td><td>Améliorations de l'Efficacité</td><td>69</td></tr><tr><td>4.5.1</td><td>Vérification Incrémentale des Contraintes</td><td>69</td></tr><tr><td>4.5.2</td><td>Utilisation des Contraintes Flexible-Rigide</td><td>69</td></tr><tr><td>4.5.3</td><td>Utilisation des Contraintes Flexible-Flexible</td><td>69</td></tr><tr><td>4.5.4</td><td>Economie de la Scission</td><td>70</td></tr><tr><td>4.5.5</td><td>Sous-Problèmes Décidables de l'Unification</td><td>70</td></tr><tr><td>4.5.6</td><td>Priorité à la Variable la Plus à Droite</td><td>70</td></tr><tr><td>4.5.7</td><td>Normalisation de Certains Termes Mal Typés</td><td>70</td></tr><tr><td>4.6</td><td>Extension au Calcul des Constructions avec Univers</td><td>70</td></tr><tr><td>4.7</td><td>Application à la Synthèse et à l'Evaluation de Programmes</td><td>71</td></tr><tr><td>4.7.1</td><td>Synthèse de Programmes</td><td>71</td></tr><tr><td>4.7.2</td><td>Programmation Logique</td><td>71</td></tr><tr><td>4.7.3</td><td>Interprétation et Compilation</td><td>71</td></tr></table>

<table><tr><td>5</td><td>Une Restriction Incomplète</td><td>73</td></tr><tr><td>5.1</td><td>Une Restriction</td><td>73</td></tr><tr><td>5.2</td><td>Généralisation de l'Hypothèse de Récurrence</td><td>74</td></tr><tr><td>5.3</td><td>Complétude Transitive</td><td>74</td></tr><tr><td>5.4</td><td>Accès aux Axiomes</td><td>78</td></tr><tr><td>5.5</td><td>Synthèse Interactive de Preuves</td><td>79</td></tr><tr><td>5.5.1</td><td>Tactiques</td><td>79</td></tr><tr><td>5.5.2</td><td>Un Exemple Simple</td><td>80</td></tr><tr><td>5.5.3</td><td>Un Autre Exemple : Un Lemme du Théorème de Tarski</td><td>81</td></tr><tr><td>5.6</td><td>Prolégomènes à un Vernaculaire Mathématique</td><td>83</td></tr></table>

<table><tr><td>6</td><td>Unification</td><td>87</td></tr><tr><td>6.1</td><td>Unification Ouverte et Fermée</td><td>87</td></tr><tr><td>6.2</td><td>Une Méthode d'Unification Fermée</td><td>87</td></tr><tr><td>6.3</td><td>Vers une Méthode d'Unification Ouverte</td><td>88</td></tr></table>

<table><tr><td>7</td><td>Equations Décidables</td><td>91</td></tr><tr><td>7.1</td><td>Ordre d'un Type</td><td>91</td></tr><tr><td>7.2</td><td>Unification du Premier Ordre et Entre Termes à Arguments Restreints</td><td>92</td></tr><tr><td>7.3</td><td>Filtrage du Deuxième Ordre dans le λ-calcul Simplement Typé</td><td>93</td></tr><tr><td>7.3.1</td><td>Avec Variables Universelles du Troisième Ordre au Plus</td><td>93</td></tr></table>
<table><tr><td>7.3.2</td><td>Avec Variables Universelles Arbitraires</td><td>94</td></tr><tr><td>7.4</td><td>Filtrage du Deuxième Ordre dans les Systèmes de Types</td><td>95</td></tr><tr><td>7.4.1</td><td>Termes à Arguments Restreints du Deuxième Ordre</td><td>95</td></tr><tr><td>7.4.2</td><td>Equations de Garantie</td><td>96</td></tr><tr><td>7.4.3</td><td>Type des Nouvelles Variables</td><td>100</td></tr><tr><td>7.4.4</td><td>Un Algorithme de Filtrage</td><td>102</td></tr><tr><td>7.4.5</td><td>Propriétés</td><td>104</td></tr><tr><td><b>8</b></td><td><b>Equations Indécidables</b></td><td><b>109</b></td></tr><tr><td>8.1</td><td>Unification du Deuxième Ordre</td><td>109</td></tr><tr><td>8.2</td><td>Filtrage du Troisième Ordre dans les Systèmes avec Types Dépendants et Construc-teurs de Types</td><td>110</td></tr><tr><td>8.3</td><td>Filtrage dans les Systèmes Polymorphes et Systèmes avec Types Inductifs</td><td>112</td></tr></table>
Pour projeter un livre, la première chose est de savoir exclure.

Italo Calvino

La démonstration automatique a pour projet la conception de méthodes qui, partant d'une pro-
position, en construisent automatiquement une preuve, c'est-à-dire une argumentation en justifiant
la vérité.

Un sens est donné à ce projet par le caractère grammatical (ou formel) de la notion de preuve. En effet si on considère que la suite de symboles "Tous les hommes sont mortels, Socrate est un homme donc Socrate est mortel" est une preuve de la proposition "Socrate est mortel", ce n'est pas en raison de la signification des mots "Socrate", "homme", "mortel" mais uniquement en raison de la façon dont ces mots sont assemblés dans cette phrase. Cette remarque permet de distinguer deux étapes dans le projet de construction automatique de preuves. La première est la formalisation des règles qui distinguent les preuves au sein des suites de symboles, la seconde est leur automatisation. La première de ces tâches est l'objet de la *théorie de la démonstration*, théorie qui dépasse largement le cadre de la démonstration automatique et qui lui est bien antérieure, la seconde est l'objet de la *démonstration automatique* proprement dite.

Dans son projet de formalisation du raisonnement, la théorie de la démonstration n'aboutit pas à
un système formel unique, mais plusieurs peuvent prétendre être une formalisation du raisonnement
naturel. Tous ces systèmes ont plus ou moins en commun une organisation qui distingue un langage
de description des objets du discours, un langage d'expression des propositions concernant ces objets
et des règles de déductions qui permettent de démontrer certaines de ces propositions. Les choix qui
orientent vers un système ou un autre concernent deux points.

Le premier est le choix des connecteurs logiques et des règles de déduction régissant ces connec-
teurs. Aux connecteurs habituels (implication, quantification universelle et existentielle, conjonction,
disjonction, négation) peuvent s'ajouter des modalités comme la nécessité ou la possibilité. De plus
une certaine liberté est laissée dans le choix des règles régissant certains de ces connecteurs, notam-
ment des règles régissant la négation et des règles structurelles. On parle alors de logique *classique*,
*intuitionniste*, *minimale*, *linéaire*, *relevante*, *modale*, *temporelle*, etc.

L'autre point est le langage des objets du discours. Par exemple en arithmétique, on peut choisir
de traiter uniquement des entiers ou alors de traiter aussi des collections d'entiers, des fonctions des
entiers dans les entiers, etc. On parle alors de logique du *premier ordre*, du *deuxième ordre*, d'ordre *supérieur*, de systèmes de types, etc. Trois grandes étapes peuvent être distinguées dans l'histoire de ces langages :

*   En logique du premier ordre, les objets sont représentés par des arbres. Il n'est pas possible de parler de collections ou de fonctions sans passer par un codage, tel que celui proposé par la théorie des ensembles.

*   En logique d'ordre supérieur, les objets sont représentés par des $\lambda$-termes simplement typés, on peut alors parler de collections et de fonctions, mais dans un formalisme très pauvre.

*   Dans les systèmes de types, on enrichit le $\lambda$-calcul simplement typé par des types dépendants, des types polymorphes, des constructeurs de types et des types inductifs. On a alors deux propriétés essentielles : le principe de compréhension (toute fonction dont la totalité peut être prouvée peut être représentée par un terme) et la représentabilité des preuves (toute preuve peut être représentée par un terme au sens de la sémantique de Heyting et de l'isomorphisme de Curry-Howard).

Les choix relatifs aux connecteurs et aux règles de déduction sont peu explorés en démonstration automatique, on se limite en général aux logiques classique et intuitionniste. Les choix relatifs au langage des termes sont en revanche source de nombreux travaux. Une méthode de construction automatique de preuves pour la logique du premier ordre a été décrite en 1965 par Robinson sous le nom de *résolution*. Cette méthode a été généralisée par Huet en 1972 à la logique d'ordre supérieur. Nous la généralisons ici aux systèmes de types. Nous ne considérons que les systèmes de types avec types dépendants, types polymorphes et constructeurs de types, c'est-à-dire les huit systèmes du cube de Barendregt, en particulier le Calcul des Constructions. Nous n'abordons pas le problème des types inductifs mais les idées développées ici peuvent vraisemblablement se généraliser à ces systèmes.

En un certain sens, les systèmes de types étant une généralisation de la logique d'ordre supérieur, le problème de la démonstration automatique y est plus compliqué et les méthodes développées plus inefficaces. Néanmoins le fait que ces systèmes vérifient le principe de compréhension, c'est-à-dire leur richesse calculatoire, permet de rendre triviales certaines preuves d'égalités, comme (fact 6) = 720, puisque démontrer cette proposition dans un système de types revient simplement à normaliser ces deux termes et remarquer que leurs formes normales sont identiques, alors que cela demande l'utilisation répétée d'axiomes concernant la factorielle dans les systèmes précédents. Par ailleurs, nous soutenons que l'identification qui est faite dans ces systèmes entre preuves et objets et qui simplifie leur expression, simplifie également les algorithmes de construction de preuves. En particulier la distinction habituelle entre résolution et unification n'y est plus pertinente.

Après une rapide présentation des systèmes de types au chapitre 1, le chapitre 2 présente un résultat de bonne fondation utilisé à plusieurs reprises par la suite. Ce chapitre peut être omis lors d'une première lecture.

La méthode de démonstration automatique est ensuite présentée dans les chapitres 3 et 4. Cette méthode n'utilise pas un algorithme d'unification, mais celui-ci est en quelque sorte uniformément réparti dans l'algorithme de résolution. Une restriction de cette méthode est présentée au chapitre 5 ainsi que des applications à la synthèse partielle de preuves et à l'analyse de preuves partielles.

Les chapitres suivants sont consacrés à la résolution d'équations. Nous montrons au chapitre 6 qui si nous n'avons pas besoin d'un algorithme d'unification pour notre méthode de synthèse de preuves, celle-ci peut en revanche être utilisée comme algorithme d'unification, tout au moins comme méthode de recherche d'unificateurs fermés. Quelques pistes vers un algorithme de recherche d'unificateurs ouverts sont étudiées bien que l'intérêt de ce problème soit discutable. Deux cas particuliers
de l'unification sont connus comme décidables dans le λ-calcul simplement typé : l'unification du premier ordre (récemment généralisée par Miller à l'unification de termes à arguments restreints) et le filtrage du deuxième ordre. Le premier a été généralisé aux systèmes de types par Pfenning, nous généralisons le deuxième au chapitre 7. Enfin au chapitre 8 nous étudions quelques cas particuliers indécidables de l'unification : l'unification du deuxième ordre est indécidable comme dans le λ-calcul simplement typé, nous montrons également que, contrairement à ce qui se passe dans le λ-calcul simplement typé (du moins dans l'état actuel de nos connaissances), le filtrage est indécidable dès qu'on a soit des types dépendants, soit des constructeurs de types, soit des types polymorphes, soit des types inductifs.
# Préliminaires
# Chapitre 1

## Trois Formalismes Logiques

Nous présentons successivement trois systèmes logiques qui formalisent le raisonnement naturel. Dans le premier d'entre eux, la *logique du premier ordre*, tous les objets du discours appartiennent à une même collection, par exemple, en arithmétique, les nombres entiers. Le deuxième, la *logique d'ordre supérieur*, est une extension de ce système qui permet de traiter également des fonctions de cette collection dans elle-même et des parties de cette collection, mais dans un formalisme assez pauvre. Enfin, les *systèmes de types* généralisent la logique d'ordre supérieur en enrichissant le formalisme de description des fonctions et des collections.

### 1.1 Logique du Premier Ordre

#### 1.1.1 Termes

On se donne un ensemble de variables et un ensemble de symboles de fonctions. A chaque symbole de fonction on associe un entier : son arité. En arithmétique par exemple on se donne les symboles de fonction 0, $S$, + et $*$ (lire *zéro*, *successeur*, *plus* et *fois*).

**Définition 1. : Terme**

L'ensemble des termes est défini inductivement par les règles suivantes :

* les variables sont des termes,

* si $t_1, ..., t_n$ sont des termes et $F$ un symbole de fonction d'arité $n$, alors ($F t_1 ... t_n$) est un terme.

Par exemple 0, ($S$ 0), ($S$ ($S$ 0)), (+ (* $x$ $x$) ($S$ ($S$ ($S$ 0)))) sont des termes.

#### 1.1.2 Propositions

On se donne un ensemble de symboles de prédicats. A chaque symbole de prédicat on associe un entier : son arité. Par exemple, en arithmétique, on se donne les prédicats $=$ et $\le$ (lire *égal* et *inférieur ou égal*).

**Définition 2. : Proposition**

L'ensemble des propositions est défini inductivement par :

* si $t_1, ..., t_n$ sont des termes et $P$ un symbole de prédicat d'arité $n$, alors ($P t_1 ... t_n$) est une proposition,
* si P et Q sont des propositions, alors $P \to Q$ est une proposition (lire P implique Q),

* si P et Q sont des propositions, alors $P \wedge Q$ est une proposition (lire P et Q),

* si P et Q sont des propositions, alors $P \vee Q$ est une proposition (lire P ou Q),

* si P est une proposition, alors $\neg P$ est une proposition (lire non P),

* $\perp$ est une proposition (lire absurde),

* si P est une proposition, alors $\forall x.P$ est une proposition (lire pour tout x, P),

* si P est une proposition, alors $\exists x.P$ est une proposition (lire il existe x tel que P).

Par exemple $\exists x.(= (* x x)(S (S (S 0))))$ et $\exists x.(= (+ (* x x) (S 0)) 0)$ sont deux propositions exprimant respectivement l'existence d'un entier dont le carré est égal à quatre et l'existence d'un entier dont le carré plus un est nul.

### 1.1.3 Déduction Naturelle

La déduction naturelle [23] est une description des règles qui permettent de déduire une proposition (théorème) à partir d'autres propositions (axiomes ou hypothèses). Soit $\Gamma$ un ensemble de propositions et P une proposition, on note $\Gamma \vdash P$ le jugement $P$ est démontrable sous les hypothèses $\Gamma$. On définit inductivement ce jugement par un ensemble de règles. Par exemple la règle :

$$ \frac{\Gamma \vdash P \rightarrow Q \quad \Gamma \vdash P}{\Gamma \vdash Q} $$

indique que si on a déjà prouvé les propositions $P \rightarrow Q$ et P sous les hypothèses $\Gamma$, alors on peut en déduire la proposition Q sous ces mêmes hypothèses.

**Définition 3. : Variable Libre, Substitution**

Soit $x$ une variable et $t$ un terme, la variable $x$ est dite libre dans le terme $t$ si $t = x$ ou $t = (F t_1 \dots t_n)$ et $x$ est libre dans l'un des $t_i$.

Soit $x$ une variable et $Q$ une proposition, la variable $x$ est dite libre dans la proposition $Q$ si l'une des conditions suivantes est vérifiée :

* $Q = (P t_1 \dots t_n)$ et $x$ est libre dans un des termes $t_i$,

* $Q = P_1 \rightarrow P_2$, $Q = P_1 \wedge P_2$ ou $Q = P_1 \vee P_2$, et $x$ est libre dans $P_1$ ou dans $P_2$,

* $Q = \neg P$ et $x$ est libre dans $P$

* $Q = \exists y.P$ ou $Q = \forall y.P$, $y \neq x$ et $x$ est libre dans $P$.

Soit $P$ une proposition, $x$ une variable et $t$ un terme, la proposition $P[x \leftarrow t]$ est obtenue en substituant le terme $t$ à toutes les occurrences libres de $x$ dans $P$.

**Remarque :** On suppose que toutes les variables muettes ont un nom différent. De ce fait, les substitutions n'introduisent pas de captures de variables. De même on ne distingue pas les propositions $\forall x.(P x)$ et $\forall y.(P y)$ ($\alpha$-équivalence). Une présentation rigoureuse de tous les formalismes présentés ici utiliserait, par exemple, des indices de de Bruijn [2].

**Définition 4. : Règles de Déduction**

$$ \frac{P \in \Gamma \quad \frac{\Gamma \vdash P}{\Gamma \vdash Q}}{\Gamma \vdash P \rightarrow Q} \rightarrow -intro $$
$$ \frac{\Gamma \vdash P \to Q \quad \Gamma \vdash P}{\Gamma \vdash Q} \to -elim $$

$$ \frac{\Gamma \vdash P \quad \Gamma \vdash Q}{\Gamma \vdash P \wedge Q} \wedge -intro $$

$$ \frac{\Gamma \vdash P \wedge Q}{\Gamma \vdash P} \wedge -elim $$

$$ \frac{\Gamma \vdash P \wedge Q}{\Gamma \vdash Q} \wedge -elim $$

$$ \frac{\Gamma \vdash P}{\Gamma \vdash P \vee Q} \vee -intro $$

$$ \frac{\Gamma \vdash Q}{\Gamma \vdash P \vee Q} \vee -intro $$

$$ \frac{\Gamma \vdash P \vee Q \quad \Gamma \vdash P \to R \quad \Gamma \vdash Q \to R}{\Gamma \vdash R} \vee -elim $$

$$ \frac{\Gamma[P] \vdash \perp}{\Gamma \vdash \neg P} \neg - intro $$

$$ \frac{\Gamma \vdash P \quad \Gamma \vdash \neg P}{\Gamma \vdash \perp} \neg - elim $$

$$ \frac{\Gamma \vdash \perp}{\Gamma \vdash P} \perp - elim $$

$$ \frac{\Gamma \vdash P}{\Gamma \vdash \forall x.P} \forall - intro \quad x \text{ non libre dans une proposition de } \Gamma $$

$$ \frac{\Gamma \vdash \forall x.P}{\Gamma \vdash P[x \leftarrow t]} \forall - elim $$

$$ \frac{\Gamma \vdash P[x \leftarrow t]}{\Gamma \vdash \exists x.P} \exists - intro $$

$$ \frac{\Gamma \vdash \exists x.P \quad \Gamma \vdash \forall x.(P \to Q)}{\Gamma \vdash Q} \exists - elim \quad x \text{ non libre dans } Q $$

Cet ensemble de règles définit la logique *intuitionniste*. On définit la logique *classique* en ajoutant la règle :

$$ \overline{\Gamma \vdash P \vee \neg P} \text{ classique} $$
## 1.2 Logique d'Ordre Supérieur

### 1.2.1 λ-calcul

#### λ-notation

En logique du premier ordre, les termes sont des arbres. Les termes sans variables forment une collection (par exemple en arithmétique les entiers). Il n'est pas possible d'exprimer des propositions concernant les fonctions de cette collection dans elle-même, ni les parties de cette collection sans passer par un codage tel que la théorie des ensembles qui considère une collection unique qui contient pêle-mêle les objets de base, les fonctions de la collection de ces objets dans elle-même et les parties de cette collection.

Le λ-calcul [7] est une extension du formalisme des arbres dans lequel un terme sans variables est un objet de base (par exemple un entier), une fonction de l'ensemble des objets de base dans lui-même ou une partie de cet ensemble.

Ordinairement on décrit une fonction $f$ par la notation $f : x \mapsto t$ où $x$ est une variable (dite muette) et $t$ un terme. L'expression $x \mapsto t$ ne peut être utilisée que lors d'une telle définition, il n'est pas d'usage de l'utiliser à l'intérieur d'un terme.

En λ-calcul on note cette fonction $[x]t$ (ou dans la notation originale $\lambda x.t$). Par exemple $[x](+(*x x) (S(S0)))$ est la fonction qui associe à tout entier $x$ l'entier $(+(*x x)(S(S0)))$. Contrairement à l'expression $x \mapsto (+(*x x)(S(S0)))$, le terme $[x](+(*x x)(S(S0)))$ peut à son tour être utilisé à l'intérieur d'un autre terme. Par exemple, on peut appliquer ce terme au terme $(+y y)$ de façon à former $([x](+(*x x)(S(S0)))(+y y))$, dans lequel on peut ensuite abstraire la variable $y$, ce qui donne le terme $[y]([x](+(*x x)(S(S0)))(+y y))$ et ainsi de suite.

**Définition 5.** : Terme du λ-calcul

$$T ::= x \mid (T T) \mid [x]T$$

Les termes de la forme $(t t')$ s'appellent des applications et les termes de la forme $[x]t$ des abstractions.

**Remarque** : En λ-calcul, les symboles de fonctions ne forment plus une catégorie syntaxique à part, mais sont des variables ordinaires.

#### Réduction et Equivalence

Quand on applique le terme $[x](+(*x x)(S(S0)))$ à l'entier $(S0)$, on veut en fait substituer à l'argument formel $x$, l'argument effectif $(S0)$ pour obtenir le terme $(+(*S0)(S0))(S(S0))$. On dit que le terme $([x](+(*x x)(S(S0)))(S0))$ se β-réduit sur le terme $(+(*S0)(S0))(S(S0)))$. Le terme $(+(*S0)(S0))(S(S0)))$ ne peut plus se réduire, il est dit en forme β-normale. On dit également que les termes $([x](+(*x x)(S(S0)))(S0))$ et le terme $(+(*S0)(S0))(S(S0)))$ sont β-équivalents.

**Définition 6.** : Réduction et Equivalence

La relation de β-réduction (en une étape) $\triangleright$ est la plus petite relation telle que :

- $([x]t u) \triangleright t[x \leftarrow u]$,

- $\mathit{si} t_1 \triangleright t_2$, alors $(t_1 u) \triangleright (t_2 u)$,

- $\mathit{si} t_1 \triangleright t_2$, alors $(u t_1) \triangleright (u t_2)$,
— si $t_1 \triangleright t_2$, alors $[x]t_1 \triangleright [x]t_2$.

La relation de $\beta$-réduction $\triangleright^*$ est la plus petite relation réflexive et transitive qui contient la relation $\triangleright$. La relation de $\beta$-équivalence $\equiv$ est la plus petite relation d'équivalence qui contient la relation $\triangleright$. Un terme $t$ est dit normal s'il n'existe pas de terme $t'$ tel que $t \triangleright t'$.

Une autre forme similaire de réduction est la $\eta$-réduction. Si $f$ est un terme tel que $x$ ne soit pas libre dans $f$, on veut que le terme $[x](f \ f)$ se réduise sur le terme $f$. On ajoute pour cela la règle de réduction :

— $[x](f \ x) \triangleright f$ si $x$ non libre dans $f$.

## Types Simples

Les règles de formation des termes énoncées ci-dessus permettent de former le terme $\delta = [x](x \ x)$. Il est difficile de comprendre ce terme, qui est une fonction qui prend en argument une fonction et l'applique à elle-même. De plus si on applique ce terme à lui-même ($\delta \ \delta$) = $([x](x \ x) [x](x \ x))$ on obtient un terme qui se réduit sur lui-même et n'a donc pas de forme normale. Il est encore plus difficile de donner un sens à ce terme qui désigne en quelque sorte un objet en en donnant une méthode de calcul, laquelle méthode ne termine pas.

Si ces objets pathologiques peuvent être construits, c'est parce que nos règles de formation des termes sont trop laxistes. En effet la règle d'application permet d'appliquer n'importe quel terme $t$ à n'importe quel terme $t'$, sans s'assurer que $t$ est bien une fonction et $t'$ un objet du domaine de cette fonction. C'est ce que l'on fait en associant à chaque objet un type [6]. Les types sont formés grâce à deux règles :

— *Nat*, *Bool*, etc. sont des types,

— si $T$ et $T'$ sont deux types, $T \to T'$ est un type (lire *le type des fonctions de T dans T*')

On associe à chaque variable un type qu'on indique, pour les variables libres, dans un contexte de déclarations et pour les variables muettes là où elles sont liées.

**Définition 7.** : Terme du $\lambda$-calcul simplement typé

$$T ::= x \mid (T \ T) \mid [x : U]T$$

où $U$ est un type.

Par exemple le terme $[x : Nat](+ (* x x) (S (S 0)))$ est de type $Nat \to Nat$ dans le contexte $[0 : Nat; S : Nat \to Nat; + : Nat \to Nat \to Nat; * : Nat \to Nat \to Nat]$.

Ces types généralisent la notion d'arité. Remarquons que, à la différence des termes du premier ordre, dans un terme du $\lambda$-calcul, il n'est pas nécessaire d'appliquer un symbole de fonction à tous ses arguments pour obtenir un terme bien formé, par exemple les termes $+$, $(+ 0)$ et $(+ 0 0)$ sont bien formés et leurs types respectifs sont $Nat \to Nat \to Nat, Nat \to Nat$ et $Nat$.

Plus précisément pour éviter de fixer une fois pour toutes les types de base $Nat, Bool$, etc. On décide que tous les types sont eux mêmes des termes et que leur type est un unique type de base $Set$.

**Définition 8.** : Terme du $\lambda$-calcul simplement typé

$$T ::= Set \mid T \to T \mid x \mid (T \ T) \mid [x : T]T$$
Le contexte ci-dessus doit maintenant s'écrire :

$[Nat : Set; 0 : Nat; S : Nat \to Nat; + : Nat \to Nat \to Nat; * : Nat \to Nat \to Nat]$

Remarquons que si Set est le type de tous les types, il n'est pas lui-même de type Set.

**Définition 9.** : $\lambda$-calcul Simplement Typé

Soit $\Gamma$ un contexte, on note $\Gamma \vdash t : T$ le jugement $t$ a le type $T$ dans le contexte $\Gamma$ et $\Gamma$ bien formé le jugement de bonne formation de $\Gamma$.

Le contexte vide est bien formé :

$[ ]$ bien formé

Déclaration d'une variable de type :

$\Gamma$ bien formé
$\Gamma[A : Set]$ bien formé

Les variables de type sont des types :

$A : Set \in \Gamma$
$\Gamma \vdash A : Set$

Formation des types fonctionnels :

$\Gamma \vdash A : Set \quad \Gamma \vdash B : Set$
$\Gamma \vdash A \to B : Set$

Déclaration d'une variable :

$\Gamma \vdash A : Set$
$\Gamma[x : A]$ bien formé

Les variables sont des termes :

$x : A \in \Gamma$
$\Gamma \vdash x : A$

Application :

$\Gamma \vdash t : A \to B \quad \Gamma \vdash t' : A$
$\Gamma \vdash (t t') : B$

Abstraction :

$\Gamma \vdash A : Set \quad \Gamma[x : A] \vdash B : Set \quad \Gamma[x : A] \vdash t : B$
$\Gamma \vdash [x : A]t : A \to B$

**Remarque** : Comme précédemment, on suppose que les variables muettes ont des noms différents. De ce fait, dans les règles de déclaration de variables, on suppose que le nom de la variable déclarée est un nouveau nom, qui n'est pas déjà pris par une autre variable du contexte.

**Définition 10.** : Terme Bien Typé

Un terme $t$ est bit bien typé dans un contexte $\Gamma$ s'il existe un type $T$ tel que $\Gamma \vdash t : T$.

**Proposition 1.** : La $\beta\eta$-réduction est fortement normalisable et conflueente, sur les termes typés. C'est-à-dire que si $t$ est un terme bien typé dans un contexte $\Gamma$, alors toute réduction issue de ce terme termine sur une forme normale et deux réductions issues d'un même terme terminent sur la même forme normale.

**Démonstration** : Voir [63] [61].
### 1.2.2 Logique d'Ordre Supérieur

La logique d'ordre supérieur [6] est une extension de la logique du premier ordre dans laquelle les termes ne sont plus des arbres mais des λ-terms simplement typés.

En logique d'ordre supérieur, un prédicat tel que $\le$ ne peut plus comme au premier ordre s'appliquer à n'importe quel terme mais uniquement à des termes de type Nat. On exprime cela en lui associant un type. On pose un nouveau type de base Prop, le type des propositions et on ajoute la règle de typage :

$$ \frac{\Gamma \text{ bien formé}}{\Gamma \vdash \mathit{Prop} : \mathit{Set}} $$

Le prédicat $\le$ est désormais simplement une variable de type $Nat \to Nat \to Prop$.

On ajoute les règles suivantes pour les connecteurs :

$$ \frac{\Gamma \text{ bien formé}}{\Gamma \vdash : \mathit{Prop} \to \mathit{Prop} \to \mathit{Prop}} $$

$$ \frac{\Gamma \text{ bien formé}}{\Gamma \vdash \wedge : \mathit{Prop} \to \mathit{Prop} \to \mathit{Prop}} $$

$$ \frac{\Gamma \text{ bien formé}}{\Gamma \vdash \vee : \mathit{Prop} \to \mathit{Prop} \to \mathit{Prop}} $$

$$ \frac{\Gamma \text{ bien formé}}{\Gamma \vdash \neg : \mathit{Prop} \to \mathit{Prop}} $$

$$ \frac{\Gamma \text{ bien formé}}{\Gamma \vdash \bot : \mathit{Prop}} $$

Quand on écrit la proposition $\forall x.(\le 0 x)$ on veut pouvoir substituer à $x$ non pas, comme au premier ordre, n'importe quel terme, mais uniquement un terme de type Nat. On écrit donc $\forall_{Nat}([x : Nat] (\le 0 x))$ (ou de façon équivalente $\forall x : Nat.(\le 0 x)$). On se donne donc un quantificateur universel par type et les règles :

$$ \frac{\Gamma \vdash T : \mathit{Set}}{\Gamma \vdash \forall_T : (T \to \mathit{Prop}) \to \mathit{Prop}} $$

$$ \frac{\Gamma \vdash T : \mathit{Set}}{\Gamma \vdash \exists_T : (T \to \mathit{Prop}) \to \mathit{Prop}} $$

Remarquons que le fait de pouvoir quantifier sur une variable de n'importe quel type autorise la quantification sur les variables fonctionnelles et aussi sur les variables de prédicat.

On considère une notion de contexte étendu où sont déclarés les variables et les axiomes. La règle de déclaration d'un axiome est la suivante :

$$ \frac{\Gamma \vdash P : \mathit{Prop}}{\Gamma[P] \text{ bien formé}} $$

#### Définition 11. : Logique d'Ordre Supérieur

Le jugement $\Gamma$ bien formé et $\Gamma \vdash t : T$ sont définis comme en λ-calcul simplement typé sauf qu'on ajoute les règles ci-dessus pour les propositions. Le jugement $\Gamma \vdash P$ ($P$ est démontrable dans
le contexte $\Gamma$) est défini par les mêmes règles qu'au premier ordre avec une légère modification pour les règles des quantificateurs :

$$ \frac{\Gamma[x:T] \vdash P}{\Gamma \vdash \forall x : T.P} \quad \forall - \text{intro} $$

$$ \frac{\Gamma \vdash \forall x : T.P \quad \Gamma \vdash t : T}{\Gamma \vdash P[x \leftarrow t]} \quad \forall - \text{elim} $$

$$ \frac{\Gamma \vdash P[x \leftarrow t] \quad \Gamma \vdash t : T}{\Gamma \vdash \exists x : T.P} \quad \exists - \text{intro} $$

$$ \frac{\Gamma \vdash \exists x : T.P \quad \Gamma \vdash \forall x : T.(P \to Q) \quad \Gamma \vdash Q : \mathit{Prop}}{\Gamma \vdash Q} \quad \exists - \mathit{elim} $$

**Remarque** : On prendra soin de ne pas confondre $\Gamma \vdash P : \mathit{Prop}$ qui est le jugement que $P$ est une proposition bien formée indépendamment de tout critère de vérité et $\Gamma \vdash P$ qui est le jugement que $P$ est démontrable sous les axiomes de $\Gamma$.

**Remarque** : En logique d'ordre supérieur, comme au premier ordre, on considère que tous les types sont habités même si on ne peut pas en exhiber un habitant. Cela peut s'exprimer en ajoutant la règle de déduction :

$$ \frac{\Gamma \vdash P \quad \vdash T : \mathit{Set}}{\Gamma \vdash \exists x : T.P} $$

où $x$ n'est pas une variable libre de $P$.

**Remarque** : En logique d'ordre supérieur, les symboles de prédicat ne forment plus une catégorie syntaxique à part, mais sont des variables ordinaires. De même les propositions sont simplement les termes de type $\mathit{Prop}$.

## Prédicativité - Imprédicativité

En logique du premier ordre, on ne peut pas exprimer le principe de récurrence sur les entiers par un axiome unique, mais on a besoin de poser un nombre infini d'axiomes :

$$ (P 0) \rightarrow \forall x.((P x) \rightarrow (P (S x))) \rightarrow \forall x.(P x) $$

où $P$ décrit l'ensemble des prédicats sur les entiers. A l'ordre supérieur, la possibilité de quantifier sur les prédicats permet de poser un axiome unique :

$$ \forall P : \mathit{Nat} \rightarrow \mathit{Prop}.((P 0) \rightarrow \forall x : \mathit{Nat}.((P x) \rightarrow (P (S x))) \rightarrow \forall x : \mathit{Nat}.(P x)) $$

Une question essentielle se pose alors : cet axiome est-il lui-même une proposition, ou est-il une méta-proposition. Si on décide que cet axiome $R$ est lui-même une proposition, alors le terme $[x : \mathit{Nat}]R$ a pour type $\mathit{Nat} \rightarrow \mathit{Prop}$ et est donc susceptible d'être substitué à $P$ dans $R$. On voit ici que décréter $R$ de type $\mathit{Prop}$ permet de donner à cette phrase un sens autoréférent.

Un système qui permet l'application d'un schéma d'axiome à lui-même est dit *imprédicatif*, un système qui l'interdit est dit *prédicatif*. La logique d'ordre supérieur telle que nous l'avons présentée est imprédicative. L'imprédicativité est due au fait que les quantificateurs $\forall_T$ et $\exists_T$ ont le type $(T \rightarrow \mathit{Prop}) \rightarrow \mathit{Prop}$ y compris quand le symbole $\mathit{Prop}$ a une occurrence dans $T$.
Un moyen d'exprimer le principe de récurrence tout en restant prédicatif est de décréter une stra-
tification entre propositions du premier niveau auxquelles on est susceptible d'appliquer le principe
de récurrence et méta-propositions dont fait partie l'axiome de récurrence.

Quand le symbole *Prop* a une occurrence dans le type *T*, alors les symboles $\forall_T$ et $\exists_T$ ont
le type (*T* → *Prop*) → *MétaProp*. On a également besoin de quantificateurs $\forall'_T$ et $\exists'_T$ de type
(*T* → *MétaProp*) → *MétaProp* pour quantifier dans les méta-propositions.

Le terme $\forall P : Nat \to Prop.((P \ 0) \to \forall x : Nat.((P \ x) \to (P \ (S \ x))) \to \forall x : Nat.(P \ x))$ est
alors de type *MétaProp*. Remarquons que dans ce système on peut quantifier sur une variable de
n'importe quel type, à condition que ce type ne contienne pas d'occurrence du symbole *MétaProp*.

Une autre possibilité est d'interdire complètement la quantification sur les variables de prédicats (c'est-à-dire les variables de type *T* tel que le symbole *Prop* ait une occurrence dans *T*) et d'inclure le principe de récurrence dans les règles de déduction en ajoutant la règle :

$$
\frac{(P 0) \quad \forall x : \mathbf{Nat}.((P x) \rightarrow (P (S x))))}{\forall x : \mathbf{Nat}.(P x)}
$$

Depuis le paradoxe de Russell (et en fait depuis le paradoxe d'Epinemides) les logiciens ont appris
à se méfier des phrases autoréférentes comme source d'incohérences dans leurs systèmes. Pour cette
raison, certains logiciens contemporains refusent les systèmes imprédicatifs. D'autres considèrent
que l'imprédicativité n'est pas source de paradoxes. Un résultat qui vient étayer leur thèse est le
théorème de cohérence de la logique d'ordre supérieur (imprédicative).

Néanmoins, la preuve de ce théorème est ordinairement formulée dans la théorie des ensembles
(qui est imprédicative) et elle ne peut pas se formuler dans un système prédicatif. Selon les tenants
de la prédicativité ce résultat ne démontre rien car la théorie des ensembles étant elle-même impré-
dicative, ils n'ont aucune raison de la supposer cohérente. Ces problèmes de fondement n'étant pas
directement en rapport avec notre étude, nous nous garderons d'émettre une opinion.

1.2.3 Limites de la Logique d'Ordre Supérieur

Nous allons voir dans ce paragraphe deux limitations de la logique d'ordre supérieur. Ces limit-
tations sont dues à la faible expressivité du langage des termes de cette logique. Par la suite, nous
considérerons des extensions du λ-calcul simplement typé et des extensions de la logique d'ordre
supérieur qui auront ces calculs comme langage des termes.

Fonctions Représentables en λ-calcul Simplement Typé

Soit le terme `plus_deux` = [x : Nat](S (S x)). Le terme (`plus_deux` (S 0)) se réduit sur le terme
(S (S (S 0))). On peut de même chercher dans le contexte [Nat : Set; 0 : Nat; S : Nat → Nat] un
terme `plus`: Nat → Nat → Nat tel que si a et b sont des entiers, le terme (`plus a b`) se réduise sur
la somme de a et b. Nous montrerons par la suite qu'un tel terme n'existe pas.

En revanche, on peut ajouter au contexte des variables + et = et considérer les axiomes :

$$
\forall y : Nat.(+ 0 y) = y \text{ et } \forall x : Nat.\forall y : Nat.(+ (S x) y) = (S (+ x y))
$$

En utilisant ces axiomes, on peut montrer la proposition :

$$
(+ (S (S 0)) (S (S 0))) = (S (S (S (S 0))))
$$

mais le terme $(+ (S (S 0)) (S (S 0)))$ ne se réduit pas pour autant sur $(S (S (S (S 0))))$.
**Définition 12.** : Fonction des Entiers dans les Entiers

On appelle fonction des entiers dans les entiers un terme $f$ de type $Nat \to ... \to Nat \to Nat$. Le terme $b$ est appelé l'image des termes $a_1, ..., a_n$ si on peut démontrer la proposition $b = (f a_1 ... a_n)$.

**Définition 13.** : Entier

Un entier est un terme de type $Nat$ qui a la forme $(S...(S 0)...)$.

**Définition 14.** : Fonction Représentable par un Terme

Une fonction $f$ est dite représentée par un terme $t$ si pour tout $n$-uplets d'entiers $< a_1, ..., a_n >$, le terme $(t a_1 ... a_n)$ se réduit sur un entier $b$ tel qu'on puisse démontrer la proposition $b = (f a_1 ... a_n)$.

**Proposition 2.** : En logique d'ordre supérieur, les seules fonctions représentables par un terme sont les fonctions constantes et les fonctions qui ajoutent une constante à l'un de leurs arguments.

Un corollaire de cette proposition est que la somme et le produit ne sont pas représentables par des termes en logique d'ordre supérieur.

On peut opposer deux façons de démontrer une égalité : *raisonner* en utilisant des axiomes et *calculer* en réduisant deux termes et en constatant que leurs formes normales sont égales. Quand un objet est déclaré dans le contexte et ses propriétés *axiomatisées* on ne peut que raisonner pour prouver des théorèmes concernant cet objet, quand il est défini comme un terme, certains théorèmes le concernant peuvent être calculés. Un système logique est d'autant mieux adapté à la démonstration automatique qu'un maximum de fonctions sont représentables et qu'il permet de ce fait de faire un maximum de définitions et un minimum de déclarations.

La faible expressivité du $\lambda$-calcul simplement typé du point de vue de la représentabilité des fonctions est donc une limitation de la logique d'ordre supérieur.

**Représentation des Preuves par des Termes**

Considérons les propositions construites uniquement avec des variables propositionnelles et l'implication : $\to$. Pour écrire les preuves nous disposons de deux règles : le lien axiome, l'élimination et l'introduction de l'implication.

La sémantique de Heyting (due à Heyting et Kolmogorov) propose d'associer à chaque variable un ensemble : l'ensemble de ses preuves (cet ensemble est vide quand la proposition ne peut être démontrée) et de définir récursivement l'ensemble des preuves de $P \to Q$ comme l'ensemble des fonctions des preuves de $P$ dans les preuves de $Q$ (ici aussi cet ensemble peut être vide). En effet, une preuve de $P \to Q$ est un objet qui permet de construire une preuve de $Q$ dès que l'on a une preuve de $P$, c'est donc essentiellement une fonction des preuves de $P$ dans les preuves de $Q$.

Comme nous représentons les fonctions par des $\lambda$-termes simplement typés nous associons à chaque variable propositionnelle $A$ un type de base (le type de ses preuves) également noté $A$. Le type des preuves de $P \to Q$ est le type des fonctions de $P$ dans $Q$, c'est-à-dire le type $P \to Q$. On peut donc identifier types et propositions en identifiant la flèche des types et l'implication.

Quand on déclare un axiome $P$, on suppose qu'il y a un élément dans le type des preuves de $P$. Quand on veut prouver un théorème $Q$ on cherche si on peut exhiber, en utilisant les éléments donnés avec les axiomes, un élément du type des preuves de cette proposition.

Par exemple si on se donne les deux axiomes $A$ et $A \to B$ et que l'on veut prouver $B$, on se donne $a$ dans le type des preuves de $A$, c'est-à-dire un élément de type $A$ et $f$ dans le type des preuves de $A \to B$, c'est-à-dire une fonction du type des preuves de $A$ dans le type des preuves de $B$.
B, c'est-à-dire un élément de type $A \to B$. Le terme $(f a)$ est une preuve de $B$, c'est un élément du type des preuves de $B$, c'est un élément de type $B$.

Dans un autre exemple, on ne se donne aucun axiome, la fonction identité $[x : A]x$ qui associe une preuve de $A$ à toute preuve de $A$ est une preuve de $A \to A$.

**Proposition 3.** : Soit $\Gamma$ un contexte contenant des déclarations de variables de type $Prop$ et des axiomes qui sont des propositions formées uniquement avec ces variables propositionnelles et l'impli- cation. Soit $\Gamma'$ le contexte obtenu en remplaçant dans $\Gamma$ toutes les déclarations $A : Prop$ par $A : Set$ et les axiomes $P$ par la déclaration d'une variable $x : P$, alors si $Q$ est une proposition démontrable dans $\Gamma$, c'est un type habité dans $\Gamma'$.

**Démonstration** : Par récurrence sur la longueur de la preuve de $Q$.

**Remarque** : Réciproquement, chaque terme de type $Q$ dans $\Gamma'$ peut être traduit en une preuve de $Q$ dans $\Gamma$. Preuves et termes peuvent ainsi être identifiés. Cette correspondance est appelée *isomorphisme de Curry-Howard* [13] [36] [3].

Le $\lambda$-calcul simplement typé permet donc de représenter par des termes les preuves de la logique propositionnelle réduite à l'implication, il est malheureusement trop peu expressif pour permettre de représenter toutes les preuves de la logique d'ordre supérieur. Nous allons dans le paragraphe suivant considérer des extensions de ce calcul qui permettent de représenter toutes ces preuves. Règles de typage et de déduction feront alors double emploi. Nous pourrons abandonner les règles de déduction. Déclarer un axiome $P$ sera alors simplement déclarer une variable de type $P$ et prouver une proposition $P$ sera simplement donner un terme de type $P$.

# 1.3 Systèmes de Types

## 1.3.1 Quelques Systèmes de Types

### Types Dépendants

L'identification entre types et propositions nous amène à identifier les symboles *Set* et *Prop*. Cette identification nous oblige à abandonner la règle *Prop* : *Set*, qui devrait alors s'écrire *Prop* : *Prop* et qui nous mènerait à un système non normalisable [28]. Le type $Nat \to Nat \to Prop$ n'est donc plus un terme correct dans le $\lambda$-calcul simplement typé puisque c'est devenu le type d'une fonction des entiers dans les types. Nous allons donc considérer une extension de ce calcul : le $\lambda$-calcul avec types dépendants ($\lambda\Pi$-calcul) [3] [36] [33] qui autorise de telles fonctions.

Les types dépendants peuvent être considérés indépendamment de l'isomorphisme de Curry-Howard. Par exemple, quand on considère le type des listes d'entiers de longueur $n$, on introduit une fonction *list* des entiers dans les types, (*list* 0) est le type des listes de longueur 0, (*list* 1) le type des listes de longueur 1, etc.

Nous devons tout d'abord ajouter des règles qui permettent de considérer des termes comme $Nat \to Prop$, $Nat \to Nat \to Prop$, etc. Donner à ces termes le type $Prop$ mène à un système non normalisable [28]. Nous allons donc introduire un nouveau type de base : *Type* et poser $Prop : Type$, $Nat \to Prop : Type$, etc.

Nous introduisons donc une nouvelle règle de typage pour $Prop$ :

$$ \frac{\Gamma \text{ bien formé} \quad \Gamma \vdash Prop : Type}{\quad} $$
et une règle qui permet de former les types Nat → Prop, Nat → Nat → Prop, etc. :

$$ \frac{\Gamma \vdash A : \mathit{Prop} \quad \Gamma \vdash B : \mathit{Type}}{\Gamma \vdash A \rightarrow B : \mathit{Type}} $$

Nous nous donnons aussi une règle qui permet de déclarer une variable telle que list ou $\le$ dont le type du type est Type et non Prop.

$$ \frac{\Gamma \vdash T : \mathit{Type}}{\Gamma[x : T] \text{ bien formé}} $$

Ces règles permettent de considérer le contexte :

$$ [\mathit{Nat} : \mathit{Prop}; 0 : \mathit{Nat}; S : \mathit{Nat} \rightarrow \mathit{Nat}; \leq : \mathit{Nat} \rightarrow \mathit{Nat} \rightarrow \mathit{Prop}] $$

Il nous faut encore une règle pour construire les termes dont le type du type est Type et non Prop comme le terme $[x : Nat](\leq x (S (S (S (S 0)))) : Nat \rightarrow Prop$ qui est un prédicat caractérisant les entiers inférieurs à cinq :

$$ \frac{\Gamma \vdash A : \mathit{Prop} \quad \Gamma[x : A] \vdash B : \mathit{Type} \quad \Gamma[x : A] \vdash t : B}{\Gamma \vdash [x : A]t : A \rightarrow B} $$

Dans un calcul avec types dépendants, le type du résultat d'une fonction peut dépendre de la valeur des arguments de cette fonction. Par exemple, on peut considérer la fonction qui prend en argument un entier $n$ et retourne la liste de longueur $n$ contenant $n$ fois l'entier 0. On doit donc généraliser la notation $f : A \rightarrow B$ en une notation $f : (x : A)B$ qui signifie que la fonction $f$ appliquée à un objet $a$ de type $A$ donnera un résultat dont le type est $B$ dans lequel on a substitué $a$ à $x$. Par exemple, le type de la fonction qui prend en argument un entier $n$ et retourne la liste de longueur $n$ contenant $n$ fois l'entier 0 est $(n : Nat)(list \ n)$. De même le type de la fonction qui ajoute un entier en tête d'une liste est $(n : Nat)(l : (list \ n))(x : Nat)(list(+ \ n \ 1))$. La notation $A \rightarrow B$ devient une abréviation pour $(x : A)B$ quand $x$ n'apparaît pas dans $B$.

Les règles de formation des produits et des abstractions sont donc modifiées en :

$$ \frac{\Gamma \vdash A : \mathit{Prop} \quad \Gamma[x : A] \vdash B : \mathit{Prop}}{\Gamma \vdash (x : A)B : \mathit{Prop}} $$

$$ \frac{\Gamma \vdash A : \mathit{Prop} \quad \Gamma[x : A] \vdash B : \mathit{Type}}{\Gamma \vdash (x : A)B : \mathit{Type}} $$

$$ \frac{\Gamma \vdash A : \mathit{Prop} \quad \Gamma[x : A] \vdash B : \mathit{Prop} \quad \Gamma[x : A] \vdash t : B}{\Gamma \vdash [x : A]t : (x : A)B} $$

$$ \frac{\Gamma \vdash A : \mathit{Prop} \quad \Gamma[x : A] \vdash B : \mathit{Type} \quad \Gamma[x : A] \vdash t : B}{\Gamma \vdash [x : A]t : (x : A)B} $$

Il nous faut encore ajouter une règle pour que deux termes $\beta\eta$-équivalents aient les mêmes propriétés vis-à-vis du typage. On peut démontrer que si $\Gamma \vdash t : T$ et $t \equiv t'$, alors $\Gamma \vdash t' : T$, en revanche on a besoin de la règle :

$$ \frac{\Gamma \vdash t : T \quad \Gamma \vdash T : s \quad \Gamma \vdash T' : s \quad T \equiv T'}{\Gamma \vdash t : T'} s \in \{\mathit{Prop}, \mathit{Type}\} $$

Résumons maintenant le définition de ce calcul.
**Définition 15.** : Terme

$$T ::= \mathit{Prop} \mid \mathit{Type} \mid x \mid (T \ T) \mid [x:T]T \mid (x:T)T$$

**Définition 16.** : $\lambda\Pi$-calcul

Si $t$ et $t'$ sont deux termes et $x$ une variable, on note $t[x \leftarrow t']$ le terme obtenu en substituant $t'$ à $x$ dans $t$. On note $t \equiv t'$ le fait que $t$ et $t'$ soient $\beta\eta$-équivalents. Les termes $\mathit{Prop}$ et $\mathit{Type}$ sont appelés les sortes du calcul.

Un contexte est une liste de couples $\langle x, T \rangle$ (notées $x : T$) où $x$ est une variable et $T$ un terme.

Les règles de typage sont réparties en deux catégories : les règles générales qui sont une reformulation des règles du $\lambda$-calcul simplement typé et les règles spécifiques au $\lambda$-calcul avec types dépendants.
Règles générales :

$$ \begin{array}{l} \frac{\boxed{\phantom{a}} \text{ bien formé} \qquad \frac{\Gamma \vdash T : s}{\Gamma[x:T] \text{ bien formé}} s \in \{\mathit{Prop}, \mathit{Type}\}}{\Gamma \vdash T : s} \\[1.5em] \frac{\boxed{\phantom{a}} \text{ bien formé} \qquad \frac{\Gamma \vdash \mathit{Prop} : \mathit{Type}}{\Gamma \vdash x : T}}{\Gamma \vdash x : T} \\[1.5em] \frac{\boxed{\phantom{a}} \vdash T : \mathit{Prop} \quad \frac{\Gamma[x:T] \vdash T' : \mathit{Prop}}{\Gamma \vdash (x:T)T' : \mathit{Prop}}}{\Gamma \vdash (x:T)T' : \mathit{Prop}} \\[1.5em] \frac{\boxed{\phantom{a}} \vdash (x:T)T' : \mathit{Prop} \quad \frac{\Gamma[x:T] \vdash t : T'}{\Gamma \vdash [x:T]t : (x:T)T'}}{\Gamma \vdash [x:T]t : (x:T)T'} \\[1.5em] \frac{\boxed{\phantom{a}} \vdash t : (x:T)T' \quad \frac{\Gamma \vdash t' : T}{\Gamma \vdash (t:t') : T'[x \leftarrow t']}}{\Gamma \vdash (t:t') : T'[x \leftarrow t']}
\end{array} s \in \{\mathit{Prop}, \mathit{Type}\} $$

Règles spécifiques au $\lambda$-calcul avec types dépendants :

$$ \frac{\Gamma \vdash T : \mathit{Prop} \quad \frac{\Gamma[x:T] \vdash T' : \mathit{Type}}{\Gamma \vdash (x:T)T' : \mathit{Type}}}{\Gamma \vdash T : \mathit{Prop} \quad \frac{\Gamma[x:T] \vdash T' : \mathit{Type} \quad \Gamma[x:T] \vdash t : T'}{\Gamma \vdash [x:T]t : (x:T)T'}} $$

Dans le $\lambda\Pi$-calcul on peut représenter les preuves de la logique d'ordre supérieur restreinte à l'implication et à la quantification universelle limitée aux variables dont le type du type est $\mathit{Prop}$ et non $\mathit{Type}$.

En effet la sémantique de Heyting suggère de représenter une preuve de $\forall x : T.P$ comme une fonction qui associe à tout élément de $a$ une preuve de $P[x \leftarrow a]$, c'est-à-dire comme un objet de type $(x : T)P$. En identifiant la notation $\forall x : T.P$ et $(x : T)P$ on étend l'isomorphisme entre propositions et types. On montre que toute preuve de $P$ écrite en déduction naturelle peut se traduire en un $\lambda$-terme de type $P$ et que réciproquement tout terme de type $P$ peut s'interpréter comme une preuve de $P$.
## Polymorphisme

Dans le $\lambda\Pi$-calcul, le terme $(x : T)T'$ est bien typé si $T$ est de type $Prop$ et $T'$ de type $Prop$ ou $Type$. Pour pouvoir quantifier sur les prédicats dans les propositions et représenter les preuves de ces propositions par des $\lambda$-termes, il faut permettre la formation de types $(x : T)T'$ où $T'$ est de type $Prop$ et $T$ de type $Type$ et la formation de termes $[x : T]t$ où $t$ est de type $T'$, lui-même de type $Prop$ et $T$ de type $Type$. Un tel calcul est dit polymorphe.

**Définition 17.** : $\lambda$-calcul Polymorphe

Le $\lambda$-calcul polymorphe [28] est obtenu en ajoutant aux règles de base, les règles spécifiques au $\lambda$-calcul polymorphe :

$$ \frac{\Gamma \vdash T : Type \quad \Gamma[x : T] \vdash T' : Prop}{\Gamma \vdash (x : T)T' : Prop} $$ $$ \frac{\Gamma \vdash T : Type \quad \Gamma[x : T] \vdash T' : Prop \quad \Gamma[x : T] \vdash t : T'}{\Gamma \vdash [x : T]t : (x : T)T'} $$

Par exemple, le terme $[P : Prop][x : P]x$ est une preuve de $(P : Prop)(P \to P)$. Qui se lit : "Pour toute proposition $P$, $P$ implique $P$". Cette phrase est de type $Prop$ (imprédicativité), elle affirme donc en particulier qu'elle s'implique elle-même.

Naturellement, en considérant les règles de base, celles spécifiques au $\lambda$-calcul avec types dépendants et au $\lambda$-calcul polymorphe, on obtient le $\lambda$-calcul polymorphe avec types dépendants.

## Types Inductifs

Soit $R$ l'axiome de récurrence sur les entiers :

$$ R : \forall P : Nat \rightarrow Prop.((P 0) \rightarrow \forall x : Nat.((P x) \rightarrow (P (S x))) \rightarrow \forall x : Nat.(P x)) $$

Quand on a un prédicat $P$ et les preuves $a : (P 0)$, $b : \forall x : Nat.((P x) \rightarrow (P (S x)))$, on peut en déduire $(R P a b) : \forall x : Nat.(P x)$ puis appliquer cette proposition à un entier $n$ pour obtenir une preuve de la proposition $(P n)$. Cette proposition a aussi une autre preuve beaucoup plus concrète qui consiste à appliquer une fois l'hypothèse $a$ puis $n$ fois l'hypothèse $b$ pour prouver successivement $(P 0)$, $(P 1)$, $(P 2)$, ..., $(P n)$. Par exemple, le terme $(b 4 (b 3 (b 2 (b 1 (b 0 a))))$ est une preuve de $(P 5)$.

Le $\lambda$-calcul avec types inductifs permet d'identifier ces deux preuves de la même proposition.

**Définition 18.** : Types Inductifs

Le $\lambda$-calcul avec types inductifs [30] [50] est obtenu en ajoutant au $\lambda$-calcul polymorphe les règles de réduction :

* $(R P a b 0) \triangleright a,$

* $(R P a b (S x)) \triangleright (b x (R P a b x))$

et des règles similaires pour les types autres que $Nat$.

**Remarque** : Dans un système prédicatif où la quantification sur les prédicats est interdite et le principe de récurrence traduit par une règle :

$$ \frac{(P 0) \quad \forall x : Nat.((P x) \rightarrow (P (S x))))}{\forall x : Nat.(P x)} $$
on peut représenter les preuves par des termes en ajoutant un symbole primitif $R$ et une règle de typage :

$$ \frac{\Gamma \vdash a : (P 0) \quad \Gamma \vdash b : \forall x : Nat.((P x) \rightarrow (P (S x)))}{\Gamma \vdash (R a b) : \forall x : Nat.(P x)} $$

Un tel système (même s'il n'est pas polymorphe) peut s'étendre par l'adjonction de types inductifs en ajoutant les règles de réduction :

* $(R a b 0) \triangleright a$,

* $(R a b (S x)) \triangleright (b x (R a b x))$.

## Constructeurs de Types

Un prédicat peut être vu comme un ensemble : l'ensemble des valeurs qui vérifient ce prédicat. Quantifier sur les prédicats revient donc à quantifier sur les ensembles. La possibilité suivante, qui est donnée en logique d'ordre supérieur, est de quantifier sur les ensembles d'ensembles, c'est-à-dire quantifier sur les objets du type $(Nat \rightarrow Prop) \rightarrow Prop$ par exemple. Cela demande simplement de donner à ces objets le type *Type*. Si $T$ et $T'$ sont de type *Type* on décide donc que $(x : T)T'$ est aussi de type *Type*. De même, pour former des objets de ce type, il faut autoriser les abstractions correspondantes. Un tel calcul est dit admettre des constructeurs de types [28].

**Définition 19.** : Constructeurs de Types

Le $\lambda$-calcul avec constructeurs de types [28] est obtenu en ajoutant aux règles de base les règles :

$$ \frac{\Gamma \vdash T : Type \quad \Gamma[x : T] \vdash T' : Type}{\Gamma \vdash (x : T)T' : Type} $$

$$ \frac{\Gamma \vdash T : Type \quad \Gamma[x : T] \vdash T' : Type \quad \Gamma[x : T] \vdash t : T'}{\Gamma \vdash [x : T]t : (x : T)T'} $$

## 1.3.2 Classification des Systèmes de Types

### Cube de Barendregt

L'extension du $\lambda$-calcul simplement typé avec types dépendants, types polymorphes et constructeurs de types est appelée le *Calcul des Constructions* [8] [11].

Les règles de ce calcul peuvent être ainsi agrégées :

**Définition 20.** : Calcul des Constructions

$$ \frac{\text{[ ] bien formé}}{\frac{\Gamma \vdash T : s}{\Gamma[x : T] \text{ bien formé}} s \in \{Prop, Type\}}} $$
$$ \frac{\text{\Gamma bien formé}}{\Gamma \vdash \text{Prop} : Type} $$
$$ \frac{\Gamma \text{ bien formé } x : T \in \Gamma}{\Gamma \vdash x : T} $$
$$ \frac{\Gamma \vdash T : s \quad \Gamma[x : T] \vdash T' : s'}{\Gamma \vdash (x : T)T' : s'} <s, s' > \in R $$

$$ \frac{\Gamma \vdash (x : T)T' : s \quad \Gamma[x : T] \vdash t : T'}{\Gamma \vdash [x : T]t : (x : T)T'} s \in \{Prop, Type\} $$

$$ \frac{\Gamma \vdash t : (x : T)T' \quad \Gamma \vdash t' : T}{\Gamma \vdash (t t') : T'[x \leftarrow t']$$

$$ \frac{\Gamma \vdash T : s \quad \Gamma \vdash T' : s \quad \Gamma \vdash t : T \quad T \equiv T'}{\Gamma \vdash t : T'} s \in \{Prop, Type\} $$

$$ \text{où } R = \{Prop, Type\}^2. $$

Dans la règle de formation des produits, le couple $<s, s' > = <Prop, Type>$ permet la formation de types dépendants, le couple $<s, s' > = <Type, Prop>$ permet la formation de types polymorphes, le couple $<s, s' > = <Type, Type>$ permet la formation de constructeurs de types.

En prenant pour $R$ non plus l'ensemble $\{Prop, Type\}^2$ mais uniquement une partie de cet ensemble on choisit d'inclure ou non chacune de ces trois propriétés au calcul que l'on définit. Ces trois choix binaires déterminent huit systèmes appelés les systèmes du cube de Barendregt [1]. Chacun de ces systèmes peut s'étendre en ajoutant des types inductifs.

<table><thead><tr><th>Types<br>Dépendants</th><th>Polymorphisme<br>de Types</th><th>Constructeurs<br>Inductifs</th><th>Types<br>Dépendants</th><th>Polymorphisme<br>de Types</th><th>Constructeurs<br>Inductifs</th></tr></thead><tbody><tr><td>N</td><td>N</td><td>N</td><td>N</td><td>N</td><td>Simplement Typé (Church [6])</td></tr><tr><td>O</td><td>N</td><td>N</td><td>N</td><td>N</td><td>λΠ (de Bruijn [3] / Howard [36] /<br>Harper-Honsel-Plotkin [33])</td></tr><tr><td>N</td><td>O</td><td>N</td><td>N</td><td>N</td><td>F (Girard [28])</td></tr><tr><td>O</td><td>O</td><td>N</td><td>N</td><td>N</td><td>λP2</td></tr><tr><td>N</td><td>O</td><td>O</td><td>N</td><td>N</td><td>F<sub>ω</sub> (Girard [28])</td></tr><tr><td>O</td><td>O</td><td>O</td><td>N</td><td>N</td><td>CoC(Coquand-Huet [8] [11])</td></tr><tr><td>N</td><td>N</td><td>N</td><td>O</td><td>O</td><td>T(Gödel [30])</td></tr><tr><td>O</td><td>N</td><td>N</td><td>O</td><td>O</td><td>ITT (Martin-Löf [50])</td></tr><tr><td>N</td><td>O</td><td>N</td><td>O</td><td>O</td><td>F<sup>ind</sup></td></tr><tr><td>O</td><td>O</td><td>N</td><td>O</td><td>O</td><td>λP2<sup>ind</sup></td></tr><tr><td>N</td><td>O</td><td>O</td><td>O</td><td>O</td><td>F<sub>ω</sub><sup>ind</sup></td></tr><tr><td>O</td><td>O</td><td>O</td><td>O</td><td>O</td><td>CIC(Coquand-Paulin [12])</td></tr></tbody></table>

Sur ces sept systèmes nous n’en avons présentés que douze, les constructeurs de types sans les types polymorphes menant à des systèmes de peu d’intérêt.

## Systèmes de Types Purs

Nous avons vu que des restrictions du Calcul des Constructions pouvaient être obtenues en restreignant la règle de formation des produits. On peut donc paramétrer un système de types par un ensemble de règles pour obtenir les huit systèmes du cube de Barendregt. On peut également le
paramétrer par l'ensemble des sortes considéré et par les règles telles que *Prop : Type*. Cette idée est due à Geuvers, Berardi et Terlouw.

Un système de types est donc défini par un ensemble *S* de sortes, un ensemble *Ax* de couples de sortes (appelés *axiomes*), un ensemble *R* de triplets de sortes (appelés *règles*).

**Définition 21.** : Terme

$$
T ::= s | x | (T T) | [x : T] T | (x : T) T
$$

**Définition 22.** : Règles de Typage

$$
\begin{align*}
& \boxed{\phantom{\Gamma \vdash T : s}} \text{ bien formé} \\
& \frac{\Gamma \vdash T : s}{\Gamma[x : T] \text{ bien formé}} s \in S \\
& \frac{\Gamma \text{ bien formé}}{\Gamma \vdash s : s'} <s, s' > \in Ax \\
& \frac{\Gamma \text{ bien formé}}{\Gamma \vdash x : T} x : T \in \Gamma \\
& \frac{\Gamma \vdash T : s \quad \Gamma[x : T] \vdash T' : s'}{\Gamma \vdash (x : T) T' : s''} <s, s', s'' > \in R \\
& \frac{\Gamma \vdash (x : T) T' : s \quad \Gamma[x : T] \vdash t : T'}{\Gamma \vdash [x : T] t : (x : T) T'} s \in S \\
& \frac{\Gamma \vdash t : (x : T) T' \quad \Gamma \vdash t' : T}{\Gamma \vdash (t t') : T'[x \leftarrow t']}
\end{align*}
\[
\frac{\Gamma \vdash T : s \quad \Gamma \vdash T' : s \quad \Gamma \vdash t : T \quad T \equiv T'}{\Gamma \vdash t : T'} s \in S
\]
$$

Exemples de Systèmes de Types Purs

Dans le Calcul des Constructions le terme *Type* n'est pas bien typé. On peut étendre ce système en un système *le Calcul des Constructions avec Univers* où tout terme type d'un terme est bien typé.

**Définition 23.** : Calcul des Constructions avec Univers

On se donne un nombre infini de sortes : *Prop*, *Type*₀(**Type**), *Type*₁, *Type*₂, ..., les *axiomes*
*Prop* : *Type*₀ et *Type*ᵢ : *Type*ᵢ₊₁ et les *règles* :

$$
\begin{align*}
& < \mathit{Prop}, \mathit{Prop}, \mathit{Prop} > \\
& < \mathit{Prop}, \mathit{Type}_i, \mathit{Type}_i > \\
& < \mathit{Type}_i, \mathit{Prop}, \mathit{Prop} > \\
& < \mathit{Type}_i, \mathit{Type}_j, \mathit{Type}_{\max\{i,j\}} >
\end{align*}
$$
**Remarque** : La règle `<Typeᵢ, Prop, Prop>` donne à ce système un caractère imprédicatif "au niveau *Prop*", mais la règle `<Typeᵢ, Typeⱼ, Type<sub>max{i,j}</sub>`> lui donne un caractère prédicatif "au niveau *Type*". En effet, si *P* est de type *Typeⱼ*, (*x* : *Typeᵢ*)*P* est de type *Type<sub>max{i+1,j}</sub>* donc n'est pas de type *Typeᵢ*. Un système imprédicatif à deux niveaux (comme le système avec la règle `<Typeᵢ, Typeⱼ, Typeⱼ>`) n'est pas normalisable [28].

Enfin ce système peut être étendu en ajoutant une règle de cumulativité qui permet d'inclure le type *Typeᵢ* dans le type *Typeᵢ+₁*, voir [9] [49].

Un deuxième exemple de système de types pur est le système *Méta* que nous utiliserons dans l'expression de nos algorithmes de synthèse de preuves et de résolution d'équations.

**Définition 24.** : *Méta*

$$ \mathit{M\'eta} = <S', Ax', R'> $$

$$ S' = \{ \mathit{Prop}, \mathit{Type}, \mathit{Extern} \} $$

$$ Ax' = \{ \langle \mathit{Prop}, \mathit{Type} \rangle, \langle \mathit{Type}, \mathit{Extern} \rangle \} $$

$$ R' = \{ \langle \mathit{Prop}, \mathit{Prop}, \mathit{Prop} \rangle, \langle \mathit{Prop}, \mathit{Type}, \mathit{Type} \rangle, \langle \mathit{Type}, \mathit{Prop}, \mathit{Prop} \rangle, \\ \langle \mathit{Type}, \mathit{Type}, \mathit{Type} \rangle, \langle \mathit{Prop}, \mathit{Extern}, \mathit{Extern} \rangle, \langle \mathit{Type}, \mathit{Extern}, \mathit{Extern} \rangle \} $$

**Remarque** : Ce système est un sous-système du Calcul des Constructions avec Univers, dans lequel la sorte *Type₁* est notée *Extern*.

**Remarque** : L'intérêt de ce système vient du fait que si $\mathcal{T}$ un système de types du Cube, alors pour tout terme $t$ bien typé dans le système $\mathcal{T}$, il est possible de déclarer dans le système *Méta* une variable qui a le type de $t$ (par exemple avec $t = \mathit{Prop}$, il est possible de déclarer dans le système *Méta* une variable de type *Type*). De plus, si $t : T'$ est bien typé dans le système *Méta* dans le contexte $\Gamma[x : T]$ et $T' \neq \mathit{Extern}$, alors $f = [x : T]t$ est également bien typé.

### 1.3.3 Propriétés des Systèmes de Types Purs

**Définition 25.** : *Système de Types Fonctionnel*

Un système de types est dit fonctionnel si :

$$ \langle s, s' \rangle \in Ax \text{ et } \langle s, s'' \rangle \in Ax \text{ implique } s' = s'' $$

$$ \langle s, s', s'' \rangle \in R \text{ et } \langle s, s', s''' \rangle \in R \text{ implique } s'' = s''' $$

**Proposition 4.** : *Les Calculs du Cube, le système *Méta* et le Calcul des Constructions avec Univers sont fonctionnels.*

**Définition 26.** : *Terme Bien Typé*

Un terme $t$ est dit bien typé dans un contexte $\Gamma$ s'il existe un terme $T$ tel que $\Gamma \vdash t : T$.

**Proposition 5.** : *Dans un système de types fonctionnel un terme $t$ bien typé dans un contexte $\Gamma$ a un type unique modulo $\beta\eta$-équivalence.*
**Démonstration** : Par récurrence sur la structure de $t$.

**Théorème 1.** : Normalisation Forte et Confluence de la Réduction

Tout terme $t$ bien typé dans un contexte $\Gamma$, dans un calcul du cube, dans le système Méta ou dans le Calcul des Constructions avec Univers à une forme normale unique.

**Démonstration** : Voir [9] [60] [25].

**Remarque** : Le théorème précédent ne s'applique qu'aux calculs du cube, au système Méta et au Calcul des Constructions avec Univers et non à tous les systèmes de types purs. Par exemple, dans le système avec une unique sorte *Prop*, l'axiome *Prop* : *Prop* et la règle < *Prop*, *Prop*, *Prop* >, on peut typer des termes non normalisables [28].

**Définition 27.** : *Type*

Un terme $T$ est dit être un type dans un contexte $\Gamma$ s'il existe une sorte $s$ telle que $\Gamma \vdash T : s$.

**Proposition 6.** : Si $\Gamma \vdash t : T$, alors $T$ est un type ou une sorte.

**Démonstration** : Par récurrence sur la longueur de la dérivation de $\Gamma \vdash t : T$.

**Définition 28.** : *Terme Atomique*

Un terme $t$ est dit atomique s'il est de la forme $(x c_1 \dots c_n)$ où $x$ est une variable ou une sorte. Le symbole $x$ est appelé la tête du terme $t$.

**Proposition 7.** : Soit $t$ un terme normal et bien typé, $t$ est une abstraction, un produit ou un terme atomique.

**Démonstration** : Si le terme $t$ n'est ni une abstraction ni un produit, alors il peut être écrit d'une façon unique :

$$t = (u c_1 \dots c_n)$$

où $u$ n'est pas une application.

Le terme $u$ n'est pas un produit (si $n \neq 0$ parce qu'un produit est de type $s$ pour une sorte $s$ et ne peut donc pas être appliqué et si $n = 0$ parce que $t$ n'est pas un produit). Ce n'est pas une abstraction (si $n \neq 0$ parce que $t$ est en forme normale et si $n = 0$ parce que $t$ n'est pas une abstraction). C'est donc une variable ou une sorte.

**Proposition 8.** : Soit $T$ un type normal, $T$ s'écrit de manière unique $T = (x_1 : P_1)...(x_n : P_n)P$ avec $P$ atomique.

**Démonstration** : Par récurrence sur la structure de $T$.

**Définition 29.** : *Forme $\eta$-longue*

Soit $\Gamma$ un contexte et $t$ un terme $\beta\eta$-normal bien typé dans $\Gamma$. La forme $\eta$-longue de ce terme est définie de la façon suivante :

— Si $t = [x : U]u$, alors soit $U'$ la forme $\eta$-longue de $U$ dans $\Gamma$ et $u'$ celle de $u$ dans $\Gamma[x : U]$, on définit la forme $\eta$-longue de $t$ comme le terme $[x : U']u'$,

— Si $t = (x : U)V$, alors soit $U'$ la forme $\eta$-longue de $U$ dans $\Gamma$ et $V'$ celle de $V$ dans $\Gamma[x : U]$, on définit la forme $\eta$-longue de $t$ comme le terme $(x : U')V'$,
— Si $t = (w c_1 \dots c_p)$, alors soit $T = (x_1 : P_1)\dots(x_n : P_n)P$ (P atomique) la forme normale du type de t. Soit $c'_i$ la forme $\eta$-longue de $c_i$ dans $\Gamma$, $P'_i$ celle de $P_i$ dans $\Gamma[x_1 : P_1; \dots; x_{i-1} : P_{i-1}]$ et $x'_i$ celle de $x_i$ dans $\Gamma[x_1 : P_1; \dots; x_i : P_i]$. On définit la forme $\eta$-longue de t comme le terme $[x_1 : P'_1]\dots[x_n : P'_n](w c'_1 \dots c'_p x'_1 \dots x'_n)$.

La bonne fondation de cette définition est prouvée au chapitre suivant.

De façon évidente, la forme $\eta$-longue d'un terme $\beta\eta$-normal est $\beta$-normale, ce qui motive la définition :

**Définition 30. : Forme $\beta$-normale $\eta$-longue**

Soit $t$ un terme bien typé dans un contexte $\Gamma$, la forme $\beta$-normale $\eta$-longue de $t$ est la forme $\eta$-longue de sa forme $\beta\eta$-normale.

Par la suite, tous les termes seront supposés en forme $\beta$-normale $\eta$-longue.

**Fonctions Représentables**

Nous allons maintenant voir que ces extensions du $\lambda$-calcul simplement typé qui ont été motivées par des considérations de représentabilité des preuves sont également plus riches du point de vue de la représentabilité des fonctions.

Dans le $\lambda$-calcul simplement typé, les seules fonctions des entiers dans les entiers représentables sont les fonctions constantes et celles qui ajoutent une constante à l'un de leurs arguments. Cet ensemble de fonctions peut être défini comme le plus petit ensemble qui contient les projections, la fonction nulle, la fonction successeur et qui est clos par composition. Une construction manque pour obtenir les fonctions récursives primitives : la définition par récurrence.

Une première tentative pour obtenir cette construction est de définir les entiers non plus avec deux variables pour zéro et le successeur, mais comme des itérateurs : les entiers de Church. On se donne un type $T$ de base, on définit l'entier $n$ comme le terme :

$$n = [x : T][f : T \to T](f \dots (f x) \dots) \quad (n \text{ fois})$$

Les entiers sont alors des termes de type $T \to (T \to T) \to T$. Quand on a une fonction $g$ et un entier $n$ le terme $[x : T](n x g)$ est la fonction $g$ itérée $n$ fois $g \circ g \circ \dots \circ g$. Malheureusement cette possibilité d'itération est très restreinte : il n'est possible d'itérer que des fonctions de type $T \to T$ et pas celles de type $Nat \to Nat$ et, de ce fait, il n'est pas possible de représenter toutes les fonctions primitives récursives par un $\lambda$-terme simplement typé :

**Proposition 9. :** *Les fonctions sur les entiers de Church représentables comme des termes dans le $\lambda$-calcul simplement typé sont les polynômes étendus par le test à zéro.*

**Démonstration :** Voir [62].

En revanche dans les systèmes polymorphes, on peut définir l'entier $n$ comme le terme :

$$n = [T : Prop][x : T][f : T \to T](f \dots (f x) \dots) \quad (n \text{ fois})$$

et ainsi itérer des fonctions de type $T \to T$ pour n'importe quel type $T$, en particulier le type $Nat$ lui-même et les types où $Nat$ a une occurrence (imprédicativité).
**Proposition 10.** : Les fonctions récursives primitives sont représentables par des termes dans le $\lambda$-calcul polymorphe, et également les fonctions récursives primitives avec paramètres fonctionnels comme la fonction d'Ackermann.

**Démonstration** : Voir [28] [29].

Un résultat plus fort est le suivant :

**Proposition 11.** : Les fonctions représentables dans le $\lambda$-calcul polymorphe sont les fonctions de l'arithmétique du deuxième ordre. Les fonctions représentables dans le $\lambda$-calcul polymorphe avec constructeurs de types sont les fonctions de l'arithmétique d'ordre supérieur.

**Démonstration** : Voir [28].

Dans les systèmes avec types inductifs, en revanche, il n'est plus nécessaire de définir les entiers comme des itérateurs pour pouvoir représenter les fonctions récursives primitives. En effet, si $a$ est un terme de type $Nat$ et $b$ un terme de type $Nat \to Nat \to Nat$, en posant $P = [x : Nat]Nat$ et $f = (R P a b)$, le terme $(f 0)$ se réduit sur $a$ et $(f (S x))$ sur $(b x (f x))$ (les cas de récursion avec paramètres sont très similaires). Ainsi :

**Proposition 12.** : Les fonctions primitives récursives sont représentables par des termes dans le $\lambda$-calcul avec type inductif, et également les fonctions récursives primitives avec paramètres fonctionnels.

**Démonstration** : Voir [30] [29].

**Remarque** : Si on s'intéresse à présent non plus aux fonctions représentables mais aux algorithmes représentables, on s'aperçoit que le formalisme avec types inductifs est plus riche que le $\lambda$-calcul polymorphe.

### 1.3.4 Une Extension de la Logique d'Ordre Supérieur : Le Calcul des Constructions

Si on étend la logique d'ordre supérieur restreinte à l'implication et à la quantification universelle, en prenant comme langage des objets non plus le $\lambda$-calcul simplement typé mais le Calcul des Constructions, on obtient un système où toute preuve d'une proposition $P$ peut être traduite en un terme de type $P$ et vice versa. Règles de typage et de déduction font double emploi, on peut donc abandonner les règles de déduction. Déclarer un axiome $P$ est simplement déclarer une variable de type $P$ et prouver une proposition $P$ est simplement donner un terme de type $P$. Le système logique se réduit donc ainsi à un $\lambda$-calcul typé.

#### Connecteurs

Jusqu'à maintenant nous nous sommes restreints à ne considérer qu'un connecteur et un quantificateur : l'implication et le quantificateur universel. Cela vient du fait qu'une fois que l'on dispose de ce connecteur et de ce quantificateur on peut les utiliser pour coder les règles de déduction concernant les autres connecteurs et quantificateurs comme des propositions [28]. En effet, ces règles permettent de déduire des propositions d'autres propositions, ce sont donc essentiellement des implications. Par
ailleurs elles contiennent des variables libres qui sont implicitement universellement quantifiées. Par exemple, on peut déclarer la conjonction par :

$$ and : Prop \to Prop \to Prop $$

et poser les règles de déduction comme des axiomes exprimés avec l'implication et la quantification universelle :

$$ and\_intro : (A : Prop)(B : Prop)(A \to B \to (and A B)) $$

$$ and\_elim1 : (A : Prop)(B : Prop)((and A B) \to A) $$

$$ and\_elim2 : (A : Prop)(B : Prop)((and A B) \to B) $$

En fait, il est même possible de définir le symbole *and* et de prouver ces règles.

**Définition 31. : Connecteurs**

*On pose :*

$$ and = [A : Prop][B : Prop](C : Prop)((A \to B \to C) \to C) $$

$$ and\_intro = [A : Prop][B : Prop][x : A][y : B][C : Prop][u : A \to B \to C](u \ x \ y) $$

$$ and\_elim1 = [A : Prop][B : Prop][u : (and A B)](u A [x : A][y : B]x) $$

$$ and\_elim2 = [A : Prop][B : Prop][u : (and A B)](u B [x : A][y : B]y) $$

$$ or = [A : Prop][B : Prop](C : Prop)((A \to C) \to (B \to C) \to C) $$

$$ or\_intro1 = [A : Prop][B : Prop][x : A][C : Prop][u : A \to C][v : B \to C](u x) $$

$$ or\_intro2 = [A : Prop][B : Prop][x : B][C : Prop][u : A \to C][v : B \to C](v x) $$

$$ or\_elim = [A : Prop][B : Prop][C : Prop][x : (or A B)][u : (A \to C)][v : B \to C](x C u v) $$

$$ bot = (C : Prop)C $$

$$ bot\_elim = [C : Prop][u : bot](u C) $$

$$ ex = [T : Prop][P : T \to Prop](C : Prop)((((x : T)(P x) \to C) \to C) \to C) $$

$$ ex\_intro = [T : Prop][P : T \to Prop][t : T][u : (P t)][C : Prop][v : ((x : T)(Px) \to C)](v t u) $$

$$ ex\_elim = [T : Prop][P : T \to Prop][C : Prop][u : (exTP)][v : ((x : T)(Px) \to C)](u C v) $$
**Proposition 13. :**

On a :

$$ \mathit{and\_intro} : (A : \mathit{Prop})(B : \mathit{Prop})(A \to B \to (\mathit{and} A B)) $$

$$ \mathit{and\_elim1} : (A : \mathit{Prop})(B : \mathit{Prop})((\mathit{and} A B) \to A) $$

$$ \mathit{and\_elim2} : (A : \mathit{Prop})(B : \mathit{Prop})((\mathit{and} A B) \to B) $$

$$ \mathit{or\_intro1} : (A : \mathit{Prop})(B : \mathit{Prop})(A \to (\mathit{or} A B)) $$

$$ \mathit{or\_intro2} : (A : \mathit{Prop})(B : \mathit{Prop})(B \to (\mathit{or} A B)) $$

$$ \mathit{or\_elim} : (A : \mathit{Prop})(B : \mathit{Prop})(C : \mathit{Prop})((\mathit{or} A B) \to (A \to C) \to (B \to C) \to C) $$

$$ \mathit{bot\_elim} : (C : \mathit{Prop})(\mathit{bot} \to C) $$

$$ \mathit{ex\_intro} : (T : \mathit{Prop})(P : T \to \mathit{Prop})(t : T)((P t) \to (\mathit{ex} T P)) $$

$$ \mathit{ex\_elim} : (T : \mathit{Prop})(P : T \to \mathit{Prop})(C : \mathit{Prop})((\mathit{ex} T P) \to ((x : T)(P x) \to C) \to C) $$

**Remarque** : Pour la négation, on pose ($\neg A$) = $A \to \perp$, les règles $\neg$-intro et $\neg$-elim sont des cas particuliers de $\to$-intro et $\to$-elim.

## Cohérence

**Proposition 14.** : Dans le contexte vide, le type $\perp = (P : \mathit{Prop})P$ est vide.

**Démonstration** : S'il existait un terme de type $(P : \mathit{Prop})P$, il en existerait aussi un normal, donc un terme de type $P$ dans le contexte $[P : \mathit{Prop}]$. D'après la proposition 7, ce terme est une abstraction, un produit ou un terme atomique. Ce ne peut être une abstraction ou un produit pour des raisons évidentes de type, c'est donc un terme atomique. Sa tête ne peut être ni le symbole $\mathit{Prop}$ ni $\mathit{Type}$ ni $P$ pour des raisons évidentes de type, d'où contradiction.

Un corollaire est qu'on ne peut pas démontrer à la fois $P$ et $\neg P$ dans le contexte vide. Cette propriété s'appelle la *cohérence* du système logique.

**Remarque** : L'apparente simplicité de cette preuve de cohérence ne doit pas masquer le fait qu'elle s'appuie sur le théorème de normalisation du calcul qui est, quant à lui, difficile.
## Représentabilité des Fonctions

Le Calcul des Constructions, comme le λ-calcul polymorphe avec constructeurs de types, permet de représenter les fonctions de l'arithmétique d'ordre supérieur. Mais comme ces fonctions sont également celles du Calcul des Constructions, on obtient une relation très étroite entre les aspects logique et calculatoire de ce système :

**Théorème 2.** : *Principe de Compréhension*

Pour tout prédicat $P : Nat \to \dots \to Nat \to Prop$ tel qu'on puisse prouver la proposition $\forall x_1 : Nat \dots \forall x_n : Nat. \exists y : Nat.(P x_1 \dots x_n y)$, dans le Calcul des Constructions et sous les axiomes de l'arithmétique, il existe un terme $f$ tel que pour tout $n$-uplets d'entiers $< a_1, \dots, a_n >$, le terme $(f a_1 \dots a_n)$ se réduise sur un entier $b$ tel que $(P a_1 \dots a_n b)$.

## Quelques Variantes

Nous avons vu précédemment que l'isomorphisme de Curry-Howard nous poussait à identifier *Prop* et *Set* et donc à abandonner la règle *Prop* : *Set*. Une autre possibilité consiste à ne pas appliquer l'isomorphisme de Curry-Howard à la lettre et à identifier *Set* et *Type*. Ainsi, on peut garder la règle *Prop* : *Set*. Dans ce cas, on a besoin de donner un type au terme *Type* (= *Set*) pour pouvoir déclarer des variables de type *Set*. On se place donc dans un sous-système du Calcul des Constructions avec Univers, qui contient au moins les sortes *Prop*, *Type* et *Type*₁. Dans ce système le langage des preuves est imprédicatif, mais celui des termes prédicatif.

Enfin une autre variante consiste à garder les symboles *Prop*, *Set* et *Type* avec les règles *Prop* : *Type* et *Set* : *Type*. Dans ce cas, preuves et termes se correspondent par isomorphisme mais ne sont pas identifiés. Dans ce système, aussi bien le langage des preuves que le langage des termes est imprédicatif.

Ces systèmes sont comparés dans [24].
# Chapitre 2

## Bonne Fondation de la Récursion
Simultanée sur le Type et les
Sous-Termes Stricts d'un Terme

Nous nous plaçons dans ce chapitre dans un quelconque sous-système du Calcul des Construc-
tions avec Univers. Par exemple un système du cube, le système *Méta* ou le Calcul des Constructions
avec Univers lui-même.

Considérons un programme qui prend en argument un terme normal *t* et s'appelle lui-même
sur un sous-terme strict de *t*. Ce programme termine de façon évidente. Considérons de même un
programme qui prend en argument un terme normal *t* et s'appelle lui-même sur la forme normale du
type de *t* (si *t* n'est pas une sorte). Ce programme termine également car si *t* n'est pas une sorte, son
type est une sorte ou le type de son type en est une. Si maintenant le programme s'appelle lui-même
soit sur un sous-terme strict de *t* soit sur le type de *t*, il n'est plus évident qu'il termine. En effet,
du fait de la présence de types dépendants, un sous-terme d'un type n'est pas nécessairement un
type. Par exemple en partant de la liste vide [] (de type (*list* 0)), on engendre la suite de termes [],
(*list* 0), 0, *Nat*, *Prop*. Cette suite est finie. Nous allons montrer dans ce chapitre que c'est toujours
le cas, c'est-à-dire que la récursion simultanée sur le type et les sous-termes stricts d'un terme est
bien fondée.

Ce résultat de bonne fondation sera utilisé par la suite pour prouver la complétude d'une méthode de démonstration automatique (chapitre 4). En effet, pour synthétiser un terme *t* de type *T*, nous aurons comme tâche intermédiaire à synthétiser des sous-termes de *t* et aussi les types de certains de ces sous-termes. La complétude de cette méthode repose sur le fait que ces tâches intermédiaires ne forment pas une régression infinie, mais sont ordonnées de façon bien fondée. De même un algorithme de résolution d'équation (au chapitre 7) demandera, pour résoudre une équation *a* = *b*, de résoudre d'abord des équations entre des sous-termes de *a* et *b* et également entre les types de certains de ces sous-termes. La complétude et la terminaison de cet algorithme reposent encore sur le fait que ces équations sont ordonnées de façon bien fondée.

**Définition 32.** : *Sous-Terme*

On considère des termes bien typés normaux indicés par le contexte dans lequel ils sont bien
typés : $t_Γ$.

Soit $t_Γ$ un tel terme, on définit par récurrence sur la structure de $t_Γ$ l'ensemble des sous-termes
stricts de $t_Γ$ :

- si $t$ est une sorte ou une variable, alors $Sub(t_Γ) = \{\}$,

- si $t = (u v)$, alors $Sub(t_Γ) = \{u_Γ, v_Γ\} \cup Sub(u_Γ) \cup Sub(v_Γ)$,

- si $t = [x : P]u$, alors $Sub(t_Γ) = \{P_Γ, u_Γ[x: P]\} \cup Sub(P_Γ) \cup Sub(u_Γ[x: P])$,

- si $t = (x : P)u$, alors $Sub(t_Γ) = \{P_Γ, u_Γ[x: P]\} \cup Sub(P_Γ) \cup Sub(u_Γ[x: P])$.

**Définition 33.** : La Relation <

Soit < la plus petite relation transitive définie sur les termes normaux telle que :

- si $t_Γ$ est un sous-terme strict de $t'_Δ$, alors $t_Γ < t'_Δ$,

- si $T_Γ$ est la forme $\beta$-normale $\eta$-longue du type de $t_Γ$ dans $Γ$ et le terme $t$ n'est pas une sorte, alors $T_Γ < t_Γ$.

Nous allons montrer dans ce chapitre que la relation < est bien fondée.

## 2.1 Termes Marqués

On définit une syntaxe pour les systèmes de types dans laquelle chaque terme est marqué par son type. En fait tous les termes sont marqués sauf les sortes.

**Définition 34.** : Termes Marqués

$$T ::= s \mid x^T \mid (T \ T)^T \mid ([x : T]T)^T \mid ((x : T)T)^T$$

Soit $t$ et $u$ deux termes marqués et $x$ une variable. On note $t[x \leftarrow u]$ le terme obtenu en substituant $u$ à $x$ dans $t$. Remarquons que comme la variables $x$ peut apparaître dans le terme même et dans les marques, la substitution doit être effectuée aussi bien dans le terme lui-même que dans les marques.

On note $t \equiv u$ la relation de $\beta\eta$-équivalence entre les termes $t$ et $u$. Ici aussi, des conversions peuvent être effectuées aussi bien dans le terme que dans les marques.

Un contexte marqué est une liste de couples $<x, T>$ (notées $x : T$) où $x$ est une variable et $T$ un terme marqué.

**Définition 35.** : Règles de Typage

On définit inductivement deux jugements : $Γ$ est bien formé et $t$ a le type $T$ dans $Γ$ ($Γ \vdash t : T$) où $Γ$ est un contexte marqué et $t$ et $T$ deux termes marqués.

[] bien formé

$$\frac{\Gamma \vdash T : s}{\Gamma[x : T] \text{ bien formé}} s \in S$$

$$\frac{\Gamma \text{ bien formé}}{\Gamma \vdash s : s'} <s, s' > \in Ax$$

$$\frac{\Gamma \text{ bien formé} \quad x : T \in \Gamma}{\Gamma \vdash x^T : T}$$

$$\frac{\Gamma \vdash T : s \quad \Gamma[x : T] \vdash U : s'}{\Gamma \vdash ((x : T)U)^{s''} : s''} <s, s', s''> \in R$$
$$
\frac{\Gamma \vdash ((x : T)U)^s : s \quad \Gamma[x : T] \vdash t : U}{\Gamma \vdash ([x : T]t)^{((x:T)U)^s} : ((x : T)U)^s} s \in S
$$
$$
\frac{\Gamma \vdash t : ((x : T)U)^s \quad \Gamma \vdash u : T}{\Gamma \vdash (t \ u)^{U[x \leftarrow u]} : U[x \leftarrow u]}
$$
$$
\frac{\Gamma \vdash T : s \quad \Gamma \vdash U : s \quad \Gamma \vdash t : T \quad T \equiv U}{\Gamma \vdash t : U} s \in S
$$

**Proposition 15.** : *Soit Γ un contexte et t et T deux termes tels que t ne soit pas une sorte et Γ ⊢ t : T. Le terme T est alors équivalent à la marque la plus externe de t. Par exemple, si t = (u v)U, alors T est équivalent à U.*

**Démonstration** : Par récurrence sur la longueur de la dérivation de Γ ⊢ t : T.

**Démonstration 36.** : Terme Marqué Bien Typé

Un terme *t* est dit bien typé dans un contexte $\Gamma$ s'il existe un terme *T* tel que $\Gamma \vdash t : T$.

**Démonstration 37.** : Contenu d'un Terme Marqué

Soit *t* un terme marqué, le contenu de *t* est le terme sans marques *t#* défini par récurrence sur la structure de *t* :

- si $t$ est une sorte, alors $t^# = t$,

- si $t = x^T$, alors $t^# = x$,

- si $t = (u v)^T$, alors $t^# = (u^# v^#)$,

- si $t = ([x: P]u)^T$, alors $t^# = [x: P^#]u^#$,

- si $t = ((x: P)U)^T$, alors $t^# = (x: P^#)U^#$.

**Démonstration 38.** : Contenu d'un Contexte

Soit $\Gamma = [x_1 : P_1; \dots; x_n : P_n]$ un contexte marqué, le contenu de $\Gamma$ est le contexte :

$$
\Gamma^{\#} = [x_1 : P_1^{\#} ; \dots ; x_n : P_n^{\#}]
$$

**Proposition 16.** : *Soit $t$ un terme marqué de type $T$ dans un contexte $\Gamma$. Le terme $t^#$ est bien typé et de type $T^#$ dans $\Gamma^#$.*

**Démonstration** : Par récurrence sur la longueur de la dérivation de Γ ⊢ t : T.

## 2.2 Normalisation des Termes Marqués

**Démonstration 39.** : $\beta\eta$-réduction

On note $\vdash$ la relation de $\beta\eta$-réduction (en une étape). Le radical réduit peut aussi bien se trouver dans le terme que dans les marques.

On note $\vdash^*$ la relation de $\beta\eta$-réduction en un nombre quelconque d'étapes et $\vdash^+$ la relation de $\beta\eta$-réduction en au moins une étape.

**Démonstration 40.** : Traduction d'un Terme Marqué en un Terme non Marqué.

Soit $t$ un terme marqué qui est bien typé ou une sorte, soit $T$ son type dans le Calcul des
Constructions avec Univers et $s$ le type de $T$. On définit par récurrence sur la structure de $t$ un
terme $t^\circ$ du Calcul des Constructions avec Univers :
— si t est une sorte on pose $t^° = t$,

— si $t = x^T$, alors on pose $t^° = (([z : s]x) T^°)$,

— si $t = (u v)^T$, alors on pose $t^° = ((([z : s](u^° v^°)) T^°)$,

— si $t = ([x : P]u)^T$, alors on pose $t^° = ((([z : s][x : P^°]u^°) T^°)$,

— si $t = ((x : P)Q)^T$, alors on pose $t^° = ((([z : s](x : P^°)Q^°) T^°)$.

Cette traduction est similaire à celles définies dans [33] [26].

**Définition 41.** : Traduction d'un Contexte Marqué en un Contexte non Marqué

Soit $\Gamma = [x_1 : P_1; \dots; x_n : P_n]$ un contexte marqué, on pose $\Gamma^° = [x_1 : P_1^°; \dots; x_n : P_n^°]$

**Proposition 17.** : Soit $\Gamma$ un contexte marqué et $t$ et $T$ deux termes marqués tels que $\Gamma \vdash t : T$. On $a \Gamma^° \vdash t^° : T^°$.

**Démonstration** : Par récurrence sur la longueur de la dérivation de $\Gamma \vdash t : T$.

**Proposition 18.** : $a^°[x \leftarrow b^°] \triangleright^* (a[x \leftarrow b])^°$

**Démonstration** : Par récurrence sur la structure de $a$.

Si $a = x^T$ alors :

$$a^° = [z : s]x T^°$$

$$a^°[x \leftarrow b^°] = [z : s]b^° T^°[x \leftarrow b^°] \triangleright^* b^° = (x^T[x \leftarrow b])^° = (a[x \leftarrow b])^°$$

Les autres cas sont une simple application de l'hypothèse de récurrence. Par exemple si $a$ est une application $a = (t u)^T$, on a :

$$a^° = [z : s](t^° u^°)T^°$$

Donc :

$$a^°[x \leftarrow b^°] = [z : s](t^°[x \leftarrow b^°] u^°[x \leftarrow b^°])T^°[x \leftarrow b^°]$$

Par hypothèse de récurrence on a :

$$t^°[x \leftarrow b^°] \triangleright^* (t[x \leftarrow b])^°$$

$$u^°[x \leftarrow b^°] \triangleright^* (u[x \leftarrow b])^°$$

$$T^°[x \leftarrow b^°] \triangleright^* (T[x \leftarrow b])^°$$

Donc :

$$\begin{align*}
a^°[x \leftarrow b^°] \triangleright^* [z : s]((t[x \leftarrow b])^° (u[x \leftarrow b])^°)(T[x \leftarrow b])^° \\
&= ((t[x \leftarrow b] u[x \leftarrow b])^{T[x \leftarrow b]})^° = (a[x \leftarrow b])^°
\end{align*}$$

**Proposition 19.** : Si $a \triangleright b$, alors $a^° \triangleright^+ b^°$.

**Démonstration** : Si $a = (([x : P]t)^T u)^U$ et $b = t[x \leftarrow u]$,

$$a^° = ([z : s]((([z' : s'][x : P^°]t^°) T^°) u^°) U^°)$$

$$b^° = (t[x \leftarrow u])^°$$
Dans $a^{\circ}$, on réduit d'abord trois $\beta$-radicaux pour obtenir le terme $t^{\circ}[x \leftarrow u^{\circ}]$, puis un certain nombre de radicaux pour obtenir le terme $b^{\circ}$.

Si $a = ([x: P](t x^P)^T)^U$ et $b = t$,

$$a^{\circ} = ([z:s][x:P^{\circ}]/[z':s'](t^{\circ}([z'':s'']x)P^{\circ}))T^{\circ})U^{\circ}$$
$$b^{\circ} = t^{\circ}$$

On réduit trois $\beta$-radicaux et un $\eta$-radical pour obtenir le terme $b^{\circ}$.

Et de même si on réduit un radical dans un sous-terme.

**Lemme 1. :** La $\beta\eta$-réduction sur les termes marqués est fortement normalisable.

**Démonstration :** S'il existait une réduction infinie issue d'un terme marqué $t$, il en existerait aussi une issue de $t^{\circ}$, ce qui est en contradiction avec la normalisation forte du Calcul des Constructions avec Univers.

**Proposition 20. :** Soient $a$ et $b$ deux termes marqués normaux bien typés dans un contexte marqué $\Gamma$. Si $a^{\#} = b^{\#}$, alors $a = b$.

**Démonstration :** Par récurrence sur la structure de $a$. Comme $a$ et $b$ ont le même contenu, ce sont ou bien deux sortes, ou bien deux variables, ou bien deux abstractions, ou bien deux produits ou bien deux applications.

Si ce sont par exemple deux applications, $a = (t u)^T$, $b = (v w)^U$, alors les termes $t$ et $v$ bien typés et normaux dans $\Gamma$ et ont même contenu, ils sont donc égaux. De même les termes $u$ et $w$ sont bien typés dans $\Gamma$ et ont même contenu, ils sont donc égaux. Soit $V$ le type de $a^{\#} = b^{\#}$ dans $\Gamma^{\#}$. Les termes $T$ et $U$ sont bien typés et normaux dans $\Gamma$, ils ont tous deux le contenu $V$, ils sont donc égaux. Donc $a = b$.

Et de même si $a$ et $b$ sont deux sortes, variables, abstractions ou produits.

**Proposition 21. :** Soit $a$ et $b$ deux termes marqués. Si $a \triangleright^* b$, alors $a^{\#} \triangleright^* b^{\#}$.

**Démonstration :** Par récurrence sur la longueur de la dérivation de $a \triangleright^* b$.

**Proposition 22. :** Unicité de la Forme Normale

Soit $\Gamma$ un contexte et $t$, $a$ et $b$ des termes bien typés dans $\Gamma$ tels que $a$ et $b$ sont normaux et $t$ se réduit (en un nombre arbitraire d'étapes) sur $a$ et $b$, alors $a = b$.

**Démonstration :** Les termes $a$ et $b$ sont bien typés dans $\Gamma$ et leur contenu est la forme normale de $t^{\#}$.

## 2.3 Terme Marqué Associé à un Terme non Marqué

On veut associer à chaque terme non marqué un terme marqué. On pourrait considérer le terme non marqué et marquer chacun de ses sous-termes par son type, mais nous devrions alors marquer les nouveaux sous-termes introduits comme marques et prouver que ce processus termine. Il est en fait plus simple de construire le terme marqué par récurrence sur la longueur de la dérivation de typage du terme non marqué.
**Proposition 23.** : Soit $a$ et $b$ deux termes marqués. Si $a \equiv b$, alors $a^\# \equiv b^\#$.

**Démonstration** : Par récurrence sur la longueur de la dérivation de $a \equiv b$.

**Proposition 24.** : Soit $a$ et $b$ deux termes marqués bien typés dans le contexte marqué $\Gamma$. Si $a^\# \equiv b^\#$, alors $a \equiv b$.

**Démonstration** : Soit $c$ la forme normale de $a$ et $d$ celle de $b$. Le terme $c^\#$ est la forme normale de $a^\#$ et $d^\#$ la forme normale de $b^\#$. Comme $a^\# \equiv b^\#$, on a $c^\# = d^\#$, donc $c = d$ et de ce fait $a \equiv b$.

**Définition 42.** : Traduction d'un Terme non Marqué en un Terme Marqué

Par récurrence sur la longueur de la dérivation non marquée $\Delta \vdash a : A$ ou $\Delta$ bien formé, on construit un contexte marqué $\Delta^*$ et des termes marqués $a^*$ et $A^*$ tels que $\Delta^* \vdash a^* : A^*$ et $\Delta^* \# = \Delta$, $a^* \# = a$ et $A^* \# = A$ ou un contexte bien formé $\Delta^*$ tel que $\Delta^* \# = \Delta$.

— Si la dernière règle est :

$\underline{[] \text{ bien formé}}$

on pose $\Delta^* = []$.

— Si la dernière règle est :

$\frac{\Gamma \vdash T : s}{\Gamma[x : T] \text{ bien formé}}$

alors par hypothèse de récurrence on a construit $\Gamma^*$ et $T^*$. On pose $\Delta^* = \Gamma^*[x : T^*]$.

— Si la dernière règle est :

$\frac{\Gamma \text{ bien formé}}{\Gamma \vdash s : s'}$

alors par hypothèse de récurrence on a construit $\Gamma^*$. On pose $\Delta^* = \Gamma^*$, $a^* = s$ et $A^* = s'$.

— Si la dernière règle est :

$\frac{x : T \in \Gamma}{\Gamma \vdash x : T}$

alors par hypothèse de récurrence on a construit $\Gamma^*$ et $T^*$ et $x : T^* \in \Gamma^*$. On pose $\Delta^* = \Gamma^*$, $a^* = x^{T^*}$ et $A^* = T^*$.

— Si la dernière règle est :

$\frac{\Gamma \vdash T : s \quad \Gamma[x : T] \vdash U : s'}{\Gamma \vdash (x : T)U : s''}$

alors par hypothèse de récurrence on a construit $\Gamma^*$, $T^*$ et $U^*$.

On pose $\Delta^* = \Gamma^*$, $a^* = ((x : T^*)U^*)^{s''}$ et $A^* = s''$.

— Si la dernière règle est :

$\frac{\Gamma \vdash ((x : T)U) : s \quad \Gamma[x : T] \vdash t : U}{\Gamma \vdash [x : T]t : (x : T)U}$

alors par hypothèse de récurrence on a construit $\Gamma^*$, $((x : T)U)^*$, $T^*$, $t^*$ et $U^*$. On pose $\Delta^* = \Gamma^*$, $a^* = ([x : T^*]t^*)((x : T^*)U^*)^s$ et $A^* = ((x : T^*)U^*)^s$.
— Si la dernière règle est :

$$ \frac{\Gamma \vdash t : (x : T)U \quad \Gamma \vdash u : T}{\Gamma \vdash (t \ u) : U[x \leftarrow u]} $$

alors par hypothèse de récurrence on a construit $\Gamma^*$, $t^*$, $((x : T)U)^*$, $u^*$ et $T^*$. Comme $((x : T)U)^* \# = ((x : T)U)$ le terme $((x : T)U)^*$ est un produit $((x : T)U)^* = ((x : P)Q)^s$ avec $P^\# = T$ et $Q^\# = U$. On pose $\Delta^* = \Gamma^*$, $a^* = (t^* u^*)^{Q[x \leftarrow u^*]}$ et $A^* = Q[x \leftarrow u^*]$.

— Si la dernière règle est :

$$ \frac{\Gamma \vdash T : s \quad \Gamma \vdash U : s \quad \Gamma \vdash t : T \quad T \equiv U}{\Gamma \vdash t : U} $$

alors par hypothèse de récurrence on a construit $\Gamma^*$, $t^*$, $T^*$ et $U^*$. On a $T^* \# \equiv U^* \#$, donc $T^* \equiv U^*$. On pose $\Delta^* = \Gamma^*$, $a^* = t^*$ et $A^* = U^*$.

**Remarque** : Soit $\Delta$ un contexte et $a$ et $A$ deux termes tels que $\Delta \vdash a : A$. Deux dérivations de $\Delta \vdash a : A$ peuvent mener à construire deux terme $a_1^*$ et $a_2^*$ distincts. Mais on a $a_1^* \# = a_2^* \# = a$. Donc d'après la proposition 24, $a_1^* \equiv a_2^*$ et donc $a_1^*$ et $a_2^*$ ont même forme normale.

## 2.4 Forme $\eta$-longue d'un Terme Marqué

**Définition 43.** : Mesure d'un Terme Marqué

Soit $\Gamma$ un contexte marqué et $t$ un terme marqué bien typé dans $\Gamma$. On définit par récurrence sur la structure de $t$, la mesure $\mu(t)$ de $t$ :

— Si $t$ est une sorte, alors $\mu(t) = 1$,

— Si $t = x^T$, alors $\mu(t) = \mu(T)$,

— Si $t = (u \ v)^T$, alors $\mu(t) = \mu(u) + \mu(v) + \mu(T)$,

— Si $t = ([x : U]v)^T$, alors $\mu(t) = \mu(U) + \mu(v) + \mu(T)$,

— Si $t = ((x : U)V)^T$, alors $\mu(t) = \mu(U) + \mu(V) + \mu(T)$.

**Définition 44.** : Forme $\eta$-longue d'un Terme Marqué

Soit $\Gamma$ un contexte marqué et $t$ un terme marqué $\beta\eta$-normal bien typé dans $\Gamma$. La forme $\eta$-longue du terme $t$ est définie par récurrence sur $\mu(t)$ :

— Si $t = ([x : U]u)^T$, alors soit $U'$ la forme $\eta$-longue de $U$ dans $\Gamma$, $T'$ la forme $\eta$-longue de $T$ dans $\Gamma$ et $u'$ la forme $\eta$-longue de $u$ dans $\Gamma[x : U]$, on définit la forme $\eta$-longue de $t$ comme le terme $([x : U']u')^{T'}$.

— Si $t = ((x : U)V)^T$, alors soit $U'$ la forme $\eta$-longue de $U$ dans $\Gamma$, $T'$ la forme $\eta$-longue de $T$ dans $\Gamma$ et $V'$ la forme $\eta$-longue de $V$ dans $\Gamma[x : U]$, on définit la forme $\eta$-longue de $t$ comme le terme $((x : U')V')^T$.

— Si $t = (((w^{T_0} c_1)^{T_1}) ... c_p)^{T_p}$, alors notons $T = T_p$ le type de $t$.

Soit $T = ((x_1 : P_1)...((x_n : P_n)P)^{U_n}...)^{U_1}$ (P atomique). On pose $c'_i$ la forme $\eta$-longue de $c_i$ dans $\Gamma$, $T'_i$ la forme $\eta$-longue de $T_i$ dans $\Gamma$, $P'_i$ la forme $\eta$-longue de $P_i$ dans le contexte $\Gamma[x_1 : P_1; ...; x_{i-1} : P_{i-1}]$, $U'_i$ la forme $\eta$-longue de $U_i$ dans ce même contexte et $x'_i$ la forme $\eta$-longue de $x'_i$ dans le contexte $\Gamma[x_1 : P_1; ...; x_i : P_i]$. On définit la forme $\eta$-longue de $t$ comme le terme :

$$ [x_1 : P'_1]...[x_n : P'_n]((( (w^{T'_0} c'_1)^{T'_1} ... c'_p)^{T'_p} x'_1)^{V'_1} ... x'_n)^{V'_n} $$

$$ \text{où } V'_i = ((x_{i+1} : P'_1)...((x_{i+1} : P'_n)P')^{U'_n}...)^{U'_1}. $$
**Proposition 25.** : La définition de la forme η-longue des termes non marqués donnée au chapitre précédent est bien fondée.

**Démonstration** : Soit $\Gamma$ un contexte non marqué et $t$ un terme non marqué normal bien typé dans $\Gamma$. Soit $u$ la forme normale de sa traduction $t^*$. On pose $\mu(t) = \mu(u)$. La définition de la forme η-longue des termes non marqués donnée au chapitre précédent est une récurrence sur $\mu(t)$.

## 2.5 Bonne Fondation de la Relation <

**Définition 45.** : Traduction Normale d'un Terme non Marqué

Soit $t$ un terme bien typé dans le contexte $\Gamma$, on définit sa traduction normale $t^+$ comme la forme η-longue de la forme normale de sa traduction $t^*$.

**Lemme 2.** : La relation < est bien fondée.

**Démonstration** : Soient $t$ et $u$ deux termes non marqués normaux, si $t$ est la forme normale η-longue du type de $u$ et le terme $u$ n’est pas une sorte alors $t^+$ est la marque la plus externe de $u^+$, c’est donc un sous-terme strict de $u^+$. Si $t$ est un sous-terme strict de $u$, alors par récurrence sur la structure de $u$, le terme $t^+$ est un sous-terme strict de $u^+$. On en déduit donc que si $t < u$, alors $t^+$ est un sous-terme strict de $u^+$.
Première partie

Démonstration Automatique
# Chapitre 3

## Contextes Quantifiés Contraints, Substitution

### 3.1 Preuves Incomplètes

#### Variables Universelles et Variables Existentielles

Plaçons-nous dans un système de types quelconque et considérons le contexte :

$$ \Gamma = [A : Prop; B : Prop; C : Prop; u : B \to C; v : A \to B; w : A] $$

Dans ce contexte on cherche une preuve de la proposition C. Une preuve de cette proposition est $(u(vw))$. Toute l'idée de la méthode de démonstration automatique que nous présentons ici revient à pouvoir inférer cette preuve étape par étape, en considérant par exemple dans une première étape que la preuve commence par la variable u. Nous allons développer dans ce chapitre le matériel technique qui nous permettra de considérer ainsi des étapes extrêmement élémentaires dans la construction des preuves.

La première notion dont nous avons besoin est celle de preuve incomplète. Dans notre exemple, l'axiome $B \to C$ nous permet de nous ramener à la recherche d'une preuve de B. En effet, si on trouve une preuve $t$ de B, le terme $(ut)$ sera une preuve de C. Cette information peut s'exprimer par le fait que $(ux)$ est une preuve incomplète de C. La variable $x$ est de type B, la recherche d'une preuve de B, se traduit par la recherche d'un terme par lequel instancier cette variable. Une fois un terme trouvé, l'application de la substitution $x \leftarrow t$ à la preuve $(ux)$ donnera la preuve $(ut)$.

Cette méthode n'est qu'une reformulation de l'idée de base des méthodes algébriques. En effet lorsqu'on recherche un entier dont le carré plus six est égal au quintuple, on déclare une variable $x$ pour cet entier, ce qui nous permet de considérer les entiers incomplets $x^2 + 6$ et $5x$ et d'exprimer la contrainte :

$$ x^2 + 6 = 5x $$

Une solution de cette équation est une substitution qui lie un entier à la variable $x$, par exemple la substitution $x \leftarrow 2$. En considérant une expression comme $x^2+6$, nous avons enrichi le formalisme des entiers en ajoutant une catégorie syntaxique : les variables.

Il est tentant, pour considérer des preuves incomplètes, de s'inspirer de cette méthode c'est-à-dire d'ajouter au formalisme des termes une nouvelle sorte d'objets (les variables), définir une
notion de typage pour ces termes étendus, une notion de substitution, etc. Cette méthode est en fait excessivement lourde. En effet elle n’exploite pas une particularité essentielle du λ-calcul, qui est que ce formalisme à la différence de celui des entiers, comporte déjà une notion de variable. Notre opinion est qu’il est beaucoup plus économique d’utiliser cette notion que de la dupliquer, en considérant deux classes de variables : les variables du λ-calcul et des méta-variables dénotant des λ-termes. Ainsi, pour nous, du point de vue de la bonne formation des contextes et du typage des termes, rien ne distingue les variables $x$ et $u$, en particulier le terme $(u x)$ n’est bien typé que dans un contexte dans lequel aussi bien les variables $u$ que $x$ sont déclarées. En revanche, ces variables ont des propriétés différentes vis-à-vis de la substitution : $x$ peut être instanciée par une substitution et $u$ ne le peut pas.

Cette information binaire est exprimée en associant un quantificateur à chaque variable d'un contexte, le quantificateur universel aux variables qui ne peuvent pas être instanciées et le quantificateur existentiel à celles qui le peuvent. Ce choix vient du fait qu'une méthode pour prouver $\forall x : T.(P x)$ consiste à prouver $(P x)$ en ajoutant au contexte une variable que l'on ne peut pas instancier $x : T$ alors qu'une méthode pour prouver $\exists x : T.(P x)$ consiste à prouver $(P x)$ en ajoutant au contexte une variable que l'on peut instancier $x : T$.

La terminologie classique de l'unification oppose variable et constante, le mot "constante" étant déjà utilisé dans les systèmes de types à d'autres fins nous lui préférerons celui de variable universelle, opposé à variable existentielle.

Pour définir la notion de substitution, le premier problème qui se pose est celui des nouvelles variables existentielles qui apparaissent dans le terme substitué. Reprenons notre exemple ci-dessus. Dans le contexte $\Gamma$ on cherche une preuve de $C$, on introduit donc une variable existentielle de type $C$ :

$$ \Gamma[\exists p : C] $$

On veut substituer à $p$ le terme $(u x)$ où $x$ est une nouvelle variable existentielle, afin d'obtenir le contexte :

$$ \Gamma[\exists x : B] $$

La déclaration de $p$ a bien entendu disparu puisque cette variable a été instanciée, mais une nouvelle variable existentielle $x$ est apparue dans le contexte, les informations concernant cette variable doivent figurer dans la substitution, qui doit donc s'écrire $p \leftarrow [\exists x : B](u x)$. Ensuite, en appliquant les substitutions $x \leftarrow [\exists y : A](v y)$ puis $y \leftarrow []$,$w$, on obtient le contexte $\Gamma$ qui ne contient plus de variables existentielles. La composition de ces trois substitutions donne la substitution $p \leftarrow [], (u (v w))$ et donc la preuve $(u (v w))$ pour $C$.

## Contraintes

Lorsqu'on applique une substitution à une variable $x$, il faut que le terme substitué à $x$ ait le même type que la variable $x$. Considérons le contexte :

$$ \Gamma = [\forall A : \mathit{Prop}; \exists X : \mathit{Prop}; \exists y : X \to A] $$

a priori on ne peut pas substituer le terme $[x : X]x$ à la variable $y$ car le terme $[x : X]x$ est de type $X \to X$ et $y$ est de type $X \to A$.

Mais si on applique d'abord la substitution $X \leftarrow []$, $A$, la substitution $y \leftarrow []$, $[x : A]x$ devient autorisée. Pour appliquer la substitution $y \leftarrow []$, $[x : X]x$ il faut donc d'abord unifier le type de $y$ et
celui de $[x : X]x$ (c'est-à-dire rechercher les substitutions qui rendent ces deux termes identiques) pour ensuite appliquer la substitution $y \leftarrow []$, $[x : A]x$. Il faut donc passer par une étape d'unification avant chaque substitution. L'unification dans les systèmes de types n'est pas un problème simple, notre objectif dans ce chapitre est de permettre l'expression d'étapes de construction de preuves aussi élémentaires que possible, en aucun cas la résolution d'un problème d'unification ne peut être considéré comme une étape élémentaire. Nous allons donc autoriser la substitution $y \leftarrow []$, $[x : X]x$ mais en gardant dans le contexte la contrainte $X \to X = X \to A$ pour rappeler qu'en appliquant cette substitution, nous avons pris l'engagement de résoudre, d'une façon ou d'une autre, cette équation, même si nous ne voulons pas le faire immédiatement.

## 3.2 Contextes Quantifiés Contraints

**Définition 46. : Contextes Quantifiés Contraints**

Une déclaration quantifiée est un triplet $<Q, x, T>$ (noté $Qx : T$) où $Q$ est un quantificateur ($\forall$ ou $\exists$), $x$ une variable et $T$ un terme. Une contrainte est un couple de termes $<a, b>$ (noté $a = b$). Un contexte quantifié contraint est une liste $\Gamma = [e_1; ...; e_n]$ telle que $e_i$ est ou bien une déclaration quantifiée ou bien une contrainte. Ces contextes quantifiés contraints sont des généralisations des préfixes mixtes de Miller [51] qui sont des listes de déclarations quantifiées.

Les contextes non quantifiés et non contraints sont identifiés avec les contextes quantifiés contraints qui ne comportent que des variables universelles.

**Définition 47. : Equivalence Modulo Contraintes**

Soit $\Gamma$ un contexte quantifié contraint, on définit la relation entre termes $\equiv_\Gamma$ comme la plus petite relation d'équivalence compatible avec la structure des termes qui contiennent la $\beta\eta$-équivalence et les équations de $\Gamma$.

Elle est définie inductivement par :

- si $t \equiv t'$, alors $t \equiv_\Gamma t'$,

- si $(a = b) \in \Gamma$, alors $a \equiv_\Gamma b$,

- si $t \equiv_\Gamma t'$, alors $t' \equiv_\Gamma t$,

- si $t \equiv_\Gamma t'$ et $t' \equiv_\Gamma t''$, alors $t \equiv_\Gamma t''$,

- si $t \equiv_\Gamma t'$, alors $[x : u]t \equiv_\Gamma [x : u]t'$,

- si $t \equiv_\Gamma t'$, alors $[x : t]u \equiv_\Gamma [x : t']u$,

- si $t \equiv_\Gamma t'$, alors $(x : u)t \equiv_\Gamma (x : u)t'$,

- si $t \equiv_\Gamma t'$, alors $(x : t)u \equiv_\Gamma (x : t')u$,

- si $t \equiv_\Gamma t'$, alors $(t : u) \equiv_\Gamma (t' : u)$,

- si $t \equiv_\Gamma t'$, alors $(u : t) \equiv_\Gamma (u : t')$.

**Définition 48. : Règles de Typage**

D'abord on modifie les règles de typage pour tenir compte de la nouvelle syntaxe des contextes. On remplace la règle :

$$ \frac{\Gamma \vdash T : s}{\Gamma[x : T] \text{ bien formé}} s \in S $$

par :

$$ \frac{\Gamma \vdash T : s}{\Gamma[Qx : T] \text{ bien formé}} s \in S $$
On remplace de même la règle :

$$ \frac{\Gamma \text{ bien formé } x : T \in \Gamma}{\Gamma \vdash x : T} $$

par :

$$ \frac{\Gamma \text{ bien formé } Qx : T \in \Gamma}{\Gamma \vdash x : T} $$

Et on ajoute la règle :

$$ \frac{\Gamma \vdash a : T \quad \Gamma \vdash b : T}{\Gamma[a = b] \text{ bien formé}} $$

Ensuite on étend le système en remplaçant la règle :

$$ \frac{\Gamma \vdash T : s \quad \Gamma \vdash T' : s \quad \Gamma \vdash t : T \quad T \equiv T'}{\Gamma \vdash t : T'} s \in S $$

par :

$$ \frac{\Gamma \vdash T : s \quad \Gamma \vdash T' : s \quad \Gamma \vdash t : T \quad T \equiv_T T'}{\Gamma \vdash t : T'} s \in S $$

On définit ainsi deux nouveaux jugements : $\Gamma$ est bien formé en utilisant les contraintes et $t$ est de type $T$ dans $\Gamma$ en utilisant les contraintes.

**Remarque** : Un terme peut être bien typé en utilisant les contraintes sans être normalisable. Par exemple, dans le contexte $\Gamma = [\exists T : Prop; T = T \to T]$ le terme $([x : T](x x)[x : T](x x))$ est bien typé et n'est pas normalisable.

**Remarque** : Dans le $\lambda\Pi$-calcul, on ne considère jamais de variables existentielles de type. Elliott [20] [21] et Pym [58] ont montré en substance que tout terme bien typé dans le $\lambda\Pi$-calcul, dans un contexte quantifié contraint sans contraintes reliant deux termes rigides (voir ci-dessous) a une forme normale de tête. L'exemple ci-dessus montre que ce théorème ne se généralise pas aux systèmes polymorphes.

**Définition 49.** : Terme Bien Typé Sans Utiliser les Contraintes

Soit $\Gamma$ un contexte et $t$ et $T$ deux termes. Le terme $t$ est dit de type $T$ dans $\Gamma$ sans utiliser les contraintes s'il existe un sous-contexte $\Delta$ de $\Gamma$ (c'est-à-dire obtenu en effaçant certains éléments de $\Gamma$) tel que $\Delta$ ne comporte pas de contraintes, $\Delta$ soit bien formé et $\Delta \vdash t : T$.

**Proposition 26.** : Un terme bien typé sans utiliser les contraintes a une forme normale unique.

**Définition 50.** : Forme Normale d'un Contexte

Soit $\Gamma$ un contexte, la forme normale de $\Gamma$ est obtenue en mettant en forme $\beta$-normale $\eta$-longue tous les types des variables qui sont bien typés sans utiliser les contraintes et toutes les contraintes dont les termes sont bien typés sans utiliser les contraintes.

**Définition 51.** : Terme sans Variables Existentielles

Un terme $t$ est dit sans variables existentielles dans $\Gamma$ si aucune variable existentielle n'a d'occurrence dans ce terme.
**Définition 52.** : Terme Fermé

Un terme est dit fermé dans $\Gamma$ s'il est héréditairement sans variables existentielles c'est-à-dire si pour chaque variable $x$ de type $T$, libre dans ce terme, $x$ est universelle dans $\Gamma$ et $T$ est fermé dans le préfixe de $\Gamma$ déclaré à gauche de $x$. Il est dit ouvert sinon.

**Proposition 27.** : Si $\Gamma$ est un contexte bien formé, alors le contexte $\Gamma'$ obtenu en effaçant les contraintes reliant deux termes identiques est également bien formé et $\Gamma \vdash t : T$ si et seulement si $\Gamma' \vdash t : T$.

**Démonstration** : Par récurrence sur la longueur de la dérivation de $\Gamma$ bien formé ou $\Gamma \vdash t : T$.

**Définition 53.** : Contextes Equivalents

Deux contextes $\Gamma$ et $\Gamma'$ (bien formé ou non) sont dits équivalents si les contextes obtenus en effaçant dans $\Gamma$ et $\Gamma'$ les contraintes reliant des termes identiques sont identiques.

Par la suite, on identifiera les contextes équivalents.

**Définition 54.** : Termes Flexibles et Rigides

Soit $t$ un terme bien typé sans utiliser les contraintes dans un contexte $\Gamma$ et normal. Si $t$ est une abstraction, un produit ou un terme atomique ($w c_1 ... c_n$) où $w$ est une variable universelle, il est dit rigide. Si $t$ est atomique ($w c_1 ... c_n$) et $w$ est existentielle, il est dit flexible.

**Définition 55.** : Contexte de Succès et Contexte d'Echec

Un contexte normal $\Gamma$ est dit contexte de succès s'il ne comporte que des variables universelles et des contraintes reliant des termes identiques, il est dit contexte d'échec s'il comporte une contrainte reliant deux termes sans variables existentielles qui sont différents.

**Proposition 28.** : Soit $\Gamma$ un contexte normal qui n'est ni un contexte de succès ni un contexte d'échec. Il existe dans $\Gamma$ une variable existentielle $x : T$ dont le type $T$ est bien typé sans utiliser les contraintes et à la forme $(x_1 : P_1)...(x_n : P_n)P$ avec $P$ atomique rigide dans $\Gamma[\forall x_1 : P_1; ...; \forall x_n : P_n]$.

**Démonstration** : Considérons l'objet le plus à gauche de $\Gamma$ qui n'est ni une variable universelle ni une contrainte normale reliant deux termes identiques (un tel objet existe car le contexte n'est pas un contexte de succès). Cet objet n'est pas une contrainte. En effet, supposons le contraire, et posons $\Gamma = \Delta[a = b]\Delta'$. Les termes $a$ et $b$ sont bien typés dans $\Delta$, donc comme il n'y a pas de variables existentielles ni de contraintes autres que triviales dans $\Delta$, $a$ et $b$ sont sans variables existentielles et bien typés sans utiliser les contraintes dans $\Gamma$. Comme $a$ et $b$ ne sont pas identiques, $\Gamma$ est alors un contexte d'échec ce qui contredit l'hypothèse.

Cet objet est donc la déclaration d'une variable existentielle $\exists x : T$, le terme $T$ est bien typé sans utiliser les contraintes et sans variables existentielles.

## 3.3 Substitution

**Définition 56.** : Contexte Existentiel

Un contexte (bien formé ou non) est dit existentiel s'il ne contient que des déclarations de variables existentielles et des contraintes mais pas de déclarations de variables universelles.
**Définition 57.** : *Substitution*

Soit $\sigma$ un ensemble fini de triplets $<x, \gamma, t>$ où $x$ est une variable, $\gamma$ un contexte existentiel et $t$ un terme. L'ensemble $\sigma$ est appelé substitution si pour toute variable $x$, il y a au plus un triplet de la forme $<x, \gamma, t>$ dans $\sigma$.

Dans le cas où $\sigma$ est réduite à un seul triplet $<x, \gamma, t>$ on note $\sigma = x \leftarrow \gamma, t$, et $\sigma = x \leftarrow t$ quand $\gamma$ est le contexte vide.

**Définition 58.** : *Variable Liée par une Substitution*

Soit $x$ une variable et $\sigma$ une substitution. Si la substitution $\sigma$ contient un triplet $<x, \gamma, t>$, alors $x$ est dite liée par $\sigma$. Le contexte $\gamma$ est appelé le contexte associé à $x$ dans $\sigma$.

**Définition 59.** : *Substitution Appliquée à un Terme*

Soit $x$ une variable et $\sigma$ une substitution. S'il existe un triplet $<x, \gamma, t>$ dans $\sigma$, alors on pose $\sigma x = t$, sinon on pose $\sigma x = x$. Cette définition s'étend aux termes de manière directe par :

- $\sigma s = s$,

- $\sigma(t u) = (\sigma t \sigma u)$,

- $\sigma[x : T]u = [x : \sigma T]\sigma u$,

- $\sigma(x : T)u = (x : \sigma T)\sigma u$.

**Définition 60.** : *Application d'une Substitution à un Contexte*

On définit par récurrence sur la longueur de $\Gamma$ une relation de compatibilité $\sigma$ est bien typée dans $\Gamma$ et si $\sigma$ est bien typée dans $\Gamma$ un contexte bien formé $\sigma\Gamma$.

- Dans le cas où $\Gamma = []$, $\sigma$ est bien typée dans $\Gamma$ et $\sigma\Gamma = []$.

- Dans le cas où $\Gamma = \Delta[\forall x : T]$, si $\sigma$ est bien typée dans $\Delta$ et $\sigma\Delta[\forall x : \sigma T]$ est bien formé, alors $\sigma$ est bien typée dans $\Gamma$ et $\sigma\Gamma = \sigma\Delta[\forall x : \sigma T]$. Sinon $\sigma$ n'est pas bien typée dans $\Gamma$.

- Dans le cas où $\Gamma = \Delta[\exists x : T]$, si $x$ est liée par $\sigma$, alors il existe un triplet unique $<x, \gamma, t>$ dans $\sigma$, sinon on pose $t = x$ et $\gamma = [\exists x : \sigma T]$.

Si $\sigma$ est bien typée dans $\Delta$, $(\sigma\Delta)\gamma$ est bien formé et $(\sigma\Delta)\gamma \vdash t : \sigma T$, alors $\sigma$ est bien typée dans $\Gamma$ et $\sigma\Gamma = (\sigma\Delta)\gamma$. Sinon $\sigma$ n'est pas bien typée dans $\Gamma$.

- Dans le cas où $\Gamma = \Delta[a = b]$, si $\sigma$ est bien typée dans $\Delta$ et $(\sigma\Delta)[\sigma a = \sigma b]$ est bien formé, alors $\sigma$ est bien typée dans $\Gamma$ et $\sigma\Gamma = (\sigma\Delta)[\sigma a = \sigma b]$. Sinon $\sigma$ n'est pas bien typée dans $\Gamma$.

**Définition 61.** : *Substitution Equivalentes*

Deux substitutions $\sigma$ et $\sigma'$ sont dites équivalentes si les variables liées par ces substitutions sont les mêmes, et pour toute variable $x$ liée par ces substitutions $\sigma x = \sigma'x$ et les contextes $\gamma$ et $\gamma'$ associés à $x$ par $\sigma$ et $\sigma'$ sont équivalents.

Par la suite, on identifiera les substitutions équivalentes.

**Proposition 29.** : Si $\Delta\Delta'$ et $\Delta\gamma$ sont des contextes bien formés, alors $\Delta\gamma\Delta'$ aussi. De même si $\Delta\Delta' \vdash t : T$ et $\Delta\gamma$ est un contexte bien formé, alors $\Delta\gamma\Delta' \vdash t : T$.

**Démonstration** : Par récurrence sur la longueur de la dérivation de $\Delta\Delta'$ bien formé ou $\Delta\Delta' \vdash t : T$.

**Notation** : Soit $\Gamma = [e_1, ..., e_n]$ un contexte (bien formé ou non), $x$ une variable non déclarée dans $\Gamma$ et $t$ un terme, on note $\Gamma[x \leftarrow t]$ le contexte $[e_1[x \leftarrow t], ..., e_n[x \leftarrow t]]$ où on définit $(Qy : T)[x \leftarrow t]$ comme $Qy : T[x \leftarrow t]$ et $(a = b)[x \leftarrow t]$ comme $(a[x \leftarrow t] = b[x \leftarrow t])$.
**Proposition 30.** : Soit $\Gamma$ un contexte, $x$ une variable non déclarée dans $\Gamma$ et $T$, $T'$ et $u$ des termes tels que $T \equiv_{\Gamma} T'$, alors $T[x \leftarrow u] \equiv_{\Gamma[x \leftarrow u]} T'[x \leftarrow u]$.

**Démonstration** : Par récurrence sur la longueur de la dérivation de $T \equiv_{\Gamma} T'$.

**Proposition 31.** : Si $\Delta[Qx : U]\Delta' \vdash t : T$ et $\Delta \vdash u : U$, alors le contexte $\Delta(\Delta'[x \leftarrow u])$ est bien formé et $\Delta(\Delta'[x \leftarrow u]) \vdash t[x \leftarrow u] : T[x \leftarrow u]$.

**Démonstration** : Par récurrence sur la longueur de la dérivation de $\Delta[Qx : U]\Delta' \vdash t : T$.

**Proposition 32.** : Soit $\Gamma$ un contexte, $\sigma$ une substitution bien typée dans $\Gamma$, $t$ et $T$ deux termes tels que $\Gamma \vdash t : T$. On a $\sigma\Gamma \vdash \sigma t : \sigma T$.

**Démonstration** : Par récurrence sur le nombre de variables de $\Gamma$ liées par $\sigma$.

Si aucune des variables de $\Gamma$ n'est liée par $\sigma$ le résultat est immédiat.

Sinon soit $\exists x : P$ la variable existentielle liée par $\sigma$ la plus à droite de $\Gamma$.

On écrit $\Gamma = \Delta[\exists x : P][e_1; \dots; e_p]$.

Soit $\gamma$ le contexte associé à $x$ par $\sigma$. Soit $\tau = \sigma - \{<x, \gamma, \sigma x>\}$.

Comme $x$ est la variable liée par $\sigma$ la plus à droite de $\Gamma$, pour toute variable $y$ déclarée dans $\Gamma$ distincte de $x$, $x$ n'a pas d'occurrence dans $\tau y$ et donc $\sigma y = \tau y = \tau y[x \leftarrow \sigma x]$. Pour la variable $x$ on a $x = \tau x$ donc $\sigma x = \tau x[x \leftarrow \sigma x]$. On en déduit par récurrence sur la structure de $t$ que pour tout terme $t$ on a $\sigma t = (\tau t)[x \leftarrow \sigma x]$.

Par hypothèse de récurrence, pour tout contexte $\Xi$ tel que la substitution $\tau$ soit bien typée dans $\Xi$ et tous termes $u$ et $U$ tel que $\Xi \vdash u : U$, on a $\tau\Xi \vdash \tau u : \tau U$.

Par une récurrence simple sur la longueur de $\Delta$ on prouve que $\sigma$ et $\tau$ sont bien typées dans $\Gamma$ et :

$$ \tau\Gamma = (\tau\Delta)[\exists x : \tau P][\tau e_1; \dots; \tau e_p] = (\sigma\Delta)[\exists x : \tau P][\tau e_1; \dots; \tau e_p] $$

En utilisant la propriété de $\tau$ on a :

$$ \tau\Gamma \vdash \tau t : \tau T $$

c'est-à-dire :

$$ (\sigma\Delta)[\exists x : \tau P][\tau e_1; \dots; \tau e_p] \vdash \tau t : \tau T $$

Comme $\sigma$ est bien typée dans $\Gamma$ on a :

$$ (\sigma\Delta)\gamma \text{ bien formé} $$

D'après la proposition 29 :

$$ (\sigma\Delta)\gamma[\exists x : \tau P][\tau e_1; \dots; \tau e_p] \vdash \tau t : \tau T $$

Donc, en utilisant la proposition 31 :

$$ (\sigma\Delta)\gamma[(\tau e_1)[x \leftarrow \sigma x]; \dots; (\tau e_p)[x \leftarrow \sigma x]] \vdash (\tau t)[x \leftarrow \sigma x] : (\tau T)[x \leftarrow \sigma x] $$

c'est-à-dire :

$$ (\sigma\Delta)\gamma[\sigma e_1; \dots; \sigma e_p] \vdash \sigma t : \sigma T $$

soit :

$$ \sigma\Gamma \vdash \sigma t : \sigma T $$
**Définition 62.** : *Composition de Substitutions*

Soit un contexte $\Gamma$ et $\sigma$ et $\tau$ deux substitutions. On définit la substitution $\tau \circ \sigma$ comme :

$$ (\tau \circ \sigma) = \{ \langle x, \tau\gamma, \tau t \rangle \mid \langle x, \gamma, t \rangle \in \sigma \} \cup \{ \langle x, \gamma, t \rangle \mid \langle x, \gamma, t \rangle \in \tau \text{ et } x \text{ non liée par } \sigma \} $$

où $\tau\gamma$ est défini par récurrence par :

- si $\gamma = []$, alors $\tau\gamma = []$,

- si $\gamma = \gamma'[\exists y : U]$ alors $\tau\gamma = (\tau\gamma')\gamma''$ avec $\gamma''$ contexte associé à $y$ par $\tau$ si la variable $y$ est liée par cette substitution et $\gamma'' = [\exists y : \tau U]$ sinon,

- si $\gamma = \gamma'[a = b]$, alors $\tau\gamma = (\tau\gamma')[\tau a = \tau b]$.

**Proposition 33.** : *Soit $\sigma$ et $\tau$ deux substitutions et $t$ un terme, $(\tau \circ \sigma)t = \tau\sigma t$.*

**Démonstration** : Par récurrence sur la structure de $t$.

**Proposition 34.** : *Soit $\Gamma$ un contexte et $\sigma$ et $\tau$ deux substitutions, telles que $\sigma$ est bien typée dans $\Gamma$ et $\tau$ est bien typée dans $\sigma\Gamma$, alors $\tau \circ \sigma$ est bien typée dans $\Gamma$ et $(\tau \circ \sigma)\Gamma = \tau\sigma\Gamma$.*

**Démonstration** : Par récurrence sur la longueur de $\Gamma$.

- Si $\Gamma = \Delta[a = b]$, alors puisque $\sigma$ est bien typée dans $\Gamma$, $\sigma$ est bien typée dans $\Delta$, $(\sigma\Delta)[\sigma a = \sigma b]$ est bien formé et $\sigma\Gamma = (\sigma\Delta)[\sigma a = \sigma b]$.

Comme $\tau$ est bien typée dans $\sigma\Gamma$, $\tau$ est bien typée dans $\sigma\Delta$, $(\tau\sigma\Delta)[\tau\sigma a = \tau\sigma b]$ est bien formé et $\tau\sigma\Gamma = (\tau\sigma\Delta)[\tau\sigma a = \tau\sigma b] = (\tau\sigma\Delta)[(\tau \circ \sigma)a = (\tau \circ \sigma)b]$.

Par hypothèse de récurrence, $(\tau \circ \sigma)$ est bien typée dans $\Delta$ et $(\tau \circ \sigma)\Delta = \tau\sigma\Delta$, donc $((\tau \circ \sigma)\Delta)[(\tau \circ \sigma)a = (\tau \circ \sigma)b]$ est bien formé.

Donc $(\tau \circ \sigma)$ est bien typée dans $\Gamma$ et $(\tau \circ \sigma)\Gamma = ((\tau \circ \sigma)\Delta)[(\tau \circ \sigma)a = (\tau \circ \sigma)b] = \tau\sigma\Gamma$.

- Si $\Gamma = \Delta[\forall x : T]$, alors puisque $\sigma$ est bien typée dans $\Gamma$, $\sigma$ est bien typée dans $\Delta$, $(\sigma\Delta)[\forall x : \sigma T]$ est bien formé et $\sigma\Gamma = (\sigma\Delta)[\forall x : \sigma T]$.

Comme $\tau$ est bien typée dans $\sigma\Gamma$, $\tau$ est bien typée dans $\sigma\Delta$, $(\tau\sigma\Delta)[\forall x : \tau\sigma T]$ est bien formé et $\tau\sigma\Gamma = (\tau\sigma\Delta)[\forall x : \tau\sigma T] = (\tau\sigma\Delta)[\forall x : (\tau \circ \sigma)T]$.

Par hypothèse de récurrence, $(\tau \circ \sigma)$ est bien typée dans $\Delta$ et $(\tau \circ \sigma)\Delta = \tau\sigma\Delta$, donc $((\tau \circ \sigma)\Delta)[\forall x : (\tau \circ \sigma)T]$ est bien formé.

Donc $(\tau \circ \sigma)$ est bien typée dans $\Gamma$ et $(\tau \circ \sigma)\Gamma = ((\tau \circ \sigma)\Delta)[\forall x : (\tau \circ \sigma)T] = \tau\sigma\Gamma$.

- Si $\Gamma = \Delta[\exists x : T]$, alors soit $\gamma$ le contexte associé à $x$ par $\sigma$ si $x$ est liée par $\sigma$ et $\gamma = [\exists x : \sigma T]$ sinon. On écrit $\gamma = [e_1; \dots; e_n]$. Comme $\sigma$ est bien typée dans $\Gamma$, $\sigma$ est bien typée dans $\Delta$, $(\sigma\Delta)[e_1; \dots; e_n]$ est bien formé, $\sigma\Gamma = (\sigma\Delta)[e_1; \dots; e_n]$ et $\sigma\Gamma \vdash \sigma x : \sigma T$.

Si l'objet $e_i$ est la déclaration d'une variable existentielle $y : U$ liée par $\tau$, on pose $\gamma'_i$ le contexte associé par $\tau$ à $y$, si c'est la déclaration d'une variable existentielle $y : U$ qui n'est pas liée par $\tau$, on pose $\gamma'_i = [\exists y : \tau U]$ et si c'est la contrainte $(a = b)$ on pose $\gamma'_i = [(\tau a = \tau b)]$.

Comme $\tau$ est bien typée dans $\sigma\Gamma$, il est bien typé dans $\sigma\Delta$, $(\tau\sigma\Delta)\gamma'_1 \dots \gamma'_n = (\tau\sigma\Delta)(\tau\gamma)$ est bien formé et :

$$ \tau\sigma\Gamma = (\tau\sigma\Delta)\gamma'_1 \dots \gamma'_n = (\tau\sigma\Delta)(\tau\gamma) $$

Comme $\sigma\Gamma \vdash \sigma x : \sigma T$, on a $\tau\sigma\Gamma \vdash \tau\sigma x : \tau\sigma T$.

Enfin par hypothèse de récurrence $(\tau \circ \sigma)$ est bien typée dans $\Delta$ et $(\tau \circ \sigma)\Delta = \tau\sigma\Delta$. Donc $((\tau \circ \sigma)\Delta)(\tau\gamma)$ est bien formé, $\tau\sigma\Gamma = ((\tau \circ \sigma)\Delta)(\tau\gamma)$ et $((\tau \circ \sigma)\Delta)(\tau\gamma) \vdash (\tau \circ \sigma)x : (\tau \circ \sigma)T$.

Donc $(\tau \circ \sigma)$ est bien typée dans $\Gamma$ et $(\tau \circ \sigma)\Gamma = ((\tau \circ \sigma)\Delta)(\tau\gamma) = \tau\sigma\Gamma$.
# Chapitre 4

## Une Méthode Complète de Synthèse de Preuves

### 4.1 Approches

#### 4.1.1 Résolution et Unification

En logique du premier ordre ou d'ordre supérieur, on distingue deux catégories syntaxiques : les termes et les preuves. Les termes sont des arbres (en logique du premier ordre) ou des λ-termes simplement typés (en logique d'ordre supérieur) et les preuves sont des arbres construits avec les règles de déduction naturelle. Ces règles permettent de construire des preuves en combinant d'autres preuves et des termes. Par exemple la règle d'élimination de l'implication :

$$ \frac{\Gamma \vdash A \rightarrow B \quad \Gamma \vdash A}{\Gamma \vdash B} $$

permet de former une preuve (de B) en combinant deux preuves (l'une de $A \rightarrow B$ et l'autre de A). La règle d'élimination du quantificateur universel :

$$ \frac{\Gamma \vdash \forall x : A.B \quad \Gamma \vdash t : A}{\Gamma \vdash B[x \leftarrow t]} $$

permet de former une preuve (de $B[x \leftarrow t]$) en combinant une preuve (de $\forall x : A.B$) et un terme (de type A).

Les preuves sont donc des arbres hétérogènes. Dans les méthodes de démonstration automatique pour ces deux logiques [59] [37], les preuves sont synthétisées par l'algorithme de résolution. Quand au cours de la recherche d'une preuve, il est nécessaire de synthétiser un terme, on appelle un autre algorithme : l'algorithme d'unification. Dans les systèmes de types, termes et preuves appartiennent à une catégorie syntaxique unique. De ce fait notre méthode de synthèse de preuves est constituée d'un seul algorithme qui mêle résolution et unification.

Nous présentons maintenant les algorithmes d'unification et de résolution à l'ordre supérieur [37] [40] [41]. Nous cherchons à montrer qu'une même idée sur l'énumération des termes sous-tend ces deux algorithmes.
### 4.1.2 Unification à l'Ordre Supérieur

Soit $\Gamma$ un contexte et $a$ et $b$ deux termes, l'unification consiste à chercher s'il existe une substitution $\sigma$ bien typée dans $\Gamma$ telle que $\sigma a = \sigma b$.

La méthode d'unification à l'ordre supérieur [40] [41] est basée sur un algorithme énumérant tous les termes normaux en forme $\eta$-longue d'un type donné dans le $\lambda$-calcul simplement typé.

Soit un type $T_1 \rightarrow \dots \rightarrow T_n \rightarrow T$ (T atomique). Tous les termes normaux en forme $\eta$-longue de ce type commencent par $n$ abstractions :

$$t = [x_1 : T_1]...[x_n : T_n]t'$$

Le terme $t'$ a le type $T$, c'est donc un terme atomique. Une variable $w : U_1 \rightarrow \dots \rightarrow U_p \rightarrow U$ qui est une variable du contexte ou l'un des $x_i$ peut être tête de ce terme seulement si $U = T$. Dans ce cas, cette variable doit être appliquée à $p$ termes afin d'obtenir un terme du bon type. Donc :

$$t = [x_1 : T_1]...[x_n : T_n](w c_1 \dots c_p)$$

Pour marquer la dépendance des $c_i$ par rapport aux $x_j$ on écrit :

$$t = [x_1 : T_1]...[x_n : T_n](w (d_1 x_1 \dots x_n) \dots (d_p x_1 \dots x_n))$$

Enfin pour synthétiser les $d_i$ on utilise récursivement le même algorithme. On pose donc dans un premier temps :

$$t = [x_1 : T_1]...[x_n : T_n](w (h_1 x_1 \dots x_n) \dots (h_p x_1 \dots x_n))$$

puis on utilise récursivement le même algorithme pour instancier les $h_i : T_1 \rightarrow \dots \rightarrow T_n \rightarrow U_i$.

Dans l'algorithme d'unification, les équations entre un terme flexible et un terme rigide sont résolue en utilisant cette méthode pour instancier la variable de tête du terme flexible. Dans ce cas, le choix de la variable $w$ est très restreint par le terme rigide. Les équations entre termes rigides sont simplifiées et les équations entre termes flexibles ont une solution triviale.

La méthode d'énumération des termes sous-tendant l'algorithme d'unification à l'ordre supérieur peut donc être résumée ainsi :

* essayer toutes les variables de tête possibles pour la forme normale du terme,

* déclarer de nouvelles variables pour le reste du terme,

* engendrer une contrainte de type pour assurer le bon typage du terme,

* utiliser récursivement cette méthode pour instancier ces variables.

### 4.1.3 Résolution à l'Ordre Supérieur

Présentons maintenant la méthode de résolution à l'ordre supérieur [37]. Nous présentons en fait uniquement une restriction incomplète de cette méthode pour les clauses de Horn, c'est-à-dire les propositions de la forme $P_1 \rightarrow \dots \rightarrow P_n \rightarrow Q$ où $P_1, \dots, P_n$ et $Q$ sont des propositions atomiques (on considère que les variables libres dans ces propositions sont quantifiées universellement en tête de la clause).

Quand le but $B$ est atomique, on l'unifie avec la tête $Q$ d'une hypothèse $P_1 \rightarrow \dots \rightarrow P_n \rightarrow Q$, on engendre les buts dérivés $\sigma P_1, \dots, \sigma P_n$ et on cherche récursivement à prouver ces propositions.
Quand le but est aussi une clause de Horn $A_1 \rightarrow \dots \rightarrow A_n \rightarrow B$, la mise en forme clausale de la négation de cette proposition introduit les hypothèses $A_1, \dots, A_n$ et le but atomique $B$.

Cette restriction est appelée la méthode d'introduction-résolution. Elle peut être présentée par deux règles : la règle de résolution entre un but atomique et une hypothèse est appelée résolution et celle qui permet pour prouver $A \rightarrow B$ de prouver $B$ après avoir introduit l'hypothèse $A$ est appelée introduction. Cette méthode est incomplète. Dans [37] une autre règle (la règle de scission (splitting)) est ajoutée afin d'obtenir une méthode complète.

Remarquons enfin que cette méthode peut aussi être utilisée pour les clauses de Horn héréditaires c'est-à-dire des propositions de la forme $P_1 \rightarrow \dots \rightarrow P_n \rightarrow Q$, où $Q$ est une proposition atomique et $P_1, \dots, P_n$ des clauses de Horn héréditaires.

### 4.1.4 Introduction-Résolution dans les Systèmes de Types

Dans un système de types, toutes les propositions peuvent être considérées comme des clauses de Horn héréditaires où l'implication est généralisée en un produit. On peut donc appliquer la méthode précédente.

Par ailleurs, dans un système de types, la preuve d'une proposition $P$ est un terme $t$ de type $P$, une méthode de synthèse de preuves ne doit donc pas se contenter d'affirmer que la proposition considérée est prouvable, mais aussi exhiber un terme-preuve de cette proposition.

L'algorithme d'introduction-résolution peut être ainsi présenté :

* **Introduction** : Pour trouver une preuve de la proposition $(x : A)B$ dans un contexte $\Gamma$, trouver une preuve de $B$ dans le contexte $\Gamma[x : A]$.

Quand on a une preuve $b$ de $B$, le terme $[x : A]b$ est une preuve de $(x : A)B$ dans $\Gamma$.

* **Résolution** : Pour trouver une preuve de $B$ dans un contexte $\Gamma$ dans lequel il y a une proposition :

$$f : (x_1 : P_1) \dots (x_n : P_n) Q$$

unifier $B$ et $Q$ (considérer $x_1, \dots, x_n$ comme des variables existentielles dans $Q$), puis pour les $x_i$ qui n'ont pas été instanciées par l'unification, démontrer $\sigma P_i$.

Pour chaque $i$, on obtient (par unification ou comme preuve d'un but dérivé) un terme $c_i$ de type $P_i[x_1 \leftarrow c_1, \dots, x_{i-1} \leftarrow c_{i-1}]$, le terme $(f c_1 \dots c_n)$ est alors une preuve de $B$.

Cette méthode est décrite en détail dans [35]. Donnons un exemple. On a une hypothèse :

$$f : (x : T)(y : T)(z : T)(u : (R x y))(v : (R y z))(R x z)$$

et on veut prouver $(R a c)$. Pour cela on unifie $(R x z)$ et $(R a c)$, ce qui donne la substitution $x \leftarrow a, z \leftarrow c$. Ensuite, on construit récursivement des termes $b : T, t : (R a b)$ et $t' : (R b c)$. On obtient le terme $(f a b c t t')$ qui est une preuve de $(R a c)$.

Cette méthode est en général incomplète. Un autre défaut est qu'il n'y a pas d'algorithme général d'unification connu pour les systèmes de types. Des algorithmes sont uniquement connus pour le $\lambda$-calcul simplement typé [40] [41] et pour le $\lambda\Pi$-calcul [20] [21] [58].

Une présentation alternative de cette méthode est la suivante :

* **Introduction** : On donne le terme $[x : A]h$ comme preuve du but initial, la variable $h$ représente le but dérivé à prouver.

* **Résolution** : On donne le terme $(f h_1 \dots h_p)$ comme preuve du but initial et l'équation $Q[x_1 \leftarrow h_1, \dots, x_p \leftarrow h_p] = B$ (dans notre exemple $(R h_1 h_3) = (R a b)$) garantit que ce terme a le type $B$.
La résolution de cette équation va instancier certaines variables (ici $h_1$ et $h_3$), les autres variables (ici $h_2$, $h_4$ et $h_5$) représentent les buts dérivés à prouver.

Quand pour prouver une proposition on applique d'abord la règle d'introduction $n$ fois, puis la règle de résolution, on obtient la preuve : $[x_1 : A_1]...[x_n : A_n](f h_1 ... h_p)$. La variable $f$ apparaît comme variable de tête de cette preuve. Remarquons que la dépendance des $h_i$ par rapport aux $x_j$ est implicite.

La méthode d'énumération des termes qui sous-tend la méthode d'introduction-résolution est
donc :

* essayer toutes les variables de tête possibles pour la forme normale du terme,

• déclarer de nouvelles variables pour le reste du terme,

• engendrer une contrainte de type pour assurer le bon typage du terme,

• utiliser récursivement cette méthode pour instancier ces variables.

C'est donc essentiellement la même méthode que celle qui sous-tend l'algorithme d'unification.

4.1.5 Une Méthode d'Enumeration des Termes d'un Type Donné

Nous allons maintenant utiliser cette méthode pour construire un algorithme de synthèse de
preuves dans les systèmes de types.

Pour énumérer les termes $t$ qui peuvent être substitués à une variable $x$ de type $T$ on imagine
la forme normale de $t$ :

$$
t = [x_1 : P_1]...[x_n : P_n](w c_1 ... c_p)
$$

ou :

$$
t = [x_1 : P_1]...[x_n : P_n](z : A)B
$$

et on considère les substitutions élémentaires :

$$
x \leftarrow [x_1 : P_1]...[x_n : P_n](w (h_1 x_1 ... x_n) ... (h_p x_1 ... x_n))
$$

$$
x \leftarrow [x_1 : P_1]...[x_n : P_n](z : (h_1 x_1 ... x_n))(h_2 x_1 ... x_n z)
$$

Ensuite, on énumère tous les termes qui peuvent être substitués aux variables $h_1, ..., h_p$.

Comme on considère des termes normaux en forme $\eta$-longue, le nombre d'abstraction $n$ est
le même que celui de produits dans le type $T$ et les types $P_1, ..., P_n$ des variables liées dans ces
abstractions sont ceux des variables liées dans ces produits.

Par complétude, on doit considérer :

— toutes les variables de tête $w$ possibles,

— tous les entiers $p$ possibles et tous les types possibles pour $h_1, ..., h_p$.

Dans une telle substitution le terme substitué à $x$ doit avoir le même type que cette variable. Cette contrainte est une équation. Dans la méthode d'introduction-résolution, la résolution de cette équation est appelée l'étape d'unification de la résolution. Dans la méthode d'unification dans le $\lambda$-calcul simplement typé, les types sont toujours des termes sans variables existentielles, il est donc juste nécessaire de vérifier que ces deux termes sont égaux, c'est la phase de sélection des variables de tête. Dans l'algorithme d'unification dans le $\lambda\Pi$-calcul [20] [21] [58] cette contrainte est ajoutée à l'ensemble d'équations, c'est l'équation de garantie (accounting equation).

Dans notre algorithme, ces équations sont gardées dans le contexte. Elles forment des contraintes
que les substitutions à venir devront vérifier. Puisque nous n'avons pas d'algorithme spécial pour
résoudre ces équations et puisque les variables apparaissant dans ces équations sont instanciées par
l'algorithme ordinaire, notre méthode est constituée d'un seul algorithme qui mêle résolution et unification.

### 4.1.6 Nombre d'Applications

Dans la méthode d'introduction-résolution, quand on veut prouver une proposition atomique $T$ et qu'on utilise la règle de résolution avec une hypothèse $w : (y_1 : Q_1)...(y_q : Q_q)Q$ (Q atomique) on ne considère que les preuves de la forme $(w h_1 ... h_q)$ et la contrainte est que le type de ce terme doit être égal à $T$, c'est-à-dire $Q[y_1 \leftarrow h_1, ..., y_p \leftarrow h_p] = T$. Mais dans les systèmes de types polymorphes, le type du terme $(w c_1 ... c_q)$ peut encore être un produit, et on doit considérer des substitutions $(w h_1 ... h_p)$ avec $p$ strictement supérieur à $q$. C'est pour cette raison que la méthode d'introduction-résolution est incomplète et qu'une règle de scission est nécessaire dans [37].

Ici nous considérons une infinité de possibilités pour ce nombre d'applications, et donc un arbre infiniment branchant. Dans une méthode incomplète mais plus efficace, nous considérerons une restriction similaire à celle de la méthode introduction-résolution.

### 4.1.7 Variables dans la Proposition à Prouver

Dans certains systèmes, les variables $h_i$ peuvent avoir des occurrences dans le type de $h_j$ pour $j > i$. On pourrait instancier d'abord la variable $h_i$ puis n'instancier $h_j$ que quand son type est sans variables existentielles, mais il est plus efficace de commencer par $h_j$ quand cela est possible.

Par exemple, pour énumérer les termes de type $T = \exists x : Nat.(P x)$, il ne faut pas énumérer tous les termes $n$ de type $Nat$ puis énumérer les termes de type $(P n)$, mais au contraire, commencer par énumérer les termes de type $(P x)$.

De ce fait dans les systèmes de types polymorphes, quand une proposition à prouver $P$ comporte une variable, il n'est pas toujours possible de connaître le nombre d'abstractions dans une preuve $t$ de cette proposition, car une substitution peut augmenter le nombre de produits dans $P$ et donc le nombre d'abstractions dans $t$. Dans ce cas, il faut retarder l'instanciation de $x : T$ jusqu'à ce que $T$ ait été instancié en un terme $(x_1 : P_1)...(x_n : P_n)P$ où la variable de tête de $P$ n'est pas une variable existentielle.

## 4.2 Une Méthode Complète

**Définition 63. : Substitutions Elémentaires**

Soit $\Gamma$ un contexte bien formé dans le système de types Méta et normal tel que le type de toutes les variables universelles soit Prop ou Type mais pas Extern et qui n'est ni un contexte de succès ni un contexte d'échec. On définit un ensemble de substitutions $\Sigma(\Gamma)$.

On choisit parmi celles de $\Gamma$, une variable existentielle $x$ dont le type est normal et de la forme $(x_1 : P_1)...(x_n : P_n)P$ avec $P$ atomique rigide dans $\Gamma[\forall x_1 : P_1; ...; \forall x_n : P_n]$ (une telle variable existe parce que $\Gamma$ n'est ni un contexte de succès ni un contexte d'échec).

**Notation :** Quand $t$ est un terme, $(\vec{x} : \vec{P})t$ est une abréviation pour $(x_1 : P_1)...(x_n : P_n)t$.

— Pour toute variable universelle $w$ déclarée à gauche de $x$ dans $\Gamma$ ou qui est l'un des $x_i$ :

$$ \Gamma[\forall x_1 : P_1; \dots; \forall x_n : P_n] \vdash w : (y_1 : Q'_1) \dots (y_q : Q'_q) Q' (Q' \text{ atomique}) $$
On pose :

$$
\begin{align*}
Q_1 &= Q'_1 \\
Q_2 &= [y_1 : Q'_1]Q'_2 \\
\vdots \\
Q_q &= [y_1 : Q'_1] \dots [y_{q-1} : Q'_{q-1}] Q'_q \\
Q &= [y_1 : Q'_1] \dots [y_q : Q'_q] Q'
\end{align*}
$$

$$
w : (y_1 : Q_1)(y_2 : (Q_2 y_1))\dots(y_q : (Q_q y_1 \dots y_{q-1}))(Q y_1 \dots y_q)
$$

Pour tout $r \ge 0$ on considère les substitutions de degré de scission $r$ :

Soit s la sorte type de $Q'$ et s' la sorte type de $P$, dans $\Gamma[\forall x_1 : P_1; \dots; \forall x_n : P_n]$.

Pour tout $s_1, s'_1, \dots, s_i, s'_i, \dots, s_r, s'_r$ tel que $< s_1, s'_1, s > \in R$, $\dots, < s_i, s'_i, s'_{i-1} > \in R$ et $s'_r = s'$,
on pose le contexte existentiel $\gamma$ :

$$
\gamma = \varphi \chi_1 \dots \chi_r \psi
$$

où :

$$
\begin{align*}
\varphi &= [\exists h_1 : (\vec{x} : \vec{P}) Q_1; \\
&\quad \exists h_2 : (\vec{x} : \vec{P}) (Q_2 (h_1 x_1 \dots x_n)); \\
&\quad \dots; \\
&\quad \exists h_q : (\vec{x} : \vec{P}) (Q_q (h_1 x_1 \dots x_n) \dots (h_{q-1} x_1 \dots x_n))] \\
\chi_1 &= [\exists H_1 : (\vec{x} : \vec{P}) s_1; \\
&\quad \exists K_1 : (\vec{x} : \vec{P}) (z : (H_1 x_1 \dots x_n)) s'_1; \\
(\vec{x} : \vec{P}) (Q (h_1 x_1 \dots x_n) \dots (h_q x_1 \dots x_n)) &= (\vec{x} : \vec{P}) (z : (H_1 x_1 \dots x_n)) (K_1 x_1 \dots x_n z); \\
\exists h_{q+1} : (\vec{x} : \vec{P}) (H_1 x_1 \dots x_n)]
\end{align*}
$$

et pour tout $i$, $1 < i \le r$ :

$$
\begin{align*}
\chi_i &= [\exists H_i : (\vec{x} : \vec{P}) s_i; \\
&\quad \exists K_i : (\vec{x} : \vec{P}) (z : (H_i x_1 \dots x_n)) s'_i; \\
(\vec{x} : \vec{P}) (K_{i-1} x_1 \dots x_n (h_{q+i-1} x_1 \dots x_n)) &= (\vec{x} : \vec{P}) (z : (H_i x_1 \dots x_n)) (K_i x_1 \dots x_n z); \\
\exists h_{q+i} : (\vec{x} : \vec{P}) (H_i x_1 \dots x_n]
\end{align*}
$$

enfin, si $r=0$ :

$$
\psi = [(\vec{x} : \vec{P})(Q(h_1 x_1 \dots x_n) \dots (h_q x_1 \dots x_n)) = (\vec{x} : \vec{P})P]
$$

et dans les autres cas :

$$
\psi = [(\vec{x} : \vec{P})(K_r x_1 \dots x_n (h_{q+r} x_1 \dots x_n)) = (\vec{x} : \vec{P})P]
$$

L'ensemble $\Sigma(\Gamma)$ est l'ensemble des substitutions qui associent à $x$ le contexte $\gamma$ et le terme :

$$
[x_1 : P_1] \dots [x_n : P_n] (w (h_1 x_1 \dots x_n) \dots (h_{q+r} x_1 \dots x_n))
$$
— Si P est une sorte, alors :

pour toute sorte s, telle que <s, P>∈ Ax, on ajoute à Σ(Γ) la substitution qui associe à la variable x le contexte vide [] et le terme :

$$[x_1 : P_1]...[x_n : P_n]s$$

et pour toutes sortes s, s' telles que <s, s', P>∈ R on pose :

$$\gamma = [\exists h : (\vec{x} : \vec{P})s ; \exists k : (\vec{x} : \vec{P})(y : (h x_1 ... x_n))s']$$

on ajoute à Σ(Γ) la substitution qui associe à la variable x le contexte γ et le terme :

$$[x_1 : P_1]...[x_n : P_n](y : (h x_1 ... x_n))(k x_1 ... x_n y)$$

## Définition 64. : Dérivation

Une dérivation d'un contexte Γ est une liste de contextes [Γ₁; ... ; Γₘ] telle que Γ₁ = Γ, Γₘ est un contexte de succès et Γᵢ₊₁ = σᵢΓᵢ avec σᵢ ∈ Σ(Γᵢ).

## Définition 65. : Arbre de Recherche

Soit un contexte Γ, on définit l'arbre de recherche de Γ. Les nœuds de cet arbre sont des contextes, la racine de l'arbre est le contexte Γ et les fils d'un nœud Δ sont tous les contextes σΔ pour σ ∈ Σ(Δ). Les contextes de succès et d'échec sont les feuilles de cet arbre. Les nœuds de succès sont en bijection avec les dérivations de Γ. Un semi-algorithme de synthèse de preuves consiste à énumérer les nœuds de cet arbre jusqu'à trouver un nœud de succès. Comme le nombre de fils d'un nœud de cet arbre peut être infini, pour énumérer tous ses nœuds il faut retarder l'exploration des nœuds de degré de scission r de r générations.

## Explication Informelle :

Dans les solutions de degré de scission nul, les q premiers éléments de γ (φ) sont les déclarations des nouvelles variables h₁, ..., hq apparaissant dans le terme substitué à x et le dernier (ψ) est une contrainte exprimant que cette substitution est bien typée.

Dans les solutions de degré de scission r (r ≥ 1), on déclare d'abord les variables h₁, ..., hq (φ) puis il faut que le type (Q (h₁ x₁ ... xₙ) ... (hq x₁ ... xₙ)) du terme (w (h₁ x₁ ... xₙ) ... (hq x₁ ... xₙ)) soit un produit (z : (H₁ x₁ ... xₙ))(K₁ x₁ ... xₙ z). On déclare pour cela (χ₁) deux variables existentielles H₁ et K₁ ainsi qu'une contrainte :

$$(\vec{x} : \vec{P})(Q (h_1 x_1 ... x_n) ... (h_q x_1 ... x_n)) = (\vec{x} : \vec{P})(z : (H_1 x_1 ... x_n))(K_1 x_1 ... x_n z)$$

Ensuite on peut déclarer la variable hq₊₁ avec le type $(\vec{x} : \vec{P})(H_1 x_1 ... x_n)$.

Le type de (w (h₁ x₁ ... xₙ) ... (hq₊₁ x₁ ... xₙ)) est alors (K₁ x₁ ... xₙ (hq₊₁ x₁ ... xₙ)). Si r = 1 on a juste besoin d'une dernière contrainte (ψ) pour assurer que la substitution est bien typée :

$$(\vec{x} : \vec{P})(K_1 x_1 ... x_n (h_{q+1} x_1 ... x_n)) = (\vec{x} : \vec{P})P$$

Dans le cas général on déclare ainsi quatre éléments par degré de scission et ensuite la contrainte (ψ) pour assurer que la substitution est bien typée.

Les autres substitutions sont celles où la variable x est instanciée par un terme de la forme $[x_1 : P_1]...[x_n : P_n]u$ où u est une sorte ou un produit.
**Remarque** : Quand on a un contexte qui contient plusieurs variables existentielles, on peut choisir la variable que l'on instancie en premier. Le choix de cette variable est déterminant pour des questions d'efficacité. Des heuristiques seront développées par la suite. Néanmoins, le choix de la variable est limité par le fait que la variable à instancier doit avoir un type bien typé sans utiliser les contraintes et de tête rigide. Cette condition impose donc une séquentialisation partielle de la résolution.

## 4.3 Exemples

### 4.3.1 Un Exemple au Premier Ordre

Soit $\Delta = [\forall T : Prop; \forall R : T \to T \to Prop; \forall Eq : T \to T \to Prop; \forall Antisym : (x : T)(y : T)((R x y) \to (R y x) \to (Eq x y)); \forall a : T; \forall b : T; \forall u : (R a b); \forall v : (R b a)]$ et $\Gamma = \Delta[\exists x : (Eq a b)]$.

On substitue à $x$ le terme qui a pour tête *Antisym* et un degré de scission nul :

$$x \leftarrow (\text{Antisym } h_1 h_2 h_3 h_4)$$

On obtient le contexte :

$$\Delta[\exists h_1 : T; \exists h_2 : T; \exists h_3 : (R h_1 h_2); \exists h_4 : (R h_2 h_1); (Eq h_1 h_2) = (Eq a b)]$$

On substitue à $h_1$ le terme qui a pour tête $a$ et un degré de scission nul :

$$h_1 \leftarrow a$$

et à $h_2$ le terme qui a pour tête $b$ et un degré de scission nul :

$$h_2 \leftarrow b$$

On obtient le contexte $\Delta[\exists h_3 : (R a b); \exists h_4 : (R b a)]$.

(Les contraintes reliant des termes identiques sont omises.)

On substitue à $h_3$ le terme qui a pour tête $u$ et un degré de scission nul :

$$h_3 \leftarrow u$$

On obtient le contexte $\Delta[\exists h_4 : (R b a)]$.

On substitue à $h_4$ le terme qui a pour tête $v$ et un degré de scission nul :

$$h_4 \leftarrow v$$

Et on obtient le contexte de succès $\Delta$.

Soit $\theta$ la composition de ces substitutions, $\theta x = (\text{Antisym } a b u v)$.

Comme nous le verrons par la suite, dans cet exemple, à chaque étape, toutes les substitutions sauf celle considérée mènent de façon évidente à des contextes voués à l'échec.

### 4.3.2 Un Exemple avec Scission

Soit :
$$ \Delta = [\forall A : Prop; \forall B : Prop; \forall I : Prop \to Prop; \forall u : (P : Prop)((I P) \to P); \forall v : (I(A \to B)); \forall w : A] $$
et $\Gamma = \Delta[\exists p : B]$.

On substitue à $p$ le terme qui a pour tête $u$ et 1 pour degré de scission :

$$p \leftarrow (u h_1 h_2 h_3)$$

avec les nouvelles variables : $h_1 : \mathit{Prop}$, $h_2 : (I h_1)$, $H : \mathit{Prop}$, $K : H \to \mathit{Prop}$ et $h_3 : H$.

On obtient le contexte :

$$\Delta[\exists h_1 : \mathit{Prop}; \exists h_2 : (I h_1); \exists H : \mathit{Prop}; \exists K : H \to \mathit{Prop}; \exists h_3 : H; h_1 = (x : H)(K x); (K h_3) = B].$$

On substitue à $h_1$ un produit :

$$h_1 \leftarrow (x : h')(k' x)$$

On obtient le contexte :

$$\Delta[\exists h' : \mathit{Prop}; \exists k' : h' \to \mathit{Prop}; \exists h_2 : (I (x : h')(k' x)); \exists H : \mathit{Prop}; \exists K : H \to \mathit{Prop}; \exists h_3 : H; \\ (x : H)(K x) = (x : h')(k' x); (K h_3) = B].$$

On substitue à $h_2$ le terme qui a pour tête $v$ et un degré de scission nul :

$$h_2 \leftarrow v$$

On obtient le contexte :

$$\Delta[\exists h' : \mathit{Prop}; \exists k' : h' \to \mathit{Prop}; (I (x : h')(k' x)) = (I (A \to B)); \exists H : \mathit{Prop}; \exists K : H \to \mathit{Prop}; \\ \exists h_3 : H; (x : H)(K x) = (x : h')(k' x); (K h_3) = B].$$

On substitue à $h'$ le terme qui a pour tête $A$ et un degré de scission nul :

$$h' \leftarrow A$$

$$\Delta[\exists k' : A \to \mathit{Prop}; (I (x : A)(k' x)) = (I (A \to B)); \exists H : \mathit{Prop}; \exists K : H \to \mathit{Prop}; \exists h_3 : H; \\ (x : H)(K x) = (x : A)(k' x); (K h_3) = B].$$

On substitue à $k'$ le terme qui a pour tête $B$ et un degré de scission nul :

$$k' \leftarrow [x : A]B$$

On obtient le contexte :

$$\Delta[\exists H : \mathit{Prop}; \exists K : H \to \mathit{Prop}; \exists h_3 : H; (x : H)(K x) = (A \to B); (K h_3) = B].$$

On substitue à $H$ le terme qui a pour tête $A$ et un degré de scission nul :

$$H \leftarrow A$$

On obtient le contexte :

$$\Delta[\exists K : A \to \mathit{Prop}; \exists h_3 : A; (x : A)(K x) = (A \to B); (K h_3) = B].$$

On substitue à $K$ le terme qui a pour tête $B$ et un degré de scission nul :

$$K \leftarrow [x : A]B$$

On obtient le contexte :

$$\Delta[\exists h_3 : A]$$

On substitue à $h_3$ le terme qui a pour tête $w$ et un degré de scission nul :

$$h_3 \leftarrow w$$

Et on obtient le contexte de succès $\Delta$.

Soit $\theta$ la composition de ces substitutions, $\theta p = (u (A \to B) v w)$.
## 4.4 Propriétés

### 4.4.1 Typage

Soit $\Gamma$ un contexte et $x$ une variable existentielle de $\Gamma$. Ecrivons $\Gamma = \Delta[\exists x : T]\Delta'$. Soit $\sigma \in \Sigma(\Gamma)$, $\sigma = x \leftarrow \gamma, t$. Nous montrons à présent que $\sigma$ est bien typé dans $\Gamma$. Pour cela nous procédons en deux étapes : d'abord nous montrons que $\Delta\gamma$ est bien formé, c'est-à-dire que les types des nouvelles variables existentielles et les nouvelles contraintes sont bien typés, ensuite nous montrons que dans $\Delta\gamma$, le terme $t$ est bien typé et a même type que $x$.

**Proposition 35.** : Les types des nouvelles variables existentielles et les nouvelles contraintes sont bien typés dans le système de types Méta.

**Démonstration** : Comme $(x_1 : P_1)...(x_n : P_n)P$ est bien typé dans le système de types Méta, les termes $P_i$ sont bien typés dans le système de types Méta du type Prop ou Type (mais pas Extern).

Le terme $(y_1 : Q'_1)...(y_q : Q'_q)Q'$ est ou bien le type d'une variable universelle ou bien l'un des $P_i$. C'est donc un terme de type Prop ou Type mais pas Extern. Le type des $Q'_i$ et de $Q'$ est donc Prop ou Type mais pas Extern. Les termes $Q_i$ et $Q$ sont donc bien typés dans le système de types Méta.

Les termes $(H_i x_1 ... x_n)$ et $(h x_1 ... x_n)$ sont bien typés dans le système de types Méta et ont le type $s$ avec $<s, s', s''> \in R$ pour des sortes $s'$ et $s''$. Donc $s$ est égal à Prop ou Type mais pas Extern.

Les termes $(Q_i (h_1 x_1 ... x_n) ... (h_{i-1} x_1 ... x_n))$, $s_i$, $s'_i$, $(H_i x_1 ... x_n)$, $(K_i x_1 ... x_n z)$, $(K_i x_1 ... x_n (h_i x_1 ... x_n))$, $P$, $s$, $s'$, $(h x_1 ... x_n)$ et $(k x_1 ... x_n y)$ sont bien typés dans le système de types Méta et ont le type Prop, Type ou Extern.

Donc le type des variables existentielles et les contraintes sont bien typés dans le système de types Méta.

**Proposition 36.** : Le terme $t$ est bien typé dans $\Delta\gamma$ et a le même type que $x$ dans le système Méta.

**Démonstration** : Pour les substitutions de degré de scission nul, on a :

$$[x_1 : P_1]...[x_n : P_n](w (h_1 x_1 ... x_n) ... (h_q x_1 ... x_n)) : (\vec{x} : \vec{P})(Q (h_1 x_1 ... x_n) ... (h_q x_1 ... x_n))$$

donc en utilisant la contrainte $\psi$ :

$$[x_1 : P_1]...[x_n : P_n](w (h_1 x_1 ... x_n) ... (h_q x_1 ... x_n)) : (\vec{x} : \vec{P})P$$

Pour les substitutions de degré de scission $r$ ($r \ge 1$), on prouve par récurrence sur $i$ que pour tout $i$, $i \ge 1$, on a dans le contexte $\Delta\gamma$ :

$$[x_1 : P_1]...[x_n : P_n](w (h_1 x_1 ... x_n) ... (h_{q+i} x_1 ... x_n)) : (\vec{x} : \vec{P})(K_i x_1 ... x_n (h_{q+i} x_1 ... x_n))$$

Pour $i = 1$ on a :

$$[x_1 : P_1]...[x_n : P_n](w (h_1 x_1 ... x_n) ... (h_q x_1 ... x_n)) : (\vec{x} : \vec{P})(Q (h_1 x_1 ... x_n) ... (h_q x_1 ... x_n))$$

donc en utilisant la contrainte de $\chi_1$ :

$$[x_1 : P_1]...[x_n : P_n](w (h_1 x_1 ... x_n) ... (h_q x_1 ... x_n)) : (\vec{x} : \vec{P})(z : (H_1 x_1 ... x_n))(K_1 x_1 ... x_n z)$$
dans le contexte $\Delta\gamma[\forall x_1 : P_1; \dots; \forall x_n : P_n]$ on a :

$$ (w (h_1 x_1 \dots x_n) \dots (h_q x_1 \dots x_n)) : (z : (H_1 x_1 \dots x_n))(K_1 x_1 \dots x_n z) $$

et comme :

$$ h_{q+1} : (\vec{x} : \vec{P})(H_1 x_1 \dots x_n) $$

on déduit :

$$ (w (h_1 x_1 \dots x_n) \dots (h_{q+1} x_1 \dots x_n)) : (K_1 x_1 \dots x_n (h_{q+1} x_1 \dots x_n)) $$

donc dans le contexte $\Delta\gamma$ :

$$ [x_1 : P_1]...[x_n : P_n](w (h_1 x_1 \dots x_n) \dots (h_{q+1} x_1 \dots x_n)) : (\vec{x} : \vec{P})(K_1 x_1 \dots x_n (h_{q+1} x_1 \dots x_n)) $$

Puis, si on suppose cette proposition vérifiée pour $i$ :

$$ [x_1 : P_1]...[x_n : P_n](w (h_1 x_1 \dots x_n) \dots (h_{q+i} x_1 \dots x_n)) : (\vec{x} : \vec{P})(K_i x_1 \dots x_n (h_{q+i} x_1 \dots x_n)) $$

En utilisant la contrainte de $\chi_i$ :

$$ [x_1 : P_1]...[x_n : P_n](w (h_1 x_1 \dots x_n) \dots (h_{q+i} x_1 \dots x_n)) : (\vec{x} : \vec{P})(z : (H_{i+1} x_1 \dots x_n))(K_{i+1} x_1 \dots x_n z) $$

on a donc, dans le contexte $\Delta\gamma[\forall x_1 : P_1; \dots; \forall x_n : P_n]$ :

$$ (w (h_1 x_1 \dots x_n) \dots (h_{q+i} x_1 \dots x_n)) : (z : (H_{i+1} x_1 \dots x_n))(K_{i+1} x_1 \dots x_n z) $$

et comme :

$$ h_{q+i+1} : (\vec{x} : \vec{P})(H_{i+1} x_1 \dots x_n) $$

on en déduit :

$$ (w (h_1 x_1 \dots x_n) \dots (h_{q+i+1} x_1 \dots x_n)) : (K_{i+1} x_1 \dots x_n (h_{q+i+1} x_1 \dots x_n)) $$

donc dans le contexte $\Delta\gamma$ :

$$ [x_1 : P_1]...[x_n : P_n](w (h_1 x_1 \dots x_n) \dots (h_{q+i+1} x_1 \dots x_n)) : (\vec{x} : \vec{P})(K_{i+1} x_1 \dots x_n (h_{q+i+1} x_1 \dots x_n)) $$

Donc on déduit :

$$ [x_1 : P_1]...[x_n : P_n](w (h_1 x_1 \dots x_n) \dots (h_{q+r} x_1 \dots x_n)) : (\vec{x} : \vec{P})(K_r x_1 \dots x_n (h_{q+r} x_1 \dots x_n)) $$

et en utilisant la dernière contrainte $(\psi)$ :

$$ [x_1 : P_1]...[x_n : P_n](w (h_1 x_1 \dots x_n) \dots (h_{q+r} x_1 \dots x_n)) : (\vec{x} : \vec{P})P $$

Si $P$ est une sorte et $\sigma$ une substitution supplémentaire, $\sigma t$ est bien typé de façon évidente.

**Proposition 37.** : Soit $\Gamma$ un contexte et $\sigma$ une substitution, si $\sigma \in \Sigma(\Gamma)$, alors $\sigma$ est bien typée dans $\Gamma$.

**Démonstration** : Par récurrence sur la longueur de $\Gamma$ et en utilisant les deux propositions ci-dessus et la proposition de préservation des jugements de typage par application d'une substitution bien typée.
### 4.4.2 Correction

**Lemme 3.** : Soit un contexte $\Gamma$, s'il existe une dérivation $[\Gamma_1, ..., \Gamma_m]$ de $\Gamma$, alors il existe une substitution $\theta$ telle que $\theta\Gamma$ soit un contexte de succès. La substitution $\theta$ est appelée substitution dénotée par cette dérivation.

**Démonstration** : Soit $\theta = \sigma_{m-1} \circ \dots \circ \sigma_1$, $\theta\Gamma = \Gamma_m$ est un contexte de succès.

Prouvons maintenant que la substitution $\theta$ qui est bien typée dans le système *Méta* est aussi bien typée dans le système originel $\mathcal{T}$.

**Proposition 38.** : Soit un contexte $\Gamma$ bien formé dans le système de types $\mathcal{T}$ et $T$ un type bien typé dans $\Gamma$ dans le système de types $\mathcal{T}$.

Soit $t$ un terme tel que $\Gamma \vdash t : T$ dans le système de types *Méta* et tel que pour tout sous-terme de $t$ qui est un produit $(x : U)U'$, si on pose $s$ le type de $U$, $s'$ le type de $U'$ et $s''$ le type de $(x : U)U'$, on a $<s, s', s''> \in R$ (l'ensemble de règles du système $\mathcal{T}$) et que pour tout sous-terme de $t$ qui est une sorte $s$, on a $s = \text{Prop}$ (et non Type). On a $\Gamma \vdash t : T$ dans le système $\mathcal{T}$.

**Démonstration** : Par récurrence sur la structure de $t$ :

- Si $t = [x : U]u'$, alors $T = (x : U)U'$ est bien typé dans le système $\mathcal{T}$ donc $U'$ est bien typé dans le contexte $\Gamma[\forall x : U]$ dans ce système $\mathcal{T}$ et par hypothèse de récurrence $\Gamma[\forall x : U] \vdash u' : U'$ dans le système $\mathcal{T}$, donc $\Gamma \vdash t : T$ dans le système $\mathcal{T}$.

- Si $t = (x : U)U'$, alors par hypothèse de récurrence $U$ et $U'$ sont bien typés dans le système $\mathcal{T}$ et comme la règle $<s, s', s''> \text{ est une règle de ce système, on a } \Gamma \vdash t : T \text{ dans le système } \mathcal{T}$.

- Si $t = (x c_1 \dots c_n)$ et $x$ est une variable déclarée dans $\Gamma$, alors $x$ est bien typé dans $\Gamma$ dans le système $\mathcal{T}$ et on prouve par récurrence sur $i$ que le type de $c_i$ est bien typé dans le système $\mathcal{T}$ et donc que $c_i$ est bien typé dans le système $\mathcal{T}$, on en conclut que $\Gamma \vdash t : T$ dans le système $\mathcal{T}$.

- Si $t$ est une sorte, alors par hypothèse $t = \text{Prop}$, ce terme est bien typé dans le système $\mathcal{T}$.

**Proposition 39.** : Soit un contexte $\Gamma$ bien formé dans le système $\mathcal{T}$, $[\Gamma_1; \dots; \Gamma_m]$ une dérivation de $\Gamma$ et $\theta$ la substitution dénotée par cette dérivation. Soit $x$ une variable existentielle de $\Gamma$ et $t = \theta x$. Pour tout sous-terme de $t$ qui est un produit $(x : U)U'$, si on pose $s$ le type de $U$, $s'$ le type de $U'$ et $s''$ le type de $(x : U)U'$, on a $<s, s', s''> \in R$ (l'ensemble de règles du système $\mathcal{T}$) et pour tout sous-terme de $t$ qui est une sorte $s$, on a $s = \text{Prop}$ (et non Type).

**Démonstration** : Par récurrence sur $m$.

**Proposition 40.** : Soit un contexte $\Gamma$ bien formé dans le système $\mathcal{T}$, $[\Gamma_1; \dots; \Gamma_m]$ une dérivation de $\Gamma$ et $\theta$ la substitution dénotée par cette dérivation. La substitution $\theta$ est bien typée dans $\Gamma$ dans le système $\mathcal{T}$.

**Démonstration** : Par récurrence sur la longueur de $\Gamma$.

**Théorème 3.** : Correction

Soit un contexte (non quantifié et non contraint) et $P$ un type bien typé dans $\Gamma$. Soit le contexte $\Gamma_1 = \Gamma[\exists x : P]$. S'il existe une dérivation de $\Gamma_1$, alors il existe une preuve $t$ de $P$ dans $\Gamma$ dans $\mathcal{T}$. La preuve $t$ est appelée la preuve dénotée par la dérivation.
**Démonstration** : Soit $\theta$ la substitution dénotée par la dérivation de $\Gamma_1$. La substitution $\theta$ est bien typée dans $\Gamma_1$ dans le système $\mathcal{T}$ et $\Gamma_m = \theta\Gamma_1$ est un contexte de succès. Comme le terme $P$ est sans variables existentielles, $\theta P = P$.

Soit $t = \theta x$ et $\gamma$ le contexte associé à $x$ par $\theta$, $\theta\Gamma = \Gamma$, donc $\theta\Gamma_1 = \Gamma_m = \Gamma\gamma \vdash t : P$. Le contexte $\Gamma_m$ est un contexte de succès et $\gamma$ est un contexte existentiel, donc ce contexte est une liste de contraintes reliant des termes identiques, donc $\Gamma \vdash t : P$.

### 4.4.3 Complétude

**Définition 66.** : Taille d'un Terme

Soit un contexte $\Gamma$ et t un terme bien typé dans $\Gamma$. Soit $T$ la forme normale du type de t dans $\Gamma$. On définit par récurrence sur l'ordre $<$, la taille de $t_\Gamma$ ($|t_\Gamma|$) :

- Si $t$ est une sorte, alors $|t_\Gamma| = 1$,

- Si $t$ est une variable, alors $|t_\Gamma| = |T_\Gamma|$,

- Si $t = (u v)$, alors $|t_\Gamma| = |u_\Gamma| + |v_\Gamma| + |T_\Gamma|$,

- Si $t = [x : U]u$, alors $|t_\Gamma| = |u_\Gamma[x:U]|$,

- Si $t = (x : U)V$, alors $|t_\Gamma| = |U_\Gamma| + |V_\Gamma[x:U]| + |T_\Gamma|$.

**Définition 67.** : Taille d'une Substitution

La taille d'une substitution $\theta = \{<x_i, \gamma_i, t_i>\}$ où les $t_i$ sont normaux est la somme de la taille des $t_i$.

**Proposition 41.** : Si $\Gamma$ est un contexte d'échec, alors pour toute substitution $\sigma$ bien typée dans $\Gamma$, $\sigma\Gamma$ est aussi un contexte d'échec et de ce fait n'est pas un contexte de succès.

**Démonstration** : Soit $a = b$ une contrainte de $\Gamma$ reliant deux termes sans variables existentielles et différents, la contrainte $(\sigma a = \sigma b)$ est la contrainte $(a = b)$ qui est une contrainte reliant deux termes sans variables existentielles et différents.

**Lemme 4.** : Soit $\Gamma$ un contexte et $\theta$ une substitution telle que $\theta\Gamma$ soit un contexte de succès. Il existe une dérivation de $\Gamma$ qui dénote la substitution $\theta$.

**Démonstration** : Par récurrence sur la taille de $\theta$.

Le contexte $\theta\Gamma$ étant un contexte de succès, tous les contextes associés aux variables existentielles de $\Gamma$ sont des listes de contraintes reliant des termes sans variables existentielles et égaux. On peut donc considérer ces contextes comme vides.

Le contexte $\Gamma$ n'est pas un contexte d'échec car il existe une substitution $\theta$ telle que $\theta\Gamma$ est un contexte de succès. Si $\Gamma$ est un contexte de succès, alors $[\Gamma]$ est une dérivation de $\Gamma$.

Sinon choisissons parmi celles de $\Gamma$, une variable existentielle $x$ dont le type est normal et de la forme $(x_1 : P_1)...(x_n : P_n)P$ avec $P$ est atomique rigide et posons $t = \theta x$.

Le type de $t$ est $(x_1 : \theta P_1)...(x_n : \theta P_n)\theta P$. Comme $P$ est atomique rigide, il en est de même de $\theta P$. Donc $t = [x_1 : \theta P_1]...[x_n : \theta P_n]u$ avec $u$ terme atomique ou produit (forme $\eta$-longue).

- Si $u = (w u_1 ... u_p)$, alors soit $q$ le nombre de produits dans le type de $w$ et $r = p-q$. Comme le type de $u$ est atomique $p \ge q$, donc $r \ge 0$. Posons :

$$ \sigma = \{<x, \gamma, [x_1 : P_1]...[x_n : P_n](w (h_1 x_1 ... x_n) ... (h_p x_1 ... x_n))>\} $$

avec $\gamma$ défini dans l'algorithme.
Construisons à présent les termes devant être substitués aux variables $h_i$ ($1 \le i \le p$) et $H_i$ et $K_i$ ($1 \le i \le r$). Posons :

$$u'_{i} = [x_{1} : P_{1}]...[x_{n} : P_{n}]u_{i}$$

Et pour tout $i$, $1 \le i \le r$, $(w u_1 ... u_{q+i-1})$ a un type qui est un produit. Soit $(y : U_i)V_i$ ce produit. Posons :

$$U'_{i} = [x_{1} : P_{1}]...[x_{n} : P_{n}]U_{i}$$

$$V'_{i} = [x_{1} : P_{1}]...[x_{n} : P_{n}][y : U_{i}]V_{i}$$

$$\theta' = \theta - \{< x, [ ], \theta x >\} \cup \{< h_i, [ ], u'_i >\} \cup \{< H_i, [ ], U'_i >, < K_i, [ ], V'_i >\}$$

Nous avons $\theta = \theta' \circ \sigma$.

Prouvons à présent que la substitution $\theta'$ a une plus petite taille que $\theta$ :

$\theta x = [x_1 : \theta P_1]...[x_n : \theta P_n](w u_1 ... u_p)$. Soit $T_i$ le type de $(w u_1 ... u_p)$.

$$ 
\begin{align*}
|\theta x| &= |(w u_1 \dots u_p)| = |T_0| + |u_1| + |T_1| + \dots + |u_p| + |T_p| \\
&> |T_q| + \dots + |T_{p-1}| + |u_1| + \dots + |u_p| = |(y : U_1)V_1| + \dots + |(y : U_r)V_r| + |u_1| + \dots + |u_p| \\
&> |U_1| + \dots + |U_r| + \dots + |V_1| + \dots + |V_r| + |u_1| + \dots + |u_p| \\
&= |U'_1| + \dots + |U'_r| + |V'_1| + \dots + |V'_r| + |u'_1| + \dots + |u'_p|.
\end{align*}
$$

Donc $|\theta| > |\theta'|$.

$$\sigma = \{< x, \gamma, [x_1 : P_1]...[x_n : P_n](y : (h x_1 ... x_n))(k x_1 ... x_n y) >\}$$

avec $\gamma$ défini dans l'algorithmme.

Construisons les termes qui doivent être substitués aux variables $h$ et $k$. Posons :

$$U' = [x_1 : P_1]...[x_n : P_n]U$$

$$V' = [x_{1} : P_{1}]...[x_{n} : P_{n}][y : U]V$$

$$\theta' = \theta - \{< x, [ ], \theta x >\} \cup \{< h, [ ], U' >, < k, [ ], V' >\}$$

Nous avons $\theta = \theta' \circ \sigma$.

Prouvons à présent que la substitution $\theta'$ a une plus petite taille que $\theta$ :

$\theta x = [x_1 : \theta P_1]...[x_n : \theta P_n](y : U)V.$

$$|\theta x| = |(y : U)V| > |U| + |V| = |U'| + |V'|.$$

Donc $|\theta| > |\theta'|$.

Dans les deux cas, par hypothèse de récurrence, il existe une dérivation $D$ de $\sigma\Gamma$ qui dénote la substitution $\theta'$ et $[\Gamma]D$ est une dérivation de $\Gamma$ qui dénote $\theta$.

### Théorème 4. : Compléture

Soit $\Gamma$ un contexte (non quantifié et non contraint) et $P$ un type bien typé dans $\Gamma$ tel qu'il existe un terme $t$ tel que $\Gamma \vdash t : P$. Alors il existe une dérivation de $\Gamma_1 = \Gamma[\exists x : P]$ qui dénote la preuve $t$.

**Démonstration** : Soit $\theta = x \leftarrow [ ], t$. On a $\theta\Gamma_1 = \Gamma$, donc il existe une dérivation de $\Gamma_1$ qui dénote la substitution $\theta$.
## 4.5 Améliorations de l'Efficacité

Pour améliorer l'efficacité de la méthode, il faut reconnaître le plus tôt possible les nœuds qui ne peuvent en aucun cas conduire à un nœud de succès pour élaguer l'arbre de recherche.

### 4.5.1 Vérification Incrémentale des Contraintes

Tout d'abord nous devons vérifier incrémentalement les contraintes. Pour ce faire, nous définissons une fonction de simplification des contraintes très similaire à la fonction SIMPL de [40] [41].

Pour pouvoir définir cette fonction nous modifions une peu la syntaxe des contraintes : une contrainte est à présent un triplet $< \delta, a, b >$ où $\delta$ est un contexte qui ne contient que des variables universelles. Si $\Gamma = \Delta[< \delta, a, b >] \Delta'$, alors les termes $a$ et $b$ doivent être bien typés et du même type dans $\Delta \delta$.

**Définition 68.** : Simplification

Tant qu'il y a, dans un contexte $\Gamma$, une contrainte bien typée sans utiliser les contraintes et reliant deux termes rigides et que la simplification n'a pas échoué, on répète le processus consistant à remplacer ce contexte $\Gamma$ par le contexte $\Gamma'$ défini ci-dessous.

Soit $\delta, a = b$ une contrainte de $\Gamma$ bien typée sans utiliser les contraintes et reliant deux termes rigides. On écrit $\Gamma = \Delta[\delta, a = b] \Delta'$.

- Si $a$ et $b$ sont deux abstractions $a = [x : T]a'$, $b = [x : U]b'$, comme les termes $a$ et $b$ ont le même type dans $\Delta \delta$, on a $T = U$, on pose $\Gamma' = \Delta[\delta[\forall x : T], a' = b'] \Delta'$.

- Si $a$ et $b$ sont deux produits $a = (x : T)a'$, $b = (x : U)b'$ et $T$ et $U$ ont le même type, on pose $\Gamma' = \Delta[\delta, T = U][\delta[\forall x : T], a' = b'] \Delta'$.

- Si $a$ et $b$ sont deux termes atomiques et ont la même variable de tête appliquée au même nombre de termes, $a = (w u_1 ... u_p)$, $b = (w t_1 ... t_p)$, on pose $\Gamma' = \Delta[\delta, u_1 = t_1]...[\delta, u_p = t_p] \Delta'$.

- Dans les autres cas la simplification échoue.

Quand la simplification échoue, le nœud ne peut pas mener à une nœud de succès et cette branche de l'arbre peut être élaguée.

### 4.5.2 Utilisation des Contraintes Flexible-Rigide

Quand on a dans un contexte une contrainte bien typée reliant un terme flexible à un terme rigide, et que la tête du terme flexible est instanciable (c'est-à-dire quand la tête de son type est rigide) il faut instancier cette contrainte en premier, les seuls candidats pour la variable de tête du terme substitué à cette variable sont la variable de tête du terme rigide et les variables liées dans une abstraction [40] [41].

Les autres substitutions mènent à des contraintes reliant deux termes rigides dont la simplification échoue.

### 4.5.3 Utilisation des Contraintes Flexible-Flexible

Quand on a une contrainte bien typée reliant deux termes flexibles et que l'on peut instancier la variable de tête de l'un des termes, il faut l'instancier en premier. Cette contrainte n'aidera pas à restreindre les substitutions pour cette variable, mais on peut, en la substituant ainsi, la transformer
en une contrainte reliant un terme flexible à un terme rigide. De plus, résoudre une contrainte permet de rendre d'autres contraintes bien typés sans utiliser les contraintes et donc exploitables.

### 4.5.4 Economie de la Scission

Le terme $(Q (h_1 x_1 ... x_n) ... (h_q x_1 ... x_n))$ est atomique, s'il est rigide, il est inutile de considérer les solutions avec un degré de scission non nul, car elles mènent à des contraintes reliant des termes rigides dont la simplification échoue.

En particulier dans le $\lambda\Pi$-calcul, on ne considère jamais de variables existentielles de type ou de prédicat, et donc la scission peut toujours être évitée.

### 4.5.5 Sous-Problèmes Décidables de l'Unification

Quand une contrainte bien typée sans utiliser les contraintes est un problème d'unification décidable (unification du premier ordre, filtrage du deuxième ordre, etc.), on peut la résoudre et appliquer les substitutions ainsi obtenues au contexte $\Gamma$. La seconde partie de cette thèse est consacrée à l'étude de ces contraintes.

Dans un système possédant une telle heuristique, l'élimination d'un quantificateur universel du premier ordre est une opération élémentaire alors que l'élimination d'un quantificateur universel à l'ordre supérieur est une opération plus complexe qui peut nécessiter une exploration non déterministe.

### 4.5.6 Priorité à la Variable la Plus à Droite

Quand on a deux variables existentielles $x$ et $y$ telles que $y$ est déclarée à droite de $x$ et $x$ a une occurrence dans le type de $y$, si ces deux variables peuvent être instanciées, il faut commencer par le variable la plus à droite. Considérons par exemple le cas où on a un axiome $u : (P n)$ et où on cherche un entier $x$ tel que $(P x)$. On a deux variables existentielles : $x : Nat$ et $y : (P x)$, instancier $y$ par $u$ donnera la contrainte $x = n$ et $x$ sera automatiquement instancié par $n$ alors que si on commence par $x$ on va l'instancier par 0, 1, 2, etc. et échouer dans la recherche d'une preuve de $(P 0)$, $(P 1)$, $(P 2)$, etc. avant d'arriver à $x = n$.

### 4.5.7 Normalisation de Certains Termes Mal Typés

Une amélioration importante de cette méthode consisterait à reconnaître certains termes mal typés mais néanmoins normalisables, ce qui permettrait d'utiliser les contraintes plus efficacement.

Par exemple, on peut montrer que si $t$ est un terme normal et $\sigma$ une substitution élémentaire de la forme $x \leftarrow [x_1 : P_1]...[x_n : P_n]u$ où $u$ est un produit ou un terme atomique dont la variable de tête est une variable universelle ou une sorte (mais pas l'un des $x_i$), alors $\sigma t$ est normalisable.

## 4.6 Extension au Calcul des Constructions avec Univers

Dans une extension de cette méthode au Calcul des Constructions avec Univers, il n'est plus nécessaire de considérer un système de types *Méta* car tous les termes considérés dans cet algorithme sont bien typés dans le Calcul des Constructions avec Univers. Mais un nouveau problème survient : quand nous voulons instancier $x : Prop$ par un produit, il y a une infinité de possibilités $(y : h)(k y)$
avec $h : Type_i$ et $k : (y : h)Prop$. Ce problème peut être résolu en utilisant la méthode des univers flottants [43] [34].

Quand on a aussi une règle de cumulativité, un terme bien typé n'a plus nécessairement un type unique (ce problème est également résolu en utilisant la méthode des univers flottants) et les contraintes ne sont plus des égalités mais deviennent des inégalités pour la relation de cumulativité.

# 4.7 Application à la Synthèse et à l'Evaluation de Programmes

## 4.7.1 Synthèse de Programmes

Une application possible de la synthèse de preuves est la synthèse de programmes. En effet si $S : T \to U \to Prop$ est une spécification d'un programme prenant en entrée un objet de type $T$ et retournant un objet de type $U$, d'une preuve constructive de la proposition $\forall x : T. \exists y : U.(S x y)$ on peut extraire un terme (programme) $f$ de type $T \to U$ tel que $\forall x : T.(S x (f x))$ [53] [54]. En composant un algorithme de synthèse de preuves avec un algorithme d'extraction de programmes on obtient un algorithme de synthèse de programmes à partir de spécifications.

Pour pouvoir extraire des programmes non triviaux, il faut se placer dans un système logique dont le langage des termes est suffisamment riche. Il est donc exclu de se placer au premier ordre ou à l'ordre supérieur, les systèmes des types sont en revanche de bons candidats.

## 4.7.2 Programmation Logique

Dès le premier ordre il est néanmoins possible d'utiliser la synthèse de preuves pour programmer. Une spécification $S : T \to U \to Prop$ et une valeur d'entrée $t : T$ données, il est possible de synthétiser une preuve constructive de $\exists y : U.(S t y)$ et d'extraire de cette preuve un terme $u$ tel que $(S t u)$. Cette méthode est celle utilisée par l'interpréteur Prolog. Le fait qu'un programme Prolog soit en fait une spécification et que l'évaluation de ce programme soit en quelque sorte la synthèse d'un programme d'arité nulle $u$, explique le décalage entre programmation fonctionnelle et logique [47]. En effet en programmation fonctionnelle, une spécification est une proposition, un programme est une preuve de cette spécification et l'évaluation de ce programme est la normalisation de cette preuve, alors qu'en programmation logique c'est le programme qui est une proposition et son évaluation est la recherche d'une preuve de cette proposition.

## 4.7.3 Interprétation et Compilation

Le fait qu'au premier ordre, la recherche de preuve ne puisse se faire qu'une fois la valeur d'en-trée connue et que à l'ordre supérieur (dans les systèmes de types) cette recherche puisse se faire avant, met en lumière une analogie entre les oppositions premier ordre / ordre supérieur (systèmes de types) et interprétation / compilation. Une méthode de synthèse de programmes fonctionnels à partir de spécifications peut être vue comme une méthode de compilation des programmes lo-giques en programmes fonctionnels. Cette compilation élimine toute recherche non déterministe à l'exécution, en quelque sorte le programme logique est suffisamment analysé à la compilation pour qu'on soit capable de distinguer en fonction de la valeur d'entrée quelles sont les branches de l'arbre d'évaluation qui sont vouées à l'échec et se diriger directement vers une branche vouée au succès.

La synthèse de preuves dans les systèmes de types semble donc ouvrir des voies prometteuses en programmation logique. Naturellement ces voies sont encore trop floues pour qu'on puisse dire
aujourd'hui si elles sont réalistes ou si la compilation d'un programme logique en un programme fonctionnel déterministe demande la synthèse d'une preuve beaucoup trop complexe. Néanmoins la question mérite d'être posée.
# Chapitre 5

## Une Restriction Incomplète

### 5.1 Une Restriction

Revenons à l'exemple que nous avons considéré au chapitre précédent :

$$ 
\begin{array}{l}
\Delta = [\forall A : \mathit{Prop}; \forall B : \mathit{Prop}; \forall I : \mathit{Prop} \to \mathit{Prop}; \forall u : (P : \mathit{Prop})((I P) \to P); \forall v : (I (A \to B)); \\
\forall w : A] \\
\text{et } \Gamma = \Delta[\exists p : B].
\end{array}
$$

Pour obtenir la preuve $(u (A \to B) v w) : B$, nous avons dû appliquer une substitution avec un degré de scission égal à 1 :

$$ p \leftarrow (u h_1 h_2 h_3) $$

où le terme substitué à $p$ a trois applications alors que le type de $u$ ne commence que par deux produits. Comme nous considérons tous les degrés de scission possibles, notre méthode est assez inefficace. On la rend beaucoup plus réaliste en restreignant à des substitutions de degré de scission nul et un nombre d'abstractions compris entre zéro et le nombre de produits dans le type de la variable existentielle substituée. Appelons cet algorithme scission faible (par opposition, l'algorithme précédent sera appelé algorithme avec scission forte).

L'arbre de recherche de l'algorithme avec scission faible est finiment branchant.

Cette méthode avec scission faible ne peut pas synthétiser la preuve de $B$ ci-dessus. En revanche elle peut synthétiser une preuve de $A \to B$. En effet, soit $p'$ une variable existentielle $p' : A \to B$. Appliquons la substitution :

$$ p' \leftarrow (u h_1 h_2) $$

avec $h_1 : \mathit{Prop}, h_2 : (I h_1)$ (remarquons que bien que le type de $p'$ commence par un produit, le nombre d'abstractions dans $(u h_1 h_2)$ est nul). La contrainte $h_1 = A \to B$ suggère la substitution :

$$ h_1 \leftarrow (A \to B) $$

puis pour la variable existentielle $h_2 : (I (A \to B))$, on applique la substitution :

$$ h_2 \leftarrow v $$

La preuve synthétisée est $(u (A \to B) v) : (A \to B)$. Remarquons que ce terme n'est pas en forme $\eta$-longue, sa forme $\eta$-longue est $[w : A](u (A \to B) v w) : (A \to B)$.
## 5.2 Généralisation de l'Hypothèse de Récurrence

Dans les deux preuves que nous avons considérées (celles de $B$ et $A \to B$), le problème était de remarquer que le terme $u : (P : Prop)((I P) \to P)$ devait être appliqué à la proposition $(A \to B)$.

L'algorithme avec scission forte trouve cette proposition dans les deux preuves, le prix payé est l'inefficacité de cet algorithme. L'algorithme avec scission faible ne trouve cette proposition que dans le cas de la preuve de $A \to B$.

Cela signifie que quand on utilise une hypothèse avec un quantificateur sur une proposition ou un prédicat (par exemple un principe de récurrence), l'algorithme avec scission faible ne trouve la proposition à laquelle appliquer cette hypothèse que quand cette proposition peut être lue dans le but à prouver et non quand la preuve demande une généralisation de l'hypothèse de récurrence (induction loading) [35] (ici de $B$ à $A \to B$).

Cette méthode avec scission faible est similaire à la méthode d'introduction-résolution pour un certain algorithme d'unification. En fait certaines preuves qui ne sont pas synthétisées par introduction-résolution le sont avec scission faible : par exemple dans un contexte qui contient les variables universelles $u : (P : Prop)(P \to A)$ et $v : (B \to C)$, la preuve $(u (B \to C) [x : C](v x)) : A$ est synthétisée par l'algorithme avec scission faible mais pas par la méthode d'introduction-résolution.

Pour obtenir exactement la méthode d'introduction-résolution, il faudrait supprimer totalement la règle de produit.

## 5.3 Complétude Transitive

Nous allons maintenant montrer que cette méthode avec scission faible bien qu'incomplète est transitivement complète, c'est-à-dire que pour toute preuve $t$ d'une proposition $P$ dans un contexte $\Gamma$ il existe une suite de lemmes, tels que chacun d'eux peut être démontré par l'algorithme avec scission faible si on admet ceux qui le précèdent et dont le dernier est la proposition $P$. De plus, en composant les preuves de ces lemmes, on obtient la preuve $t$. Cette propriété tire son importance du fait qu'elle montre que, sous réserve d'être guidée par un utilisateur qui lui indique les lemmes intermédiaires, la méthode avec scission faible peut construire toutes les preuves. Cette méthode peut donc servir de base à un système d'aide à la mise au point interactive de preuves et à un langage de preuve de haut niveau que nous détaillerons par la suite.

Il nous faut d'abord préciser la notion de lemme. Pour cela nous allons étendre la notion de contextes en lui ajoutant une notion de constante.

**Définition 69. : Constante**

Une constante est un couple de termes $<c, T>$ (noté $c : T$). Un contexte quantifié contraint avec constantes est une liste $\Gamma = [e_1; ...; e_n]$ telle que $e_i$ est une déclaration quantifiée, une contrainte ou une constante.

**Définition 70. : Règles de Typage**

On ajoute les deux règles de typage suivantes qui permettent de manipuler ces constantes :

$$ \frac{\Gamma \vdash c : T}{\Gamma[c : T] \text{ bien formé}} $$

$$ \frac{c : T \in \Gamma}{\Gamma \vdash c : T} $$
**Remarque** : Dans la définition que nous avons donnée, les constantes n'ont pas de nom. Nous évitons ainsi les problèmes liés à l'expansion des noms de constantes dans les propositions à prouver. En quelque sorte nos constantes sont toujours expansées.

Les règles que nous rajoutons n'apportent rien quant à la syntaxe des termes ou à la possibilité de typer ces termes. Il est en effet très facile de vérifier que si $\Gamma \vdash t : T$ et $\Gamma'$ est obtenu en effaçant toutes les constantes de $\Gamma$, alors $\Gamma'$ est bien formé et $\Gamma' \vdash t : T$.

**Définition 71.** : Algorithme de Synthèse de Preuves avec Lemmes

Nous étendons les algorithmes de synthèse de preuves développés ci-dessus en permettant d'utiliser les constantes comme les variables dans les substitutions élémentaires.

Par exemple considérons le contexte :

$$ 
\begin{array}{l}
\Delta = [\forall A : \mathit{Prop}; \forall B : \mathit{Prop}; \forall I : \mathit{Prop} \to \mathit{Prop}; \forall u : (P : \mathit{Prop})((I P) \to P); \forall v : I(A \to B); \\
\forall w : A; (u (A \to B) v) : A \to B] \\
\text{et } \Gamma = \Delta[\exists p : B].
\end{array}
$$

L'algorithme avec scission faible engendre une dérivation de $\Gamma$ en effet en appliquant une substitution élémentaire avec la constante $(u (A \to B) v) : A \to B$ comme tête :

$$ p \leftarrow (u (A \to B) v h) $$

avec $h : A$. On obtient le contexte $\Delta[\exists h : A]$ puis en appliquant une substitution élémentaire avec la variable $w$ comme tête :

$$ h \leftarrow w $$

On obtient le contexte de succès $\Delta$.

La preuve dénotée par cette dérivation est $(u (A \to B) v w)$.

**Définition 72.** : Clôture Transitive d'un Algorithme de Synthèse de Preuves

Soit un algorithme de synthèse de preuves, on note $\Gamma \rightsquigarrow t : T$ le jugement indiquant qu'il existe une dérivation de $\Gamma[\exists x : T]$ engendrée par l'algorithme avec scission faible qui dénote la preuve $t$. On définit inductivement le jugement $\Gamma \mapsto t : T$.

$$ \frac{\Gamma \mapsto c_1 : Q_1 \dots \Gamma \mapsto c_n : Q_n \quad \Gamma [c_1 : Q_1; \dots; c_n : Q_n] \rightsquigarrow t : P}{\Gamma \mapsto t : P} $$

**Définition 73.** : Complétude Transitive

Une méthode de synthèse de preuves est dite transitivement complète si $\Gamma \vdash t : T$ (t normal) implique $\Gamma \mapsto t : T$.

**Proposition 42.** : Soit $\Gamma$ un contexte contenant une variable existentielle $y : (x_1 : P_1)...(x_n : P_n)P$. Soit $x : P$ une variable universelle ou une constante déclarées à gauche de $y$ ou l'un des $x_i$.

Il existe une suite de contextes engendrée par l'algorithme avec scission faible dont le premier élément est $\Gamma$, qui dénote la substitution :

$$ y \leftarrow [x_1 : P_1]...[x_n : P_n]x' $$

où $x'$ est la forme $\eta$-longue de $x$.
**Démonstration** : Par récurrence sur la structure de $x'$.

Ecrivons $P = (y_1 : Q_1)...(y_p : Q_p)Q$ (Q atomique). On a :

$$y : (x_1 : P_1)...(x_n : P_n)(y_1 : Q_1)...(y_p : Q_p)Q \quad (Q \text{ atomique})$$

On considère la substitution $\sigma$ :

$$y \leftarrow [x_1 : P_1]...[x_n : P_n][y_1 : Q_1]...[y_p : Q_p](x (h_1 x_1 \dots x_n y_1 \dots y_p) \dots (h_p x_1 \dots x_n y_1 \dots y_p))$$

On obtient un contexte qui contient les variables :

$$\exists h_1 : (x_1 : P_1)...(x_n : P_n)(y_1 : Q_1)...(y_p : Q_p)Q_1$$

$$\exists h_p : (x_1 : P_1)...(x_n : P_n)(y_1 : Q_1)...(y_p : Q_p)Q_p$$

Par hypothèse de récurrence, il existe une suite de contextes dont le premier contexte est $\sigma\Gamma$, engendrée par l'algorithme avec scission faible que dénote la substitution $\sigma_1$ :

$$h_1 \leftarrow [x_1 : P_1]...[x_n : P_n][y_1 : Q_1]...[y_p : Q_p]y'_1$$

Puis une dont le premier contexte est $\sigma_1\sigma\Gamma$ qui dénote la substitution $\sigma_2$ :

$$h_2 \leftarrow [x_1 : P_1]...[x_n : P_n][y_1 : Q_1]...[y_p : Q_p]y'_2$$

etc., enfin une dont le premier contexte est $\sigma_{p-1}...\sigma_1\sigma\Gamma$ qui dénote la substitution $\sigma_p$ :

$$h_p \leftarrow [x_1 : P_1]...[x_n : P_n][y_1 : Q_1]...[y_p : Q_p]y'_p$$

La composée de ces substitutions est la substitution :

$$y \leftarrow [x_1 : P_1]...[x_n : P_n][y_1 : Q_1]...[y_p : Q_p](x y'_1 \dots y'_p)$$

c'est-à-dire :

$$y \leftarrow [x_1 : P_1]...[x_n : P_n]x'$$

**Proposition 43.** : La méthode de synthèse de preuves avec scission faible est transitivement complète.

**Démonstration** : Soit $\Gamma, t$ et $T$ tels que $\Gamma \vdash t : T$, montrons par récurrence sur la taille de $t$ que $\Gamma \hookrightarrow t : T$.

• Si $t = [x_1 : P_1]...[x_n : P_n](w c_1 \dots c_p)$.

Le terme $t$ est en forme $\eta$-longue, donc $(w c_1 \dots c_p)$ a un type atomique.

Pour tout $i$ posons $d_i = [x_1 : P_1]...[x_n : P_n]c_i$. et $D_i$ le type de $d_i$ dans $\Gamma$.

On définit la suite finie $t_1, \dots, t_k = t$.

Soit $q_1$ le nombre de produits dans le type de $w$, on pose $t_1 = [x_1 : P_1]...[x_n : P_n](w c_1 \dots c_{q_1})$.

Si $t_1 = t$, on pose $k = 1$. Sinon, soit $q_2$ le nombre de produits dans le type de $(w c_1 \dots c_{q_1})$, on pose $t_2 = [x_1 : P_1]...[x_n : P_n](t_1 x_1 \dots x_n c_{q_1+1} \dots c_{q_1+q_2}) = [x_1 : P_1]...[x_n : P_n](w c_1 \dots c_{q_1+q_2})$, etc.
On pose $T_i$ le type de $t_i$ dans $\Gamma$. On a $T_k = T$ et d'après la proposition précédente :

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p; t_1 : T_1; \dots; t_k : T_k] \rightsquigarrow t_k : T_k $$

c'est-à-dire :

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p; t_1 : T_1; \dots; t_k : T_k] \rightsquigarrow t : T $$

Montrons maintenant par récurrence descendante sur $i$ que pour tout $i$, $0 \le i \le k$

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p; t_1 : T_1; \dots; t_i : T_i] \rightsquigarrow t : T $$

Nous avons déjà prouvé cette proposition pour $i = k$. Admettons-la pour $i$ :

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p; t_1 : T_1; \dots; t_i : T_i] \hookrightarrow t : T $$

On a :

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p; t_1 : T_1; \dots; t_{i-1} : T_{i-1}] \rightsquigarrow t_i : T_i $$

En effet, considérons le contexte :

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p; t_1 : T_1; \dots; t_{i-1} : T_{i-1}; \exists h : T_i] $$

On applique à $h$ la substitution élémentaire de tête $t_{i-1}$ et avec $n$ abstractions :

$$ h \leftarrow [x_1 : P_1]...[x_n : P_n](t_{i-1} (h_1 x_1 \dots x_n) \dots (h_n x_1 \dots x_n) (k_1 x_1 \dots x_n) \dots (k_{q_i} x_1 \dots x_n)) $$

Puis d'après la proposition précédente, il existe une suite de contextes engendrée par l'algorithme avec scission faible telle que la substitution dénotée par cette suite instancie les $h_j$ par le terme $[x_1 : P_1]...[x_n : P_n]x'_j$ et les $k_j$ par le terme $d'_{q_1+...+q_{i-1}+j}$. La substitution dénotée par cette suite est donc :

$$ h \leftarrow [x_1 : P_1]...[x_n : P_n](t_{i-1} x'_1 \dots x'_n c_{q_1+\dots+q_{i-1}+1} \dots c_{q_1+\dots+q_{i-1}+q_i}) $$

c'est-à-dire :

$$ h \leftarrow t_i $$

Donc :

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p; t_1 : T_1; \dots; t_{i-1} : T_{i-1}] \rightsquigarrow t_i : T_i $$

Comme par ailleurs on sait que :

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p; t_1 : T_1; \dots; t_i : T_i] \hookrightarrow t : T $$

On en déduit :

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p; t_1 : T_1; \dots; t_{i-1} : T_{i-1}] \hookrightarrow t : T $$

On a donc :

$$ \Gamma[d_1 : D_1; \dots; d_p : D_p] \hookrightarrow t : T $$

Par hypothèse de récurrence $\Gamma \hookrightarrow d_i : D_i$, donc :

$$ \Gamma \hookrightarrow t : T $$
* Si $t = [x_1 : P_1]...[x_n : P_n](z : U)V$, alors on pose :

$$u = [x_1 : P_1]...[x_n : P_n]U$$
$$v = [x_1 : P_1]...[x_n : P_n][z : U]V$$

Par hypothèse de récurrence :

$$\Gamma \hookrightarrow u : (x_1 : P_1)...(x_n : P_n)s$$

et :

$$\Gamma \hookrightarrow v : (x_1 : P_1)...(x_n : P_n)(z : U)s'$$

en appliquant la règle de produit et la proposition précédente :

$$\Gamma[u : (x_1 : P_1)...(x_n : P_n)s; v : (x_1 : P_1)...(x_n : P_n)(z : U)s'] \rightsquigarrow t : T$$

donc :

$$\Gamma \hookrightarrow t : T$$

* Si $t = [x_1 : P_1]...[x_n : P_n]s$ (où $s$ est une sorte), on a :

$$\Gamma \rightsquigarrow t : T$$

donc :

$$\Gamma \hookrightarrow t : T$$

## 5.4 Accès aux Axiomes

Dans la section précédente nous avons vu que quand on a un axiome ou un lemme $x : T$ dans le contexte $\Gamma$, prouver cette proposition peut demander plusieurs étapes en fonction de la forme $\eta$-longue de $x$. Dans certaines applications cela est ennuyeux. On peut donc ajouter une règle à notre méthode : la règle d'accès aux axiomes. Quand on instancie une variable existentielle de type $(x_1 : P_1)...(x_n : P_n)P$ (P atomique), on considère toutes les substitutions $[x_1 : P_1]...[x_k : P_k]x'$ où $x$ est une variable ou une constante du contexte de type $(x_{k+1} : P_{k+1})...(x_n : P_n)P$.

**Définition 74.** : Algorithme avec Scission Faible, Accès aux Axiomes et Nombre d'Itérations Borné par Deux

On considère l'algorithme avec scission faible et accès aux axiomes et on note $\Gamma \rightsquigarrow_2 t : P$ le jugement indiquant qu'il existe une dérivation de $\Gamma[\exists x : P]$ qui dénote la preuve $t$, dans laquelle on instancie $x$ par un terme introduisant éventuellement des variables existentielles $h_1, ..., h_p$, puis on instancie les variables $h_1, ..., h_p$ par des termes n'introduisant pas de nouvelles variables existentielles. (On dit dans ce cas que le nombre d'itérations est borné par deux.)

**Proposition 44.** : L'algorithme avec scission faible, accès aux axiomes et nombre d'Itérations borné par deux termine toujours et est transitivement complet.
**Démonstration** : Pour la terminaison, il suffit de remarquer que l'arbre de recherche est finiment branchant et ses branches finies car en associant au nœud initial l'ordinal $\omega$ et aux autres leur nombre de variables existentielles, on obtient une suite d'ordinaux strictement décroissante le long d'une branche.

Pour la complétude transitive, on reprend la démonstration ci-dessus, en remarquant que grâce à la règle d'accès aux axiomes toutes les dérivations considérées ont un nombre d'itérations borné par deux.

## 5.5 Synthèse Interactive de Preuves

### 5.5.1 Tactiques

Nous allons maintenant utiliser l'algorithme avec scission faible pour mettre en œuvre un système d'aide à la mise au point de preuves par tactiques, dans l'esprit du système LCF [32].

Dans ce système, l'utilisateur déclare d'abord un contexte et l'énoncé d'un théorème. Cet énoncé est compris par la machine comme le type d'une nouvelle variable existentielle. Puis il donne des instructions à la machine. Ces instructions sont de deux sortes : appliquer une substitution élémentaire de l'algorithme avec scission faible et accès aux axiomes ou déclarer l'énoncé d'un lemme pour ce théorème. A chaque étape, la machine simplifie les contraintes, résout les contraintes décidables qui ont une solution unique (par exemple en s'appuyant sur [57]) et affiche la liste des types des variables existentielles du contexte.

Dans ce système, quand on veut prouver une proposition $A \to B$, il n'est pas possible d'ajouter au contexte une proposition $A$ et de chercher à prouver $B$. En effet cette transformation n'est pas l'application d'une substitution au contexte courant. Il est néanmoins beaucoup plus pratique de procéder ainsi que d'aller jusqu'à la forme normale de tête de la preuve et de marquer explicitement la dépendance des buts intermédiaires par rapport aux hypothèses comme nous l'avons fait.

Une façon de procéder est d'introduire un mécanisme de sections et de portées des identificateurs dans le contexte [4] [5]. Grossièrement, on peut dire que quand on a une variable existentielle de type $y: A \to B$ et que l'on introduit l'hypothèse $A$, localement l'hypothèse $A$ est visible et $y$ est de type $B$, mais du point de vue des autres objets du contexte, l'hypothèse $A$ n'est pas visible et $y$ a toujours le type $A \to B$.

Du fait de la présence de cette règle d'introduction, la règle de substitution peut se limiter à des termes sans abstraction.

On obtient alors un système très proche de ceux qui comportent les tactiques introduction, résolution, produit et accès aux axiomes. Un progrès qui apparaît dans ce système par rapport à ces systèmes est qu'il est à tout moment possible à l'utilisateur d'interrompre sa preuve, pour introduire un lemme ou une hypothèse. Egalement, la tactique de résolution n'est pas limitée par un algorithme d'unification (du premier ordre par exemple) mais elle engendre une contrainte arbitrairement complexe. Deux cas peuvent alors se produire : si la contrainte engendrée appartient à une classe que l'on sait résoudre, alors elle est résolue, sinon elle reste dans le contexte et l'utilisateur peut, en quelque sorte, guider la machine dans l'arbre d'unification de la même façon qu'il la guide dans l'arbre de synthèse de preuves.
### 5.5.2 Un Exemple Simple

Voici un exemple des instructions données à la machine pour montrer que tout booléen est égal à *True* ou à *False* dans un prototype d'un tel système. Ce prototype comporte également la possibilité de définir des constantes nommées, c'est-à-dire qu'après une définition $a := t$ où $a$ est un symbole et $t$ un terme bien typé dans le contexte courant, on peut utiliser le symbole $a$ et tout se passe comme si ce symbole était remplacé par le terme $t$ à chacune de ses occurrences.

Déclarons tout d'abord le type des booléens et les deux variables *True* et *False* :

Parameter Bool:Prop. (* Prop = Set *)

Parameter True:Bool.

Parameter False:Bool.

Pour exprimer le fait que le type *Bool* ne contient rien d'autre que ces deux éléments, déclarons un axiome de récurrence sur les booléens :

Axiom RecB.

Assumes (P:Bool -> Prop)((P True) -> (P False) -> (x:Bool)(P x)).

Déclarons ensuite une relation (d'égalité) réflexive sur ce type :

Parameter Eq: (Bool -> Bool -> Prop).

Axiom Refl.

Assumes (x:Bool)(Eq x x).

Nous pouvons maintenant démontrer notre théorème :

Theorem True_or_False.

Variable b:Bool.

Statement ((Eq b True)\/(Eq b False)).

Resolution RecB.

Go x1.

Local P = [x:Bool]((Eq x True)\/(Eq x False)).

Assumption P.

Resolution or_intro2.

Resolution Refl.

Resolution or_intro1.

Resolution Refl.

Lors de l'application de la tactique *Resolution RecB*. la contrainte engendrée n'est pas une contrainte triviale. La machine affiche donc quatre buts x1, x2, x3 et x4. Ainsi que la contrainte :

$$ (x1 \ x4) == (Eq \ b \ True)\/(Eq \ b \ False). $$

en fait, dans cette contrainte, la définition de la disjonction est développée (voir chapitre 1) et elle s'écrit donc :
$(x1 x4) == (C:Prop)((Eq b True)->C)->((Eq b False)->C)->C.

<<<< Begin Section True_or_False

*** [b :Bool]

<<<< Begin Section x1

*** [?x1 :Bool->Prop]

>>> End Section x1

<<<< Begin Section x2

*** [?x2 : (x1 True)]

>>> End Section x2

<<<< Begin Section x3

*** [?x3 : (x1 False)]

>>> End Section x3

<<<< Begin Section x4

*** [?x4 :Bool]

>>> End Section x4

[[ ]] (x1 x4) == (C:Prop)((Eq b True)->C)->((Eq b False)->C)->C

True_or_False : (Eq b True)\/(Eq b False)

>>> End Section True_or_False

La double ligne indique que le but considéré par défaut est x4. On change de but par l'instruction Go x1. Puis on définit une constante locale P et on instancie x1 par P. Par cette instanciation la contrainte devient, après simplification, x4 = b. Elle est maintenant triviale est donc x4 est automatiquement instanciée. Les buts restant à prouver sont donc :

x2:((Eq True True)\/(Eq True False))

et :

x3:((Eq False True)\/(Eq False False)).

Pour x3 par exemple, on applique la tactique Resolution or_intro2 qui nous ramène à la proposition (Eq False False) qui est prouvée par Resolution Refl. Remarquons que dans ces deux cas la contrainte engendrée est triviale et est donc résolue automatiquement par la machine.

### 5.5.3 Un Autre Exemple : Un Lemme du Théorème de Tarski

Déclarons tout d'abord un type T, une relation d'égalité Eq et une relation R antisymétrique et transitive.

Parameter T:Prop. (* Prop = Set *)

Parameter Eq:T->T->Prop.

Parameter R:T->T->Prop.
Axiom Antisym.

Assumes (x:T)(y:T)(R x y) -> (R y x) -> (Eq x y).

Axiom Trans.

Assumes (x:T)(y:T)(z:T)(R x y) -> (R y z) -> (R x z).

Déclarons ensuite une fonction croissante de $T$ dans $T$ et définissons l'ensemble des pré-points-fixes.

Parameter $f:T->T$.

Axiom Incr.

Assumes (x:T)(y:T)(R x y) -> (R (f x) (f y)).

Definition $\text{Pre} = [x:T](R x (f x)).$

Déclarons ensuite un élément de $T$ et supposons que c'est la borne supérieure de l'ensemble des pré-points-fixes.

Parameter $M:T$.

Axiom Up.

Assumes (x:T) (Pre x) -> (R x M).

Axiom Least.

Assumes (y:T)((x:T)(Pre x)->(R x y))-(R M y).

Démontrons maintenant que $M$ est un point fixe de $f$.

Theorem Tarski.

Statement (Eq M (f M)).

Resolution Antisym.

Resolution Up.

Resolution Incr.

Resolution Least.

Intro.

Intro. (* x13 *)

Resolution Trans.

Resolution Incr.

Resolution Up.

Resolution x13.

Resolution x13.

Resolution Least.

Intro.
Intro. (* x27 *)
Resolution Trans.
Resolution Incr.
Resolution Up.
Resolution x27.
Resolution x27.

## 5.6 Prolégomènes à un Vernaculaire Mathématique

Dans l'exemple ci-dessus, on peut introduire des lemmes (c'est-à-dire des constantes) et rendre
ainsi la preuve de chaque proposition beaucoup plus courte.

Theorem Tarski.

Statement (Eq M (f M)).

Remark One.

Variable y:T.

Hypothesis v.

Assumes (Pre y).

Statement (R y (f M)).

Remark Rem.

Statement (R y M).

Resolution Up. Resolution v.

Remark Rem'.

Statement (R (f y) (f M)).

Resolution Incr. Resolution Rem.

Resolution Trans. Resolution Rem'. Resolution v.

Remark Two.

Statement (R M (f M)).

Resolution Least. Assumption One.

Remark Three.

Statement (R (f M) (f (f M))).

Resolution Incr. Resolution Two.

Remark Four.

Statement (R (f M) M).