Schema du Cours de Sémantique, année academique 2000-2001
1 Introduction
Panoramique et motivations.
2 Rappels fondamentaux
- Induction
- mathématique et complète
- Relations bien fondées
- définitions et exemples
- Principe d'induction bien fondée
- et preuve
- Composition de relations bien fondées
- lexicographique, produit etc.
3 Sigma-Algèbres, termes du premier ordre
- Definition de signature et sigma-algèbre
- Definition de Tsigma(X)
- termes, environnements, interpretations
- Egalité
- validité, satisfiabilité, notion syntaxique et remplacement d'égaux par égaux
4 Théorème de Birkhoff
- Définition de Mod(E)
- le modèle de termes Tsigma(X)/E
- Relation entre syntaxe et sémantique
- Théorème de Birkhoff
5 Réécriture
- Réécriture
- notion de relation de Réécriture abstraite,
- Propriétés des systèmes de réécriture abstraits
- confluence faible, confluence, confluence forte, normalisation faible et normalisation forte.
- Propositions
- Lemme de Newman (confluence faible + normalisation forte implique confluence), prouvé par induction bien fondée
- Egalite engendree par une relation de réécriture
- propriété de Church-Rosser, et équivalence avec la confluence.
- Réécriture sur termes du premier ordre
- paire critiques et lemme de Knuth-Bendix.
6 Unification, Lambda calcul non typé
- Algorithme d'Unification
- abstrait.
- Introduction au lambda calcul
- lamda termes, substitution, notion de reduction b et d'égalité b
7 Lambda calcul non typé
- Codage de l'arithmetique et de la recursion
- dans le calcul non typé
- Confluence du lambda calcul
- preuve par le biais de la technique des reductions parallèles
8 Lambda calcul: evaluation
- Généralités
- sur la Sémantique operationnelle structurée (SOS, ou à la Plotkin, ou des petits pas, ou small steps), et sur la Sémantique opérationnelle naturelle (à la Khan, big steps ou des grands pas)
- Sémantique du lambda calcul
- appel par nom et par valeur, en style SOS et naturel, avec définition de la notion de valeur (les abstractions)
- Propriétés
- determinisme, correspondence entre SOS et naturelle
- Evaluateur
- naif en appel par nom et par valeur