Révisions de Lambda-Calcul

Exercices, projets etc relatifs au Master d'Informatique
Post Reply
User avatar
Vincent
Posts: 3077
Joined: Fri Apr 07, 2006 12:10 pm
Location: Schtroumpf
Contact:

Révisions de Lambda-Calcul

Post by Vincent » Thu Oct 16, 2008 12:06 pm

Hier, les sujets suivants ont été couverts:

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 :?
{ Vincent Hugot }

Post Reply

Who is online

Users browsing this forum: No registered users and 71 guests