David Madore's WebLog: Débriefing de mon cours Logique et Fondements de l'Informatique

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]

↓Entry #2791 [older| permalink|newer] / ↓Entrée #2791 [précédente| permalien|suivante] ↓

(mardi)

Débriefing de mon cours Logique et Fondements de l'Informatique

J'avais expliqué il y a quelques mois que je m'étais engagé à monter un nouveau cours d'informatique théorique (ou faut-il dire de maths de l'informatique ?) pour certains élèves de première année à Télécom PlusÀParis, intitulé Logique et Fondements de l'Informatique (nom de code interne : INF110). (J'avais d'ailleurs publié un premier jeu de transparents dans de billet.) L'occurrence 2023–2024 de ce cours a eu lieu de à , le contrôle le , et maintenant (enfin, quelques mois après) que j'ai à la fois rendu les notes finales et reçu les retours (anonymes) des étudiants je suis en mesure d'en faire un premier bilan. L'idée de ce billet n'est pas tellement d'entrer dans le fond du sujet (même si je ne peux pas ne pas en parler du tout), à ce sujet voir plutôt les deux paragraphes ci-dessous, mais de parler au niveau méta : pourquoi ce cours, pourquoi ce sujet, comment je l'ai organisé et préparé, ce qui a bien marché et ce qui n'a pas bien marché. Le but est de me permettre à moi-même de faire le point, et donc de réfléchir à ce que je veux changer l'an prochain, et aussi de préparer un exposé où je dois raconter tout ça (cf. la fin du présent billet).

☞ Pour le fond du sujet, je renvoie notamment à ce billet sur la correspondance de Curry-Howard et à celui-ci sur la réalisabilité propositionnelle, qui sont largement adaptés de certains bouts de mon cours, même si la présentation est différente et qu'ils vont plus loin (surtout le second). Je peux aussi renvoyer à ce billet sur des sujets variés en vrac sur lesquels j'ai appris des choses en préparant ce cours. Enfin, je fais un lien vers ce billet sur les degrés de Turing et leur généralisation parce qu'il touche à des questions adjacentes, même si je n'ai pas fait plus qu'évoquer la définition de degré de Turing (ordinaire) dans mon cours.

☞ Pour ce qui est des documents pédagogiques accompagnant le cours, voici quelques liens (dont, malgré ma passion pour la stabilité des URL, je ne garantis pas qu'ils seront pérennes, parce que je ne sais pas comment je vais les réorganiser à l'avenir). D'abord le PDF des transparents (qui est la concaténation idiote de trois parties inégales : ① calculabilité, ② typage simple et calcul propositionnel et ③ introduction aux quantificateurs ; j'ai aussi fait une version « imprimable » des transparents : , et ). Les exercices d'entraînement sont : ici sans corrigé et ici avec corrigé. Et le sujet du contrôle est ici sans corrigé et ici avec corrigé. Et si des gens sont intéressés par le source de tout ça, le dépôt Git est ici.

Avertissement usuel : même si j'évoque ici mon travail d'enseignant-chercheur à Télécom, je dois rappeler que, dans ce billet comme ailleurs sur ce blog, je m'exprime à titre purement personnel et que les avis et opinions que je peux exprimer ici (ou ailleurs) sont juste les miens et n'engagent en aucun cas mon employeur (ni qui que ce soit d'autre que moi, et d'ailleurs ils ne m'engagent même pas moi vu que que je me réserve le droit d'en changer à tout moment et sans prévenir). J'ajoute que si vous faites partie des personnes qui ont besoin d'un tel avertissement, il vous est interdit de lire la suite de ce billet.

Plan du billet

Le contexte

Comme je l'ai expliqué dans les billets déjà liés ci-dessus (celui-ci et celui-là), la France a récemment créé une filière MPI (maths, physique et informatique) dans ses classes préparatoires scientifiques[#]. En particulier, les élèves entrant à Télécom par le concours commun peuvent arriver avec trois niveaux de formation en informatique : le socle commun MP/PC (où il n'y a pas grand-chose en info), l'option informatique en MP (qui existait déjà), et la nouvelle filière MPI (qui va encore plus loin). Les programmes de toutes ces filières sont trouvables par exemple sur ce site). Ceci nous a imposé une réforme de nos enseignements en première année : jusqu'à l'été 2023 notre première année était complètement uniforme (en gros, tout le monde avait les mêmes cours, le choix d'une filière de spécialisation se faisant en seconde année), mais ce mode de fonctionnement devenait intenable, au moins pour ce qui est de l'informatique, avec de telles différences de formation à l'entrée (si on s'adapte à ceux qui en ont fait le moins, ceux qui en ont fait plus s'ennuient, et si on s'adapte à ceux qui en ont fait le plus, ceux qui en ont fait le moins sont largués).

[#] Au niveau de la reconnaissance de l'informatique comme une science à part entière, il y a aussi eu création d'une agrégation d'informatique pour le recrutement des enseignants alors que l'informatique était jusqu'alors considérée comme une option de l'agrégation de mathématiques. Et, un peu avant, des changements au niveau lycée avec la création d'une spécialité NSI, c'est-à-dire numérique et sciences informatiques, mais ça ne me concerne que beaucoup plus indirectement : de ce que je comprends, à cause de la limitation à deux spécialités en terminale, la (grande ?) majorité des élèves de prépa, y compris MPI, n'ont pas suivi cette spécialité NSI en terminale, mais bien maths et physique-chimie.

Mais ce n'est pas, en fait, qu'une question de niveau en entrée : les élèves ayant choisi la filière MPI semblent avoir des attentes et des intérêts différents de ceux de la filière MP (même « option info »), au sens où ils semblent généralement plus intéressés par l'informatique pour elle-même et pas juste comme un outil dans un travail d'ingénieur (parce qu'évidemment tout le monde utilise l'informatique de nos jours). Et un des buts de la réforme que nous avons mise en place est de rentre Télécom plus attirante pour les préparationnaires vraiment intéressés par l'informatique, avec notamment l'idée qu'il ne faut pas qu'ils s'ennuient en cours.

La première année à Télécom est (maintenant) divisée en quatre périodes. Pour ce qui est de l'enseignement d'informatique, voici comment nous avons organisé l'année. La période P1 (septembre–octobre) a été dédiée à une introduction générale à la programmation, du matériel au haut niveau, tandis que les élèves venus de la filière MPI (et uniquement eux) ont un cours spécifique sur la compilation. La période P2 (novembre–janvier) est consacrée à la théorie de l'informatique, et c'est celle qui me concerne et dont je vais reparler. La période P3 (février–avril) propose le choix entre différents paradigmes de programmation. Et la période P4 (avril–juin) est consacrée aux réseaux. Sur chacune de ces périodes, les élèves ont environ 40h d'informatique (sauf en P3, moitié moins), c'est-à-dire environ 4h½ par semaine pendant les 9 semaines que dure la période. (Pendant le même temps, les élèves ont bien sûr aussi des cours dans les autres domaines : maths, physique+électronique, sciences économiques et sociales, langues et humanités ; plus des projets et stages variés, notamment entre les périodes. Je dis ça pour situer un peu l'enseignement dans son volume global.)

Pour ce qui est de l'enseignement d'informatique de la période P2 de première année, donc, nous avons divisé la population d'élèves en deux sous-populations inégales : ceux qui sont entrés par les filières MPI ou MP option info du concours commun ainsi que les admis sur titres après une licence d'informatique, soit au total ~90 élèves, et tous les autres, qui doivent représenter à peu près ~120 élèves. Les premiers ont eu le cours INF110 dont je me suis chargé et dont je parle ici, tandis que les seconds ont eu un cours (INF109) plus général sur l'algorithmique fondamentale et quelques rudiments de la calculabilité (recouvrant notamment une partie de ce que les autres élèves avaient déjà vu en prépa).

Bref, s'agissant de INF110, j'avais à m'occuper de 39 heures d'enseignement (contrôle de connaissances non compris), étalées sur 9 semaines, pour ~90 élèves. Nous avons décidé de séparer ces 39h en 21h de cours magistraux, et 18h de TD+TP lesquels ont été pris en charge par mon collègue Théo Z. Pour des raisons d'organisation de l'emploi du temps global de la première année, il n'était pas possible de regrouper les élèves tous ensemble pendant les cours magistraux, donc j'ai donné deux fois chaque séance (on arrive donc à 42h pour moi, si vous suivez).

De l'opportunité d'enseigner des sujets théoriques

Il faut que je dise ici un mot pour évoquer la question qui revient de façon récurrente dès qu'on parle de dispenser des cours assez « théoriques » (whatever that means) à des élèves majoritairement[#2] futurs ingénieurs. J'avais déjà droit à ce genre de remarques quand j'enseignais l'analyse de Fourier (cf. par exemple ce billet) : à quoi ça sert d'expliquer à des futurs ingénieurs la différence entre la transformée de Fourier dans L¹ et dans L² ? ce n'est pas ça qui va leur servir : de toute façon leur signal sera un ensemble fini de valeurs. Donc inévitablement on peut se demander pourquoi enseigner la calculabilité ou la logique intuitionniste quand ce même temps pourrait être employé à faire des cours de JavaScript et de Python, parce que c'est ça qui va leur servir — ou bien d'IA puisque maintenant tout le monde se rue sur l'IA comme des lemmings sur la falaise.

[#2] Je précise que majoritairement ne signifie pas exclusivement. Même sans parler des cas vraiment exotiques, et il y en a toujours (après tout, j'ai dans ma promo à Normale Sup un camarade qui a décidé que la passion de sa vie c'était le cirque, et qui a donc fait carrière dans les arts du spectacle après une thèse de physique quantique), il y a quand même une proportion, faible mais non complètement négligeable, d'élèves à Télécom qui décident de faire de la recherche plus ou moins théorique, c'est-à-dire de faire une thèse et éventuellement d'en faire carrière. Néanmoins, j'entends bien l'argument selon lequel l'enseignement ne doit pas se construire en fonction des intérêts d'une minorité. Donc ce n'est pas l'argument que j'invoque ici pour justifier l'intérêt de mon cours.

J'avais déjà répondu à cette objection, mais je ne sais pas si ma réponse me satisfait beaucoup. Disons que si un ingénieur n'est pas un chercheur (dont le métier consiste à proposer de nouvelles théories), il n'est pas non plus un technicien (dont le métier consiste à appliquer des techniques existantes) : l'ingénieur est justement là pour faire le pont entre les deux, pour appliquer la théorie à la création de nouvelles techniques ou au perfectionnement de celles qui existent, ce qui implique de bien maîtriser la théorie de son domaine, avec un certain recul sur celle-ci, pas juste comme des recettes de cuisine apprises par cœur. (Je devrais, ici, faire référence à la nouvelle Profession d'Asimov, mais c'est un peu difficile à faire sans divulgâcher ; donc je vais me contenter de dire : lisez-la.)

On se trompe gravement, je pense, en voulant centrer l'enseignement sur ce qui sert (ou plutôt, on se trompe gravement en ne mesurant pas toutes les manières dont quelque chose peut servir) : le but de l'enseignement, quel que soit son niveau, n'est pas principalement, ou en tout cas pas exclusivement, de fournir des outils qui serviront mais aussi des clés de compréhension de phénomènes, des cadres dans lesquels analyser ce à quoi on est confronté. Les outils, ce n'est pas qu'il ne faut pas les apprendre, mais ils ont tendance à être hautement spécifiques à une tâche précise, les outils nécessaires à tel ou tel métier s'apprennent normalement en entrant dans ce métier, ce n'est tout simplement pas le rôle de l'enseignement de former à s'en servir (sauf dans la mesure où ces outils sont extrêmement transverses). S'agissant de l'informatique, donc, on se trompe par exemple en pensant qu'il faut enseigner les langages de programmation qui seront utilisés ensuite : un langage de programmation, ça s'apprend rapidement, l'intérêt de les enseigner n'est pas d'enseigner ce qui servira mais d'enseigner ce qui permet de comprendre les différentes approches[#3] de la programmation et les différentes façon de concevoir une tâche.

[#3] Sur les langages de programmation, ce que je dis c'est que ça n'a, selon moi, aucun intérêt de se dire je vais apprendre/enseigner JavaScript et Python parce que c'est ce qui me/leur servira après ; il faut plutôt se dire je vais viser un échantillon représentatif des différents styles de langages de programmation pour comprendre les différentes approches : un langage bas niveau pour comprendre comment fonctionne la gestion de la mémoire, un langage purement fonctionnel et paresseux pour comprendre comment conceptualiser les tâches par une programmation d'ordre supérieur, un langage orienté objet pour comprendre le concept d'héritage, un langage distribué pour comprendre les difficultés de la programmation asynchrone et la manière dont on les résout, etc.

Donc l'intérêt d'enseigner la calculabilité, ce n'est certainement pas parce que ça va servir (même s'il est certainement utile qu'un ingénieur sache que certaines tâches ne sont pas réalisables algorithmiquement — et qu'en gros toute tentative d'analyser le comportement d'un programme devra reposer sur des heuristiques qui seront fatalement imparfaites), mais aussi parce que cela amène à prendre du recul sur les concepts fondamentaux de l'informatique (la récursion, l'auto-référence, la nature de l'évaluation dans les langages de programmation, la raison pour laquelle on se retrouve si facilement à être Turing-complet par accident — et peut-être aussi le fait que ce n'est pas très pertinent de chercher à l'éviter). À titre d'exemple, s'agissant de l'auto-référence, je dirais que quelqu'un qui a du recul sur la calculabilité et le théorème de récursion de Kleene ne sera absolument pas surpris par le fameux hack de Ken Thompson[#4] (d'ailleurs, Thompson lui-même explique le lien entre les quines et son hack), et c'est pertinent pour pouvoir prétendre maîtriser la sécurité informatique. Je peux dire quelque chose d'analogue pour le typage : ce n'est pas juste que c'est utile de comprendre les bases du typage et du polymorphisme parce que certains langages réellement utilisés en ont, mais c'est aussi nécessaire pour comprendre ce qui se passe (par exemple quand on cache des valeur dans une clôture, quand on passe des valeurs par continuation — ce qui sont des paradigmes de programmation qui servent vraiment).

[#4] Dans Reflections on Trusting Trust, Thompson explique qu'il avait introduit une backdoor dans le programme login, puis modifié le compilateur C pour introduire lui-même cette backdoor si elle ne s'y trouvait pas, puis pour introduire cette backdoor dans le compilateur C lui-même, si bien qu'au final il pouvait recompiler le compilateur avec les sources d'origine et la backdoor persistait dans le binaire. Voilà quelque chose qui, au minimum, ne doit pas surprendre un ingénieur en sécurité informatique.

Maintenant, prendre du recul n'est pas quelque chose qui se fait en un jour, ni même en un trimestre : c'est une maturation progressive (et j'ai dit que j'avais moi-même pris conscience de certaines choses en préparant ce cours), donc je ne peux certainement pas m'attendre à ce qu'après ce que je leur ai raconté pendant 21h ces élèves aient été Éclairés quant à la nature de l'auto-référence ou du passage par continuations, qui sont des questions méritant une réflexion assez prolongée[#5], mais j'espère au moins leur avoir donné des clés pour comprendre (et des directions dans lesquelles chercher) des choses qui ne s'apprennent pas aussi facilement qu'un (++n)-ième langage de programmation.

[#5] À un certain niveau, j'ai été tenté de renvoyer mes élèves au livre Gödel, Escher, Bach de Hofstadter, et d'ailleurs j'y ai quelquefois fait référence. Dans une autre direction, j'ai aussi fait référence au Wizard Book, et peut-être que certains auront la bonne idée d'aller le lire, ce qui est indiscutablement une expérience enrichissante. (Dans mon cas ces deux livres ont profondément transformé ma perception de l'informatique et de la programmation.)

Le point est potentiellement contentieux, ce qui est la raison pour laquelle j'ai pris l'espace de le développer ici, mais en fait j'ai été agréablement surpris de voir que, dans les retours (anonymes) que les élèves nous ont faits sur ce cours, les reproches du style c'est trop abstrait, c'est trop théorique, je ne vois pas à quoi ça sert ne revenaient pas trop souvent. Je ne dis pas qu'ils étaient absents, mais ils sont loin d'être majoritaires. Au contraire, il y avait plus de commentaires selon lesquels le sujet du cours était intéressant (et par ailleurs, un collègue qui a eu certains des mêmes étudiants après mon cours m'a dit que certains étaient vraiment fascinés par le λ-calcul[#6]). Et ce n'est pas forcément surprenant : on parle d'élèves qui sont (pour l'essentiel) sortis de classes préparatoires, où l'enseignement (qu'il s'agisse de maths, d'info ou de physique) est tout de même très théorique dans toutes les disciplines, et qui y ont souvent pris goût[#7] : il serait assez idiot de passer brutalement de là à un enseignement exclusivement tourné vers « ce qui sert ». Et de fait, j'ai essayé de concevoir le programme de mon cours dans la suite de ce qu'ils ont déjà vu en info en prépa.

[#6] Comme je l'ai écrit dans une note d'un billet passé, j'avais moi-même été complètement fasciné par la simplicité et l'élégance du λ-calcul quand j'ai appris le concept. (Je crois me souvenir que j'ai passé plein de temps à faire des expansions de λ-termes juste pour jouer avec.)

[#7] Pour ce qui est des maths, il y a à Télécom des élèves qui se réunissent de temps en temps pour réfléchir à des problèmes de maths pour le plaisir. On aurait donc tort de penser que ce genre de choses n'existe que dans les ENS.

Contenu et structure du cours

En concertation avec mes collègues, j'ai décidé de concentrer mon cours INF110 sur la logique, la calculabilité et le typage. C'est faire complètement l'impasse sur d'autres domaines essentiels de l'informatique théorique : algorithmique et complexité, notamment (alors que mes collègues qui enseignaient le cours parallèle INF109 se concentrent justement là-dessus) ; ce choix peut paraître surprenant (et on peut certainement le critiquer), mais il est notamment justifié, à nos yeux, par le fait que les élèves concernés ont déjà eu des cours d'algorithmique assez avancés en prépa et qu'ils auront d'autres occasions d'en faire dans le cadre d'autres cours à Télécom (soit dans le cadre d'un langage de programmation particulier, soit de façon plus abstraite pour ceux qui choisissent une filière théorique en seconde année) ; en outre, la logique, la calculabilité et le typage me semblent plus difficiles à apprendre par soi-même que tel ou tel algorithme standard.

J'ai essayé de trouver une cohérence d'ensemble (je ne sais pas si j'ai réussi à la faire passer aux élèves ni à les convaincre de son bien-fondé), ainsi que beaucoup de ponts entre les sous-sujets abordés. Le pont entre la logique et le typage, c'est la correspondance de Curry-Howard qui nous apprend que les preuves dans certains systèmes logiques correspondent exactement aux programmes dans certains langages de programmation fortement typés (encore une fois, je ne rentre pas dans le fond du sujet ici, je l'ai fait dans ce billet). Le pont entre la calculabilité et le typage, c'est le λ-calcul : si le λ-calcul non typé est équivalent à la calculabilité de Church-Turing en général, le λ-calcul typé (celui qui intervient dans Curry-Howard) peut garantir la terminaison des programmes, mais cette garantie de terminaison implique forcément une perte d'expressivité en raison du théorème de l'arrêt. Le pont entre logique et calculabilité, c'est le théorème de Gödel (qui est, après tout, aux racines de l'informatique puisque Turing était parti pour attaquer l'Entscheidungsproblem — et montrer qu'il n'existe pas d'algorithme décidant si un énoncé est ou n'est pas un théorème — quand il a introduit le concept de machine de Turing) : j'ai donc conclu le cours en donnant une preuve du théorème de Gödel dans l'esprit de Rosser et de Turing, qui s'appuie fortement sur les notions de calculabilité vues au début du cours[#8].

[#8] En gros, on écrit un programme g qui cherche en parallèle une preuve (dans l'arithmétique de Peano) que g termine et une preuve que g ne termine pas, et s'il trouve la première, il fait immédiatement une boucle infinie triviale, tandis que s'il trouve la seconde il termine immédiatement. (L'existence d'un tel programme autoréférent est garantie par l'« astuce de Quine », c'est-à-dire par le théorème de récursion de Kleene, et cette idée de preuve est très proche de celle qui m'a servi pour le théorème de l'arrêt. Il est assez facile de voir que, si l'arithmétique de Peano est cohérente, g ne va trouver ni l'une ni l'autre sorte de preuve.)

Plus en détails, et dans l'ordre dans lequel j'ai présenté les choses (en gros, sur 21h de cours magistral, j'ai passé 7h sur la grande partie ①, puis 10h sur la grande partie ②, et 4h sur la partie ③) :

① Calculabilité

✱ J'ai commencé par la calculabilité. Pour ça, j'ai choisi de définir les fonctions calculables comme celles qui sont générales récursives[#9] au sens de Herbrand-Gödel-Kleene, parce que c'est la définition qui me semble la plus à même d'être reliée aux deux autres, à savoir par les machines de Turing et par le λ-calcul.

[#9] Le terme récursif est vraiment pénible ici, parce qu'il a au moins trois sens différents : ⓐ récursif comme défini par récurrence, dû à Dedekind, ce qui est le sens dans lequel il faut comprendre fonction primitive récursive ou fonction générale récursive, ⓑ récursif comme calculable, justement comme abréviation de fonction générale récursive qui est une façon de définir la calculabilité de Church-Turing, et ⓒ récursif comme (défini par) appels récursifs, i.e., par appels à la fonction elle-même dans sa propre définition, ce qui est le sens usuel en informatique. Du coup, quand on veut expliquer que les fonctions générales récursives (au sens ⓐ ou ⓑ) permettent de réaliser la récursion (au sens ⓒ), c'est un peu confusant ! Mais bon, ça fait partie des choses qu'il est justement pertinent d'expliquer.

Je commence par parler des fonctions primitives récursives, pas tellement parce qu'elles sont importantes en elles-mêmes (même si peut-être que si), mais parce qu'elles sont très utiles pour illustrer le problème à vouloir une notion d'algorithme qui termine à tous les coups. (Tous les algorithmes classiques sont primitifs récursifs, parce qu'en gros dès qu'on est capable d'écrire une complexité explicite, fût-elle en tour d'exponentielle, la fonction est primitive récursive. Pourtant, la notion n'est pas convenable, parce qu'on ne peut pas écrire un interpréteur des fonctions primitives récursives dans le langage des fonctions primitives récursives, et je pense que c'est une leçon très importante à retenir.)

J'ai passé beaucoup de temps à parler de l'« astuce de Quine ». Le terme d'astuce de Quine est relativement courant, mais comme souvent le théorème de Machin n'est pas dû à Machin : il s'agit ici essentiellement d'une idée de Turing basée sur l'argument diagonal de Cantor, reformulée ensuite par Kleene qui l'a énoncé comme un résultat autonome, son (second) théorème de récursion ; c'est Douglas Hofstadter qui a associé le nom de Quine (en hommage à l'intérêt porté par ce logicien aux opérations de citation et de référence, voire d'auto-référence) aux programmes qui font référence à eux-mêmes dans leur construction, par exemple des programmes affichant leur propre code source. (Peut-être que j'aurais plutôt dû utiliser le terme d'astuce d'auto-référence que d'astuce de Quine, enfin peu importe.)

Il me semble que cette astuce d'auto-référence (qui a beau être essentiellement triviale dans sa preuve : finalement c'est juste un argument diagonal) est un des concepts essentiels de l'informatique théorique, à tel point qu'on oublie sa centralité[#10]. Ce n'est pas qu'un outil théorique pour prouver le théorème de Gödel et celui de Cantor, ou pour montrer l'insuffisance des fonctions primitives récursives. Ce n'est pas qu'une curiosité de savoir qu'on peut faire un programme qui affiche son propre code. Ce n'est pas qu'une façon sophistiquée de formuler la récursion. C'est aussi, il me semble, au cœur de toute notion de métaprogrammation, d'interpréteur métacirculaire, etc. (Pour en savoir plus à ce sujet, outre le Wizard Book que j'ai déjà référencé, je peux renvoyé à cet exposé de William Byrd dont voici par ailleurs un compte-rendu.)

[#10] Yiannis Moschovakis a même écrit un article de survol, Kleene's Amazing Second Recursion Theorem, pour faire le tour de quelques unes de ses conséquences.

✱ Mais ceci m'amène, justement, à passer aux fonctions générales récursives, qui ajoutent aux fonctions primitives récursives la construction de recherche non bornée, ou opérateur μ de Kleene. (Idéalement j'aurais voulu faire encore un pont entre calculabilité et logique et parler quelque part dans mon cours du principe de Markov qui est une sorte d'analogue logique de l'opérateur μ de Kleene, mais ceci partait vraiment trop loin, donc j'ai sabré cette notion.)

Ce qui différencie profondément les fonctions générales récursives des primitives récursives, c'est l'existence d'une machine universelle : il existe une fonction générale récursive qui prend en entrée le code de Gödel d'une (autre) fonction générale récursive et une entrée à celle-ci, et qui évalue la fonction en question sur cette entrée (quitte à n'être elle-même pas définie si cette évaluation n'est pas définie).

La notion de machine universelle est elle aussi un des concepts centraux de l'informatique, car il s'agit de la notion d'interpréteur (d'un langage de programmation dans un autre, y compris dans lui-même). C'est la chose essentielle qui manque aux fonctions primitives récursives : elles ne peuvent pas s'interpréter elles-mêmes, alors que les fonctions générales récursives, elles, le peuvent.

Dans mon cours, je démontre le résultat d'universalité pour les fonctions générales récursives à travers la notion d'arbre de calcul (en gros, un arbre de calcul est une trace d'exécution de la fonction générale récursive, qui atteste que le calcul a bien été mené). La preuve est, bien sûr, profondément inutiles algorithmiquement : cela revient à dire que pour exécuter un programme on va parcourir toutes les traces d'exécutions possibles jusqu'à en trouver une qui ait suivi les règles à chaque étape (enfin, nœud de l'arbre). Néanmoins, cette preuve a des leçons à nous donner (outre qu'elle montre comment on exploite l'opérateur μ de Kleene) : elle débouche notamment sur le théorème de la forme normale de Kleene, qui permet de lancer deux calculs en parallèle, et on peut dire que c'est le cœur théorique de la notion de scheduler.

Et quand on met ensemble l'auto-référence (l'astuce de Quine) et l'universalité, on obtient la notion d'appels récursifs (fonction qui s'appelle elle-même). Cette façon d'aborder la récursion est hilarante d'inefficacité algorithmique (je suis en train de dire que pour coder une fonction à appels récursifs, on peut utiliser l'astuce de Quine pour écrire la fonction de façon autoréférente, et remplacer les appels récursifs par l'évaluation d'un interpréteur qu'on aura codé dans la fonction), mais elle permet de bien comprendre pourquoi on tombe si facilement sur des langages Turing-complets, et pourquoi l'indécidabilité du problème de l'arrêt est si difficile à contourner : dès qu'on met ensemble la possibilité d'autoréférence (qui est un simple argument diagonal, donc essentiellement inévitable) avec l'universalité (qui correspond à la demande philosophique que l'opération d'exécuter un algorithme soit elle-même algorithmique, ce qui est la moindre des choses), inévitablement on va tomber sur la possibilité d'un algorithme qui s'exécute lui-même, donc des cas de récursion qui ne termine pas.

Bref, je termine cette partie en démontrant le théorème de Turing sur l'indécidabilité du problème de l'arrêt, qui est maintenant une conséquence presque immédiate des idées que j'ai introduites.

✱ Ensuite, j'ai présenté les machines de Turing et l'équivalence entre la calculabilité par machines de Turing et les fonctions générales récursives.

Pas de subtilité particulière sur ce point. J'ai globalement suivi Odifreddi (Classical Recursion Theorydisponible en ligne ici —, I.§4), à quelques détails près, pour la manière de formuler la calculabilité par machine de Turing, notamment pour la convention sur la manière dont on écrit les nombres en entrée sur le ruban et dont on lit la sortie, de manière à faire marcher l'induction. (Mais réfléchir à ce qui marche et ce qui ne marche pas a été l'occasion pour moi de me rendre compte que tout n'était pas aussi évident que je le pensais.)

Montrer constructivement l'équivalence entre fonctions générales récursives et machines de Turing est intéressant parce qu'il s'agit, quand on y réfléchit, d'écrire un compilateur (et on se rend compte que c'est assez fastidieux, ce qui est quand même instructif parce que ça rend d'autant plus frappant qu'on tombe sur la Turing-complétude dès qu'on a ne serait-ce que deux symboles différents sur la bande, une seule bande et une seule tête). Mon collègue a fait travailler les élèves là-dessus dans le cadre d'un TP.

✱ Ensuite j'ai traité de différents résultats généraux sur la calculabilité « abstraite » : la notion d'ensemble décidable (= récursif), semi-décidable (= récursivement énumérable), le fait que décidable ⇔ semi-décidable et de complémentaire semi-décidable (avec pour preuve l'idée de « lancer en parallèle » deux calculs), le fait que semi-décidable ⇔ image d'un ensemble décidable, le théorème de Rice, la notion de réduction many-to-one et de réduction de Turing.

Je ne suis pas entré dans le moindre détail sur les degrés de Turing à part juste mentionner leur définition. (Mais je note que des élèves avaient l'air intéressés par la question de l'existence de degrés semi-décidables intermédiaires entre 0 et 0′, ce qui est d'ailleurs quelque chose que je dois essayer de vulgariser dans ce blog Un Jour®.)

✱ Pour clore la grande partie sur la calculabilité, j'ai parlé de λ-calcul non typé (j'ai gardé ça pour la fin parce que ça permet de faire le pont avec le typage) : je ne suis pas entré dans trop de détails, j'ai juste défini la β-réduction, énoncé le théorème de confluence de Church-Rosser (unicité de la β-réduction), et défini la stratégie de β-réduction extérieure gauche, mais je n'ai rien dit, par exemple, sur la η-conversion.

Globalement, je suis sans doute allé trop vite sur cette partie, en supposant à tort que la β-réduction était une opération simple à comprendre, et j'ai aussi eu tort de ne pas prendre plus de temps pour expliquer le rapport avec les langages de programmation fonctionnels.

Pour l'équivalence entre fonctions générales récursives et λ-calcul non typé, j'ai de nouveau suivi Odifreddi (I.§6) : j'ai défini les entiers de Church, puis une convention pour la représentation des couples, et j'ai utilisé le combinateur Y de Curry pour montrer comment on peut faire de la récursion dans le λ-calcul même si le λ-calcul ne permet pas a priori de faire de la récursion.

Là aussi je suis certainement allé trop vite. Le sujet est délicat et il y a des chausse-trapes un peu partout[#11]. Le codage des couples n'est pas évident, l'utilisation du combinateur Y n'est pas évident, et comme mes élèves n'ont a priori pas fait de langage fonctionnel non typé avant (p.ex., pas de Scheme), ce n'est pas du tout facile de raccrocher ça à des notions qui leur parlent. Bref, il faut certainement que je retravaille cette partie, ou au moins que j'y passe plus de temps.

[#11] Par exemple, j'avais fait remarquer dans ce billet que la preuve donne des normalisations faibles — dans le cadre de mon court j'ai opté pour la β-réduction extérieure gauche — et ce n'est pas du tout évident, du coup, même si c'est vrai, que le fait qu'un terme du λ-calcul soit fortement normalisable est aussi indécidable.

② Typage simple et calcul propositionnel

✱ Deuxième grande partie de mon cours : le typage simple (i.e., sans quantificateurs / types dépendants) et son rapport avec la logique propositionnelle.

J'ai commencé par parler de typage en général en informatique, pour introduire un peu la terminologie (sous-typage, polymorphisme, familles de types, types récursifs, types dépendants, types opaques, vérification de type versus inférence de type, ce genre de choses) et expliquer la variété des systèmes de typage (il y a autant de systèmes de typage que de langages de programmation). Puis j'ai évoqué de façon très informelle la correspondance de Curry-Howard, et mentionné la notion de théories des types et le λ-cube de Barendregt (peut-être que je n'aurais pas dû).

✱ Ensuite j'ai défini de façon précise le λ-calcul simplement typé (c'est-à-dire avec uniquement des variables de type et des types ‘→’, i.e., fonctions), donné ses règles de typage, expliqué que retrouver l'arbre de typage d'un terme complètement annoté est évident, ou inversement retrouver l'annotation à partir de l'arbre de typage. J'ai énoncé le théorème de normalisation de Tait en donnant juste une idée de la preuve, mais je ne sais pas si c'était une bonne idée ni si l'idée telle que je l'ai exposée était éclairante.

✱ Puis j'ai défini le calcul propositionnel intuitionniste avec tous ses connecteurs (‘⇒’, ‘∧’, ‘∨’, ‘⊤’ et ‘⊥’), en style déduction naturelle, avec plusieurs présentations des démonstrations (arbres de séquents complets, arbres d'énoncés, drapeaux). Là ce sont des choses que les élèves sont censés avoir vu en prépa, mais pas forcément complètement (le programme de prépa ne dit rien sur la présentation des démonstrations, et ne dit même pas si la logique étudiée est la logique classique ou intuitionniste, donc tous n'ont certainement pas tout vu, et j'ai préféré ne pas supposer quoi que ce soit déjà connu).

J'en ai profité pour faire un peu d'histoire des maths et d'expliquer la raison et l'intérêt des maths constructives / de l'intuitionnisme. (À ce sujet, je renvoie au début de cet autre billet.)

Puis j'ai présenté la correspondance de Curry-Howard dans le cadre du calcul propositionnel, c'est-à-dire le lien entre le calcul propositionnel intuitionniste et le typage du λ-calcul, en introduisant des constructions (types produits, types sommes, type unité et type vide) pour correspondre aux connecteurs ‘∧’, ‘∨’, ‘⊤’ et ‘⊥’. (Là aussi, sur le fond du sujet, je renvoie à un autre billet.)

J'ai essayé d'illustrer ce que je disais par des exemples en OCaml (langage que les élèves ont vu en prépa) et/ou en Haskell (langage qu'ils n'ont pas vu), l'idée de parler des deux étant aussi une façon de les inviter à découvrir de nouveaux langages, mais apparemment certains ont été plutôt inquiétés par ça. (Notamment, je n'ai pas assez clairement fait comprendre que je ne me servais de Haskell que comme illustration occasionnelle et que je ne leur demandais pas d'en apprendre quoi que ce soit.)

✱ J'ai aussi présenté le calcul des séquents. Mon but à cet égard était de présenter sommairement le théorème d'élimination des coupures (en calcul propositionnel intuitionniste formulé en calcul des séquents), sans en donner une démonstration complète mais en esquissant l'algorithmique de l'élimination des coupures. L'intérêt est quand même surtout de savoir qu'il existe une démonstration sans coupure, parce que c'est la meilleure justification que je connaisse du fait qu'on peut décider algorithmiquement si une formule (du calcul propositionnel intuitionniste) est ou n'est pas un théorème.

Rétrospectivement, je pense que c'était une erreur. Je n'ai pas (trop) largué les élèves sur ce point, mais ce n'est pas très intéressant. En revanche, il faut quand même trouver une manière de justifier qu'on peut décider les théorèmes du calcul propositionnel intuitionniste.

J'ai aussi très rapidement parlé des combinateurs SKI et de l'élimination des lambdas. C'est intellectuellement intéressant de savoir qu'on peut faire un langage de programmation fonctionnel sans aucune variable (mais qui a bien pu faire un truc pareil ?), mais peut-être que c'était une distraction. Les axiomes de Hilbert qui correspondent aux (types des) combinateurs SKI sont cependant une façon très efficace et concise de définir le calcul propositionnel intuitionniste, donc ce n'est peut-être pas si inutile que ça.

✱ Ensuite, j'ai passé un bon bout de temps de mon cours à parler de continuations, de la fonction call/cc (=call-with-current-continuation) et de continuation-passing-style (CPS). Là il faut que je reconnaisse clairement que ça a été un désastre.

La raison pour laquelle je jugeais opportun d'un parler est la combinaison des choses suivantes :

  • Les continuations sont un concept important de programmation : c'est une abstraction de l'état de la pile ou de la notion de coroutine. C'est aussi ce qui est derrière le multitâche (coopératif, disons), c'est essentiellement la notion de « promesse » en JavaScript. En outre, cela permet de prendre du recul sur la notion de contrôle de flot d'exécution (j'aime bien faire remarquer que si la notion de clôture est une réification des variables locales qui leur fait échapper à la discipline de pile, la notion de continuation est l'analogue pour le code).
  • La conversion CPS est une technique importante pour réaliser soit un interpréteur soit un compilateur. Elle permet en outre de prendre du recul sur la notion de pile (dans un langage à recursion terminale propre, le programme converti en CPS n'utilise plus du tout la pile, tous les empilements d'appels sont transformés en créations de continuations-de-fait qui sont récupérées par le ramasse-miette).
  • Les deux points précédents concernent le call/cc non typé. Mais le call/cc typé est remarquable lui aussi, parce que son type est (enfin, correspond via Curry-Howard) précisément celui de la loi de Peirce ((PQ)⇒P)⇒P qui est une façon d'axiomatiser la logique classique au-dessus de la logique intuitionniste. En outre, la manière dont le call/cc permet d'habiter un type comme P∨¬P est instructif sur la manière dont le call/cc manipule le flot d'exécution (il permet en quelque sorte de revenir dans le temps : on commence par dire ¬P, et si quelqu'un fournit un P qui donnerait une contradiction, on « revient dans le temps » pour fournir ce P-là).
  • Et du coup, la conversion CPS correspond, via Curry-Howard, à une façon de plonger la logique classique dans la logique intuitionniste en ajoutant des ‘¬¬’ un peu partout. Ce qui s'avère utile du point de vue strictement logique.

Tout ça est à mon avis intéressant et important, mais… ça fait beaucoup trop à expliquer pour le temps et/ou le public dont je disposais. Parce qu'en plus il y a plein de subtilités cachés un peu partout, comme la distinction entre le call-by-value et le call-by-name (qui donnent deux transformations CPS différentes ; le typage n'est d'ailleurs pas évident). Je ne me suis rendu compte de ça que trop tard.

Donc ce bout du cours a été véritablement désastreux : j'ai perdu à peu près tout le monde, j'ai même certainement dégoûté certains élèves, et même en rattrapant du mieux que j'ai pu en disant que je n'attendais que le strict minimum sur ce sujet à l'examen (au final je n'ai rien mis dessus), le mal était fait. C'est dommage, et c'est indiscutablement ma faute. Je vais supprimer largement ou complètement cette partie l'an prochain (je ne sais pas si je peux en sauver quoi que ce soit ou si vraiment tout doit partir, mais c'est sûr que l'essentiel doit partir).

✱ Ensuite, j'ai fait le choix (qui n'était pas prévu initialement) de parler de sémantiques du calcul propositionnel intuitionniste. Je pense que c'est important pour plusieurs raisons : d'abord, philosophiquement, ça permet d'expliquer le « sens » de cette logique (la logique classique on comprend bien ce qu'elle veut dire à travers la notion de valeur de vérité booléenne… mais la logique intuitionniste, c'est moins clair comment il faut l'interpréter) ; ensuite, outre que la notion générale de sémantique est un concept fondamental en logique, c'est quand même la meilleure façon de prouver qu'un énoncé n'est pas démontrable, et dans le cadre de la logique intuitionniste ce n'est quand même pas terriblement compliqué. Mais en plus, chacune des sémantiques que j'ai introduites (ci-dessous) nous apporte un éclairage un peu différent sur l'intérêt du la logique intuitionniste.

J'ai donc décrit quatre sémantiques différentes (plus un numéro zéro qui est juste la sémantique booléenne, histoire d'illustrer les mots correct et complet : la sémantique booléenne est correcte et complète[#12] pour le calcul propositionnel classique, mais elle n'est que correcte pour le calcul propositionnel intuitionniste) :

  1. La sémantique de Kripke, ou des mondes possibles (en fait, c'est une sémantique pour la logique modale, mais on l'applique à une façon de comprendre la logique propositionnelle comme une logique modale particulière : je n'ai pas raconté ça en cours). Celle-ci est intéressante parce qu'elle permet de comprendre la logique propositionnelle comme parlant de possibilités qui évoluent (par exemple dans le temps).
  2. La sémantique des ouverts (due à Tarski, mais qu'il vaut mieux éviter d'appeler comme ça, parce que la sémantique tarskienne c'est plutôt autre chose). Celle-ci est intéressante parce qu'elle permet de comprendre la logique propositionnelle comme parlant de vérité locale (et de façon sophistiquée, cela débouche sur les topos de faisceaux).
  3. La sémantique de la réalisabilité propositionnelle (dont j'ai parlé de façon détaillée dans ce billet). Celle-ci est intéressante parce qu'elle parle vraiment d'algorithmes et de calculabilité (et de façon sophistiquée, c'est la partie propositionnelle du topos effectif), donc cela conduit à poser un autre regard sur Curry-Howard et sur les limitations qu'apporte le typage.
  4. La sémantique de Medvedev ou des problèmes finis, que je n'ai fait que mentionner rapidement (en gros c'est la même chose que la précédente mais avec des ensembles finis au lieu d'algorithmes : en principe c'est donc plus simple, mais pour des raisons de placement des quantificateurs cela peut paraître plus compliqué).

[#12] Peut-être est-il plus sensé de dire que c'est la logique qui est complète pour la sémantique que de dire que la sémantique est complète pour la logique, mais le second usage se trouve aussi, et donne des phrases vraiment plus simples.

Comme ça fait beaucoup, j'ai demander aux élèves de comprendre au moins une de ces quatre sémantiques (avec la promesse que si je leur demandais d'en appliquer une dans un exercice, n'importe laquelle permettrait de résoudre l'exercice).

Là je suis plutôt content parce que je crois que ça a été assez bien compris : je veux dire, ils ont compris l'intérêt d'étudier des sémantiques (le concept général), ça les a effectivement éclairé sur le sens de la logique intuitionniste (au moins sur la possibilité que ¬¬P ne soit pas la même chose que P), et ils ont généralement compris au moins un petit peu deux-trois de ces sémantiques.

C'est clairement la sémantique des ouverts qui leur a le plus « parlé » (elle est sympa parce qu'elle permet de faire des dessins qui montrent rapidement que tel ou tel énoncé est ou n'est pas démontrable, et parce que ça relie à des notions de maths qu'ils maîtrisent à peu près — même s'il faut quand même nuancer en soulignant que les ouverts de ℝ sont en fait beaucoup plus subtils que ce qu'on imagine en sortant de prépa ; et comme elle est complète, on a la garantie qu'on peut toujours s'en servir). La sémantique de TarskiKripke m'a semblé avoir été assez bien compris aussi, même si j'ai peut-être dû passer un peu trop de temps à faire des exemples. La réalisabilité propositionnelle a sans doute été moins bien comprise, mais je pense que grâce à ce qu'on avait vu sur Curry-Howard ils n'étaient pas complètement perdus non plus (je n'ai pas insisté trop longuement, mais j'ai quand même donné l'exemple de la formule de Ceitin pour montrer la non-complétude, et je pense que certains étaient intéressés). La sémantique de Medvedev n'était sans doute pas utile, mais je ne me suis pas appesanti dessus donc ce n'est pas grave.

✱ Enfin, j'ai terminé cette deuxième grande partie du cours en décrivant l'algorithme de Hindley-Milner pour l'inférence de type sur les termes du λ-calcul, parce que ça me semblait important d'expliquer un peu « ce que fait » OCaml (ou Haskell) dans la partie la plus simple de son système de typage. J'ai un peu parlé du problème du polymorphisme du let et de la restriction de valeur, mais sans entrer dans le moindre détail.

③ Introduction aux quantificateurs

✱ Après la grande partie sur la calculabilité et la grande partie sur le typage simple / logique propositionnelle, j'ai faut une troisième partie, beaucoup plus petite, sur les quantificateurs. Là il ne s'agissait clairement pas d'entrer dans autant de détails, mais juste de donner un aperçu du sujet.

J'ai donc commencé par expliquer assez informellement le sens de ‘∀’ et ‘∃’ du point de vue de la théorie des types (types produits paramétrés et types sommes paramétrés) et leurs règles d'introduction et d'élimination, et par évoquer très sommairement quelques unes des complications qui se posent et quelques unes des formes de quantifications qu'on peut admettre ou ne pas admettre (en gros, les axes du cube de Barendregt).

✱ J'ai décrit un peu plus précisément la logique du premier ordre, parce que c'est, quand même, la « logique standard » dans la vision orthodoxe des mathématiques (c'est-à-dire, à l'intuitionnisme près, la logique que les élèves sont censés avoir manipulée pendant toute leur scolarité). Du coup, j'ai introduit les axiomes de Peano et les arithmétiques de Heyting et de Peano.

(Mes transparents contiennent un certain nombre de résultats plutôt techniques sur le rapport entre arithmétique de Heyting et arithmétique de Peano : j'ai largement sauté ça en cours parce que c'était vraiment indigeste.)

✱ Enfin, j'ai fini par diverses variations autour du théorème de Gödel. Comme je l'ai dit dans une note plus haut, la preuve que j'ai donnée du théorème de Gödel (à la sauce Rosser et à la façon Turing) consiste à écrire un programme qui recherche en parallèle une preuve du fait qu'il termine et une preuve du fait qu'il ne termine pas, et qui fait trivialement le contraire de ce qu'il a trouvé. L'intérêt de cette preuve est qu'elle refait le lien avec ce qu'on a vu en calculabilité, ce qui boucle en quelque sorte la boucle du cours. J'ai aussi prouvé que l'ensemble des théorèmes (de l'arithmétique de Peano) n'est pas décidable, ce qui apporte une réponse négative forte à l'Entscheidungsproblem.

Cette dernière partie, bien sûr, relève plus des maths que de l'info, même si j'ai choisi une présentation « algorithmique » du théorème de Gödel (après tout, on construit explicitement un programme — on peut vraiment l'écrire, et le faire tourner — dont Peano, ou ZFC si on veut et si on le croit arithmétiquement correct, ne peut pas démontrer qu'il ne termine pas, bien que ce soit vrai), et même si ça nous dit quelque chose sur l'analyse de programmes (en gros, quel que soit le système formel choisi, il y a des programmes qui résistent à la preuve de programme). Mais le théorème de Gödel a un côté « spectacle », la preuve est un peu un mic drop, il faut être vraiment insensible à la logique pour ne pas être fasciné par la manière dont les choses tombent en place. Et il me semble que la plupart des élèves y ont été sensibles (même si j'ai dû en perdre pas mal).

Préparation et présentation

Vers mai 2023, j'avais décidé les grandes lignes du contenu que je voulais enseigner, en concertation avec mon collègue qui allait se charger des TD/TP. Je me suis dit que j'avais le temps de rédiger à la fois un jeu de transparents (le plus urgent), et un poly de cours avec des exercices. Famous last words! Comme le dit la loi de Hofstadter, ça prend toujours plus de temps que prévu, même quand on tient compte de la loi de Hofstadter. À force d'être toujours débordé, je me suis retrouvé à n'écrire que des transparents et exercices, et les transparents avaient de moins en moins d'avance sur le cours que je donnais, donc étaient écrits de plus en plus en vitesse, parfois même la veille au soir (donc forcément bourrés d'erreurs, dont certaines ont été corrigés en les lisant en cours, d'autres plus tard, et beaucoup restent encore à traquer). En matière de poly, tout ce que j'ai pu fournir est une version imprimable des transparents, et donc ça va constituer une de mes missions pour la rentrée prochaine que de transformer ça en un texte correctement rédigé.

Enseigner sur transparents demande une habitude que je n'ai pas vraiment. Sur certains contenus, quand il y a beaucoup de matière à couvrir et qu'on ne compte pas entrer dans les détails (ici je n'ai fait que très peu de preuves complètes), c'est difficile de faire autrement, mais personnellement je n'aime pas trop, ni comme orateur ni comme public.

En tant que public, au moins, je suis en désaccord profond avec beaucoup de conseils qu'on donne souvent sur comment faire de bons transparents. Par exemple, celui de ne pas mettre trop d'information dedans : or je trouve que c'est encore pire quand l'information n'est communiquée qu'à l'oral (si on cesse d'écouter une seconde, on perd le fil) ou bien si elle est étalée sur trop de transparents (comme on n'en voit qu'un à la fois, ça fait qu'on a une fenêtre d'attention artificiellement réduite). Je trouve aussi complètement insupportable (en tant que public) les transparents qui révèlent progressivement leur contenu : c'est infantilisant, et c'est horripilant quand je veux jeter un coup d'œil à ce qu'il y a en avant, sans compter que c'est extrêmement agaçant parce que ça me distrait de voir le texte apparaître ou changer de couleur. Personnellement, la présentation qui me plaît le plus, c'est quand le transparent liste clairement les points-clés et les informations nécessaires[#13] pour garder le fil du passé et pouvoir passer à la suite, et que l'orateur les lit (pas forcément verbatim, mais en substance) en insérant les détails nécessaires pour approfondir ou pour mieux comprendre ou pour rendre l'exposé plus vivant, mais qui peuvent être ignorés si on veut juste la substantifique moelle.

[#13] Ajoutons que, comme je n'ai pas eu le temps de faire un véritable poly, mes transparents convertis sous forme imprimable devaient en quelque sorte faire double fonction et pouvoir aussi servir de succédané de poly. Forcément, ça oblige à mettre quelque chose de pas trop elliptique sur les transparents !

Donc, un problème, déjà, c'est que je sais que la façon d'appréhender les transparents n'est pas universelle (beaucoup de gens ne sont pas d'accord avec ce que j'ai dit au paragraphe précédent), mais de l'autre je me vois mal suivre un mode de présentation que je trouve moi-même insupportable.

Je me suis retrouvé largement à lire mes transparents, et à commenter ce que je venais de lire (ou à digresser dessus). Je comprends que ça n'ait pas plu. Mais je ne sais pas vraiment comment améliorer sans faire violence à ce que je ressens moi-même comme spectateur potentiel.

Deuxième problème : je ne sais pas faire de figures. Je ne sais pas utiliser d'interfaces graphiques, et je sais encore moins utiliser TikZ correctement (à chaque fois que j'essaie de faire une figure avec TikZ, je prends cinq minutes à faire presque ce que je veux, puis cinq heures en m'arrachant les cheveux pour le persuader de faire en sorte que machin et truc aient la même taille, ou que bidule soit aligné avec chose, ou que telle flèche passe à tel endroit, ou que tel label soit bien placé). Rien que pour les malheureux arbres de preuve de mes transparents, j'en ai bavé pour qu'ils ne dépassent pas à gauche ou à droite, que les étiquettes ne se chevauchent pas, etc.

Or au moins pour illustrer des choses aussi bêtes que le fonctionnement d'une machine de Turing, les illustrations apportent vraiment une valeur ajoutée. (A posteriori je me dis que j'aurais dû proposer des points bonus pour les élèves capables de me fournir une illustration réutilisable pour éclairer un concept expliqué en cours.) À défaut, j'ai parfois gribouillé des choses très moches à la main sur ma tablette graphique.

Troisième problème, intrinsèque aux transparents : on n'en voit qu'un à la fois. Là au moins j'ai pu proposer un palliatif, qui est de donner aux élèves le lien vers un PDF avec l'ensemble du contenu (ce qui permet, au moins, de revenir à la page précédente si on a oublié de lire quelque chose). Je ne sais pas dans quelle mesure ça a vraiment servi, mais ça ne peut pas faire de mal.

Un autre défaut de ma façon d'exposer, pas exactement lié aux transparents mais néanmoins à ranger dans ce coin, c'est que je n'ai souvent pas été clair (dans ma présentation, et parfois dans ma tête) sur quelles parties du cours étaient des connaissances dont la compréhension[#14] était attendue à l'examen, lesquelles étaient présentées à titre d'explications dans l'espoir de rendre plus claires les premières, et lesquelles étaient de simples remarques culturelles obiter dicta. Par exemple, certains semblent avoir inféré du fait que je donnais de temps en temps des exemples en Haskell pour illustrer mon propos sur le typage, qu'ils devaient connaître le Haskell. J'ai éclairci ça en communiquant une liste un peu précise des attendus du cours (et de certains non-attendus explicites), mais évidemment il aurait été préférable que je dissipasse cette confusion[#15] dès le début.

[#14] L'examen était « tous documents autorisés », chose que je préfère sur le principe, mais qui présente évidemment ses propres inconvénients (par exemple celui d'encourager à imprimer des zillions de pages de cours, notes, exercices, livres apparentés, et que sais-je encore, et de se noyer dedans).

[#15] La question que tous les enseignants détestent est certainement il y aura ça à l'examen ? — et certains étudiants en abusent en faisant semblant de ne pas comprendre que quelque chose peut aider à aborder l'examen sans être explicitement dedans — mais il faut quand même reconnaître que c'est à nous de donner l'information pour devancer ce genre de question.

Mais le gros problème posé par la préparation à l'arrache de ce cours, c'est surtout celui de la coordination entre cours et TD+TP. Pendant que j'étais débordé par la préparation du cours, mon collègue a fait comme il a pu : une séance de TD sur la calculabilité, une séance de TP sur les machines de Turing, et le reste des TP en Coq pour se familiariser avec la logique et le typage[#16]. Même dans la mesure où le cours était cohérent et où les TP l'étaient, la coordination entre les deux était assez inexistante puisque nous étions chacun trop préoccupé par la préparation de notre partie pour suivre sérieusement ce que l'autre faisait : ça s'est vu, et les élèves nous l'ont (justement) reproché dans les évaluations. (Enfin, c'est surtout moi qui suis à blâmer en l'occurrence, parce que c'est moi qui suis censé être responsable de l'unité, et c'est moi qui aurais dû avoir des transparents prêts plus tôt pour que mon collègue puisse se baser dessus.)

[#16] Autrement dit, mon collègue a surtout structuré ses TP comme des exercices d'interaction avec Coq de difficulté graduée : pure logique propositionnelle d'abord, puis en allant de plus en plus vers ce qui pouvait ressembler à de la preuve de programmes.

J'ai rédigé pas mal d'exercices d'application du cours (avec corrigés), mais comme je les imaginais au fur et à mesure, ils n'étaient pas du tout prêts pour que mon collègue puisse en faire quoi que ce soit. Donc tout ce que j'ai pu en faire c'est dire aux élèves qu'ils étaient là (ça a quand même permis de dissiper le reproche qu'ils n'avaient pas de modèle[#17] sur lequel préparer l'examen).

[#17] Un retour d'élève me dit quand même estimer que l'examen n'était pas sur le modèle des exercices. C'est toujours difficile d'estimer ce genre de choses !

J'ai ajouté deux séances libres à la fin du cours, en mode venez avec vos questions, j'essaierai de répondre à tout ce que je peux, qui ont eu beaucoup de succès (en termes de nombre d'élèves qui sont venus, et de nombre de questions posées). Mais évidemment on peut voir ça comme quelque chose de moins positif : ça veut aussi dire que ces explications supplémentaires étaient nécessaires, et que ces séances auraient peut-être dû trouver leur place à un autre moment du cours.

☞ Moralité : ce que je dois surtout changer pour l'an prochain, c'est d'avoir un poly rédigé, alléger le cours en retirant ce qui est mal passé, ajouter des illustrations à mes transparents et réussir à les rendre plus digestes, et mieux me coordonner avec mon collègue pour faire, notamment, plus de TD.

Bilan

Malgré ces différents reproches que je me fais à moi-même ci-dessus, je ne crois vraiment pas que cette première itération de ce cours ait été un échec, loin de là.

C'est sûr que certains ont été un peu affolés par la densité du cours, et ont dû fournir beaucoup de travail pour suivre, mais au final les résultats étaient tout à fait satisfaisants. La moyenne de l'examen écrit a été de 14/20, ce qui ne veut rien dire en soi (surtout qu'en vrai c'était noté sur 25 et tronqué à 20 — mais ça c'est surtout parce que le sujet était long —, et il est vrai que j'avais prévu quelques questions extra faciles pour sauver les meubles), mais disons que c'est plus que ce à quoi je m'attendais a priori, et que ça montre que très peu étaient véritablement complètement largués (il n'y a eu que 6 notes <10 sur 87 copies). À juger par les questions que j'ai eues pendant les cours et par les copies que j'ai moi-même corrigées, certains ont même vraiment bien compris.

Symétriquement, les retours des élèves (qui sont anonymes, et par ailleurs collectés avant le rendu des notes ce qui exclut l'effet ils sont contents parce qu'on leur a mis des bonnes notes) sont globalement positifs : par exemple, 70% de ceux qui ont répondu se déclarent plutôt d'accord ou bien tout à fait d'accord avec l'affirmation j'ai apprécié le contenu de cette UE, et à part la partie sur le call/cc et les continuations qui comme je le reconnais ci-dessus a été un désastre, les autres parties du cours ont été plutôt appréciées individuellement (la préférée ayant été celle sur le λ-calcul, dont 67% nous disent être tout à fait d'accord avec l'affirmation qu'ils y ont réalisés des apprentissages significatifs). Bien sûr, ces sondages ne veulent pas dire énormément, et je ne cache pas qu'il y a quelques avis clairement négatifs et d'autres qui regrettent de ne pas avoir réussi à suivre, mais la plupart des critiques sont plutôt constructives (le cours gagnerait à être facultatif, les TP devraient être mieux coordonnés avec le cours, il faut plus de TD, telle partie devrait être allégée, et ma façon de lire les transparents n'est pas très utile…). Il y a quelques avis qui sont carrément enthousiastes, et ça fait toujours plaisir à lire.

Une chose dont je suis à peu près sûr, c'est que j'ai au moins rempli cette mission qu'un collègue m'a confiée : il ne faut pas que nos élèves s'ennuient en cours.

Bref, je ne pense certainement pas avoir fait quelque chose de parfait, mais ce n'était pas du tout un échec, et je crois que j'ai les pistes nécessaires pour améliorer les choses l'an prochain :

  • Supprimer les parties les plus indigestes du cours (notamment ce qui concerne les continuations, les subtilités sur le rapport entre arithmétiques de Heyting et de Peano, et les explications sur l'élimination des coupures voire tout le calcul des séquents), et mieux équilibrer mon temps sur le reste (il y a des parties où je délayais un peu parce que j'avais l'impression d'avoir trop de temps).
  • Rédiger un poly complet, et en profiter pour alléger les transparents (reste à trouver un bon équilibre à ce sujet).
  • Prévoir de vraies séances de TD au lieu de juste mettre à disposition des élèves des feuilles d'exercices corrigés.
  • Mieux me coordonner avec mon collègue pour que les TP ne semblent pas indépendants du cours.

Coda : un stage LIESSE

Télécom organise de temps à autre, en lien avec l'Union des professeurs de classes préparatoires scientifiques, des stages LIESSE (j'avoue que je ne sais pas ce que l'acronyme veut dire) d'échange avec les enseignants de classes prépa (ou éventuellement d'autres enseignants ou enseignants-chercheurs intéressés du secondaire ou du supérieur), le but étant d'exposer un sujet scientifique et de garder une interaction entre enseignants avant et après les concours des grandes écoles. J'avais déjà proposé un tel stage en 2021 (voir ce passage de ce billet (sur la théorie des langages formels (langages rationnels, langages algébriques, et automates), en 2018 (voir ce billet) sur la factorisation des entiers, et en 2015 (cf. ce billet) sur les réseaux euclidiens. J'aime bien ces rencontres parce que ça me permet de faire quelque chose d'intermédiaire entre un exposé de recherche et de la vulgarisation (cf. ce que je racontais dans ce billet) sur l'importance de tels exposés, et aussi d'exercer un peu mon éclectisme mathématique (que les sujets que je viens de lister doivent illustrer un minimum).

J'ai donc proposé de faire un stage Logique, Calculabilité, Typage, qui aura lieu (9h30–12h et 14h–16h) à Télécom (à Palaiseau[#18]). Le but est à la fois de parler du fond du cours (mais évidemment, en 2×2h je ne vais pas refaire la totalité du cours que j'ai exposé en 21h aux étudiants ! donc il y aura beaucoup de survol) et aussi des circonstances de sa mise en place à Télécom, c'est-à-dire en gros de ce que je viens de raconter dans ce billet. Les personnes intéressés à participer peuvent s'inscrire via ce lien[#19] (a priori ça concerne les enseignants, enseignants-chercheurs et chercheurs, et particulièrement les profs de prépa, mais on n'a pas l'intention de faire les difficiles ; par contre, l'inscription est obligatoire).

[#18] J'espère pouvoir mettre en place une retransmission vidéo (je mettrai sans doute le lien ici ultérieurement), mais le but est aussi de faire la pub de l'école, donc on cherche avant tout à attirer les gens sur place.

[#19] Je n'ai pas choisi l'outil d'inscription (outil qui, d'ailleurs, a été en panne vendredi et tout le week-end derniers), donc je suis désolé s'il est malcommode.

↑Entry #2791 [older| permalink|newer] / ↑Entrée #2791 [précédente| permalien|suivante] ↑

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]