Cours de lambda-calcul pour l'agrégation d'informatique

Le cours est donné par Jean Goubault-Larrecq, et est en trois parties. Les exercices sont regroupés en un seul gros document ici, et c'est à ce document que font référence les numéros d'exercices ci-dessous. En détail:

• introduction au lambda-calcul, β-réduction, α-renommage, non-terminaison, confluence: les transparents en version longue (avec animations, comme en cours), et en version courte; exercices:
  • pour s'entraîner à la β-réduction: 1, 2, 3, 4;
  • quelques propriétés de base de la β-réduction et des substitutions: 5, 7, 8, 9, 10;
  • pour s'entraîner avec la réduction parallèle: 6, 18 (faire le 17 avant);
  • pour explorer un peu plus la notion de confluence: 11, 12, 13, 14, 15, 16;
  • pour aller plus loin: 19, 20, 21, 22, 23, 24, 25;
• pouvoir expressif, théorème de Kleene (fonctions lambda-définissables=récursives=semi-calculables): les transparents en version longue (avec animations, comme en cours), et en version courte; exercices:
  • opérations arithmétiques: 26, 27, 28, 29;
  • pour aller plus loin (les listes): 30, 31, 32;
  • la fin du théorème de Kleene (nécessite la standardisation, qu'on verra au cours suivant): 60, 61, 62, 63;
  • un codage direct des machines de Turing vers le lambda-calcul: 64, 65, 66, 67, 68;
• stratégies de réduction, standardisation, et quelques techniques d'implémentation du lambda-calcul: mêmes transparents que la dernière fois; exercices:
  • appel par valeur, et une traduction par passage à la continuation: 33, 34, 35, 36, 37;
  • réductions de tête: 43, 44;
  • réductions de tête faibles: 45;
  • implémentations du lambda-calcul et machines de Krivine: 56, 57, 58, 59;
  • indices de de Bruijn: 72, 73, 74, 75, 76;
  • combinateurs de Curry-Schönfinkel: 77, 78.

En plus, quelques théorèmes non vus (ou dont la démonstration ne sera pas vue en détail) en cours:

• théorème des développements finis: 38, 39, 40, 41, 42;
• standardisation: 46, 47, 48;
• termes résolubles et formes normales de tête: 49, 50;
• étiquettes de Hyland-Wadsworth, et une autre preuve du théorème des développements finis: 51, 52;
• étiquettes de Lévy, un autre preuve de confluence, une autre stratégie standardisante (les réductions quasi-internes): 53, 54, 55;
• le théorème de Scott-Curry (un analogue du théorème de Rice en lambda-calcul): 69, 70, 71.