Cours0304

1 Introduction

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
Termes, et sigma-algebres: notion de sigma algebre, de homomorphisme, termes et substitutions, theoremes de Birkhoff Notes preliminaires de cours
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.
Introduction au lambda calcul: lamda termes, substitution, notion de reduction b et d'égalité b

Confluence du lambda calcul: preuve par le biais de la technique des reductions parallèles
Définitions de base: type, jugement de typage, derivation de typage
Propriétés: unicité de la derivation de typage, decidabilité de la typabilité,
Subject Reduction: preuve par induction sur la derivation de typage
Inférence de type: esquisse de la methode de reconstruction de type par resolution d'équations engendrées sur les noeuds de la squelette de l'arbre de derivation

Normalisation forte du lambda calcul simplement typé: par la méthode dite de réductibilité, qui utilise des relations logiques.

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)
Exemple: évaluation des nombres binaires
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, heritage des propriétés de subject reduction et de normalisation forte de la version typée

evaluateur simple: critique de l'opération de substitution
machine de Krivine: : notion de fermeture (Closure), environnement et pile; définition d'état (c,e,s) et de la table de transition
propriétés: : définition de depliage d'une fermeture et de relecture d'un état.
théorème de correction: si (c,e,s) transite sur (c',e',s'), alors les relectures sont b équivalentes.
raffinement du théorème: si (c,e,s) transite sur (c',e',s'), alors soit les relectures sont identiques, soit la prémière reduit en une étape b sur la deuxième
raffinement ultérieure: l'eventuelle étape b est bien une étape de reduction en appel par nom. Ceci donne enfin une partie de la correction de la machine.

l'approche denotationnelle de la semantique: survol
semantique d'un langage fonctionnel simple: approche simple avec les ensembles
modeliser la non terminaison:: les ordres partiels complets (CPO)
extension du langage:: erreurs, exceptions, etat
les continuations:: modelisation des sauts