Resolution Up. Resolution Three.

Resolution Antisym. Resolution Four. Resolution Two.

Cette façon d'écrire une preuve, contrairement à la précédente, au terme-preuve ou à la preuve en déduction naturelle, commence à ressembler à une preuve du théorème de Tarski telle qu'on peut la lire dans un livre de théorie des treillis.

Après de Bruijn, on appelle *vernaculaire mathématique* [4] [5] le langage dans lequel les démonstrations mathématiques sont écrites de manière naturelle par les mathématiciens. Une application de la démonstration automatique est la conception de langages formels aussi proches que possible du vernaculaire mathématique. En effet, en vernaculaire, une démonstration se présente souvent comme une liste de propositions telle que chaque proposition est *évidente* quand les précédentes sont connues. Le lecteur doit donc pour vérifier la correction de l'argumentation retrouver les petites preuves qui relient les propositions les unes aux autres. Pour qu'une machine également puisse vérifier la correction d'une telle argumentation, elle doit disposer d'un algorithme de synthèse de preuves. On écrira dans un tel formalisme la démonstration comme ci-dessus sauf que l'on remplacera les indications *Intro*, *Resolution* et *Assumption* par l'appel à un tel algorithme de synthèse de preuves auquel on indiquera, au plus, celles parmi les propositions précédentes qui peuvent être utilisées.

Pour que ce formalisme soit complet et que la correction d'une argumentation soit décidable, l'algorithme de synthèse de preuves doit être transitivement complet et toujours terminer. L'algorithme avec scission faible, accès aux axiomes et nombre d'itérations borné a ces propriétés.
Seconde partie

Résolution d'Equations
# Chapitre 6

## Unification

### 6.1 Unification Ouverte et Fermée

**Définition 75.** : Problème d'Unification

Un problème d'unification est un triplet $<\Gamma, a, b>$ tel que $\Gamma$ est un contexte quantifié (mais non contraint) bien formé et $a$ et $b$ deux termes normaux bien typés dans $\Gamma$.

**Définition 76.** : Solution (ouverte) d'un Problème d'Unification

Soit $<\Gamma, a, b>$ un problème d'unification, une solution (ouverte) de $<\Gamma, a, b>$ est une substitution $\theta$ bien typée dans $\Gamma$, telle que pour toute variable existentielle $x$ de $\Gamma$ le contexte associé à $x$ par $\theta$ ne comporte pas de contraintes (autres que triviales) et telle que les formes normales de $\theta a$ et $\theta b$ soient identiques. L'ensemble des solutions de $<\Gamma, a, b>$ est noté $U <\Gamma, a, b>$.

Au premier ordre et à l'ordre supérieur, la substitution $\theta$ n'est pas supposée instancier toutes les variables existentielles de $\Gamma$, elle peut même en introduire de nouvelles. Cette tolérance est due au fait qu'aussi bien au premier ordre qu'à l'ordre supérieur, tous les types sont supposés habités, donc l'existence d'un unificateur $\theta$ et d'un unificateur $\theta'$ tel que $\theta'\Gamma$ soit un contexte de succès est équivalente. Ce n'est plus le cas dans les systèmes de types où un type peut être habité ou vide. Ce qui motive la définition :

**Définition 77.** : Solution Fermée d'un Problème d'Unification

Soit $<\Gamma, a, b>$ un problème d'unification, une solution fermée de $<\Gamma, a, b>$ est une solution ouverte de $<\Gamma, a, b>$ telle que $\theta\Gamma$ soit un contexte de succès.

**Exemple** : Dans le contexte $\Gamma = [\exists x : (P : Prop)P]$ l'équation $x = x$ a une solution ouverte (l'identité) mais pas de solution fermée.

**Remarque** : Dans le problème de l'unification dans un contexte quantifié dans le $\lambda$-calcul simplement typé [51], les types ne sont pas tous habités, les notions d'unifiabilité ouverte et fermée ne sont donc plus équivalentes. La notion d'unifiabilité considérée est celle d'unifiabilité fermée.

### 6.2 Une Méthode d'Unification Fermée

**Proposition 45.** : Soit $<\Gamma, a, b>$ un problème d'unification et $\theta$ une substitution, $\theta$ est un unificateur fermé de $<\Gamma, a, b>$ si et seulement si $\theta(\Gamma[a = b])$ est un contexte de succès.
**Démonstration** : De façon évidente si $\theta$ est un unificateur de $<\Gamma, a, b>$, $\theta(\Gamma[a = b])$ est un contexte de succès. Réciproquement si $\theta(\Gamma[a = b])$ est un contexte de succès, alors $\theta$ est bien typée dans $\Gamma$ et pour toute variable existentielle $x$ de $\Gamma$ le contexte associé à $x$ par $\theta$ est un sous-contexte de $\theta(\Gamma[a = b])$ et donc ne comporte pas de contraintes autres que triviales, $\theta a = \theta b$ et $\theta \Gamma$ est un contexte de succès.

**Définition 78.** : Méthode d'Unification Fermée

Une méthode de semi-décision d'existence d'un unificateur fermé pour un problème $<\Gamma, a, b>$ consiste à appliquer la méthode développée au chapitre 4 au contexte $\Gamma[a = b]$. De plus, cet algorithme énumère tous les unificateurs fermés.

**Remarque** : Le lemme qui permet dans le cas de l'unification dans le $\lambda$-calcul simplement typé [40] [41] de résoudre trivialement les équations entre termes flexibles ne se généralise pas aux systèmes de types et une équation entre termes flexibles peut ne pas avoir de solution (fermée) puisque les variables de tête des équations peuvent avoir des types vides. De plus, il est montré dans [51] que dans le $\lambda$-calcul simplement typé, le problème de l'unification entre termes flexibles dans un contexte quantifié est indécidable. Cette preuve se généralise aisément aux systèmes de types.

## 6.3 Vers une Méthode d'Unification Ouverte

L'intérêt d'un algorithme d'unification ouverte n'est pas immédiat, car dans les algorithmes de synthèse de preuves (ou plus généralement dans les algorithmes qui utilisent l'unification) une variable existentielle est introduite pour être instanciée et non pour demeurer indéfiniment.

Si on cherche malgré tout un tel algorithme, on doit remarquer que le lemme qui permet dans le cas de l'unification dans le $\lambda$-calcul simplement typé [40] [41] de résoudre de façon immédiate les équations entre termes flexibles ne se généralise pas aux systèmes de types polymorphes.

**Proposition 46.** : Dans un système polymorphe, une équation entre termes flexibles peut ne pas avoir de solution ouverte.

**Démonstration** : Considérons le problème :

$$ \Gamma = [\forall A : \mathit{Prop}; \forall B : \mathit{Prop}; \forall u : A; \exists x : (P : \mathit{Prop})P] $$

$$ a = (x (A \to B) u) \quad b = (x B) $$

Les termes $a$ et $b$ sont flexibles. Pourtant le problème $<\Gamma, a, b>$ n'a pas de solution ouverte. En effet, supposons qu'il en ait une $\theta$ et posons $t = \theta x$. On a $t : (P : \mathit{Prop})P$, donc $t = [P : \mathit{Prop}]t'$ où $t'$ est de type $P$. Le terme $t'$ n'est donc ni une abstraction ni un produit. C'est un terme atomique ($f c_1 ... c_n$). Si on avait $f = P$, on aurait $n = 0$ et $t' = P$, ce qui est impossible pour des raisons de type, donc $f \neq P$. Comme $(t'[P \leftarrow (A \to B)] u) = t'[P \leftarrow B]$, on a :

$$ (f c_1[P \leftarrow (A \to B)] \dots c_n[P \leftarrow (A \to B)] u) = (f c_1[P \leftarrow B] \dots c_n[P \leftarrow B]) $$

Donc $(f c_1[P \leftarrow (A \to B)]) = f$, ce qui est impossible puisqu'une variable ne peut être une application.

Il semble difficile de décrire toutes les solutions des équations entre termes flexibles car la variable de tête d'une substitution élémentaire peut, a priori, être non seulement n'importe quelle variable du
contexte ou n'importe quelle variable liée, mais aussi n'importe quelle nouvelle variable. Il faudrait
donc utiliser un algorithme de synthèse de preuves similaire à celui développé précédemment mais
qui énumère toutes les preuves d'une proposition sous tous les ensembles d'axiomes possibles. Un
premier problème est donc de reconnaître les équations entre termes flexibles qui ont des solutions
et celles qui n'en n'ont pas et de garder les premières comme contraintes comme on le fait dans
l'unification dans le λ-calcul simplement typé. Dans ce cas, il n'est plus immédiat que les termes
considérés ont toujours une forme normale de tête. Il faut donc considérer la réduction d'un radical de
tête comme une étape de l'algorithme. Egalement des substitutions-produits doivent être appliquées
quand les variables de têtes des termes flexibles des équations (entre termes flexibles et entre un
terme flexible et un terme rigide) ont une variable de tête existentielle.

Dans l'état actuel de nos connaissances, l'unification ouverte nous apparaît donc être un problème
plutôt ardu et qui présente peu d'intérêt.
# Chapitre 7

## Equations Décidables

Dans le λ-calcul simplement typé, deux classes de problèmes sont connus comme décidables. L’unification du premier ordre [59] et le filtrage du deuxième ordre [41] [45].

L’unification du premier ordre a été récemment généralisée par Miller à l’*unification entre termes à arguments restreints* [51] [52], puis par Pfenning aux systèmes du cube [57]. Nous généralisons ici le filtrage du deuxième ordre aux systèmes du cube.

Un exemple d'application de ces algorithmes est la résolution automatique de certaines des contraintes dans un système d'aide à la mise au point de preuves par tactiques, tel que celui présenté au chapitre 5. L'unification du premier ordre (et entre termes à arguments restreints) est celle qui est effectivement utilisée dans ce prototype. Elle consiste après simplification à reconnaître les contraintes du type $x = t$ où $x$ est une variable existentielle et à instancier $x$ par $t$. (Dans le cas de l'unification entre termes à arguments restreints, on reconnaît aussi les contraintes $(x t_1 ... t_n) = t$ où $x$ est une variable existentielle et les $t_i$ sont des variables universelles distinctes déclarées à droite de $x$ dans $\Gamma$.)

Un exemple d'application du filtrage du second ordre est le cas de l'utilisation d'un axiome de récurrence avec un but fermé comme dans le cas considéré au paragraphe 5.5.2. Néanmoins cette possibilité d'application doit être modérée par le fait que la contrainte engendrée est un problème de filtrage du second ordre uniquement quand les types de données sont déclarés comme des variables de types (comme *Bool* dans l'exemple du chapitre 5) et leurs propriétés axiomatisées. Dès que les types de données sont définis, comme dans le cas des entiers de Church pour les entiers (où $Nat = (P : Prop)(P \to (P \to P) \to P)$) ou des projections pour les booléens (où $Bool = (P : Prop)(P \to P \to P)$), les contraintes obtenues ne sont plus du second ordre. En fait nous verrons au chapitre suivant que l'impératif de décidabilté du filtrage est incompatible avec celui de la richesse calculatoire du système considéré, ce qui suggère la nécessité d'un compromis.

### 7.1 Ordre d'un Type

Dans le λ-calcul simplement typé, on classe les types selon leur ordre de fonctionnalité. Les types du premier ordre sont ceux qui ne sont pas fonctionnels, c'est-à-dire les types atomiques. Les types du deuxième ordre sont les types des fonctions qui s'appliquent aux termes dont le type est du premier ordre, les types du troisième ordre sont les types des fonctionnelles qui s'appliquent à des termes dont le type est du deuxième ordre, etc. L'ordre d'un type est défini par $o(T) = 1$ si $T$
est atomique et $o(T \to U) = \max\{1 + o(T), o(U)\}$.

Dans les systèmes polymorphes, se pose le problème de l'ordre du type ($P : Prop)(P \to P$). En effet, en appliquant un terme de ce type on peut obtenir un terme dont le type a un ordre arbitrairement élevé. On prendra donc par convention l'ordre de ce type égal à l'infini. De même si $X$ est une variable existentielle de type $Prop$, $X$ peut être instanciée par un type d'ordre arbitraire, on prendra l'ordre de $X$ égal à l'infini.

**Définition 79.** : Ordre d'un Type

Soit $\Gamma$ un contexte et $T$ un type normal dans $\Gamma$. L'ordre de $T$ dans $\Gamma$ est défini comme l'élément suivant de $N \cup \{\infty\}$ :

- si $T = (y : U)V$, alors $o(T) = \max\{1 + u, v\}$ où $u$ est l'ordre de $U$ dans le contexte $\Gamma$ et $v$ l'ordre de $V$ dans le contexte $\Gamma[\exists y : U]$,

- si $T = (x t_1 \dots t_n)$, alors si $x$ est une variable universelle de $\Gamma$, alors $o(T) = 1$, si $x$ est une variable existentielle de $\Gamma$, alors $o(T) = \infty$ et si $x$ est une sorte, alors $o(T) = 2$.

**Remarque** : On prend la convention habituelle $n + \infty = \infty$ et $\max\{n, \infty\} = \infty$.

**Proposition 47.** : Soit $\Gamma$ un contexte, $T$ un type normal dans $\Gamma$ et $\sigma$ une substitution bien typée dans $\Gamma$, alors $\sigma T$ a un ordre dans $\sigma\Gamma$ inférieur ou égal à $o(T)$.

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

- Si $T = (y : U)V$, alors soit $u$ l'ordre de $\sigma U$ dans le contexte $\sigma\Gamma$ et $v$ l'ordre de $\sigma V$ dans le contexte $(\sigma\Gamma)[\exists y : \sigma U] = \sigma(\Gamma[\exists y : U])$, par hypothèse de récurrence $u \le o(U)$ et $v \le o(V)$ et donc $o(\sigma T) \le o(T)$,

- Si $T = (w t_1 \dots t_n)$, alors :

- si $w$ est universelle dans $\Gamma$, alors elle n'est pas instanciée par $\sigma$, donc $\sigma T = (w \sigma t_1 \dots \sigma t_n)$ et $o(\sigma T) = o(T) = 1$,

- si $w$ est une sorte, alors $o(\sigma T) = o(T) = 2$,

- si $w$ est existentielle dans $\Gamma$, alors $o(T) = \infty$ donc $o(\sigma T) \le o(T)$.

**Définition 80.** : Ordre d'un Problème d'Unification

On dit qu'un problème d'unification $< \Gamma, a, b >$ est d'ordre $n$ si le type de toutes les variables existentielles de $\Gamma$ est au plus d'ordre $n$.

## 7.2 Unification du Premier Ordre et Entre Termes à Arguments Restreints

L'unification du premier ordre [59] a été récemment généralisée par Miller à l'unification entre termes à arguments restreints [51] [52]. L'idée de cette généralisation est la suivante : considérons un problème d'unification du premier ordre sous un contexte quantifié $< \Gamma, a, b >$, imaginons que nous ayons dans $\Gamma$ une variable existentielle $x : T$ et juste à gauche de cette variable existentielle une variable universelle $c : U$. La variable $c$ peut apparaître dans un terme substitué à $x$. On peut marquer explicitement cette dépendance en antiskolémisant cette variable, c'est-à-dire en écrivant $x = (f c)$ où $f : U \to T$ est une variable déclarée juste à droite de $c$, et donc qui ne dépend pas de $c$. En remplaçant $x$ par $(f c)$ dans $a = b$ on obtient une équation $a' = b'$ qui n'est plus un problème du premier ordre car $f : U \to T$ peut avoir un ordre arbitraire. Malgré tout, résoudre ce problème
ne devrait pas être plus difficile que résoudre le problème initial puisque les solutions de celui-là sont les antiskolémisées des solutions de celui-ci.

Remarquons que dans le problème antiskolémisé la variable *f* ne peut apparaître que dans le terme (*f* *c*), c'est-à-dire que ses arguments sont toujours des variables universelles déclarées à sa droite. Cela motive la définition :

**Définition 81.** : Terme à Arguments Restreints

Soit $\Gamma$ un contexte quantifié et t un terme bien typé dans $\Gamma$. Le terme t est dit à arguments restreints si et seulement si tout sous-terme u de t qui a la forme $(x t_1 \dots t_n)$ où x est une variable existentielle est tel que les $t_i$ sont des termes $\eta$-équivalents à des variables universelles distinctes et déclarées à droite de x dans $\Gamma$.

**Remarque** : La définition originale est un peu plus générale, elle impose uniquement aux $t_i$ d'être $\eta$-équivalents à des termes atomiques dont les variables de tête sont universelles, distinctes et déclarées à droite de *x*

**Théorème 5.** : Décidabilité de l'Unification entre Termes à Arguments Restreints

L'unification entre termes à arguments restreints est décidable et quand un problème a une solution, il a une solution principale.

**Démonstration** : Voir [51] [52].

Ce théorème a été généralisé par Pfenning aux systèmes du cube [57].

## 7.3 Filtrage du Deuxième Ordre dans le λ-calcul Simplement Typé

Le second problème décidable dans le λ-calcul simplement typé est le filtrage du deuxième ordre [41] [45].

**Définition 82.** : Problème de Filtrage

On dit qu'un problème d'unification < Γ, a, b > est un problème de filtrage si le terme b est fermé dans Γ.

Dans [41] [45] les variables existentielles sont du deuxième ordre au plus et les variables universelles du troisième ordre au plus. On généralise ici ce problème de trois manières : (1) on considère un calcul quelconque du cube, (2) l'ordre des variables universelles est arbitraire, (3) le terme ouvert peut être non seulement du deuxième ordre mais aussi un terme à arguments restreints du deuxième ordre dans l'esprit de Miller et Pfenning. Outre son intérêt propre, la troisième généralisation est nécessaire pour atteindre les deux premières.

### 7.3.1 Avec Variables Universelles du Troisième Ordre au Plus

Commençons par nous placer dans le λ-calcul simplement typé. La méthode donnée dans [41] [45] consiste à appliquer l'algorithmme d'unification à l'ordre supérieur de [40] [41] qui termine si le problème considéré est un problème de filtrage du deuxième ordre.

**Proposition 48.** : L'algorithmme d'unification à l'ordre supérieur [40] [41] termine si le problème considéré est un problème de filtrage du deuxième ordre.
**Démonstration** : Le couple < λ', λ > où λ est la somme des tailles des termes de gauche et λ' la somme des tailles des termes de droite décroît strictement quand on applique une substitution élémentaire. Considérons une équation (f t₁ ... tₙ) = (F u₁ ... uₚ) avec f existentielle et F universelle. Dans une substitution élémentaire, on instancie f par un terme de la forme [x₁ : T₁]...[xₙ : Tₙ](w (h₁ x₁ ... xₙ)...(hq x₁ ... xₙ)). La variable w ne peut être que F ou l'un des xᵢ.

Si $w = F$ (imitation), le terme de gauche substitué commence par la variable $F$, l'équation se simplifie en des équations dont la somme des tailles des membres de droite est plus petite que la taille de $(F u_1 ... u_p)$. Si $w = x_i$ (projection), comme $f$ a un type au plus du deuxième ordre, $x_i$ a un type du premier ordre. On a donc $q = 0$ et la substitution est $f \leftarrow [x_1 : T_1]...[x_n : T_n]x_i$. Appliquer cette substitution fait diminuer la taille du terme de gauche en laissant le terme de droite inchangé.

**Remarque** : Il est aussi possible de prendre pour $\lambda$ le nombre de variables existentielles du problème.

### 7.3.2 Avec Variables Universelles Arbitraires

Dans [41] [45], les variables universelles sont au plus du troisième ordre car si on autorisait des variables universelles d'ordre plus grand, une substitution élémentaire d'imitation pourrait introduire des variables existentielles d'ordre strictement supérieur à deux. Par exemple dans le contexte :

$$[\forall T : Prop; \forall F : ((T \rightarrow T) \rightarrow T) \rightarrow T; \forall a : T; \exists f : T \rightarrow T]$$

on considère le problème :

$$(f a) = (F ([x : T \rightarrow T](x a)))$$

la substitution d'imitation est :

$$f \leftarrow [x : T](F(h x))$$

avec $h : T \rightarrow (T \rightarrow T) \rightarrow T$ qui est une variable du troisième ordre.

Malgré tout, quand on applique cette substitution, on obtient le problème :

$$(F(h a)) = (F ([x : T \rightarrow T](x a)))$$

La forme $\eta$-longue de ce problème est :

$$(F ([x : T \rightarrow T](h a [y : T](x y)))) = (F ([x : T \rightarrow T](x a)))$$

Et sa forme simplifiée :

$$(h a [y : T](x y)) = (x a)$$

Dans ce problème, la variable $h$ est appliquée à deux termes : $a$ qui était déjà un argument de $f$ et qui de ce fait est du premier ordre et $[y : T](x y)$ introduit lors de la $\eta$-expansion qui est donc $\eta$-équivalent à une variable universelle.

On généralise donc ainsi la notion de termes à arguments restreints :

**Définition 83.** : Terme à Arguments Restreints du Deuxième Ordre

Un terme $t$ est dit à arguments restreints du deuxième ordre si tout sous-terme de $t$ de la forme $u = (x t_1 ... t_n)$ avec $x$ existentielle, est tel que pour tout $i$, $t_i$ est un terme du premier ordre ou bien un terme $\eta$-équivalent à une variable universelle.
De même appelons problème de filtrage à arguments restreints du deuxième ordre un problème dont l'un des termes est à arguments restreints du deuxième ordre et l'autre fermé.

Toute substitution élémentaire appliquée à un problème à arguments restreints du deuxième ordre donne un problème à arguments restreints du deuxième ordre.

L'argument de terminaison de [41] [45] se généralise aux problèmes à arguments restreints du deuxième ordre. En effet, les imitations et les projections sur les termes η-équivalents à une variable universelle font décroître λ' et les projections sur les terme du premier ordre font décroître λ.

## 7.4 Filtrage du Deuxième Ordre dans les Systèmes de Types

### 7.4.1 Termes à Arguments Restreints du Deuxième Ordre

Dans les systèmes de types, une autre situation où les termes à arguments restreints du deuxième ordre apparaissent est l'application d'une substitution-produit. Par exemple dans le contexte :

$$[\forall T : Prop; \forall a : T; \forall Q : Prop; \exists f : T \to Prop]$$

on considère le problème :

$$(f a) = (P : Prop)Q$$

On lui applique la substitution élémentaire :

$$f \leftarrow [x : T](P : (h x))(k x P)$$

avec $h : T \to s$ et $k : (x : T)((h x) \to Prop)$. La variable $k$ a un ordre infini, mais ici encore dans le problème :

$$(P : (h a))(k a P) = (P : Prop)Q$$

elle n'est appliquée qu'à des termes du premier ordre et des termes η-équivalents à une variable universelle.

**Définition 84.** : Terme du Deuxième Ordre

Soit $\Gamma$ un contexte et $t$ un terme bien typé dans $\Gamma$. Le terme $t$ est dit du deuxième ordre dans $\Gamma$ si pour toute variable $x$ de type $T$ libre dans $t$,

- si $x$ est existentielle dans $\Gamma$, alors $T$ est d'ordre au plus 2,

- et $T$ est un terme du deuxième ordre dans le préfixe de $\Gamma$ déclaré à gauche de $x$.

**Définition 85.** : Terme à Arguments Restreints du Deuxième Ordre

Soit $\Gamma$ un contexte et $t$ un terme normal bien typé dans $\Gamma$. Le terme $t$ est dit à arguments restreints du deuxième ordre dans les cas suivants :

- $t = [x : T]u$ où $T$ est un terme à arguments restreints du deuxième ordre dans $\Gamma$ et $u$ un terme à arguments restreints du deuxième ordre dans $\Gamma[\forall x : T]$,

- $t = (x : T)u$ où $T$ est un terme à arguments restreints du deuxième ordre dans $\Gamma$ et $u$ a un terme à arguments restreints du deuxième ordre dans $\Gamma[\forall x : T]$,

- $t = (x c_1 ... c_n)$ où $x$ est une variable universelle dans $\Gamma$ et $c_1, ..., c_n$ des termes à arguments restreints du deuxième ordre dans $\Gamma$ et le type de $x$ un terme à arguments restreints du deuxième ordre dans le préfixe de $\Gamma$ déclaré à gauche de $x$,
- $t = (x c_1 \dots c_n)$ où $x$ est une variable existentielle et pour tout $i$, $c_i$ est un terme dont le type est du premier ordre dans $\Gamma$ ou un terme $\eta$-équivalent à une variable universelle de $\Gamma$, $c_i$ est un terme à arguments restreints du deuxième ordre dans $\Gamma$ et le type de $x$ est un terme à arguments restreints du deuxième ordre dans le préfixe de $\Gamma$ déclaré à gauche de $x$,

- $t$ est une sorte.

**Proposition 49.** : *Un terme du deuxième ordre est à arguments restreints du deuxième ordre.*

**Démonstration** : Par récurrence sur la structure de $t$, tous les cas sont triviaux sauf celui où $t = (x c_1 \dots c_n)$ avec $x$ existentielle. Dans ce cas, le type de $x$ est d'ordre au plus 2, donc les types des $c_i$ sont du premier ordre.

**Proposition 50.** : *Soit $t$ un terme à arguments restreints du deuxième ordre, et $t'$ la forme $\eta$-longue de $t$. Le terme $t'$ est un terme à arguments restreints du deuxième ordre.*

**Démonstration** : Par récurrence sur $\mu(t)$ :

- Si $t = [x : T]u$, alors soit $T'$ la forme $\eta$-longue de $T$ et $u'$ la forme $\eta$-longue de $u$, par hypothèse de récurrence $T'$ et $u'$ sont des termes à arguments restreints du deuxième ordre. Le terme $t' = [x : T']u'$ est donc à arguments restreints du deuxième ordre.

- Si $t = (x : T)u$, alors soit $T'$ la forme $\eta$-longue de $T$ et $u'$ la forme $\eta$-longue de $u$, par hypothèse de récurrence $T'$ et $u'$ sont des termes à arguments restreints du deuxième ordre. Le terme $t' = (x : T')u'$ est donc à arguments restreints du deuxième ordre.

- Si $t = (x c_1 \dots c_n)$ et $x$ est une variable universelle ou une sorte, alors par hypothèse de récurrence les $c'_i$, les $T'_j$ et les $x'_k$ sont à arguments restreints du deuxième ordre. Donc le terme $t' = [x_1 : T'_1] \dots [x_p : T'_p](x c'_1 \dots c'_n x'_1 \dots x'_p)$ est à arguments restreints du deuxième ordre.

- Si $t = (x c_1 \dots c_n)$ et $x$ est une variable existentielle, alors par hypothèse de récurrence les $c'_i$, les $T'_j$ et les $x'_k$ sont des termes à arguments restreints du deuxième ordre, si $c_i$ a un type du premier ordre, alors $c'_i$ aussi et si $c_i$ est $\eta$-équivalent à une variable universelle de $\Gamma$, alors $c'_i$ aussi. Les termes $x'_j$ sont $\eta$-équivalents à une variable liée et le type de $x$ est à arguments restreints du deuxième ordre. Le terme $t' = [x_1 : T'_1] \dots [x_p : T'_p](x c'_1 \dots c'_n x'_1 \dots x'_p)$ est donc à arguments restreints du deuxième ordre.

## 7.4.2 Equations de Garantie

### Equations de Garantie

Dans le $\lambda$-calcul simplement typé, avant d'appliquer une substitution élémentaire, il faut vérifier que le terme substitué et la variable à laquelle on le substitue ont même type. Comme l'ont remarqué Elliott [20] [21] et Pym [58], dans les systèmes de types, avant d'appliquer une substitution élémentaire, $x \leftarrow \gamma$, $t$ il faut unifier les types de $x$ et $t$. En général, cette équation de garantie est un problème d'unification qui peut avoir des variables existentielles dans les deux membres. Mais nous allons montrer que si le problème initial est un problème de filtrage à arguments restreints du deuxième ordre, alors cette équation de garantie est aussi un problème de filtrage à arguments restreints du deuxième ordre et peut donc être résolue.

Le lemme clé montre que si $\Gamma$ est un contexte et $t = (u c_1 \dots c_n)$ un terme à arguments restreints du deuxième ordre dont le type est fermé dans $\Gamma$ et que le type de la variable $u$ est $(x_1 : P_1) \dots (x_n : P_n) P$ (P atomique), alors $P$ est fermé dans $\Gamma[\forall x_1 : P_1; \dots; \forall x_n : P_n]$.
L'intuition est que le type de $(u c_1 ... c_n)$ est $P[x_1 \leftarrow c_1, ..., x_n \leftarrow c_n]$. Ce terme est fermé, donc $P$ doit également être fermé car les $c_i$ sont des termes atomiques ou des termes $\eta$-équivalents à une variable universelle et leur substitution ne peut donc pas effacer de variables existentielles dans $P$. Prouvons ce lemme :

**Proposition 51.** : Soit $\Gamma$ un contexte, $c$ et $T$ deux termes bien typés dans $\Gamma$ tel que le type de $c$ soit $T$ et $P$ un terme normal, en forme $\eta$-longue, bien typé dans le contexte $\Gamma[\forall x : T]$.

Si le terme $c$ a un type du premier ordre ou est $\eta$-équivalent à une variable universelle et $P$ est atomique, alors $P[x \leftarrow c]$ est atomique.

**Démonstration** : Si $P = (y c_1 ... c_n)$ où $y \neq x$, alors $P[x \leftarrow c] = (y c_1[x \leftarrow c] ... c_n[x \leftarrow c])$ qui est atomique. Si $P = (x c_1 ... c_n)$, alors si $c$ a un type du premier ordre, $x$ a aussi un type du premier ordre, donc $n = 0$, $P = x$, $P[x \leftarrow c] = c$ est un terme atomique, si $c$ est $\eta$-équivalent à une variable universelle $z$, alors $P[x \leftarrow c] = (z c_1[x \leftarrow c] ... c_n[x \leftarrow c])$ qui est atomique.

**Proposition 52.** : Soit $\Gamma$ un contexte et $t = (x c_1 ... c_n)$ un terme bien typé, à arguments restreints du deuxième ordre, en forme $\eta$-longue et $x : (x_1 : P_1)...(x_p : P_p)P$ ($P$ atomique) une variable existentielle. Alors $p = n$.

**Démonstration** : Le terme $(x c_1 ... c_n)$ n'est pas une abstraction et est en forme $\eta$-longue, donc son type n'est pas un produit. Donc $p \leq n$, en effet si on avait $n < p$ le terme $(x c_1 ... c_n)$ aurait le type :

$$ (x_{n+1} : P_{n+1}[x_1 \leftarrow c_1, ..., x_n \leftarrow c_n])...(x_p : P_p[x_1 \leftarrow c_1, ..., x_n \leftarrow c_n])P[x_1 \leftarrow c_1, ..., x_n \leftarrow c_n] $$

qui est un produit.

Le type du terme $(x c_1 ... c_p)$ est $P[x_1 \leftarrow c_1, ..., x_p \leftarrow c_p]$. Comme le terme $P$ est atomique et tous les $c_i$ sont des termes dont le type est du premier ordre ou qui sont $\eta$-équivalents à une variable universelle, le terme $P[x_1 \leftarrow c_1, ..., x_p \leftarrow c_p]$ est aussi atomique, alors si on avait $n > p$, le terme $(x c_1 ... c_n)$ serait mal typé. Donc $n = p$.

**Proposition 53.** : Soit $\Gamma$ un contexte, $c$ et $T$ deux termes bien typés dans $\Gamma$ tels que le type de $c$ soit $T$ et $P$ un terme bien typé dans le contexte $\Gamma[\forall x : T]$. Si $c$ a un type du premier ordre ou est un terme $\eta$-équivalent à une variable universelle, alors toute variable $y$, $y \neq x$ qui a une occurrence dans $P$ a aussi une occurrence dans la forme normale de $P[x \leftarrow c]$.

**Démonstration** : Par récurrence sur la structure de $P$. Le résultat est immédiat si $P$ est une abstraction, un produit ou un terme atomique avec une tête différente de $x$. Si $P = (x c_1 ... c_n)$, alors si $c$ a un type du premier ordre, $x$ aussi, donc $n = 0$, $P = x$ et il n'y a pas de variable $y \neq x$ qui ait une occurrence dans $P$, si $c$ est $\eta$-équivalent à une variable universelle $z$, alors la forme normale de $P[x \leftarrow c]$ est la forme normale de $(z c_1[x \leftarrow c] ... c_n[x \leftarrow c])$. La variable $y$ a une occurrence dans l'un des $c_i$, par hypothèse de récurrence, elle a aussi une occurrence dans la forme normale de $c_i[x \leftarrow c]$, elle a donc une occurrence dans la forme normale de $P[x \leftarrow c]$.

**Proposition 54.** : Soit $\Gamma$ un contexte, $c$ et $T$ deux termes bien typés dans $\Gamma$ tels que le type de $c$ soit $T$ et $P$ un terme bien typé dans le contexte $\Gamma[\forall x : T]$.

Si la variable $x$ a une occurrence dans $P$ et $c$ a un type du premier ordre ou est un terme $\eta$-équivalent à une variable universelle, alors toute variable $y$ qui a une occurrence dans $c$ en a aussi une dans la forme normale de $P[x \leftarrow c]$.
**Démonstration** : Par récurrence sur la structure de $P$. Le résultat est immédiat si $P$ est une abstraction, un produit ou un terme atomique avec une tête différente de $x$. Si $P = (x c_1 ... c_n)$, alors si $c$ a un type du premier ordre, $x$ aussi, $n = 0$, $P = x$, $P[x \leftarrow c] = c$, donc $y$ a une occurrence dans la forme normale de $P[x \leftarrow c]$, si $c$ est η-équivalent à une variable universelle $z$, alors la forme normale de $P[x \leftarrow c]$ est la forme normale de $(z c_1[x \leftarrow c] ... c_n[x \leftarrow c])$. La variable $y$ a une occurrence dans $c$, donc $y = z$ a une occurrence dans la forme normale de $P[x \leftarrow c]$.

**Proposition 55.** : *Soit $\Gamma$ un contexte et $P_1, ..., P_n$ des termes tels que $\Gamma' = \Gamma[\forall x_1 : P_1; ..., \forall x_n : P_n]$ est un contexte bien formé. Soit $P_{n+1}$ un terme et s une sorte tels que $\Gamma' \vdash P_{n+1} : s$. Soit $c$ un terme tel que $\Gamma \vdash c : P_1$. On a $\Gamma[\forall x_2 : P_2[x_1 \leftarrow c]; ...; \forall x_n : P_n[x_1 \leftarrow c]] \vdash P_{n+1}[x_1 \leftarrow c] : s$.*

*Si le terme $P_{n+1}[x_1 \leftarrow c]$ est fermé dans $\Gamma[\forall x_2 : P_2[x_1 \leftarrow c]; ...; \forall x_n : P_n[x_1 \leftarrow c]]$, alors $P_{n+1}$ est fermé dans $\Gamma'$.*

**Démonstration** : On considère le plus petit ensemble $I$ inclus dans $\{2, ..., n+1\}$ tel que $n+1 \in I$ et si $j \in I$ et $x_i$ est une variable libre de la forme normale de $P_j[x_1 \leftarrow c]$, alors $i \in I$.

On prouve par récurrence descendante que pour tout $i \in I$, la forme normale du terme $P_i[x_1 \leftarrow c]$ est fermée dans le contexte $\Gamma[\forall x_2 : P_2[x_1 \leftarrow c]; ...; \forall x_n : P_n[x_1 \leftarrow c]]$. Pour $i = n + 1$, c'est vrai par hypothèse. Pour $i \neq n + 1$, $x_i$ a une occurrence dans la forme normale de $P_j[x_1 \leftarrow c]$ pour $j > i$, par hypothèse de récurrence, ce terme est fermé, donc le type de $x_i$ dans $\Gamma'$ est fermé, c'est-à-dire que la forme normale de $P_i[x_1 \leftarrow c]$ est un terme fermé.

Ensuite on prouve que si $x_1$ a une occurrence dans l'un des $P_i$ ($i \in I$), alors $P_1$ est fermé. En effet si $x_1$ a une occurrence dans $P_i$, alors toutes les variables qui ont un occurrence dans $c$ ont aussi une occurrence dans la forme normale de $P_i[x_1 \leftarrow c]$. Le terme $c$ est de ce fait fermé, et donc son type $P_1$ également.

On montre ensuite par récurrence que pour tout $i \in I$, $P_i$ est fermé. Supposons que cela est vrai pour tous les $j < i$ et soit $x$ une variable libre arbitraire de $P_i$, si $x = x_1$, alors $x$ est universelle et son type est fermé, sinon $x$ est aussi une variable libre de la forme normale de $P_i[x_1 \leftarrow c]$. C'est donc une variable universelle. Si c'est l'une des $x_j$, alors $j \in I$ et par hypothèse de récurrence son type $P_j$ est fermé. Si c'est une variable déclarée dans $\Gamma$, alors son type est le même dans $\Gamma[\forall x_1 : P_1; \forall x_2 : P_2; ...; \forall x_{n+1} : P_{n+1}]$ que dans $\Gamma[\forall x_2 : P_2[x_1 \leftarrow c]; ...; \forall x_{n+1} : P_{n+1}[x_1 \leftarrow c]]$ et donc ce type est fermé.

Enfin on conclut que comme $n + 1 \in I$, $P_{n+1}$ est fermé dans $\Gamma[\forall x_1 : P_1; ...; \forall x_n : P_n]$.

**Proposition 56.** : *Soit $\Gamma$ un contexte, $P_1, ..., P_n$ des termes tels que $\Gamma' = \Gamma[\forall x_1 : P_1; ..., \forall x_n : P_n]$ est un contexte bien formé. Soit $P_{n+1}$ un terme et s une sorte tels que $\Gamma' \vdash P_{n+1} : s$. Soit $c_i$ des termes tels que $\Gamma \vdash c_i : P_i[x_1 \leftarrow c_1, ..., x_{i-1} \leftarrow c_{i-1}]$. On a $\Gamma \vdash P_{n+1}[x_1 \leftarrow c_1, ..., x_n \leftarrow c_n] : s$.*

*Si le terme $P_{n+1}[x_1 \leftarrow c_1, ..., x_n \leftarrow c_n]$ est fermé dans $\Gamma$, alors $P$ est fermé dans $\Gamma'$.*

**Démonstration** : Par récurrence sur $n$.

**Lemme 5.** : *Soit $\Gamma$ un contexte et $(u c_1 ... c_n)$ un terme à arguments restreints du deuxième ordre bien typé dans $\Gamma$. On a $\Gamma \vdash u : (x_1 : P_1)...(x_n : P_n)P$ (P atomique).*

*Si le terme $(u c_1 ... c_n)$ a un type fermé dans $\Gamma$, alors $P$ est fermé dans $\Gamma[\forall x_1 : P_1; ...; \forall x_n : P_n]$.*

**Démonstration** : Le type de $(u c_1 ... c_n)$ est $P[x_1 \leftarrow c_1, ..., x_n \leftarrow c_n]$. Ce type est fermé dans $\Gamma$ et donc $P$ est fermé dans $\Gamma[\forall x_1 : P_1; ...; \forall x_n : P_n]$.

On démontre aussi la proposition suivante :
**Proposition 57.** : Soit $\Gamma$ un contexte et $(u c_1 \dots c_n)$ un terme à arguments restreints du deuxième ordre bien typé dans $\Gamma$. On a $\Gamma \vdash u : (x_1 : P_1)\dots(x_n : P_n)P$.

Si $c_i$ est $\eta$-équivalent à une variable universelle $v$ qui a un type fermé dans $\Gamma$, alors $P_i$ est fermé dans le contexte $\Gamma[\forall x_1 : P_1; \dots; \forall x_{i-1} : P_{i-1}]$.

**Démonstration** : Le type de $(u c_1 \dots c_{i-1})$ est :

$$ (x_i : P_i[x_1 \leftarrow c_1, \dots, x_{i-1} \leftarrow c_{i-1}])\dots(x_n : P_n[x_1 \leftarrow c_1, \dots, x_{i-1} \leftarrow c_{i-1}])P[x_1 \leftarrow c_1, \dots, x_{i-1} \leftarrow c_{i-1}] $$

Le terme $P_i[x_1 \leftarrow c_1, \dots, x_{i-1} \leftarrow c_{i-1}]$ est le type de $c_i$, c'est-à-dire le type de $v$, c'est donc un terme fermé dans $\Gamma$. Donc $P_i$ est fermé dans $\Gamma[\forall x_1 : P_1; \dots; \forall x_{i-1} : P_{i-1}]$.

## Terminaison

Nous devons à présent montrer que le fait d'avoir à résoudre cette équation de garantie avant chaque substitution ne met pas en péril la propriété de terminaison de l'algorithme. C'est-à-dire que cette équation de garantie est plus petite pour une certaine mesure que l'équation initiale. Pour cela, on utilise la propriété de bonne fondation de la relation <.

**Définition 86.** : Complexité d'un Terme

Soit $\Gamma$ un contexte 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 <, la complexité $\kappa(t_\Gamma)$ de $t_\Gamma$ :

- Si $t$ est une sorte, alors $\kappa(t_\Gamma) = 1$,

- si $t$ est une variable, alors $\kappa(t_\Gamma) = 1 + \kappa(T_\Gamma)$,

- si $t = (u v)$, alors $\kappa(t_\Gamma) = \kappa(u_\Gamma) + \kappa(v_\Gamma) + \kappa(T_\Gamma)$,

- si $t = [x : U]u$, alors $\kappa(t_\Gamma) = \kappa(U_\Gamma) + \kappa(u_{\Gamma[x:U]}) + \kappa(T_\Gamma)$,

- si $t = (x : U)V$, alors $\kappa(t_\Gamma) = \kappa(U_\Gamma) + \kappa(V_{\Gamma[x:U]}) + \kappa(T_\Gamma)$.

**Définition 87.** : Complexité d'un Problème

La complexité d'un problème $< \Gamma, a, b >$ est le couple $\kappa(< \Gamma, a, b >) = < \kappa(b), \text{ex}(\Gamma) >$ où $\text{ex}(\Gamma)$ est la nombre de variables existentielles déclarées dans $\Gamma$.

**Proposition 58.** : Soit $t_\Gamma$ un sous-terme strict de $u_\Delta$. On a $\kappa(t) < \kappa(u)$.

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

**Proposition 59.** : Soit $\Gamma$ un contexte, $c$ et $T$ deux termes bien typés dans $\Gamma$ et $P$ un terme bien typé dans $\Gamma[\forall x : T]$. Si le terme $c$ a un type du premier ordre ou est $\eta$-équivalent à une variable universelle et qu'on pose $P'$ la forme normale de $P[x \leftarrow c]$, alors on a $\kappa(P) \le \kappa(P')$.

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

**Proposition 60.** : Soit $\Gamma$ un contexte bien formé et $a$ et $b$ deux termes du même type, tels que $a = (u c_1 \dots c_n)$ soit un terme à arguments restreints du deuxième ordre et $u : (x_1 : P_1)\dots(x_n : P_n)P$ est une variable existentielle de $\Gamma$. Si $b$ n'est pas une sorte, alors $\kappa(P) < \kappa(b)$.

**Démonstration** : On remarque d'abord que comme $b$ n'est pas une sorte, on a $\kappa(Q) < \kappa(b)$. Ensuite le type de $a$ et $b$ est $Q$ la forme normale de $P[x_1 \leftarrow c_1, \dots, x_n \leftarrow c_n]$ et on a $\kappa(P) \le \kappa(Q) < \kappa(b)$.
### 7.4.3 Type des Nouvelles Variables

Nous avons vu que dans les calculs polymorphes une variable $v$ dont le type commence par $p$ produits pouvait être appliquée plus de $p$ fois. Donc au moment où on applique une substitution élémentaire on n'a pas toujours toute l'information nécessaire pour calculer le type des nouvelles variables. Par exemple dans le contexte :

$$[\forall T : Prop; \forall U : Prop; \forall v : (P : Prop)P; \forall a : T; \forall G : (Prop \to T) \to Prop; \exists f : Prop \to T]$$

on considère le problème :

$$(f U) = (v (T \to T) a)$$

On veut appliquer la substitution :

$$f \leftarrow [p : Prop](v (h_1 p) (h_2 p))$$

La variable $h_1$ a le type $Prop \to Prop$ mais comme le terme $(v (h_1 p))$ a le type $(h_1 p)$ qui n'est pas encore un produit, on ne peut pas donner de type à la variable $h_2$.

Si on appliquait cette substitution on obtiendrait le problème :

$$(v (h_1 U) (h_2 U)) = (v (T \to T) a)$$

qui se simplifie en le système :

$$(h_1 U) = (T \to T)$$

$$(h_2 U) = a$$

L'idée est de résoudre d'abord la première de ces équations dérivées et de donner ensuite un type à la variable $h_2$. Cette équation a une solution :

$$h_1 \leftarrow [p : Prop](T \to T)$$

Le terme $(v (T \to T))$ a le type $T \to T$, on donne donc le type $Prop \to T$ à $h_2$ et on peut résoudre la deuxième équation :

$$(h_2 U) = a$$

Montrons maintenant que dans le cas général comme dans cet exemple, quand on a résolu les $k$ premières équations dérivées, le type de $(v ((\sigma h_1) x_1 \dots x_n) ((\sigma h_k) x_1 \dots x_n))$ est un produit.

**Proposition 61.** : Soit $\Gamma$ un contexte. Soit $u : (x_1 : P_1)...(x_n : P_n)P$ une variable existentielle de ce contexte. Soient $(u c_1 \dots c_n)$ un terme bien typé dans $\Gamma$ à arguments restreints du deuxième ordre, $(v d_1 \dots d_p)$ un terme bien typé dans $\Gamma$ et $w$ une variable telle que $w[x_1 \leftarrow c_1, \dots, x_n \leftarrow c_n] = v$. Soit $k$ un entier $0 \le k \le p-1$. Soient $\alpha_1, \dots, \alpha_k$ des termes bien typés dans $\Gamma$ tels que pour tout $i$, $1 \le i \le k$, $(\alpha_i c_1 \dots c_n) = d_i$ et tels que pour tout $i$ strictement inférieur à $k$, le terme $(w (\alpha_1 x_1 \dots x_n)...(\alpha_i x_1 \dots x_n))$ est bien typé dans $\Gamma[\forall x_1 : P_1; \dots; \forall x_n : P_n]$, son type est un produit $(x : T)T'$ et $\alpha_{i+1}$ a le type $(x_1 : P_1)...(x_n : P_n)T$.

Alors le terme $(w (\alpha_1 x_1 \dots x_n)...(\alpha_k x_1 \dots x_n))$ est bien typé dans $\Gamma[\forall x_1 : P_1; \dots; \forall x_n : P_n]$ et son type est un produit.
**Démonstration** : On a :

$$ (v d_1 \dots d_k) = (v (\alpha_1 c_1 \dots c_n) \dots (\alpha_k c_1 \dots c_n)) \\ = (w (\alpha_1 x_1 \dots x_n) \dots (\alpha_k x_1 \dots x_n))[x_1 \leftarrow c_1, \dots, x_n \leftarrow c_n] $$

Le terme $(v d_1 \dots d_k)$ est bien typé dans $\Gamma$ et son type est un produit, il en est donc de même du type de $(w (\alpha_1 x_1 \dots x_n) \dots (\alpha_k x_1 \dots x_n))[x_1 \leftarrow c_1, \dots, x_n \leftarrow c_n]$.

Soit $U$ le type du terme $(w (\alpha_1 x_1 \dots x_n) \dots (\alpha_k x_1 \dots x_n))$ dans $\Gamma[\forall x_1 : P_1; \dots; \forall x_n : P_n]$. Le terme $U[x_1 \leftarrow c_1, \dots, x_n \leftarrow c_n]$ est un produit.

Si le terme $U$ était atomique, il en serait de même de $U[x_1 \leftarrow c_1, \dots, x_n \leftarrow c_n]$ puisque les $c_i$ ont un type de premier ordre ou sont $\eta$-équivalents à une variable universelle. Le terme $U$ est donc un produit.

**Non Linéarité**

Dans l'exemple précédent, la variable $f$ n'a qu'une occurrence dans le problème et de ce fait $h_2$ n'avait pas d'occurrence dans la première équation dérivée. Si on considère à présent le problème :

$$ (f (G f)) = (v (T \rightarrow T) a) $$

en considérant à nouveau la substitution :

$$ f \leftarrow [p : \text{Prop}](v (h_1 p) (h_2 p)) $$

on peut toujours donner un type à $h_1$ mais pas à $h_2$. Et $h_2$ a une occurrence dans la première équation :

$$ (h_1 (G [p : \text{Prop}](v (h_1 p) (h_2 p)))) = (T \rightarrow T) $$

L'idée est de garder la variable $f$ dans l'équation :

$$ (h_1 (G f)) = (T \rightarrow T) $$

Pour chaque substitution $\sigma$ solution des équations dérivées, on veut instancier $f$ par le terme $t_1 = [p : \text{Prop}](v (\sigma h_1 p) (\sigma h_2 p))$, mais $f$ peut être déjà instancié par $t_2 = \sigma f$. A priori il faut unifier $t_1$ et $t_2$.

En fait nous allons voir que dans une substitution solution d'un problème de filtrage, une variable est ou bien invariante, ou bien instanciée par un terme sans variables existentielles et que, de plus, la variable tête du terme flexible est toujours instanciée par un terme sans variables existentielles. Donc le terme $t_1$ est sans variables existentielles et le terme $t_2$ est ou bien la variable $f$ ou bien un terme sans variables existentielles. Trois cas peuvent donc se produire : si $t_2$ est la variable $f$, alors $\sigma \cup \{<f, [ ], t_1 >\}$ est une solution du problème initial, si $t_1$ est sans variables existentielles et différent de $t_2$, alors $\sigma$ ne mène pas à une solution du problème initial, si $t_1 = t_2$, alors $\sigma$ est une solution du problème initial.
### 7.4.4 Un Algorithme de Filtrage

On considère maintenant des problèmes de filtrage $<\Gamma, a, b>$ tels que $\Gamma$ est un contexte quantifié bien formé dans le système de types *Méta*, $a$ et $b$ sont des termes normaux bien typés dans le système de types *Méta* dans le contexte $\Gamma$ et leur type est également bien typé dans $\Gamma$ (c'est-à-dire est différent de *Extern*). Le terme $a$ est à arguments restreints du deuxième ordre et le terme $b$ est fermé.

Par rapport à [41] [45], nous devons renforcer le contrôle sur l'algorithme. Nous définissons par récurrence sur $\kappa(<\Gamma, a, b>)$ une fonction *Sol* qui prend en argument un problème $<\Gamma, a, b>$ et retourne un ensemble de substitutions solutions du problème $<\Gamma, a, b>$.

Nous utilisons les symboles $\Sigma, \Upsilon, \Phi, \Psi, \Omega$ pour des ensembles de substitutions, étapes intermédiaires dans la construction de $Sol <\Gamma, a, b>$.

**Définition 88. : Insertion**

Soit $\Gamma$ un contexte, $x$ une variable de $\Gamma$. Soit $\Delta$ et $\Delta'$ tels que $\Gamma = \Delta[Qx : T]\Delta'$. Soit $d$ une déclaration. Le contexte $\Delta$ $[d]$ $[Qx : T]$ $\Delta'$ est appelé l'insertion de $d$ à gauche de $x$ dans $\Gamma$.

**Notation** : Soit $\Sigma$ un ensemble de substitutions et $\sigma$ une substitution, on note $\Sigma \circ \sigma$ l'ensemble :

$$ \Sigma \circ \sigma = \{\tau \circ \sigma \mid \tau \in \Sigma\} $$

**Définition 89. : Algorithme de Filtrage**

- Si les termes $a$ et $b$ sont tous les deux des abstractions, modulo $\alpha$-conversion, on peut considérer que la variable liée dans ces abstractions est la même et est différente de toutes les variables de $\Gamma$, $a = [x : U]c$ et $b = [x : U]d$. On pose :

$$ Sol <\Gamma, a, b> = Sol <\Gamma[\forall x : U], c, d > $$

- Si les termes $a$ et $b$ sont tous les deux des produits, modulo $\alpha$-conversion, on peut considérer que la variable liée dans ces produits est la même et est différente de toutes les variables de $\Gamma$, $a = (x : U)U'$ et $b = (x : V)V'$. Si $U$ et $V$ ont des types différents, alors $Sol <\Gamma, a, b> = \emptyset$, sinon on pose :

$$ \Sigma = Sol <\Gamma, U, V> $$

$$ Sol <\Gamma, a, b> = \cup_{\sigma \in \Sigma} (Sol <\sigma\Gamma[\forall x : V], \sigma U', V' > \circ \sigma) $$

- Si les termes $a$ et $b$ sont tous les deux atomiques et rigides avec la même tête et le même nombre d'arguments : $a = (v c_1 ... c_n)$ et $b = (v d_1 ... d_n)$, on pose :

$$ \Sigma_0 = \{\emptyset\} $$

$$ \Sigma_{i+1} = \cup_{\sigma \in \Sigma_i} (Sol <\sigma\Gamma, \sigma c_{i+1}, d_{i+1} > \circ \sigma) $$

$$ Sol <\Gamma, a, b> = \Sigma_n $$

- Dans tous les autres cas où $a$ et $b$ sont tous les deux rigides, on pose : $Sol <\Gamma, a, b> = \emptyset$.

Considérons maintenant le cas où le terme $a$ est flexible. Comme $a$ est atomique et en forme $\eta$-longue, le type commun de $a$ et $b$ n'est pas un produit, donc $b$ n'est pas une abstraction, c'est donc un produit ou un terme atomique.
- Si $a$ est atomique flexible $a = (u c_1 ... c_n)$ et $b$ est un produit $b = (y : V)V'$, alors posons $(x_1 : P_1)...(x_n : P_n)P$ ($P$ atomique) le type de $u$. Soit $s$ le type de $V$ dans $\Gamma$ et $s'$ le type de $V'$ dans $\Gamma[\forall y : V]$, $s$ et $s'$ sont des sortes.

On pose $\Gamma_1$ l'insertion à gauche de $u$ dans $\Gamma$ des déclarations $\exists h : (x_1 : P_1)...(x_n : P_n)s$ et $\exists k : (x_1 : P_1)...(x_n : P_n)(y : (h x_1 ... x_n))s'$. On pose :

$$ \Sigma = \mathrm{Sol} < \Gamma_1, (h c_1 ... c_n), V > $$

$$ \Upsilon = \cup_{\sigma \in \Sigma} (\mathrm{Sol} < \sigma(\Gamma_1[\forall y : V]), (k \sigma c_1 ... \sigma c_n y), V' > \circ \sigma) $$

Pour tout $\sigma \in \Upsilon$ on pose :

$$ t_{\sigma} = [x_1 : \sigma P_1]...[x_n : \sigma P_n](y : ((\sigma h) x_1 ... x_n)((\sigma k) x_1 ... x_n y)) $$

On pose :

$$ \mathrm{Sol} < \Gamma, a, b > = \{ \sigma \cup \{ < u, [ ], t_{\sigma} > \} \mid \sigma \in \Upsilon \text{ et } \sigma u = u \} \cup \{ \sigma \mid \sigma \in \Upsilon \text{ et } \sigma u = t_{\sigma} \} $$

- Si $a$ est atomique flexible $a = (u c_1 ... c_n)$ et $b$ est une sorte, alors posons $(x_1 : P_1)...(x_n : P_n)P$ ($P$ atomique) le type de $u$. On pose :

$$ \mathrm{Sol} < \Gamma, a, b > = \{ < u, [ ], [x_1 : P_1]...[x_n : P_n]b > \} $$

- Si $a$ est atomique flexible $a = (u c_1 ... c_n)$ et $b$ atomique $b = (v d_1 ... d_p)$ avec $v$ universelle, on a $u : (x_1 : P_1)...(x_n : P_n)P$ ($P$ atomique).

On pose $\Gamma' = \Gamma[\forall x_1 : P_1; ...; \forall x_n : P_n]$. Le terme $P$ est fermé dans $\Gamma'$.

Soit Heads l'ensemble contenant tous les $x_i$ tel que $c_i$ a un type du premier ordre ou est $\eta$-équivalent à $v$. Egalement si la variable $u$ est déclarée à droite de $v$, la variable $v$ est dans Heads.

- Pour toute variable $x_i$ de Heads telle que $c_i$ a un type du premier ordre, les termes $P$ et $P_i$ sont bien typés dans $\Gamma'$ et leurs types sont des sortes. Si ces sortes sont différentes, alors $\Omega_{x_i} = \emptyset$, sinon on pose :

$$ \Sigma_{x_i} = \{ \{ < u, [ ], [x_1 : \sigma P_1]...[x_n : \sigma P_n]x_i > \} \circ \sigma \mid \sigma \in \mathrm{Sol} < \Gamma', P_i, P > \} $$

$$ \Omega_{x_i} = \cup_{\sigma \in \Sigma_{x_i}} (\mathrm{Sol} < \sigma \Gamma, \sigma a, b > \circ \sigma) $$

- Pour toute variable $w$ de Heads telle que $w = v$ ou $w = x_i$ où $c_i$ est $\eta$-équivalent à $v$, par récurrence sur $i$ on construit $\Sigma_{w,i}$ l'ensemble des substitutions qui lient des variables de $\Gamma$ et aussi des variables supplémentaires $h_1, ..., h_i$.

$$ \Sigma_{w,0} = \{ \emptyset \} $$

Pour tout $\sigma \in \Sigma_{w,i}$, le terme $(w ((\sigma h_1) x_1 ... x_n) ... ((\sigma h_i) x_1 ... x_n))$ est bien typé dans $\sigma \Gamma'$ et son type est un produit $(y : T)T'$. Soit $\Gamma_{i+1}$ l'insertion à gauche de $u$ dans $\Gamma'$ de la déclaration $\exists h_{i+1} : (x_1 : P_1)...(x_n : P_n)T$. Soit $H_{i+1} = T[x_1 \leftarrow \sigma c_1, ..., x_n \leftarrow \sigma c_n]$ qui est le type de $(h_{i+1} \sigma c_1 ... \sigma c_n)$ dans $\sigma \Gamma_{i+1}$, et $D_{i+1}$ le type de $d_{i+1}$.

Les termes $H_{i+1}$ et $D_{i+1}$ sont bien typés dans $\sigma \Gamma_{i+1}$ et leurs types sont des sortes. Si elles sont différentes, alors on pose $\Phi_{w,\sigma,i+1} = \emptyset$, sinon on pose :

$$ \Upsilon_{w,\sigma,i+1} = \mathrm{Sol} < \sigma \Gamma_{i+1}, H_{i+1}, D_{i+1} > \circ \sigma $$
$$ \Phi_{w,\sigma,i+1} = \cup_{\tau \in \Gamma_{w,\sigma,i+1}} \mathrm{Sol} < \tau \Gamma_{i+1}, (h_{i+1} \tau c_1 \dots \tau c_n), d_{i+1} > \circ \tau $$

et :

$$ \Sigma_{w,i+1} = \cup_{\sigma \in \Sigma_{w,i}} \Phi_{w,\sigma,i+1} $$

Pour tout $\sigma \in \Sigma_{w,p}$, soit $T_{w,\sigma}$ le type du terme $(w ((\sigma h_1) x_1 \dots x_n) \dots ((\sigma h_p) x_1 \dots x_n))$ dans le contexte $\sigma\Gamma'$. On pose :

$$ \Psi_w = \{ \sigma \in \Sigma_{w,p} \mid T_{w,\sigma} = P \} $$

Pour tout $\sigma$ de $\Psi_w$, on pose :

$$ t_{w,\sigma} = [x_1 : \sigma P_1] \dots [x_n : \sigma P_n] (w ((\sigma h_1) x_1 \dots x_n) \dots ((\sigma h_p) x_1 \dots x_n)) $$

et :

$$ \Omega_w = \{ \sigma \cup \{ < u, [ ], t_{w,\sigma} > \} \mid \sigma \in \Psi_w \text{ et } \sigma u = u \} \cup \{ \sigma \mid \sigma \in \Psi_w \text{ et } \sigma u = t_{w,\sigma} \} $$

Enfin :

$$ \mathrm{Sol} < \Gamma, a, b > = \cup_{w \in \mathrm{Heads}} \Omega_w $$

### 7.4.5 Propriétés

**Proposition 62.** : La définition de la fonction Sol est bien fondée.

**Démonstration** : La fonction Sol est utilisée plusieurs fois dans la définition de $Sol < \Gamma, a, b >$. Dans l'un des cas le membre de droite est $b$ et le contexte a moins de variables existentielles que $\Gamma$ et dans tous les autres cas le membre de droite est de complexité strictement inférieure à $\kappa(b)$.

**Proposition 63.** : Dans le cas où le terme $a$ est flexible, le type des nouvelles variables est bien typé dans le système de type Méta dans le préfixe de $\Gamma$ déclaré à gauche de la variable $u$.

**Démonstration** : L'unique moment où de nouvelles variables sont introduites est quand $a$ est flexible. Quand $b$ est un produit, on introduit deux variables de types $(x_1 : P_1)...(x_n : P_n)s$ et $(x_1 : P_1)...(x_n : P_n)(y : (h x_1 ... x_n))s'$ et quand $b$ est atomique on introduit $n$ variables de types $(x_1 : P_1)...(x_n : P_n)T$. Dans les deux cas, les termes $P_i$ sont de types Prop ou Type.

Dans le premier, on a $s = \mathrm{Prop}$ ou $s = \mathrm{Type}$ donc $(x_1 : P_1)...(x_n : P_n)s$ est un terme bien typé. Comme le type de $b$ est Prop ou Type mais pas Extern, on a $s' = \mathrm{Prop}$ ou $s' = \mathrm{Type}$ donc $(x_1 : P_1)...(x_n : P_n)(y : (h x_1 ... x_n))s'$ est un terme bien typé.

Dans le second cas, le type du terme $(w ((\sigma h_1) x_1 \dots x_n) \dots ((\sigma h_n) x_1 \dots x_n))$ n'est pas une sorte donc il est bien typé dans le contexte $\sigma\Gamma$ et on a $T : \mathrm{Prop}$ ou $T : \mathrm{Type}$. Donc $(x_1 : P_1)...(x_n : P_n)T$ est un terme bien typé.

Prouvons maintenant que quand le problème $< \Gamma, a, b >$ est bien formé dans un système du cube $T$, alors toute substitution $\theta \in Sol < \Gamma, a, b >$ est bien typée dans $\Gamma$ dans ce même système $T$.

**Proposition 64.** : Si le problème $< \Gamma, a, b >$ est tel que tout sous-terme de $b$ qui est un produit $(x : U)U'$ est tel que $< s, s', s'' > \in R$ (l'ensemble des règles du système $T$) où $s$ est le type de $U$, $s'$ le type de $U'$ et $s''$ le type de $(x : U)U'$ et tout sous-terme de $b$ qui est une sorte est Prop mais pas Type, alors il en est de même des substitutions de $Sol < \Gamma, a, b >$.
**Démonstration** : Par récurrence sur la complexité du problème <Γ, a, b>.

**Proposition 65.** : Si le problème <Γ, a, b> est bien formé dans le système T, alors toute substitution θ ∈ Sol <Γ, a, b> est bien typée dans Γ dans le système T.

**Démonstration** : Par récurrence sur la longueur de Γ, en utilisant la proposition précédente et la proposition 38.

**Théorème 6.** : Correction

Soit <Γ, a, b> un problème, toutes les substitutions de Sol <Γ, a, b> sont dans U <Γ, a, b> (l'ensemble des substitutions solutions de <Γ, a, b>).

**Démonstration** : Par récurrence sur la complexité du problème <Γ, a, b>.

**Proposition 66.** : Pour toute substitution θ ∈ Sol <Γ, a, b> et toute variable u de Γ, θu = u ou θu est un terme sans variables existentielles dans θΓ. Et si u est la tête de a, alors θu est un terme sans variables existentielles dans θΓ.

**Démonstration** : Par récurrence sur la complexité du problème <Γ, a, b>.

**Théorème 7.** : Complétude

Soit <Γ, a, b> un problème et θ une substitution de U <Γ, a, b>, alors il existe une substitution σ ∈ Sol <Γ, a, b> et une substitution ρ bien typée dans σΓ telle que pour toute variable x de Γ, θx = (ρ ◦ σ)x.

**Démonstration** : Par récurrence sur la complexité du problème <Γ, a, b>.

Dans le cas où le terme a est rigide, a et b sont de façon évidente ou bien deux abstractions, ou bien deux produits ou bien deux termes atomiques avec la même tête et le même nombre d'arguments et les sous-termes se correspondent deux à deux par θ.

Considérons maintenant le cas où le terme a est flexible, a = (u c₁ ... cₙ).

Soit (x₁ : P₁)...(xₙ : Pₙ)P (P atomique) le type de u, le terme P est fermé dans le contexte Γ[∀x₁ : P₁; ...; ∀xₙ : Pₙ]. On considère le terme θu :

$$ \theta u = [x_1 : \theta P_1]...[x_n : \theta P_n]t $$

Comme θa = b, on a :

$$ t[x_1 \leftarrow \theta c_1, \dots, x_n \leftarrow \theta c_n] = b $$

Le terme t est fermé car b est fermé et les θcᵢ sont ou bien des termes qui ont un type du premier ordre ou bien des termes η-équivalents à une variable universelle.

— Si b est un produit b = (y : V)V', alors le terme t n'est pas une abstraction, il n'est pas atomique parce que t[x₁ ← θc₁, ..., xₙ ← θcₙ] = (y : V)V' et tous les θcᵢ sont des termes qui ont un type du premier ordre ou des termes η-équivalents à une variable universelle, c'est donc un produit t = (y : (β₁ x₁ ... xₙ))(β₂ x₁ ... xₙ y) et on a (β₁ θc₁ ... θcₙ) = V et (β₂ θc₁ ... θcₙ y) = V'.

On pose θ₁ = θ ∪ {<h, [] , β₁ >, <k, [] , β₂ >} et Γ₁ l'insertion des déclarations de h et k à gauche de u dans Γ. On a θ₁(h c₁ ... cₙ) = V donc, par hypothèse de récurrence, il existe des substitutions σ₁ ∈ Sol <Γ₁, (h c₁ ... cₙ), V > et θ₂ telles que pour chaque variable x de Γ, θ₁x = (θ₂ ◦ σ₁)x.
On a également $\theta_2(k \sigma_1 c_1 \dots \sigma_1 c_n y) = V'$ donc, par hypothèse de récurrence, il existe des substitutions $\sigma_2 \in \text{Sol} < \Gamma_2, (k \sigma_1 c_1 \dots \sigma_1 c_n y), V' >$ et $\theta_3$ telles que pour toute variable $x$ de $\Gamma_2$, $\theta_2 x = (\theta_3 \circ \sigma_2)x$.

Soit $\tau = \sigma_2 \circ \sigma_1$. On a $\tau \in \Upsilon$ et pour chaque variable $x$ de $\Gamma$, $(\theta_3 \circ \tau)x = \theta x$.

Soit $\alpha_1 = \tau h$ et $\alpha_2 = \tau k$. On a $\theta_3 \alpha_1 = \beta_1$ et $\theta_3 \alpha_2 = \beta_2$.

On considère les termes $t_1 = (y : (\alpha_1 x_1 \dots x_n))(\alpha_2 x_1 \dots x_n y)$ et $t_2 = (\tau u x_1 \dots x_n)$. Ces termes sont tous les deux bien typés et ont le type $P$ dans le contexte $\tau \Gamma[\forall x_1 : \tau P_1; \dots; \forall x_n : \tau P_n]$. On a $\theta_3 t_1 = \theta_3 t_2 = (\theta u x_1 \dots x_n)$. Le terme $t_1$ est sans variables existentielles dans ce contexte.

Le terme $\tau u$ est ou bien la variable $u$ ou bien un terme sans variables existentielles. S'il est sans variables existentielles, alors le terme $t_2$ est aussi sans variables existentielles et $t_1 = t_2$ donc $\tau u = [x_1 : \tau P_1]...[x_p : \tau P_n](y : (\alpha_1 x_1 \dots x_n))(\alpha_2 x_1 \dots x_n y)$. On pose $\sigma = \tau$ et $\rho = \theta_3$. On a $\sigma \in \text{Sol} < \Gamma, a, b >$ et pour toute variable $x$ de $\Gamma$, $\theta x = (\rho \circ \sigma)x$.

Si $\tau u = u$, on pose $\sigma = \tau \cup \{< u, [, [x_1 : \tau P_1]...[x_p : \tau P_n](y : (\alpha_1 x_1 \dots x_n))(\alpha_2 x_1 \dots x_n y) >\}$ et $\rho = \theta_3 - \{< u, \gamma, \theta_3 u >\}$ où $\gamma$ est le contexte associé à $u$ par $\theta$. On a $\sigma \in \text{Sol} < \Gamma, a, b >$ et pour toute variable $x$ de $\Gamma$, $\theta x = (\rho \circ \sigma)x$.

On a $\sigma \in \text{Sol} < \Gamma, a, b >$ et pour toute variable $x$ de $\Gamma$, $(\rho \circ \sigma)x = \theta x$.

- Si $b$ est une sorte, alors comme on a $t[x_1 \leftarrow \theta c_1, \dots, x_n \leftarrow \theta c_n] = b$, le terme $t$ est atomique et sa tête est ou bien $b$ ou bien un $x_i$. Ce n'est pas un $x_i$ parce que les $c_i$ sont ou bien des termes dont le type est du premier ordre ou bien des termes $\eta$-équivalents à une variable universelle. La tête de $t$ est donc la sorte $b$ et comme une sorte ne peut être appliquée, on a $t = b$. Donc $\theta u = [x_1 : P_1]...[x_n : P_n]b$. On pose $\sigma = \{< u, [, [x_1 : P_1]...[x_n : P_n]b >\}$ et $\rho = \theta - \{< u, \gamma, \theta u >\}$ où $\gamma$ est le contexte associé à $u$ par $\theta$. On a $\sigma \in \text{Sol} < \Gamma, a, b >$ et pour toute variable $x$ de $\Gamma$, $\theta x = (\rho \circ \sigma)x$.

- Si $b$ est atomique $b = (v d_1 \dots d_p)$ où $v$ est une variable universelle, alors comme on a $t[x_1 \leftarrow \theta c_1, \dots, x_n \leftarrow \theta c_n] = b$, le terme $t$ est atomique et sa tête est ou bien $v$ ou bien l'un des $x_i$. Si c'est l'un des $x_i$ tel que $c_i$ est $\eta$-équivalent à une variable universelle, alors cette variable universelle est $v$.

- Si la tête de $t$ est un $x_i$ tel que le type de $c_i$ est du premier ordre, alors cette variable ne peut être appliquée et $\theta u = [x_1 : \theta P_1]...[x_n : \theta P_n]x_i$.

Comme $\theta$ est bien typé dans $\Gamma$ on a $\theta P_i = \theta P$, c'est-à-dire $\theta P_i = P$. Donc, par hypothèse de récurrence, il existe une substitution $\sigma_1 \in \text{Sol} < \Gamma', P_i, P >$ et une substitution $\theta_1$ telle que pour toute variable $x$ de $\Gamma$, $\theta x = (\theta_1 \circ \sigma_1)x$.

La variable $u$ n'est pas une variable de $P_i$, donc elle n'est pas liée par $\sigma_1$, $\sigma_1 u = u$ et $\theta_1 u = [x_1 : \theta_1 \sigma_1 P_1]...[x_n : \theta_1 \sigma_1 P_n]x_i$.

On pose $\sigma_2 = \{< u, [, [x_1 : \sigma_1 P_1]...[x_n : \sigma_1 P_n]x_i >\}$ et $\theta_2 = \theta_1 - \{< u, \gamma, \theta_1 u >\}$ où $\gamma$ est le contexte associé à $u$ par $\theta_1$.

On a $\theta_1 = \theta_2 \circ \sigma_2$, donc pour toute variable $x$ de $\Gamma$, $\theta x = (\theta_2 \circ \sigma_2 \circ \sigma_1)x$.

Par hypothèse de récurrence, il existe une substitution $\sigma_3 \in \text{Sol} < \sigma_2 \sigma_1 \Gamma, \sigma_2 \sigma_1 a, b >$ et une substitution $\rho$ telle que pour toute variable $x$ de $\sigma_2 \sigma_1 \Gamma$, $\theta_2 x = (\rho \circ \sigma_3)x$.

On pose $\sigma = \sigma_3 \circ \sigma_2 \circ \sigma_1$. On a $\sigma \in \text{Sol} < \Gamma, a, b >$ et pour toute variable $x$ de $\Gamma$, $\theta x = (\rho \circ \sigma)x$.

- Si la tête de $t$ est la variable $v$ ou l'un des $x_i$ tel que $c_i$ est $\eta$-équivalent à $v$, soit $w$ cette tête.

Le type de $w$ est le type de $v$ ou le type de l'un des $x_i$ tel que $c_i$ est $\eta$-équivalent à $v$, c'est donc un terme fermé.
Dans $\theta u$ cette variable est appliquée à $p$ termes :

$$ \theta u = [x_1 : \theta P_1]...[x_n : \theta P_n](w (\beta_1 x_1 ... x_n) ... (\beta_p x_1 ... x_n)) $$

On a $\theta a = b$, donc :

$$ (v (\beta_1 \theta c_1 ... \theta c_n) ... (\beta_p \theta c_1 ... \theta c_n)) = (v d_1 ... d_p) $$

Donc pour tout $i$, on a $(\beta_i \theta c_1 ... \theta c_n) = d_i$.

Par récurrence sur $i$ on construit des substitutions $\rho_i$ et $\sigma_i$ telles que pour toute variable de $\Gamma$, $(\rho_i \circ \sigma_i)x = \theta x$ et si on pose $\alpha_j = \sigma_i h_j$, on a pour tout $j < i$, $(\alpha_j x_1 ... x_n)$ est sans variables existentielles dans $\sigma_i \Gamma[\forall x_1 : \sigma_i P_1; ... ; \forall x_n : \sigma_i P_n]$ et égal à $(\beta_j x_1 ... x_n)$.

Pour $i = 0$, on pose $\rho_0 = \theta$ et $\sigma_0 = \emptyset$.

Soit $Q_i$ le type de $(w (\alpha_1 x_1 ... x_n) ... (\alpha_i x_1 ... x_n))$ dans $\sigma_i \Gamma$. D'après la proposition 61, le terme $Q_i$ est un produit $Q_i = (y : T)T'$.

On pose $h_{i+1} : (x_1 : \sigma_i P_1)...(x_n : \sigma_i P_n)T$ et $\theta_{i+1} = \rho_i \cup \{< h_i, [ ], \beta_i >\}$.

On a $\theta_{i+1}(h_{i+1} \sigma_i c_1 ... \sigma_i c_n) = d_i$. Donc, par hypothèse de récurrence, il existe une substitution $\tau_{i+1} \in Sol < \sigma_i \Gamma, (h_{i+1} \sigma_i c_1 ... \sigma_i c_n), d_{i+1} >$ et une substitution $\rho_{i+1}$ telles que pour toute variable $x$ de $\sigma_i \Gamma$, $\theta_{i+1}x = (\rho_{i+1} \circ \tau_{i+1})x$. On pose $\sigma_{i+1} = \tau_{i+1} \circ \sigma_i$.

Pour toute variable $x$ de $\Gamma$ on a $\rho_{i+1}\sigma_{i+1}x = \rho_{i+1}\tau_{i+1}\sigma_i x = \theta_{i+1}\sigma_i x = \rho_i\sigma_i x = \theta x$.

On a alors deux substitutions $\rho_p$ et $\sigma_p$ telles que pour tout $x$ de $\Gamma$, $(\rho_p \circ \sigma_p)x = \theta x$.

On pose pour tout $i$, $\alpha_i = \sigma_i h_i$.

Soit $t_1 = (w (\alpha_1 x_1 ... x_n) ... (\alpha_p x_1 ... x_n))$ et $T$ le type de $t_1$ dans le contexte $\sigma_p \Gamma[\forall x_1 : \sigma_p P_1; ... ; \forall x_n : \sigma_p P_n]$.

Le terme $T$ est sans variables existentielles car le type de $w$ est sans variables existentielles et les $(\alpha_i x_1 ... x_n)$ sont sans variables existentielles.

On a $\rho T = P$ et le terme $T$ est sans variables existentielles donc $T = P$ et $\sigma_p \in \Psi_w$.

Soit $t_2 = \sigma_p u$. On a $\rho_p t_1 = \rho_p t_2$, $t_1$ est sans variables existentielles et $t_2$ est ou bien sans variables existentielles ou bien la variable $u$.

Si $t_2$ est sans variables existentielles, alors $t_1 = t_2$, on pose $\sigma = \sigma_p$ et $\rho = \rho_p$. Si $t_2 = u$, alors on pose $\sigma = \sigma_p \cup \{< u, [ ], [x_1 : \sigma_p P_1]...[x_p : \sigma_p P_n]t >\}$ et $\rho = \rho_p - \{< u, \gamma, \rho_p u >\}$ où $\gamma$ est le contexte associé à $u$ par $\rho_p$.

Dans les deux cas $\sigma \in Sol < \Gamma, a, b >$ et pour toute variable $x$ de $\Gamma$, $(\rho \circ \sigma) = \theta x$.

**Remarque** : Le filtrage considéré ici est ouvert au sens du chapitre précédent, pour obtenir un algorithme de filtrage fermé, il faut décider si les types des variables existentielles qui restent dans $\sigma \Gamma$ sont habités ou vides. Bien que tous ces types soient du deuxième ordre au plus, le problème est indécidable dans le plupart des systèmes.
# Chapitre 8

## Equations Indécidables

### 8.1 Unification du Deuxième Ordre

Dans le $\lambda$-calcul simplement typé, l'unification du deuxième ordre est indécidable (Goldfarb [31]). L'indécidabilité de ce problème dans ce système n'implique pas nécessairement son indécidabilité dans les extensions de ce système. En effet il n'est pas a priori équivalent pour un problème formulé dans le $\lambda$-calcul simplement typé d'avoir des solutions dans le $\lambda$-calcul simplement typé et dans une de ses extensions.

Mais la preuve d'indécidabilité de l'unification du deuxième ordre dans le $\lambda$-calcul simplement typé peut être formulée dans tous les calculs du cube. En effet, en reprenant les notations de [31], si $H$ est un système d'équations arithmétiques et $S$ est le problème d'unification codant ce système, comme dans le $\lambda$-calcul simplement typé, pour toute solution $\theta$ de $S$, les variables $F_i$ sont instanciées par des termes de la forme :

$$ \theta F_i = [w_1 : U](\overline{n_i} w_1) $$

et les variables $G_l$ pour $l = 2^i 3^j 5^k$ par des termes de la forme :

$$ \theta G_l = [w_1 : U][w_2 : U][w_3 : U](g (t_0^l w_1 w_2) (g (t_1^l w_1 w_2) \dots (g (t_{n_j-1}^l w_1 w_2) w_3))) $$

avec :

$$ t_p^l = [w_1 : U][w_2 : U](g (\overline{n_i.p} w_1) (\overline{p} w_2)) $$

$$ \overline{n} = [w_1 : U](g a \dots (g a w_1)) \quad (n \text{ fois}) $$

de tout unificateur de $S$ on peut donc déduire une solution de $H$.

**Proposition 67.** : (Goldfarb) Dans un calcul quelconque du cube il n'existe pas de méthode effective permettant de décider si un problème d'unification du deuxième ordre a une solution.

**Remarque** : L'unification considérée ici est ouverte au sens du chapitre 6. L'unification fermée est tout aussi indécidable car si le problème $< \Gamma, a, b >$ est le codage d'une équation arithmétique, alors dans toute substitution solution de ce problème les variables de $\Gamma$ sont instanciées par des termes fermés.

De plus :
**Définition 90.** : Problèmes d’Unification Elémentaires

Un problème d'unification $<\Gamma, a, b>$ est dit élémentaire au niveau des termes si le contexte $\Gamma$ est de la forme $\Gamma = [\forall U : \mathit{Prop}]\Gamma'$, pour toute variable $Qx : T$ déclarée dans $\Gamma'$, le terme $T$ est l'un des termes $U, U \to U, U \to U \to U$ ou $U \to U \to U \to U$ et le type commun de $a$ et $b$ est $U$.

Dans un calcul avec constructeurs de types, un problème d'unification est dit élémentaire au niveau des types si pour toute variable $Qx : T$ déclarée dans $\Gamma$, le terme $T$ est l'un des termes $\mathit{Prop}$, $\mathit{Prop} \to \mathit{Prop}$, $\mathit{Prop} \to \mathit{Prop} \to \mathit{Prop}$ ou $\mathit{Prop} \to \mathit{Prop} \to \mathit{Prop} \to \mathit{Prop}$ et le type commun de $a$ et $b$ est $\mathit{Prop}$.

**Proposition 68.** : Dans un calcul quelconque du cube, il n'existe pas de méthode effective permettant de décider si un problème d'unification élémentaire au niveau des termes a une solution.

Dans un calcul avec constructeurs de types, il n'existe pas de méthode effective permettant de décider si un problème d'unification élémentaire au niveau des types a une solution.

## 8.2 Filtrage du Troisième Ordre dans les Systèmes avec Types Dépendants et Constructeurs de Types

Nous avons vu précédemment que dans les algorithmes de synthèse de preuves, d'unification et de filtrage, avant d'appliquer une substitution élémentaire, il faut considérer une équation garantissant que cette substitution est bien typée. Dans le chapitre précédent, nous avons vu que dans le cas du filtrage du deuxième ordre, cette équation était également un problème de filtrage. Dès que l'on autorise des variables du troisième ordre, des variables peuvent apparaître dans les deux membres de cette équation.

Cela suggère qu'un problème d'unification du deuxième ordre peut se coder comme l'équation de garantie d'une substitution dans un problème de filtrage du troisième ordre. C'est effectivement le cas dans les systèmes de types avec types dépendants ou constructeurs de types. Le filtrage du troisième ordre est donc indécidable dans ces systèmes.

**Théorème 8.** : Indécidabilité du Filtrage du Troisième Ordre dans les Calculs avec Types Dépendants

Dans un calcul avec types dépendants, il n'existe pas de méthode effective permettant de décider si un problème de filtrage dont toutes les variables existentielles sont du troisième ordre au plus a une solution.

**Démonstration** : Pour tout problème d'unification élémentaire au niveau des termes $<\gamma, u_1, u_2>$ on construit un problème de filtrage $<\Gamma, t_1, t_2>$ tel que tous les types des variables existentielles de $\Gamma$ soient du troisième ordre au plus et $<\gamma, u_1, u_2>$ a une solution si et seulement si $<\Gamma, t_1, t_2>$ en a aussi une. On pose :

$$ \Gamma = \gamma[\forall z : U; \forall P : U \to \mathit{Prop}; \forall c : (P z); \forall d : (P z); \forall G : (P z) \to (P z) \to (P z)]; $$

$$ \exists f : (h : U \to U)(P (h u_1)) \to (P (h u_2))] $$

$$ t_1 = (G (f [x : U] z c) (f [x : U] z d)) \quad t_2 = (G c d) $$

S'il existe une substitution $\tau$ telle que $\tau u_1 = \tau u_2$, alors on pose :

$$ \sigma = \tau \cup \{<f, [], [x_1 : U \to U][x_2 : (P (x_1 (\tau u_1)))][x_2]>\} $$
La substitution $\sigma$ est bien typée dans $\Gamma$ et est solution du problème de filtrage $\sigma t_1 = t_2$.

Réciproquement, s'il existe une substitution $\sigma$ bien typée dans $\Gamma$ telle que $\sigma t_1 = t_2$, alors $\sigma$ est bien typée dans $\gamma$ et on montre que $\sigma u_1 = \sigma u_2$. Soit :

$$ 
\begin{aligned}
\Delta &= \Gamma[\forall x_1 : U \to U; \forall x_2 : (P(x_1 (\sigma u_1)))] \\
      &= v = ((\sigma f) x_1 x_2) : (P(x_1 (\sigma u_2)))
\end{aligned}
$$

L'équation $\sigma t_1 = t_2$ est équivalente au système :

$$ v[x_1 \leftarrow [x : U]z, x_2 \leftarrow c] = c \quad v[x_1 \leftarrow [x : U]z, x_2 \leftarrow d] = d $$

Le terme $v$ n'est pas une abstraction ni un produit parce que son type est $(P(x_1 (\sigma u_2)))$. C'est donc un terme atomique $v = (x r_1 ... r_p)$ où $x$ est une variable ou l'un des symboles Prop et Type. Le symbole $x$ est l'une des variables $x_1, x_2, c$ parce que $v[x_1 \leftarrow [x : U]z, x_2 \leftarrow c] = c$. Il est différent de $c$ parce que $v[x_1 \leftarrow [x : U]z, x_2 \leftarrow d] = d$. Il est différent de $x_1$ parce que le type de $v$ est différent de $U \to U$ et $U$. Donc $x = x_2$. Comme le type de $x_2$ est atomique, $p = 0$ et $v = x_2$. Les termes $v$ et $x_2$ ont donc même type et on en déduit :

$$ \sigma u_1 = \sigma u_2 $$

**Théorème 9. : Indécidabilité du Filtrage du Troisième Ordre dans les Calculs avec Constructeurs de Types**

Dans un calcul avec constructeurs de types, il n'existe pas de méthode effective permettant de décider si un problème de filtrage dont toutes les variables existentielles sont du troisième ordre au plus a une solution.

**Démonstration** : Pour tout problème d'unification élémentaire au niveau des types $\langle \gamma, u_1, u_2 \rangle$ on construit un problème de filtrage $\langle \Gamma, t_1, t_2 \rangle$ tel que tous les types des variables existentielles de $\Gamma$ soient du troisième ordre au plus et $\langle \gamma, u_1, u_2 \rangle$ a une solution si et seulement si $\langle \Gamma, t_1, t_2 \rangle$ en a aussi une. On pose :

$$ 
\begin{gather*}
\Gamma = \gamma[\forall Z : \mathit{Prop}; \forall c : Z; \forall d : Z; \forall G : Z \to Z \to Z; \exists f : (h : \mathit{Prop} \to \mathit{Prop})(h u_1) \to (h u_2)] \\
t_1 = (G (f [X : \mathit{Prop}] Z c) (f [X : \mathit{Prop}] Z d)) \quad t_2 = (G c d)
\end{gather*}
$$

S'il existe une substitution $\tau$ telle que $\tau u_1 = \tau u_2$, alors on pose :

$$ \sigma = \tau \cup \{<f, []| [x_1 : \mathit{Prop} \to \mathit{Prop}][x_2 : (x_1 (\tau u_1))]x_2 >\} $$

La substitution $\sigma$ est bien typée dans $\Gamma$ et est solution du problème de filtrage $\sigma t_1 = t_2$.

Réciproquement, s'il existe une substitution $\sigma$ bien typée dans $\Gamma$ telle que $\sigma t_1 = t_2$, alors $\sigma$ est bien typée dans $\gamma$ et on montre que $\sigma u_1 = \sigma u_2$. Soit :

$$ 
\begin{aligned}
\Delta &= \Gamma[\forall x_1 : \mathit{Prop} \to \mathit{Prop}; \forall x_2 : (x_1 (\sigma u_1))] \\
      &= v = ((\sigma f) x_1 x_2) : (x_1 (\sigma u_2))
\end{aligned}
$$
L'équation $\sigma t_1 = t_2$ est équivalente au système :

$$v[x_1 \leftarrow [X : \mathit{Prop}] Z, x_2 \leftarrow c] = c \quad v[x_1 \leftarrow [X : \mathit{Prop}] Z, x_2 \leftarrow d] = d$$

Le terme $v$ n'est pas une abstraction ni un produit parce que son type est $(x_1 (\sigma u_2))$. C'est donc un terme atomique $v = (x r_1 ... r_p)$ où $x$ est une variable ou l'un des symboles $\mathit{Prop}$ et $\mathit{Type}$. Le symbole $x$ est l'une des variables $x_1, x_2, c$ parce que $v[x_1 \leftarrow [X : \mathit{Prop}] Z, x_2 \leftarrow c] = c$. Il est différent de $c$ parce que $v[x_1 \leftarrow [X : \mathit{Prop}] Z, x_2 \leftarrow d] = d$. Il est différent de $x_1$ parce que le type de $v$ est différent de $\mathit{Prop} \to \mathit{Prop}$ et $\mathit{Prop}$. Donc $x = x_2$. Comme le type de $x_2$ est atomique, $p = 0$ et $v = x_2$. Les termes $v$ et $x_2$ ont donc même type et on en déduit :

$$\sigma u_1 = \sigma u_2$$

**Remarque** : Le filtrage considéré ici est ouvert au sens du chapitre 6. Le filtrage fermé est tout aussi indécidable car si le problème $< \gamma, u_1, u_2 >$ est le codage d'une équation arithmétique, alors dans toute substitution solution du problème $< \Gamma, t_1, t_2 >$ aussi bien les variables de $\gamma$ que la variable $f$ sont instanciées par des termes fermé.

## 8.3 Filtrage dans les Systèmes Polymorphes et Systèmes avec Types Inductifs

Rappelons d'abord quelques résultats classiques sur les algorithmes récursifs primitifs :

**Proposition 69.** : Il existe des algorithmes récursifs primitifs qui calculent les fonctions suivantes :

* l'addition et la multiplication,

* la fonction Equal telle que $(\mathit{Equal} x y) = 0$ si $x = y$ et $(\mathit{Equal} x y) = 1$ sinon,

* la fonction $\alpha$ telle que $(\alpha x n)$ est l'exposant du $n^{\text{ème}}$ entier premier dans la décomposition de $x$.

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

**Proposition 70.** : Pour toute suite finie d'entiers $a_1, ..., a_n$ il existe un entier $x$ tel que pour tout $i, 1 \le i \le n$, $a_i = (\alpha x i)$.

**Démonstration** : On prend $x = \prod_{i=1}^{n} p_n^{a_n}$ où $p_n$ est le $n^{\text{ème}}$ entier premier.

**Proposition 71.** : *Indécidabilité des Equations Primitives Récursives*

Il n'existe pas de méthode effective qui décide si un algorithme récursif primitif $f$ donné, l'équation $(f x_1 ... x_n) = 0$ a une solution.

**Démonstration** : On réduit le dixième problème de Hilbert [14] à ce problème. Soient $(P x_1 ... x_n)$ et $(Q x_1 ... x_n)$ deux polynômes. Soit $f$ l'algorithme :

$$(f x_1 ... x_n) = (\mathit{Equal} (P x_1 ... x_n) (Q x_1 ... x_n))$$

L'équation $(f x_1 ... x_n) = 0$ a une solution si et seulement si $(P x_1 ... x_n) = (Q x_1 ... x_n)$ en a aussi une.
**Remarque** : Dans la proposition précédente, on peut se restreindre à des équations à une variable en considérant l’algorithme :

$$ (f x) = (\text{Equal} (P (\alpha x 1) \dots (\alpha x n)) (Q (\alpha x 1) \dots (\alpha x n))) $$

Plaçons-nous ensuite dans un quelconque calcul polymorphe du cube.

**Proposition 72.** : Nous avons vu au chapitre 1 que si on pose :

$$ \mathrm{Nat} = (P : \mathrm{Prop})P \to (P \to P) \to P $$

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

pour tout algorithme primitif récursif f d'arité n, il existe un terme t : Nat → ... → Nat → Nat tel que si $a_1, ..., a_n$ sont des entiers, alors ($t a_1 ... a_n$) se réduit sur l'entier ($f a_1 ... a_n$).

De plus, le terme t peut être effectivement construit à partir de l'algorithme f. On dit que t est un représentant de f.

**Proposition 73.** : Soit $\Gamma$ un contexte et t un terme de type Nat dans $\Gamma$. Si la forme normale de $(t \mathrm{Nat} 0 [y : \mathrm{Nat}]y)$ est 0, alors le terme t est un entier de Church.

**Démonstration** : Ecrivons $t = [P : \mathrm{Prop}][x : P][f : P \to P]u$ où $u$ est de type $P$ dans le contexte $\Gamma[P : \mathrm{Prop}; x : P; f : P \to P]$.

Le forme normale du terme $(t \mathrm{Nat} 0 [y : \mathrm{Nat}]y)$ est 0, donc il en est de même de celle du terme $u[P \leftarrow \mathrm{Nat}, x \leftarrow 0, f \leftarrow [y : \mathrm{Nat}]y]$. On prouve par récurrence sur la structure de $u$ que $u = (f \dots (f x) \dots)$.

Le terme $u$ a le type $P$, donc ce n'est ni une abstraction ni un produit. C'est un terme atomique ($w c_1 ... c_p$). Si $w$ est différent de $P$, $f$ et $x$, la forme normale de $u[P \leftarrow \mathrm{Nat}, x \leftarrow 0, f \leftarrow [y : \mathrm{Nat}]y]$ est également atomique de tête $w$, ce n'est donc pas le terme 0. La variable $w$ est donc parmi $P$, $f$ et $x$. Ce n'est pas la variable $P$ car dans ce cas on aurait $p = 0$ et donc la forme normale de $u[P \leftarrow \mathrm{Nat}, x \leftarrow 0, f \leftarrow [y : \mathrm{Nat}]y]$ serait le terme $\mathrm{Nat}$ qui est différent de 0. La variable $w$ est donc $x$ ou $f$.

Si $w = x$, alors $p = 0$ et le terme $u$ a la forme requise. Si $w = f$, alors $p = 1$, $u = (f u')$. Le terme $u[P \leftarrow \mathrm{Nat}, x \leftarrow 0, f \leftarrow [y : \mathrm{Nat}]y]$ se réduit sur $u'[P \leftarrow \mathrm{Nat}, x \leftarrow 0, f \leftarrow [y : \mathrm{Nat}]y]$, donc la forme normale de ce terme est 0. Par hypothèse de récurrence $u' = (f \dots (f x) \dots)$, donc $u = (f (f \dots (f x) \dots))$ a la forme requise.

**Théorème 10.** : Indécidabilité du Filtrage dans les Calculs Polymorphes

Il n'y a pas de méthode effective permettant de décider si un problème de filtrage dans un système de types polymorphe a une solution.

**Démonstration** : Soit $f$ un algorithme primitif récursif unaire, on construit un problème de filtrage qui a une solution si et seulement si $f$ prend la valeur 0.

Soit $t$ un terme représentant l'algorithme $f$. Posons :

$$ \mathrm{Pair} = [x : \mathrm{Nat}][y : \mathrm{Nat}][g : \mathrm{Nat} \to \mathrm{Nat} \to \mathrm{Nat}](g x y) $$

$$ \Gamma = [\exists x : \mathrm{Nat}] $$
$$ 
\begin{aligned}
a &= (Pair (x Nat 0 [y : Nat]y) (t x)) \\
b &= (Pair 0 0)
\end{aligned}
 $$

Soit $n$ un entier tel que $(f n) = 0$, la substitution $\{< x, [ ], n >$ est solution du problème $< \Gamma, a, b >$.

Réciproquement, soit $\theta$ une solution de $< \Gamma, a, b >$, et $u = \theta x$. On a

$$ 
\begin{aligned}
(u \ Nat \ 0 \ [y : \ Nat]y) &= 0 \\
(t \ u) &= 0
\end{aligned}
 $$

Par la première équation $u$ est un entier de Church $n$ et par la seconde $(f n) = 0$.

**Remarque** : Le filtrage considéré ici est ouvert au sens du chapitre 6. Le filtrage fermé est tout aussi indécidable car dans toute substitution solution du problème $< \Gamma, a, b >$, la variable $x$ est instanciée par un terme sans variables existentielles.

**Remarque** : Le problème de filtrage considéré ici est d'ordre $\infty$. Comme nous avons montré que le filtrage du deuxième ordre est décidable, le problème de la décidabilité du filtrage dans le système $F$ avec uniquement des variables d'ordre fini est laissé ouvert. Ce problème semble lié à celui du filtrage dans le $\lambda$-calcul simplement typé.

Plaçons-nous maintenant dans un calcul avec types inductifs.

**Proposition 74.** : Nous avons vu au chapitre 1 que pour tout algorithme primitif récursif $f$ d'arité $n$, il existe un terme $t : Nat \to \dots \to Nat \to Nat$ tel que si $a_1, \dots, a_n$ sont des entiers, alors le terme $(t \ a_1 \dots \ a_n)$ se réduit sur l'entier $(f \ a_1 \dots \ a_n)$. De plus, le terme $t$ peut être effectivement construit à partir de l'algorithme $f$. On dit que $t$ est un représentant de $f$.

**Proposition 75.** : Soit $t$ un terme normal de type $Nat$ tel que le terme $(R \ 0 \ \lambda y : Nat.\lambda z : Nat.z \ t)$ ait 0 pour forme normale, alors $t$ a la forme $(S \ \dots \ (S \ 0) \ \dots)$.

**Démonstration** : Par récurrence sur la structure de $t$. Le terme $t$ est de type $Nat$, ce n'est donc ni une abstraction ni un produit, comme il est normal, c'est un terme atomique $(w \ c_1 \dots c_p)$. Si $w$ était différent de 0 et $S$, alors le terme $(R \ 0 \ \lambda y : Nat.\lambda z : Nat.z \ t)$ serait normal et différent de 0. Donc la variable $w$ est 0 ou $S$.

Si $w = 0$, alors $p = 0$, donc $t = 0$ a la forme requise. Si $w = S$, alors $p = 1$, $t = (S \ t')$. Le terme $(R \ 0 \ \lambda y : Nat.\lambda z : Nat.z \ t)$ se réduit sur $(R \ 0 \ \lambda y : Nat.\lambda z : Nat.z \ t')$, donc la forme normale de ce terme est 0. Donc par hypothèse de récurrence $t' = (S \ \dots \ (S \ 0) \ \dots)$ et $t = (S \ (S \ \dots \ (S \ 0) \ \dots))$ a la forme requise.

**Théorème 11.** : Le filtrage est indécidable dans les systèmes avec types inductifs. De plus, comme le type $Nat$ est primitif dans ces systèmes, le filtrage est indécidable dès le premier ordre.

**Démonstration** : La preuve est la même que celle pour le système $F$, sauf qu'on remplace le terme $(x \ Nat \ 0 \ \lambda y : Nat.y)$ par $(R \ 0 \ \lambda y : Nat.\lambda z : Nat.z \ x)$.

**Remarque** : Plus généralement, si on dit que les algorithmes récursifs primitifs sont fidèlement représentables dans un $\lambda$-calcul typé quand ces algorithmes sont représentables dans ce système et qu'il existe un terme $t$ de type $Nat \to Nat$ tel que $(t \ u)$ se réduise sur 0 si et seulement si $u$
représente un entier, alors le filtrage est indécidable dans les systèmes où les fonctions récursives primitives sont fidèlement représentables.

**Remarque :** Le filtrage considéré ici est ouvert au sens du chapitre 6. Le filtrage fermé est tout aussi indécidable car dans toute substitution solution du problème < Γ, a, b > la variable *x* est instanciée par un terme sans variables existentielles.
Conclusion de la Seconde Partie

Considérons un ensemble *E* d'équations tel qu'il existe une méthode permettant de décider s'il existe une solution ou non à une équation de *E*. Soit *e* une équation qui n'appartient pas à *E*, l'ensemble *E* ∪ {e} admet aussi une méthode de décision et est un sur-ensemble strict de *E*. Il n'y a donc pas de problème décidable maximal. Quand on a prouvé qu'un problème est décidable, il est donc toujours possible de raffiner ce résultat en trouvant un problème décidable plus général. De même, quand on a prouvé qu'un problème est indécidable on peut toujours trouver un problème indécidable moins général. C'est pour cela que nous avons a priori limité l'espace des problèmes auxquels nous nous intéressons. Trois critères les déterminent :

• l'ordre des variables,

• la fermeture éventuelle de l'un des termes,

• la clôture de ces problèmes par anti-skolémisation.

Pour les problèmes d’unification où on limite l’ordre des variables, mais où on n’impose pas à l’un des termes d’être fermé, le problème est résolu dans tous les systèmes du cube puisque l’unification est décidable au premier ordre et indécidable au-delà. Il est aussi résolu dans les systèmes avec types inductifs puisque l’unification est indécidable dès le premier ordre.

Pour les problèmes de filtrage où on limite l'ordre des variables et on impose à l'un des termes d'être fermé, le problème est résolu dans les six systèmes comportant des types dépendants et des constructeurs de types puisque le filtrage est décidable jusqu'au deuxième ordre et indécidable au-delà. Pour le λ-calcul simplement typé, le filtrage est décidable au deuxième ordre et la question est ouverte au-delà. Pour le système F le filtrage est décidable au deuxième ordre et indécidable à l'ordre infini. La question est ouverte entre les deux. Pour les systèmes avec types inductifs, le problème est résolu puisque le filtrage est indécidable dès le premier ordre.

Enfin si on prend la clôture des ces problèmes par anti-skolémisation, les problèmes indécidables restent indécidables (puisque ces problèmes sont plus généraux que ceux dont ils sont la clôture) et les problèmes décidables restent décidables puisque l'unification entre termes à arguments restreints est décidable et le filtrage avec un terme ouvert à arguments restreints du deuxième ordre également.
Conclusion

Dans cette thèse, nous avons décrit une méthode de semi-décision pour les systèmes de types. La vérification de preuves étant décidable dans ces systèmes, l'existence d'une telle méthode est en fait immédiate : il suffit d'énumérer toutes les chaînes de caractères jusqu'à tomber sur une preuve de la proposition à démontrer. Cette méthode (qui est souvent utilisée pour prouver la semi-décidabilité du calcul des prédicats) n'a naturellement aucune valeur pratique.

On peut la rendre moins irréaliste en énumérant tous les λ-termes typés (arbres de preuve)
normaux jusqu'à tomber sur une preuve de la proposition en question. Cette méthode est comparable
aux méthodes de recherche systématique d'un contre-modèle de Herbrand du début des années
soixante.

La résolution permet d'exclure a priori davantage de tentatives vouées à l'échec en remarquant
que dans une prémisse ∀x.(P x), il n'est utile d'instancier x par t que si (P t) est une instance
de la proposition à prouver ou d'une hypothèse d'une autre prémisse. Cette méthode formulée par
Robinson pour la logique du premier ordre est généralisée par Huet à la logique d'ordre supérieur
et ici aux systèmes de types. La notion de terme-preuve qui apparaît dans les systèmes de types
permet de rendre plus explicite l'idée d'énumération aveugle des preuves régulée par un mécanisme
d'anticipation de l'échec par exploitation des contraintes.

Le problème de l'instanciation des variables de prédicat, qui est très brutale en résolution à l'ordre supérieur, apparaît encore ici comme une source majeure d'inefficacité. Ces variables apparaissent dans trois cas : le codage des connecteurs à l'ordre supérieur, l'égalité et les principes de récurrence.

* Le codage des connecteurs à l'ordre supérieur : La méthode consistant à coder les connecteurs à l'ordre supérieur et à utiliser la méthode standard est vraisemblablement beaucoup trop naïve. Par exemple, on garde une méthode complète en se restreignant à appliquer une preuve de $A \wedge B$ aux seules propositions A et B.

* L'égalité : Remarquons d'abord que l'expressivité du langage des termes dans les systèmes de types permet de ramener de nombreuses preuves d'égalité à des calculs de formes normales. Cette idée de réduction des termes opposée à l'exploration arbitraire de substitutions est la base des méthodes de réécriture. L'intégration de ces méthodes à des méthodes générales comme celle développée ici reste à comprendre.

* Les principes de récurrence : L'investigation des méthodes de démonstration automatique confirme une remarque que chacun a faite en cherchant une preuve “à la main” : le choix de l'hypothèse de récurrence est un problème difficile dans le recherche de démonstrations. Cela suggère une utilisation de la synthèse de preuves où un utilisateur indique à la machine les propositions à prouver par récurrence et laisse la machine faire le travail de bas niveau, comme dans les systèmes développés au chapitre 5.

Ce problème du choix de l'hypothèse de récurrence sera sans doutes central dans les travaux à
venir. La question est de savoir s'il est possible de ne retenir a priori qu'un nombre fini d'hypothèses
de récurrences (de la même façon que la résolution ne retient a priori qu'un nombre fini de termes
pour instancier les variables du premier ordre) ou si l'exploration aveugle d'un nombre infini de
propositions est nécessaire à la complétude. Autrement dit, de savoir s'il n'y a que des preuves
longues, ou également des preuves difficiles. Cette question peut vraisemblablement se formuler
comme un problème de décidabilité de k-prouvabilité. Dans le cas, probable, d'une réponse négative
à cette question, il reste à comprendre quelles heuristiques mèneront à un système acceptable, à
défaut de complet.
Bibliographie

[1] H. Barendregt, Introduction to Generalized Type Systems, *Journal of Functional Programming*, à parraître.

[2] N.G. de Bruijn, Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem, *Indag. Math.*, 34, 5, 1972, pp. 381-392.

[3] N.G. de Bruijn, A Survey of the Project Automath, *To H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism*, J.R. Hindley, J.P. Seldin (Eds.), Academic Press, 1980.

[4] N.G. de Bruijn, The Mathematical Vernacular, A Language For Mathematics With Typed Sets, *Proceedings of the Workshop on Programming Logic*, Marstrand, Sweden, 1987.

[5] N.G. de Bruijn, The Mathematical Vernacular : Examples, Non publié.

[6] A. Church, A Formulation of the Simple Theory of Types, *Journal of Symbolic Logic*, 5,1, 1940, pp. 56-68.

[7] A. Church, The Calculi of Lambda-Conversion, *Princeton University Press*, 1941.

[8] Th. Coquand, Une Théorie des Constructions, *Thèse de troisième cycle*, Université Paris VII, 1985.

[9] Th. Coquand, An Analysis of Girard's Paradox, *Proceedings of Logic in Computer Science*, 1986, pp. 227-236.

[10] Th. Coquand, Metamathematical Investigations of a Calculus of Constructions, *Logic and Computer Science*, P. Odifreddi (Ed.), Academic Press, London, 1990, pp. 91-122.

[11] Th. Coquand, G. Huet, The Calculus of Constructions, *Information and Computation*, 76, 1988, pp. 95-120.

[12] Th. Coquand, Ch. Paulin, Inductively Defined Types, *Proceedings of the Internationnl Conference on Computer Logic*, P. Martin-Löf, G. Mints (Eds.) Lecture Notes in Computer Science 417, 1988, pp. 50-66.

[13] H.B. Curry, R.Feys, Combinatory Logic, Vol. 1, *North Holland*, Amsterdam, 1968.

[14] M. Davis, Hilbert's Tenth Problem is Unsolvable, *The American Mathematician Monthly*, 80, 3, 1973, pp. 233-269.

[15] G. Dowek, Naming and Scoping in a Mathematical Vernacular, *Rapport de Recherche 1283*, INRIA, 1990.

[16] G. Dowek, A Complete Proof Synthesis Method for Type Systems of the Cube.
[17] G. Dowek, L'Indécidabilité du Filtrage du Troisième Ordre dans les Calculs avec Types Dépendants ou Constructeurs de Types (The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors), *Compte Rendu à l'Académie des Sciences*, I, 312, 12, 1991, pp. 951-956.

[18] G. Dowek, A Second Order Pattern Matching Algorithm in the Cube of Typed λ-Calculi, *Proceedings of Mathematical Foundation of Computer Science*, Lecture Notes in Computer Science 520, 1991, pp. 151-160. Rapport de Recherche, INRIA, 1991.

[19] G. Dowek, The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable.

[20] C. M. Elliott, Higher-order Unification with Dependent Function Types, *Proceedings of the 3rd International Conference on Rewriting Techniques and Applications*, N. Dershowitz (Ed.), Lecture Notes in Computer Science, 355, Springer-Verlag, 1989, pp. 121-136.

[21] C. M. Elliott, Extensions and Applications of Higher-order Unification, *PhD Thesis*, Carnegie Mellon University, Pittsburgh, 1990.

[22] G. Frege, Begriffsschrift, A Formula Language, Modeled upon that of Arithmetic, for Pure Thought, 1879, reproduit dans [64].

[23] G. Gentzen, The Collected Work of Gehrard Gentzen, M.E. Szabo (Ed.), *North Holland*, 1969.

[24] H. Geuvers, Type Systems for Higher Order Logic, *Catholic University Nijmegen*.

[25] H. Geuvers, The Church-Rosser Property for $\beta\eta$-reduction in Typed Lambda Calculi, *Catholic University Nijmegen*, 1991.

[26] H. Geuvers, M.J. Nederhof, A Modular Proof of Strong Normalization for the Calculus of Constructions, *Catholic University Nijmegen*.

[27] J. Gallier, On Girard's Candidats de Réductibilité, *Logic and Computer Science*, P. Odifreddi (Ed.), Academic Press, London, 1990, pp. 123-203.

[28] J.Y. Girard, Interprétation Fonctionnelle et Elimination des Coupures dans l'Arithmétique d'Ordre Supérieur, *Thèse de Doctorat d'État*, Université de Paris VII, 1972.

[29] J.Y. Girard, Types and Proofs, translated and with appendices by P. Taylor and Y. Lafont, *Cambridge University Press*, 1989.

[30] K. Gödel, Über eine Bisher Noch Nicht Benützte Erweiterung des Finiten Standpunktes, *Dialectica*, 12, 1958.

[31] W.D. Goldfarb, The Undecidability of the Second-Order Unification Problem, *Theoretical Computer Science*, 13, 1981., pp. 225-230.

[32] M.J. Gordon, A.J. Milner, C.P. Wadsworth, Edinburgh LCF, *Lecture Notes in Computer Science* 78, Springer-Verlag, 1979.

[33] R. Harper, F. Honsell, G. Plotkin, A Framework for Defining Logics, *Proceedings of Logic in Computer Science*, 1987, pp. 194-204.

[34] R. Harper, R. Pollack, Type Checking, Universe Polymorphism and Typical Ambiguity in the Calculus of Constructions, *CCIPL, TAPSOFT'89*, Barcelona, 1989.

[35] L. Helmink, Resolution and Type Theory, *Proceedings of the ESOP Conference*, Copenhagen, Lecture Notes in Computer Science, 432, Springer-Verlag, 1990.
[36] W.A. Howard, The Formal-as-type Notion of Construction, 1969, reproduit dans *To H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism*, J.R. Hindley, J.P. Seldin (Eds.), Academic Press, 1980.

[37] G. Huet, Constrained Resolution A Complete Method for Higher Order Logic, *PhD Thesis*, Case Western Reserve University, 1972.

[38] G. Huet, A Mechanisation of Type Theory, *Proceedings of the 3rd Intern. Joint Conf. on Artificial Inteligenge*, 1973, pp. 139-146.

[39] G. Huet, The Undecidability of Unification in Third Order Logic, *Information and Control*, 22, 1973, pp. 257-267.

[40] G. Huet, A Unification Algorithm for Typed λ-calculus, *Theoretical Computer Science*, 1, 1975, pp. 27-57.

[41] G. Huet, Résolution d'Équations dans les Langages d'Ordre 1,2, ..., ω, *Thèse de Doctorat d'État*, Université de Paris VII, 1976.

[42] G. Huet, A Uniform Approach to Type Theory, *Rapport de recherche 795*, INRIA, 1988. *Logical Foundation of Functional Programming*, G. Huet (Ed.), Addison-Wesley, 1990, pp. 337-397.

[43] G. Huet, Adding Type :Type to the Calculus of Constructions, Non publié, 1988.

[44] G. Huet, The Constructive Engine, *A Perspective in Theoretical Computer Science*, Commemorative Volume for Gift Siromoney, R. Narasimhan (Ed.), World Scientific Publishing, 1989.

[45] G. Huet, B. Lang, Proving and Applying Program Transformations Expressed with Second Order Patterns, *Acta Informatica*, 11, 1978, pp. 31-55.

[46] D.C. Jensen T. Pietrzykowski, Mecanizing ω-order type theory through unification, *Theoretical Computer Science*, 3, 1976, pp. 123-171.

[47] Y. Lafont, Communication Personelle.

[48] C. L. Lucchesi, The Undecidability of the Unification Problem for Third Order Languages, *Report CSRR 2060*, Department of Applied Analysis and Computer Science, University of Waterloo, 1972.

[49] Z. Luo, An Extended Calculus of Constructions, *PhD Thesis*, University of Edinburgh, 1990.

[50] P. Martin-Löf, Intuitionistic Type Theory, *Bibliopolis*, Napoli, 1984.

[51] D. A. Miller, Unification Under a Mixed Prefix, *Journal of Symbolic Computation*, à parlaître.

[52] D. A. Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification *Extension of Logic Programming*, P. Schroeder-Heister (Ed.), Lecture Notes in Computer Science 475, Springer-Verlag, 1991, pp. 253-281. Report ECS-LFCS-91-159, University of Edinburgh, 1991. Journal of Logic and Computation, à parlaître.

[53] Ch. Paulin-Mohring, Extraction de Programmes dans le Calcul des Constructions, *Thèse de Doctorat*, Université Paris VII, 1989.

[54] Ch. Paulin-Mohring, Extracting $Fω$ Programs from Proofs in the Calculus of Constructions, *Proceedings of Principles of Programming Languages*, 1989.

[55] T. Pietrzykowski, D.C. Jensen, A Complete Mechanization of ω-order Type Theory, *Assoc. Comp. Mach. Nat. Conf.*, 1972 Vol 1, pp. 82-92.
[56] F. Pfenning, Logic Programming in the LF Logical Framework, Logical Frameworks I, G. Huet et G. Plotkin (Eds.), Cambridge University Press, 1991.

[57] F. Pfenning, Unification and anti-Unification in the Calculus of Constructions, Proceedings of Logic in Computer Science, 1991.

[58] D. Pym, Proof, Search and Computation in General Logic, PhD thesis, University of Edinburgh, 1990.

[59] J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the Association for Computing Machinery, 12, 1, 1965, pp. 23-41.

[60] A. Salvesen, The Church-Rosser Theorem for LF with $\beta/\eta$-reduction, Manuscrit, University of Edinburgh, 1989.

[61] L.E. Sanchis, Functionals Defined by Recursion, Notre Dame Journal of Formal Logic, VIII, 3, 1967, pp. 161-174.

[62] H. Schwichtenberg Definierbare Funktionen im Lambda-Calcul mit Typen, Archiv Logik Grundlagenforsch, 17, 1976, pp. 113-114.

[63] W.W. Tait, Intensional Interpretation of Functionals of Finite Type I, Journal of Symbolic Logic, 32, 2, 1967, pp. 198-212.

[64] J. van Heijenoort, From Frege to Gödel, Harvard University Press, Cambridge, Massachusetts, 1967.

[65] A. Yasuhara, Recursive Function Theory and Logic, Academic Press, New York, 1971.
# Index

<, 40

Extern, 32

Méta (système de types), 32

Prop, 21

Type, 26

α-équivalence, 16

βη-normal (terme), 18

βη-réduction, 18

βη-équivalence, 18

β-normal (terme), 18

β-réduction, 18

β-équivalence, 18

⊥, 16

o, 56

∃, 16, 49

∀, 16, 49

¬, 16

->, 16, 19

‡, 16, 20

V, 16

∧, 16

abstraction, 18

accès aux axiomes, 82

application, 18

arguments restreints (terme à), 97

arguments restreints du deuxième ordre (terme à), 99

atomique (terme), 33

axiome, 16

bien formé (contexte), 20

bien typé (terme), 20, 33

bien typé sans utiliser les contraintes (terme), 52

Calcul des Constructions, 29

classique (logique), 17

clôture transitive, 79

complexité (d'un terme), 103

complétude transitive, 79

composition, 56

constructeurs de types, 29

contenu (d'un terme marqué), 41

contexte, 19

contexte quantifié contraint, 51

contrainte, 50

cube de Barendregt, 29

degré de scission, 64

déduction naturelle, 16

dérivation, 65

existentiel (contexte), 54

existentielle (variable), 49

fermé (terme), 53

fermée (solution), 91

filtrage, 97

flexible (terme), 53

fonctionnel (système de types), 33

forme η-longue, 34, 45

forme normale (d'un contexte), 53

garantie (équation de), 62, 100

imprédicativité, 22

insertion, 106

introduction-résolution, 61

intuitionniste (logique), 17

isomorphisme de Curry-Howard, 25

libre (variable), 16

marqué (terme), 40

mesure (d'un terme), 45, 46

nombre d'itérations borné, 82
ordre (d'un problème d'unification), 96
ordre (d'un type), 96
ordre supérieur (logique d'), 21
ouverte (solution), 91

polymorphisme, 28
premier ordre (logique du), 15
principe de compréhension, 38
proposition, 15, 22
prédicativité, 22

représentable (fonction), 23, 34
rigide (terme), 53
règles générales, 27
résolution (à l'ordre supérieur), 60

sans variables existentielles (terme), 53
scission, 61
scission faible (algorithme avec), 77
scission forte (algorithme avec), 77
simplement typé (λ-calcul), 19, 20
simplification, 73
solution (d'un problème d'unification), 91
sous-terme, 39
substitution, 16, 54
substitution élémentaire, 63
succès (contexte de), 53
synthèse de preuves avec lemmes, 79
sémantique de Heyting, 24

taille (d'un terme), 71
taille (d'une substitution), 71
terme du λ-calcul, 18
terme du λ-calcul simplement typé, 19, 20
terme du λ-calcul typé, 27, 31
terme du premier ordre, 15
théorème, 16
type, 19, 33
types dépendants, 25
types inductifs, 28

unification, 91
unification (à l'ordre supérieur), 60
univers, 31
universelle (variable), 49
vernaculaire mathématique, 87

échec (contexte d'), 53
élémentaire (problème d'unification), 114
équivalence modulo contraintes, 51
Résumé

Le Calcul des Constructions est une extension de la logique d'ordre supérieur dans laquelle le langage des termes est un λ-calcul typé comprenant des types dépendants, des types polymorphes et des constructeurs de types. La richesse de ce système de types permet, en se basant sur la sémantique de Heyting et l'isomorphisme de Curry-Howard, de représenter les preuves par des termes. Sa puissance calculatoire en fait également un outil bien adapté au raisonnement sur des programmes et à la preuve de leur correction.

La démonstration automatique dans un système logique est l'étude des méthodes qui, partant d'une proposition, en construisent automatiquement une preuve. Dans la première partie de cette thèse nous développons une telle méthode pour le Calcul des Constructions. Cette méthode s'inscrit dans la lignée de celles développées par Robinson pour la logique du premier ordre et Huet pour la logique d'ordre supérieur sous le nom de résolution. En ce qui concerne la démonstration automatique, la nouveauté qu'apportent les systèmes de types, tels que le Calcul des Constructions, par rapport aux systèmes logiques précédents concerne le rôle respectif de la résolution et de l'unification. Au premier ordre et à l'ordre supérieur résolution et unification sont séparées. Dans les systèmes de types, où termes et preuves sont de même nature, résolution et unification se mêlent en un algorithme unique.

Dans la seconde partie de cette thèse, nous étudions les problèmes de résolution d'équations dans le Calcul des Constructions et certaines de ses restrictions. Tout d'abord nous montrons que l'algorithme de synthèse de preuves de la première partie peut être utilisé comme algorithme d'unification, ou plus exactement comme algorithme d'unification fermée. Ensuite, nous étudions les cas particuliers décidables et indécidables de l'unification. Nous montrons que dans le Calcul des Constructions, comme dans le λ-calcul simplement typé, le filtrage du deuxième ordre est décidable. Nous montrons également que le filtrage d'ordre supérieur est indécidable dans tous les calculs qui comportent des types dépendants, des types polymorphes, des constructeurs de types ou des types inductifs.

Mots-Clés

Démonstration Automatique, Résolution, Unification, Filtrage, λ-calcul, Logique d'Ordre Supérieur, Théorie des Types, Calcul des Constructions.