motivation du lambda-calcul
définition formelle de l'ensemble des lambda termes
"sens" des lambda-termes. Parallèle avec les maths
alpha-équivalence
variables libres et liées
définition formelle de l'ensemble des variables libres
substitution brutale et capture de variable
beta-redex
beta-réduction
beta-forme normale
évaluation par nom/valeur
théorème de church-rosser (unicité bnf)
existence de la Beta-forme normale?
et je crois que c'est tout.
Pour une prochaine séance, je propose
retour rapide sur la def des lambda termes: voir les lambda termes non plus comme un ensemble, mais comme un langage
contruction des booleens
fonctions logiques (and etc)
construction des entiers de church
arithmétique sur les entiers de church
théorème du point fixe (curry, turing)
application aux équations
définition de factorielle en lambda-calcul
eta-réduction et eta-equivalence
même chose avec beta-eta
indécidabilité de l'existence d'une beta-forme normale
et avec ça, je pense qu'on aura quand-même l'essentiel du cours d'Hufflen
Un horaire possible en dehors du jeudi est le Lundi après la réunion de Compilation
