Comme je le disais il y a un mois, je me suis engagé à organiser à Télécom Paris(PlusÀParis) un cours de Logique et Fondements de l'Informatique où je dois parler de calculabilité, logique et typage. Je suis évidemment complètement à la bourre sur la préparation de ce cours, qui commence , mais bon, j'ai au moins provisoirement fini d'écrire des transparents pour la partie « calculabilité » qui devrait occuper, je pense, bien 6h de cours (sur 22h au total pour le cours magistral ; il y a des TD/TP à côté). Autant que je rende ça public dès maintenant, des fois que des gens voudraient m'aider à corriger les fautes. Donc :
Ces transparents sont en ligne ici
(Je compte concaténer ceux de la suite du cours quand il seront écrits. Je ne sais pas encore comment je veux diviser ça donc ce n'est pas évident de choisir des adresses intelligemment.)
J'ai à peine commencé à les relire, donc c'est certainement bourré de typos et de fautes plus ou moins graves. J'espère quand même qu'il n'y a pas d'erreur tellement grave qu'elle m'obligerait à tout restructurer.
Si vous faites des commentaires, pensez à me donner l'identifiant
Git (en bas du premier transparent) auxquels ils se rapportent. (Au
moment où j'écris ce billet, c'est 31080ea Wed Nov 1 11:06:40
2023 +0100 ; l'arbre Git avec le
source est
ici.)
Il faut préciser que ça s'adresse à des élèves ayant déjà fait de l'informatique en prépa (filière MPI ou filière MP option info, plus quelques uns venus de licences d'info ; les programmes des classes prépa sont ici), donc d'une part ce n'est pas comme s'ils découvraient tout, d'autre part on peut les espérer motivés par le sujet.
Dans cette partie calculabilité, je présente les fonctions
primitives récursives et surtout générales récursives, les machines de
Turing et le λ-calcul non typé, l'esquisse de l'équivalence entre les
trois présentations de la calculabilité (fonctions générales
récursives, machines de Turing et λ-calcul non typé), ainsi que divers
résultats classiques fondamentaux : théorème s-m-n, théorème de
récursion de Kleene, existence d'une machine universelle, résultats
élémentaires sur les ensembles décidables (= calculables) et
semi-décidables (= calculablement énumérables), et bien sûr
l'indécidabilité du problème de l'arrêt (et aussi l'incalculabilité de
la fonction « castor affairé »). Dans la suite du cours, il est prévu
de parler de λ-calcul simplement typé en lien avec le calcul
propositionnel intuitionniste, puis de diverses extensions (logique
classique, logique du premier ordre, et évoquer divers bouts du cube
de Barendregt). Le fil conducteur du cours est censé être quelque
chose comme ceci : L'indécidabilité du problème de l'arrêt signifie
que tout langage informatique qui garantit la terminaison des
programmes est nécessairement limité ; des systèmes de typage de plus
en plus puissants cherchent à rendre cette limitation aussi faible que
possible.
J'ai renoncé à parler, même allusivement, de machines avec oracle ou de degrés de Turing ; mais les gens qui veulent en savoir plus sur ce sujet peuvent se référer à ce billet interminable pour lequel les notes ci-dessus suffisent largement en matière de prérequis.
Ajout () : Suivant ce qu'on
m'a fait remarquer en commentaire, j'ai ajouté (Git 1cdc719 Thu
Nov 2 17:08:48 2023 +0100) des choses sur le théorème de Rice
et les réductions (many-to-one et de Turing). Il
est cependant vraisemblable que j'en saute au moins une partie.
Le fait de me replonger dans le λ-calcul non typé, et de vouloir en savoir plus que le minimum que j'enseigne, m'a obligé à réapprendre plein de choses à son sujet[#], que j'avais complètement oublié ou jamais sues, et redécouvrir toutes les petites crottes de ragondin qui polluent un sujet qui a superficiellement l'air simple et élégant (comme : la différence entre β-réduction et βη-réduction, la différence entre termes normalisables et fortement normalisables, la différence entre stratégie de réduction extérieure gauche et intérieure gauche, la différence entre forme normale, forme normale de tête et forme normale de tête faible, etc.) ; le livre de Barendregt (The Lambda Calculus: Its Syntax and Semantics) est assez abominable en matière de dissection de crottes de ragondin, et celui de Krivine (Lambda-calcul : types et modèles — disponible en ligne en traduction anglaise) ne l'est pas moins. Un des problèmes est sans doute qu'on n'a pas vraiment idée de ce que sont les termes du λ-calcul non typé (prima facie, ce sont des fonctions qui prennent en entrée une autre fonction de même sorte et renvoient une autre fonction de même sorte : ce n'est pas du tout clair qu'on puisse fabriquer un objet qui soit aussi l'objet des morphismes de lui-même dans lui-même !) : divers gens (en commençant par Dana Scott à la fin des années 1960) ont réussi à en donner des modèles, ce qui éclaircit un peu la sémantique, mais là aussi on se perd entre les différentes manières de fabriquer des modèles du λ-calcul et les zillions de relations d'équivalence entre types que fournissent ces façons de fabriquer des modèles. (J'ai commencé à lire plein de choses sur le sujet, et surtout à me noyer dans les notations pourries. J'espère que l'article From computation to foundations via functions and application: The λ-calculus and its webbed models de Chantal Berline m'aidera à y voir plus clair.)
Je suis assez étonné, en revanche, de ne pas trouver d'implémentation (libre, flexible et largement disponible) du λ-calcul non typé, qui permettrait de tester un peu les choses (transformer les notations, réécrire les termes à la main ou de façon automatisée, comparer les stratégies de réduction, etc.). Est-ce que j'en ai raté une évidente ?
[#] La première fois que j'ai appris des choses sur le λ-calcul, ça devait être vers 1990 quand on m'a offert le livre de vulgarisation scientifique The Emperor's New Mind de Roger Penrose (j'en ai parlé dans une section d'une entrée récente), qui décrit un peu le λ-calcul et les entiers de Church, et ça m'a complètement fasciné que des règles typographiques aussi simples et élégantes (← mais bon, en fait, une bonne quantité de poussière avait été glissée sous le tapis) puissent donner quelque chose d'aussi puisant.
Ajout () : Par pure
coïncidence, la chaîne de télé Arte vient de produire, dans le cadre
de sa série Voyages au pays des maths, un
mini-documentaire de vulgarisation (10 minutes)
intitulé L'Entscheidungsproblem ou la fin des
mathématiques ?
(ici sur
YouTube, ici sur le site web d'Arte) et qui porte
justement sur le sujet dont je parle ici. Je ne suis pas d'accord
avec tous les choix de présentation, mais ça donne au moins une idée
de ce dont il est question (et notamment, tenter de vulgariser
l'équivalence entre fonctions générales récursives, machines de Turing
et λ-calcul était un défi pas du tout évident, et je trouve qu'il s'en
sort pas mal). Surajout :
voir ce nouveau billet où je
décortique un peu plus cette vidéo.