Comments on Transparents de cours de calculabilité

@Ruxor: Des nouvelles sur les résultats/le sondage ?

Vu le programme quand même assez ambitieux du cours (rapporté au nombre d'heures), est-ce que les élèves s'en sont sortis ? En fait je suis assez curieux de l'enseignement « de l'autre côté » (celui de l'enseignant), et je me demande si on arrive à avoir une idée claire de la mesure dans laquelle les élèves ont compris le cours avant d'avoir corrigé l'examen…

@Thomas : en complément de l'explication de Ruxor, mon intuition de la fonction d'Ackermann, c'est que c'est en gros la suite qui commence par « addition », « multiplication », « puissance », i.e. la suite de suite qui commence par (𝑛+2), (2𝑛), (2^𝑛) (avec des constantes pour que la définition récursive soit simple).

La définition de la fonction de Ackermann semble sortie de nulle part, est-il possible de motiver un peu cette définition ?

Par ailleurs, existe-t-il des fonctions calculables (pas nécessairement totales) non primitives récursives qui sont vraiment intéressantes ? (utilisées en pratique dans des algorithmes)

Micro erreur dans le transparent 111 de la version Git: 33da1b1 Tue Nov 28 21:52:42 2023 +0100 : Rust a des types affines, pas linéaires. Il a fallu du temps avant que ce soit clarifié, d'ailleurs – chercher « leakpocalypse ». Il y a des discussions assez intéressantes sur l'ajout de types linéaires au langage.

Aujourd'hui, quand on parle de "programme informatique", on ne pense pas vraiment à un système qui prend une entrée et produit une sortie. Un programme est plutôt un système avec lequel on interagit, comme un serveur ou un jeux vidéo. Peut-être qu'il est immédiat de faire le lien avec une machine de Turing (un programme serait une machine qui prend un état et une entrée et produit un nouvel état et une sortie ?), mais ça mériterait quand même un développement.

De même pour les résultats d'impossibilité. Le modèle déterministe semble trop restrictif puisqu'en pratique on se contenterait d'algo probabilistes. D'ailleurs, il me semble que c'est ce qu'on fait en crypto quand on veut s'assurer que les codages ont les bonnes propriété de sécurité ?

Est-ce qu'il y a des résultats d'impossibilité sur des algos qui décideraiten de l'arrêt de manière probabiliste ? peut-etre des bornes de complexité ?

Je crois avoir repéré deux fautes dans le transparent 22 de la version actuellement en ligne (e98be11) :
- dans le cas e=《4,k,d,c》, le f doit être remplacé par ψ_e^{k+1}
- dans la note en bas de page, si j'en crois mon ordinateur, l'entier codé par 《4,1,《3,3,《2》,《0,3,2》》,《0,1,1》》est plutôt 1459411784487397180665432815832307065632600695406339535461638364986332341606302743434469111701693720708889497441914383776091303156789216767401627793923901338422595140605108945602813975090365543263502665356443008336975907222679611893212612182044162755894964678671838414598993125867377260376127580775038296803673221020020845958664079779303000005016780615609825
(pas sûr que ça tienne sur le transparent, ceci dit 😅, 358 chiffres, quand même…).

Quelques petites coquilles repérées vite fait (je n'ai pas tout relu…) :

p.9, deux fautes d'accord : l.6, "associé" -> "associée" et l.7, "simple" -> "simples".

p.39 l.-1: "Mutatis mutandis pour p.r." -> tu veux dire pour les générales récursives ?

Il existe cette implémentation du lambda calcul non typé mais ça reste quelque chose d'assez confidentiel et ça nécessite le bouquin associé pour vraiment l'utiliser…
https://www.cis.upenn.edu/~bcpierce/tapl/checkers/untyped/

Le Hindley & Seldin est assez agréable pour se documenter sur le lambda calcul.

Au transparent 95 de la version f190c1e Thu Nov 2 19:19:21 2023 +0100, il manque un S dans « illible ».

A la fin les maths c'est ça, aride et il faut faire des efforts pour les comprendre et les apprécier, commme pour toutes les autres disciplines académiques. Ces transparents ne comptent que pour une partie dans les coours magistraux et le rôle du professeur est de bien les présenter, expliquer ou illustrer ou à l'invrerse et ils ne sont là que pour être un support permanent du cours qui a eu lieu.

Pour les schémas, soit les faire au tableau, en expliquant en même temps. Ou sur papier et ajouter la copie dans les slides. Ça peut sembler moche, mais c'est pas important (même des pontes le font dans des grandes confs).

Tout ça est extrêmement aride. Je sais que c'est comme ça qu'on enseigne traditionnellement ces sujets, et qu'on a besoin de formalisme pour pouvoir faire des preuves. Mais j'ai quand même le sentiment qu'on noie les concepts dans des notations. Il est probable que beaucoup d'étudiants ne retiennent rien à cause de ça.

@Ruxor : De rien, et désolé d'avoir été sans doute un poil trop assuré (oui, j'ai aussi l'expérience des gens qui pinaillent sur un truc que vous avez passé des heures à écrire ☺).

> Je vais peut-être dire quelque chose sur les réductions, aussi, même si je ne sais pas bien quoi (ni comment éviter de commencer à parler d'oracles, ce qui m'entraînerait plus loin que je voudrais).

Pour vous (et moi), une réduction est un objet de première classe (« réifié » ?), à savoir une machine de Turing à oracle pour une réduction de Turing, et une bête fonction calculable pour une réduction many-to-one. Mais dans une intro à la calculabilité, peut-être qu'il serait raisonnable de ne présenter les réductions comme des raisonnement stéréotypés, qui suivent le schéma « Je raisonne par l'absurde, je suppose qu'il existe un algorithme qui décide X, j'exhibe un algorithme qui décide alors Y, or Y est indécidable » ?

En fait, à votre place, j'insisterais surtout sur le fait « méta-mathématique » qu'on prouve rarement l'indécidabilité d'un problème par une preuve directe parce que c'est fastidieux (à un degré qui dépend du formalisme, mais tout de même). On cherche plutôt à trouver un problème connu comme indécidable qui soit vaguement proche (arrêt, PCP, 10ème problème de Hilbert, …) et on essaye de le réduire.

Ça peut aussi valoir le coup d'en parler rien que pour la terminologie : je vous prédis en particulier qu'il faudra quelques heures de TD avant que plus aucun élève ne se plante en disant « je réduis X au problème de l'arrêt » au lieu de « je réduis le problème de l'arrêt à X » ☺

On parle (au moins 2 fois, dans un texte ni cliquable ni infobullé) de fonctions générales récursives avant de les avoir définies.

"Hyper inefficace ? On s’en fout."

Ici il convient de fleurir le lexique AMHA.

"Distinction entre intention (l’algorithme)"

Intension ou intention ?

Puisque vous appelez explicitement aux relecteurs, quelques remarques en vrac :

- Je suis un peu gêné que la fonction d'Ackermann prenne trois paramètres. Ce qu'on appelle usuellement « la » fonction d'Ackermann est une fonction à deux paramètres. Moi aussi, je préfère la version à trois paramètres, mais ce n'est pas ce qu'on note normalement A (Wikipédia la note φ).

- Sur le même transparent, il y a « définition algorithmique (par appels récursifs), donc calculable » → il faudrait quand même mentionner que l'algorithme termine toujours. Ce n'est pas bien sorcier, par bien-fondation de l'ordre lexicographique sur ℕ^2, mais la formulation escamote cette vérification.

- Une suggestion à tout hasard. Un formalisme Turing-complet qui pourrait être intéressant à mentionner, ce sont les systèmes de réécriture, peut-être en intro au λ-calcul. C'est plus facile à comprendre que le λ-calcul car pas de problèmes d'α-équivalence, et plus facile à programmer aussi — on traduit très naturellement les types inductifs et le pattern matching. Par exemple, l'addition des entiers naturels en réécritures

+(0, b) → b
+(S(a), b) → S(+(a, b))

est quand même plus intuitive que l'addition des entiers de Church

+ := λ a ⋅ λ b ⋅ λ f ⋅ λ x ⋅ a f (b f x)

- Pour le codage des couples et des listes : ce n'est qu'une suggestion, mais (p, q) ↦ 2^p × 3^q, bien que non bijective mais seulement injective, me paraît beaucoup plus naturelle, surtout que les listes se font facilement sur le même principe.

- Transparent 17 : manque un « si z = 0 » ?

- Transparent 22 : je trouve la définition un peu bizarre parce qu'il y a une redondance d'information : vous mettez k dans ψ_e^(k) mais aussi dans e. Autant enlever k des formes possibles pour e, ou définir ψ_e : ℕ^(k(e)) ⇢ ℕ (je préfère intuitivement le deuxième, où l'entier e contient l'information de l'arité de la fonction qu'il code, et où on n'a pas deux fonctions d'arité différentes codées par le même entier).

- Transparent 23 : une fonction p.r. a *toujours* beaucoup d'indices, et même une infinité, vu que f(x) = f(x)+1-1 = f(x)+1-1+1-1, etc.

Je m'arrête là pour l'instant…

Quand même deux autres remarques sur le plan général à vue de nez :

Vous ne parlez pas du tout de réduction ? (??) Le théorème de la forme normale me paraît bien anecdotique par comparaison (je ne le connaissais même pas…).

Et vous ne parlez pas du théorème de Rice ? Autant le théorème S-m-n par exemple est fondamental pour la théorie mais évident en pratique, autant le théorème de Rice, en plus d'être puissant et pas bien compliqué à prouver, dit quand même quelque chose qui me semble important à savoir même pour un ingénieur qui ne s'intéresse pas du tout à la théorie, à savoir qu'on ne peut pas espérer analyser statiquement des programmes en toute généralité.

Ah bien joué ! Je me suis longtemps demandé comment je pouvais insérer le numéro de commit dans le pdf.
(les plus paranos diront que lancer LaTeX avec write18 activé est une faille de sécurité, mais je suis mal placé pour faire la remarque).

Par contre, une habitude que j'ai prise pour les versions «faites moi des commentaires», c'est de laisser le paquet 'showlabels'. Comme ça les gens peuvent dire «il y a un problème juste après l'équation EQfoobar» plutôt que «il y a un problème juste après l'équation (4.53) de la version 31080ea»