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.