Table des matières
Chapitre 1 Introduction
Chapitre 2 Définitions préliminaires
2.1 Introduction
2.2 Rappels sur la notion de relation binaire
2.3 Terminaison et confluence
2.4 Réécriture du premier ordre
2.4.1 Algèbre de termes
2.4.2 Règles et systèmes de réécriture du premier ordre
2.4.3 Remplacement du premier ordre
2.4.4 Relation induite par un système de réécriture
2.5 Le λ-calcul
2.5.1 Le λ-calcul non typé
2.5.2 Le système de types simples
2.5.3 Extensions aux systèmes de substitutions explicites
Chapitre 3 Normalisation forte du λ
σ
w
-calcul
3.1 Définition du formalisme λ
σ
3.2 Le calcul λ
σ
w
3.3 Preuve de normalisation forte
Chapitre 4 Le calcul λ
P
w
4.1 Définition du calcul
4.1.1 Grammaire
4.1.2 Variables libres et liées
4.1.3 Règles de réduction
4.1.4 Variables libres localisées et termes acceptables
4.1.5 Correction de λ
P
w
4.2 Confluence de λ
P
w
4.2.1 Confluence et terminaison de →
es
4.2.2 Définition et confluence de la relation →
λ
P
w
i
4.2.3 Confluence de →
λ
P
w
4.3 Un système de types pour λ
P
w
4.3.1 Définition du système de dérivation de type
4.3.2 Préservation de types par réduction
4.4 Normalisation forte pour λ
P
w
4.4.1 Préliminaires
4.4.2 Définition de λ
P
w
/
≡
4.4.3 Expression du λ
P
w
/
≡
-calcul réductible
4.4.4 Préservation de la réductibilité par composition
Chapitre 5 Systèmes de réduction d'expressions avec motifs
5.1 Définition des ERSP
5.2 Règles de réécriture et relation de réduction
5.3 Un exemple concret
5.4 Vers un ensemble d'ERSP confluents
5.5 Confluence des ERSP
Chapitre 6 Conclusions
Bibliographie