Cours de λ-calcul pour l’agrégation d’informatique

Le cours est donné par Jean Goubault-Larrecq, et est en trois parties—oups, en deux parties pour 2023-24. 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 λ-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 λ-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, 64;
    • un codage direct des machines de Turing vers le λ-calcul: 65, 66, 67, 68, 69;
  • stratégies de réduction, standardisation, et quelques techniques d’implémentation du λ-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 λ-calcul et machines de Krivine: 56, 57, 58, 59;
    • indices de de Bruijn: 73, 74, 75, 76, 77;
    • combinateurs de Curry-Schönfinkel: 78, 79.

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 λ-calcul): 70, 71, 72.