Définitions préliminaires

Le but de ce chapitre est de donner un certain nombre de définitions et de résultats classiques. Le lecteur familier avec les notions de base de la réécriture (algèbre de termes, système de réécriture, confluence, normalisation forte, λ-calcul, typage…) peut passer ce chapitre.

Nous commencerons par rappeler les définitions de base concernant les relations binaires sur un ensemble. Nous donnerons alors des définitions formelles de normalisation et de confluence pour une relation ainsi que quelques résultats concernant ces notions. Nous définirons ensuite les notions d'algèbre de termes, de règle et de système de réécriture du premier ordre et nous présenterons quelques résultats simples ayant trait à la confluence et à la normalisation des systèmes de réécriture du premier ordre. Nous conclurons ce chapitre par une présentation rapide du λ-calcul [Chu41] et d'une extension du λ-calcul possédant un mécanisme explicite de gestion des substitutions [BR95].

2.2 Rappels sur la notion de relation binaire

Définition 1 Soit E un ensemble:

Une relation binaire R sur E est un sous ensemble de E× E. Si (e₁,e₂)∈ R, nous dirons que e₁ est en relation avec e₂ (par R) (l'inverse n'étant pas forcément vrai). Nous utiliserons désormais la notation e₁ R e₂ pour exprimer le fait que l'élément e₁ est en relation avec e₂.
Une relation réflexive est une relation binaire R sur E telle que tout élément de E est en relation avec lui-même.
Une relation antiréflexive est une relation binaire R sur E telle qu'aucun élément de E n'est en relation avec lui-même.
Une relation symétrique est une relation binaire R sur E telle que pour tout couple d'éléments e₁ et e₂ de E, si e₁ R e₂ alors e₂ R e₁.
Une relation R est antisymétrique si pour tout couple d'éléments e₁,e₂ de E: si e₁ R e₂ et si e₂ R e₁ alors e₁ = e₂.
Une relation R est transitive si pour tous d'éléments e₁ ,e₂ et e₃ tels que e₁ R e₂ et si e₂ R e₃ alors e₁ R e₃.
Une relation R est une relation d'équivalence si R est symétrique, transitive et réflexive.
Une relation R est un ordre si R est réflexive, transitive et antisymétrique.
R est un ordre strict si R est antiréflexive (donc antisymétrique) et transitive.
Un ordre (strict) > est dit nœthérien s'il n'existe pas de suite infinie (t_i)_i∈N telle que pour tout i∈N, t_i > t_i+1.

Si nous considérons l'ensemble des entiers naturels N: l'égalité est une relation d'équivalence sur cet ensemble alors que la relation d'ordre usuelle > est un ordre strict au sens de la définition précédente. Cet ordre est, de plus, nœthérien.

Définition 2 (Extensions d'une relation binaire) Soient E un ensemble et → une relation binaire sur cet ensemble.

La clôture transitive →⁺ de → est la plus petite relation (pour l'inclusion) transitive contenant →.
La clôture réflexive et transitive →^* de → est la plus petite relation réflexive et transitive contenant →.

Si →₁ et →₂ sont deux relations binaires, nous définissons leur union, notée →₁ ∪ →₂, comme étant la plus petite relation contenant à la fois →₁ et →₂.

Définition 3 (Ordre lexicographique) Soient E₁ et E₂ deux ensembles et >₁ et >₂ deux ordres sur, respectivement, E₁ et E₂. Nous définissons l'ordre lexicographique >_lex induit par >₁ et >₂ sur l'ensemble E₁× E₂ comme suit:

(e₁,e₂)>_lex(e₁',e₂') ⇔

⎧
⎪
⎨
⎪
⎩

e₁	>₁	e₁'
ou
e₁	=	e₁'	et	e₂	>₂	e₂'

2.3 Terminaison et confluence

Définition 4 (Réduit d'un terme et formes normales) Soient E un ensemble et → une relation binaire sur E.

Un élément e ' de E est un réduit (en un pas) pour → d'un élément e si e→ e '. Il nous arrivera dans la suite d'écrire que e ' est un →-réduit de e.
Si un élément e ne possède pas de réduit par →, cet élément est dit en forme normale pour →. Il nous arrivera dans la suite d'écrire que e est une →-forme normale.
Étant donné un élément e, on appelle forme normale de e pour la relation →, tout élément e ' en forme normale pour → tel que e→^* e '. Il nous arrivera dans la suite d'écrire que e ' est une →-forme normale de e.
L'élément e de E est être faiblement normalisable par (la relation) → s'il existe une forme normale pour e.
Un élément e est dit fortement normalisable par (la relation) → si toute suite de réduction de e conduit en un nombre fini de pas à une forme normale i.e. il n'existe pas de suite infinie (e_i)_i∈N d'éléments de E telle que pour tout i e_i→ e_i+1 et e=e₀.
La relation → est dite faiblement normalisante si tout élément de E est faiblement normalisable par →, elle est dite fortement normalisante si tout élément de E est fortement normalisable par →.

Lemme 5 (Relation entre les différentes notions de normalisabilité) Soit E un ensemble.

Si → est une relation sur E, alors tout élément de E fortement normalisable par → est faiblement normalisable par →.
Toute relation → fortement normalisante sur E est faiblement normalisante sur E.

Remarque 6 Soient E un ensemble et → une relation binaire sur cet ensemble. La relation → est fortement normalisante sur E si et seulement si la relation →⁺ est fortement normalisante sur E.

Lemme 7 Soient E un ensemble et → une relation binaire sur E. La relation → est fortement normalisante sur E si et seulement s'il existe un ordre nœthérien strict > tel que: e→ e ' implique e>e '.

Nous utiliserons le lemme suivant pour prouver la terminaison de certains systèmes de réécriture.

Lemme 8 Soit O un ensemble. Soient R₁ et R₂ deux relations sur O telles que:

R₂ est fortement normalisante,
Il existe un ensemble O', une relations R' sur cet ensemble et une fonction T de O dans O' tels que:
1. a→_R₁ b implique T(a)—→_R'⁺ T(b)
2. a→_R₂ b implique T(a)= T(b)

Pour tout terme a∈ O tel que T(a) est R'-fortement normalisable, a est (R₁∪ R₂)-fortement normalisable.

Les propriétés de normalisation (faible ou forte) garantissent l'existence d'une "valeur" pour les éléments de E mais pas l'unicité de cette valeur. L'unicité (en cas d'existence) est assurée par la notion de confluence décrite ci-dessous.

Définition 9 (Confluence) Soient E un ensemble et → une relation binaire sur E.

La relation → est dite confluente si:
    ∀ e, e₁, e₂,
        e →^* e₁

        e →^* e₂

⎫
⎬
⎭ ⇒ ∃ e ', ⎧
⎨
⎩
        e₁ →^* e '

        e₂ →^* e '
La relation → est dite localement confluente si:
    ∀ e, e₁, e₂,
        e → e₁

        e → e₂

⎫
⎬
⎭ ⇒ ∃ e ', ⎧
⎨
⎩
        e₁ →^* e '

        e₂ →^* e '
La relation → est dite fortement confluente ou possède la propriété du diamant si:
    ∀ e, e₁, e₂,
        e → e₁

        e → e₂

⎫
⎬
⎭ ⇒ ∃ e ', ⎧
⎨
⎩
        e₁ → e '

        e₂ → e '

Remarque 10 Toute relation confluente est localement confluente.

Lemme 11 (Newman) Toute relation localement confluente et fortement normalisante sur un ensemble est confluente sur cet ensemble.

Il est à remarquer que les deux conditions de ce lemme sont nécessaires. En effet, il existe des relations localement confluentes et non fortement normalisantes qui ne sont pas confluentes et bien évidement toute relation non localement confluente n'est pas confluente.

Nous ne donnerons ici qu'un exemple du premier cas. Considérons la relation → définie sur l'ensemble { a,b,c,d } et dont le graphe est le suivant:

Cette relation est trivialement non fortement normalisante (bien que faiblement normalisante), puisque par exemple a→ b→ a… Elle est non confluente car, par exemple, a—→^* c et a—→^* d bien que c et d ne possèdent pas de réduit en commun. Pourtant cette relation est localement confluente.

Lemme 12 Toute relation fortement confluente est confluente.

Lemme 13 (Lemme d'interprétation) Soit R= R₁∪ R₂ l'union de deux relations. Si:

R₁ est confluente et fortement normalisante,
il existe une relation R' sur les R₁-formes normales telle que:
1. R'⊂ R^*,
2. Pour toutes expressions e₁ et e₂:
  e₁→_R₂ e₂ implique R₁(e₁)—→^*_R' R₁(e₂)
  
  où R₁(e) désigne l'unique forme normale pour R₁ de e.

alors R est confluente si et seulement si R' l'est.

2.4 Réécriture du premier ordre

2.4.1 Algèbre de termes

Définition 14 (Signature) Une signature est un ensemble Σ muni d'une fonction d'arité, notée ar( ), de Σ dans N. Les éléments d'une signature seront par la suite généralement notés f, g,…

Notation 15 Dans la suite de ce document, nous nous autoriserons à partitionner l'ensemble Σ en une union infinie d'ensembles (Σ_i)_i∈N où chaque Σ_i est l'image réciproque de l'entier i par la fonction ar( ).

Définition 16 (Algèbre de termes du premier ordre) Étant donné une signature Σ et un ensemble X de variables, possiblement infini, nous définissons l'algèbre des termes A=T(Σ, X) comme suit:

Toute variable x∈ X est un terme (un élément de A).
Si f est un élément de Σ_n et si t₁,…,t_n sont des termes alors f(t₁,…,t_n) est un terme.

Cette notion d'algèbre de termes nous permettra de définir tous les systèmes de réécriture du premier ordre. Pour les systèmes de réécriture d'ordre supérieur nous aurons aussi besoin d'une notion de lieur.

Exemple 17

Définissons la signature Σ₁=({0,s},{ar(0)=0, ar(s)=1}). L'algèbre A₁=T(Σ₁,∅) est une représentation de l'ensemble des entiers naturels puisque tout entier naturel peut être vu soit comme l'entier nul représenté par 0, soit comme le successeur d'un entier n représenté par s(n) où n est la représentation de n.
Définissons maintenant la signature Σ₂ en ajoutant à la signature Σ₁ le symbole plus d'arité 2. L'algèbre A₂=T(Σ₂,∅) est une représentation des sommes d'entiers telles que:
plus(3,plus(7,4)).

Définition 18 (Variables d'un terme) Étant donné une algèbre de termes A=T(Σ, X), et un terme t de cette algèbre, nous définissons l'ensemble des variables de t, BV(t) par induction sur la structure de t comme suit:

Si t=x∈ X alors BV(t)={x}
Si t=f(t₁,…,t_n) alors BV(t)=∪_i=1ⁿ BV(t_i)

Définition 19 (Termes clos) Soit A une algèbre de termes. Nous appellerons dans la suite terme clos tout terme t de cette algèbre tel que BV(t)=∅.

Définition 20 (Position dans un terme) Une position est une suite finie (un mot) d'entiers naturels strictement positifs. Nous noterons par la suite une position i₁.i₂.… i_n quand la suite ne sera pas vide et є la suite vide.

Étant donné une algèbre de termes T(Σ, X), et un terme t de cette algèbre, nous définissons l'ensemble des positions de t, Pos(t) par induction sur la structure de t comme suit:

Si t=x∈ X, Pos(t)={є}.
Si t=f∈Σ₀, Pos(t)={є}.
Si t=f(t₁,…,t_n) où n>0, Pos(t)={є}∪∪_i=1ⁿ(∪_{p∈Pos(t_i)}i.p).

Nous appellerons position propre toute position autre que la position є.

Ainsi l'ensemble des positions de plus(s(0),s(s(y))) est {є,1,2,1.1,2.1,2.1.1}

Les positions dans un terme nous permettent, de définir les notions de sous-terme à une position donnée et de sous-terme d'un terme.

Définition 21 (Sous-termes d'un terme) Étant donné un terme t et une position p de ce terme, nous définissons le sous-terme de t à la position p, notée t∣_p, par induction sur p:

Si p=є, alors t∣_є=t.
Si p=i.p', alors t=f(t₁,…,t_i,…,t_n) et t∣_p=t_i∣_p'.

Nous dirons qu'un terme t' est un sous-terme d'un terme t s'il existe une position p∈Pos(t) telle que t'=t∣_p.

Ainsi, plus(s(0),s(s(y)))∣_1.1=s(0)∣₁=0∣_є=0 et plus(s(0),s(s(y)))∣₂=s(s(y)).

Définition 22 (Greffe d'un terme à une position) Soient t et t' deux termes et p une position de t. Nous définissons la greffe du terme t' à la position p dans le terme t, noté t[t']_p par induction sur p comme suit:

Si p=є alors t[t']_є = t'.
Si p=i.p' et t=f(t₁,…,t_i,…,t_n) alors:
t[t']_i.p'=f(t₁,…,t_i[t]_p',…,t_n)

2.4.2 Règles et systèmes de réécriture du premier ordre

Dans cette section, nous allons définir la notion de règle de réécriture et de système de réécriture du premier ordre.

Définition 23 (Règles de réécriture) Supposons donnée une algèbre de termes A=T(Σ, X). Une règle de réécriture, notée g → d, est la donnée de deux termes g et d appelés respectivement membre gauche et membre droit de la règle tels que:

g n'est pas une variable,
BV(d)⊂ BV(g).

Ainsi, suivant cette définition, si on considère l'algèbre représentant l'ensemble des expression entières:

Définition 24 (Système de réécriture) Un système de réécriture sur une algèbre de termes est la donnée d'un ensemble de règles de réécriture de cette algèbre.

Avant de définir la notion de relation de réduction du premier ordre engendrée par un système de réécriture il nous faut préciser la notion de substitution du premier ordre (ou remplacement).

2.4.3 Remplacement du premier ordre

Cette section est consacrée à la définition de la notion de remplacement de premier ordre. Un remplacement est une fonction des variables d'une algèbre de termes dans les termes de cette algèbre. Nous utiliserons de tels objets pour transformer les termes.

Définition 25 (Remplacement) Soit T(Σ, X) une algèbre de termes. Un remplacement σ est une fonction de X dans T(Σ, X) telle que pour toute variable x de X, sauf un nombre fini d'entre elles, σ(x)=x.

Nous appellerons par la suite domaine d'un remplacement σ, noté dom(σ), l'ensemble des variables x∈ X telles que σ(x)≠ x et codomaine de ce remplacement, noté codom(σ), l'ensemble ∪_x∈dom(σ) BV(σ(x)).

Remarquons que nous pouvons aussi représenter les remplacements comme étant des ensembles (finis) de couples (x,t) où x est une variable et t un terme.

Définition 26 (Application d'un remplacement à un terme) Étant donné un remplacement σ et un terme t, nous définissons l'application de σ à t, notée t σ, par induction sur la structure du terme t comme suit:

xσ=σ(x) si x est une variable.
f(t₁,…,t_n)σ=f(t₁σ,…,t_nσ).

Définition 27 (Renommage) Un renommage est un remplacement ρ tel que ∀ x∈dom(ρ), ρ(x)∈ X.

Définition 28 Nous dirons par la suite que deux termes t₁ et t₂ sont unifiables si et seulement s'il existe un remplacement σ, appelé unificateur de t₁ et t₂, tel que t₁σ=t₂σ.

Définition 29 Étant donné deux remplacements ρ₁ et ρ₂, nous dirons que ρ₁ est plus général que ρ₂, ce que nous noterons dans la suite de ce document ρ₁>>ρ₂, si et seulement s'il existe un remplacement ρ₃ tel que: ρ₂=ρ₃∘ρ₁

Définition 30 (Unificateur le plus général de deux termes) Nous appellerons un unificateur le plus général de deux termes unifiables t₁ et t₂, un élément de l'ensemble des unificateurs de t₁ et t₂ qui est minimal pour l'ordre >>.

2.4.4 Relation induite par un système de réécriture

Nous allons, dans cette section, définir la relation (de réduction) induite par un système de réécriture, pour cela nous avons besoin de définir la notion de clôture par contexte d'une relation binaire.

Définition 31 (Relation de réduction en tête) Soient A= A(Σ, X) une algèbre de termes et R un système de réécriture sur A. La relation de réduction en tête induite par R, notée —→_R^h , est définie comme suit. Le terme e ' est un réduit du terme e par la relation —→_R^h si et seulement si:

Il existe une règle G→ D appartenant au système R,
Il existe un remplacement de premier ordre σ,
e=Gσ et e '=Dσ .

Exemple 32 Le terme 3 est un réduit en tête de plus(3,0) par le système de réécriture {plus(n,0)→ n}. Il suffit de prendre σ={n↦ 3}

Définition 33 (Contexte) Un contexte C pour une algèbre T(Σ,X) est un terme de l'algèbre T(Σ∪{ },X) contenant exactement une occurrence du symbole 0-aire (d'arité 0) ∉Σ.

Étant donné un contexte C et un terme t∈ T(Σ,X), la notation C(t) désigne le terme Cσ de l'algèbre T(Σ,X) où σ={(,t)}.

Définition 34 (Clôture par contexte d'une relation) Soient A= A(Σ, X) une algèbre de termes et R une relation binaire sur A.

La relation R est dite close par contexte pour A si: Pour tout symbole de fonction n-aire f de Σ, pour tous termes t₁,…,t_n, s'il existe un i∈[1… n] et un terme t_i' tel que t_i R t_i' alors:

f(t₁,…,t_i,…,t_n) R f(t₁,…,t_i',…,t_n)

ou, de manière équivalente, pour tout contexte C et pour tous termes t R t', C(t) R C(t').

La clôture par contexte d'une relation R est la plus petite relation R' contenant R et close par contexte.

Remarque 35 Un terme t₁ est un sous-terme d'un terme t₂ si et seulement si il existe un contexte C tel que t₂=C(t₁).

Il nous est maintenant possible de définir la notion de relation (de réduction) induite par un système de réécriture.

Définition 36 (Relation de réduction) Soient A= A(Σ, X) une algèbre de termes et R un système de réécriture sur A. La relation de réduction induite par R, notée →_R , est définie comme étant la clôture par contexte de la relation —→_R^h .

Ainsi, le terme plus(0,3) est un réduit du terme plus(0,plus(3,0)) par la relation induite par le système de réécriture { plus(n,0)→ n}.

Définition 37 Soient l₁→ r₁ et l₂→ r₂ deux règles d'un système de réécriture R telles que l₁ soit unifiable avec un sous-terme de l₂ qui ne soit pas une variable (ce sous-terme doit être propre si l₁→ r₁ = l₂→ r₂).

Dans ce cas, il existe un contexte C, un terme u et un unificateur plus général σ de u et l₁ tels que l₂=C(u). Nous appellerons alors le couple de terme (C(r₁)σ,r₂σ) une paire critique du système R.

Une paire critique (t₁,t₂) est dite joignable s'il existe un terme t tel que:

possède une paire critique obtenue en applicant l'unificateur le plus général ρ={ x↦ i(t), y↦ t } à ses deux règles. Cette paire est: (f(i(t),f(t,z)) , f(e,z) )

La notion de paire critique est très importante vis à vis de celle de confluence. En effet:

Lemme 38 (Paires critiques du premier ordre et confluence locale [BN98]) Soit R un système de réécriture du premier ordre. Si toutes les paires critiques sont joignables alors le système R est localement confluent.

Concluons ce rapide aperçu de la notion de réécriture du premier ordre et d'algèbre de terme par la définition de congruence.

Définition 39 (Congruence) Supposons donnée une algèbre de termes A=T(Σ, X). Une congruence (sur A) est une relation d'équivalence ≡ telle que:

t₁≡ t₁', … t_n≡ t_n' ⇒ f(t₁,…,t_n)≡ f(t₁',…,t_n')

Définition 40 (Réécriture modulo) Supposons données une algèbre de termes A=T(Σ, X), ≡ une congruence et → une relation de réécriture. Nous dirons qu'un terme t₁ se réécrit par la relation → quotientée par la congruence ≡ en un terme t₂ si et seulement si:

∃ t₁', ∃ t₂', t₁≡ t₁' → t₂'≡ t₂

2.5 Le λ-calcul

Les algèbres de termes du premier ordre, (définition 16), et les systèmes de réécriture du premier ordre ne permettent pas de modéliser les fonctions d'ordre supérieur (telles que, par exemple, la fonction map). Ces fonctions ne peuvent être modélisées que dans le cadre des formalismes de réécriture d'ordre supérieur.

Comme nous l'avons déjà mentionné dans l'introduction de ce document, le λ-calcul [Chu41] est le plus ancien et, sans doute, le mieux connu des systèmes de réécriture d'ordre supérieur. Les formalismes présentés dans la suite de ce document n'en sont que des extensions.

Nous présenterons, dans cette section, le λ-calcul avant de rappeler que ce formalisme n'est pas fortement normalisant. Nous présenterons alors un système de types simples permettant de retrouver la terminaison ainsi que de garantir la cohérence des données. Nous conclurons cette section par la présentation d'une extension très simple de ce calcul à la gestion explicite du mécanisme de substitution.

2.5.1 Le λ-calcul non typé

Intuitivement, le λ-terme λ x. t représente une fonction qui associe la valeur t à la variable x. Le terme f t représente l'application de la fonction f à un argument t.

Comme en mathématiques, la variable x de la construction λ x. t est une variable muette (ou liée) au sens où, par exemple, les deux termes λ x. x et λ y. y représentent la même fonction. Ces deux termes seront dit α-équivalents. Nous allons maintenant donner une formalisation de cette notion. Pour cela il nous faut introduire la notion d'ensemble des variables libres d'un λ-terme.

Définition 41 (Variables Libres) L'ensemble des variables libres d'un λ-terme t, noté FV(t), est défini par induction sur la structure de t comme suit:

FV(x)	=	{x}
FV( t₁ t₂)	=	FV(t₁)∪ FV(t₂)
FV(λ x. t₁)	=	FV(t₁)∖{x}

Définition 42 (Variables liées) L'ensemble des variables liées d'un λ-terme t, noté BV(t), est défini par induction sur la structure de t comme suit:

BV(x)	=	∅
BV( t₁ t₂)	=	BV(t₁)∪ BV(t₂)
BV(λ x. t₁)	=	{x}∪ BV(t₁)

Définition 43 (Application d'un remplacement à un λ-terme) Un remplacement σ dans le λ-calcul est un remplacement tel que défini pour le premier ordre (Définition 25) mais à valeur dans l'ensemble des λ-termes.

L'application d'un remplacement ρ={(x₁,t₁),…,(x_n,t_n)} à un λ-terme est défini comme suit:

xσ	=_def	σ(x)
( t₁ t₂)σ	=_def	t₁σ t₂σ
(λ x_i. t)ρ	=_def	λ x_i. (tρ'_i)	où ρ'_i={(x_j,t_j)}_{j∈{1,…,i−1,i+1,…,n}}
(λ y. t)ρ	=_def	λ y. (tρ)	où y∉{x₁,…,x_n}

Nous sommes désormais en mesure de définir formellement la notion de termes α-équivalents.

Définition 44 (α-équivalence) Deux termes t₁ et t₂ sont dit α-équivalents, ce que nous noterons par la suite t₁=_α t₂, si et seulement si:

Ou bien t₁=t₂=x
Ou bien t₁=( t₁¹ t₁²), t₂=( t₂¹ t₂²), t₁¹=_α t₂¹ et t₁²=_α t₂²,
Ou bien t₁=λ x₁. t₁', t₂=λ x₂. t₂' et pour tous renommages ρ₁={(x₁,z)} et ρ₂={(x₂,z)}, sauf un nombre fini, t₁'ρ₁=_α t₂'ρ₂.

Nous travaillerons désormais tout au long de cette section modulo α-équivalence.

Définition 45 (Substitution) Une substitution σ est un couple { x ← t } formé d'une variable x et d'un λ-terme t. Étant donné un λ-terme t et une substitution σ={ x ← t' } , nous définissons l'application de σ au terme t par induction sur t comme suit:

x	{ x ← t' } =_def	t'
y	{ x ← t' } =_def	y	si y≠ x
( t₁ t₂)	{ x ← t' } =_def	( t₁{ x ← t' } t₂{ x ← t' } )
(λ y. t₁)	{ x ← t' } =_def	λ y. (t₁{ x ← t' } )	si x≠ y et y∉ FV(t')

Remarquons que la condition sur l'abstraction n'est pas restrictive puisque si y∈{x}∪ FV(t'), il nous suffit de remplacer λ y. t₁ par un terme λ z. t₁' qui lui soit α-équivalent et tel que z∉{x}∪ FV(t).

Nous pouvons également remarquer que l'application d'une substitution à un λ-terme n'est pas défini à l'aide de règles du λ-calcul mais en dehors de ce calcul (de manière implicite).

Grâce à la notion de substitution du λ-calcul, nous pouvons désormais définir l'unique règle de réduction du λ-calcul:

Notation 46 Nous noterons →_λ (ou, quand la confusion ne sera pas possible, → ) la clôture par contexte de la β-règle:

Lemme 47 (Confluence du λ-calcul [Bar84]) Le système de réécriture induit par la β-règle est confluent.

Cependant, le λ-calcul ne possède pas la propriété de normalisation forte comme le prouve l'exemple suivant:

Exemple 48 (Contre exemple de terminaison du λ-calcul) Le terme Ω Ω où Ω=_defλ x. ( x x) n'est pas fortement normalisant. En effet, nous avons la séquence de réduction infinie suivante:

Ω Ω	=_def	λ x. ( x x) Ω
	→	( x x){ x ← Ω }
	=	Ω Ω
	⋮

Lemme 49 (Indécidabilité de la terminaison) Il n'est pas possible de décider de la normalisation forte des λ-termes.

Il est donc nécessaire de donner un critère syntaxique de normalisation forte pour les λ-termes. Ce critère devra bien évidement être correct (tout λ-terme le vérifiant devant être fortement normalisable) mais ne pourra être complet (il existera des λ-termes fortement normalisables qui ne vérifierons pas ce critère).

L'un des critères les plus connus est sans doute le "bon typage" dans un système de types simples.

2.5.2 Le système de types simples

De nombreux systèmes de types ont été proposés pour le λ-calcul [Bar93]. Nous présenterons ici le plus simple d'entre eux.

Définition 50 (Types simples) L'ensemble des types simples du λ-calcul [Bar84] est défini par la grammaire suivante:

(Types) A	::=	ι	(Type primitif)
	∣	A→A	(Type fonctionnel)

Intuitivement, le type ι représente les types de bases (entiers,réels, (chaînes de) caractères …) alors que les types fonctionnels représentent les types des fonctions. Le type int→bool est le type des fonctions des entiers dans les booléens (par exemple celui de la fonction est_paire).

Nous utiliserons désormais les notations A, B, C …pour désigner des types simples.

Définition 51 (λ-termes annotés) L'ensemble des λ-termes annotés est donné par la même grammaire que l'ensemble des λ-termes mais où nous avons remplacé la construction λ x. t du λ-calcul par λ x : A. t où A est un type.

Définition 52 (Environnement de types) Un environnement de types, Γ, est un ensemble de couples x : A, où x est une variable et A est un type simple, tel que toute variable x apparaît au plus une fois dans Γ.

Définition 53 (Jugement de typage) Un jugement de typage est un triplet Γ⊢ t : A où Γ est un environnement de types, t est un λ-terme annoté et A est un type.

Nous dirons que le λ-terme annoté t possède le type A dans l'environnement Γ s'il est possible de dériver le jugement Γ⊢ t : A en appliquant l'ensemble de règles suivant:

Γ⊢ x : A

(Var)

si (x,A)∈Γ

x : A,Γ⊢ t : B

Γ⊢λ x : A. t : A→B

(Abs)

Γ⊢ t₁ : A→B Γ⊢ t₂ : A

Γ⊢ ( t₁ t₂) : B

(App)

Notation 54 Dans la suite, nous utiliserons la notation Γ⊢ t : A pour exprimer que t possède le type A dans l'environnement Γ.

Théorème 55 (Préservation de types par réduction [Bar93]) Soient t et t' deux λ-termes, Γ un environnement de types et A un type. Si Γ⊢ t : A et t→ t' alors Γ⊢ t' : A.

Théorème 56 (Normalisation forte du λ-calcul simplement typé [Bar93]) Soient t un λ-terme, Γ un environnement de types et A un type. Si Γ⊢ t : A alors t est fortement normalisable.

2.5.3 Extensions aux systèmes de substitutions explicites

Nous présentons ici la plus simple des extensions du λ-calcul permettant la gestion explicite de la substitution: le λ_x-calcul [BR95, BG99]. L'idée principale de ce calcul est d'enrichir la syntaxe du λ-calcul d'un constructeur de substitution explicite en remplaçant la méta--notation t{ x ← t' } par la construction syntaxique t [ x/t' ] et de transposer les méta--règles de substitutions du λ-calcul en des règles explicites du λ_x-calcul.

Définition 57 (Grammaire du λ_x-calcul) Les termes du λ_x-calcul sont donnés par la grammaire suivante:

*(Termes)* t	::=	x	(Variable)	où x∈ X.
	∣	t t	(Application)
	∣	λ x. t	(Abstraction)
	∣	t [ x/t ]	(Substitution Explicite)

Remarquons que les termes du λ-calcul sont en particulier des termes du λ_x-calcul.

Définition 58 (Variables libres et liées d'un terme du λ_x-calcul) Soit t un terme du λ_x calcul. L'ensemble des variables libres de t est défini par induction sur t comme suit:

FV(x)	=	{x}
FV( t₁ t₂)	=	FV(t₁)∪ FV(t₂)
FV(λ x. t₁)	=	FV(t₁)∖{x}
FV( t [ x/t' ] )	=	( FV(t)∖{x})∪ FV(t')

L'ensemble des variables liées de t est défini par induction sur t comme suit:

BV(x)	=	∅
BV( t₁ t₂)	=	BV(t₁)∪ BV(t₂)
BV(λ x. t₁)	=	{x}∪ BV(t₁)
BV( t [ x/t' ] )	=	{x}∪ BV(t)∪ BV(t')

Définition 59 (Règles de réduction du λ_x-calcul) Les règles de réductions du λ_x-calcul sont:

(λ x. t) t'	→	t [ x/t' ]
x [ x/t ]	→	t
y [ x/t ]	→	y	si y≠ x
( t₁ t₂) [ x/t' ]	→	t₁ [ x/t' ] t₂ [ x/t' ]
(λ y. t) [ x/t' ]	→	λ y. ( t [ x/t' ] )	si y≠ x

Nous noterons →_{λ_x} la relation engendrée par les règles ci-dessus.

Lemme 60 (Confluence du λ_x-calcul [BR95]) La relation →_{λ_x} est confluente.

Théorème 61 (Simulation [BG99]) Si t et t' sont deux λ-termes tels que t→_λ t' alors t—→_{λ_x}⁺ t'.

Une conséquence de ce théorème est la non terminaison des λ_x-termes. Il nous faut donc donner un système de types pour le λ_x-calcul. Pour cela, nous gardons la grammaire des types (Définition 50) et nous étendons la notion de λ-termes annotés aux λ_x-termes.

Définition 62 (Système de types pour le λ_x-calcul) Les règles de typage du λ_x-calcul sont: