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

@jeanas : ce que je raconte est avant tout le discours confus de quelqu'un qui découvre ces notions :)

Disons que je m'imaginais que :
* les termes du lambda-calcul permettaient de capturer la notion de fonction et de compositions de celles-ci — y compris par juxtaposition
* que (je ne sais comment) on pourrait capturer la notion de « forme normale » dans cette interprétation
* qu'alors (je ne sais comment) le théorème de Church-Rosser pourrait s'interpréter comme l'unicité de la valeur prise par une fonction, indépendamment de l'ordre de calcul

En lisant <URL: https://math.stackexchange.com/a/4004730/23001>, je réalise que la juxtaposition n'est même pas associative (et en re-regardant je vois que David l'a indiqué aussi), donc mon premier point tombe déjà à l'eau.

@Thomas : Le théorème de Church-Rosser (dont il ne me semble pas que David le prouve) n'est absolument pas trivial. Je ne vois pas à quoi tu penses en le reliant à une sémantique mais je ne connais pas de méthode purement sémantique pour le prouver.

Je connais trois méthodes, qui sont toutes traitées plus ou moins en détail dans le poly <URL:http://www.lsv.fr/~goubault/Lambda/lambda.pdf> (cours de λ-calcul de L3 de Jean Goubault-Larrecq à l'ENS Paris-Saclay) :

‣ La méthode des réductions parallèles de Tait et Martin-Löf, exercice 8.

‣ Une méthode qui passe par le théorème des développements finis et le lemme de Newman, section 2.2. Il y a une variante dans le livre de Barendregt « Lambda Calculi with Types » (Handbook of Logic in Computer Science, volume II, à ne pas confondre avec « Lambda Calculus with Types » du même auteur…), définition 2.3.10 à théorème 2.3.17, qui utilise aussi des développements finis mais apparemment ne prouve pas le théorème des développements finis et utilise de la semi-confluence (je n'ai pas pris le temps de la comprendre).

‣ Une méthode qui passe par des lemmes qui servent aussi à prouver le théorème de standardisation, exercice 23.

Dans tous les cas, on met les doigts dans le cambouis de la syntaxe avec une plâtrée de récurrences assez subtiles.

Le même poly contient aussi une partie sur les modèles à la Scott.

Merci à vous deux pour ces réponses.

Je rejetais un œil aux transparents de David (ce cours est vraiment sans fin…), cette fois-ci sur le lambda-calcul, et deux questions me sont venues à l'esprit :

1 - Est-ce que tu prouves le théorème de Church-Rosser dans ton cours ? Si oui, comment ?
2 - Qu'en est-il des sémantiques du lambda-calcul ? En parles-tu ?

Je pose la question 2 car j'essayais de me convaincre que le théorème de Church-Rosser était évident en construisant dans ma tête une sémantique pour le lambda-calcul, mais je bloquais et l'article Wikipedia sur le lambda-calcul semble dire que ce n'est pas simple.

@Thomas, @Ruxor : Pour répondre à cette partie de la question

> Est-ce que la présentation à la Hilbert se prête moins à la correspondance de Curry-Howard ?

Il semble qu'il soit possible de représenter certaines théories des types plus compliquées que le λ-calcul simplement typé avec des combinateurs, mais ça devient franchement abominable : <URL:https://stackoverflow.com/questions/11406786/what-is-the-combinatory-logic-equivalent-of-intuitionistic-type-theory>.

De mon point de vue : la déduction naturelle, c'est la vie (c'est intuitif, c'est ça qui correspond vraiment aux preuves informelles, c'est ça qui fait bien marcher Curry-Howard) ; le calcul des séquents, c'est bizarre mais utile (notamment parce que la logique linéaire ne se présente qu'en calcul des séquents) ; les systèmes à la Hilbert, ce sont de simples curiosités. (Pour la logique, je précise, parce que pour le λ-calcul non typé, ça a son importance, vu que l'idée des systèmes de combinateurs est derrière la définition des algèbres combinatoires partielles, qui permettent de présenter de façon unifiée la réalisabilité.)

Une autre question qui me vient à l'esprit :

Il me semble que l'on peut présenter le calcul propositionnel (intuitioniste ou classique) selon une forme axiomatique avec pour seule règle d'inférence le modus ponens (présentation "à la Hilbert").

Pourquoi as-tu préféré une autre présentation ("déduction naturelle" ?) ?
Est-ce que la présentation à la Hilbert se prête moins à la correspondance de Curry-Howard ? ce système de déduction est-il moins utilisé en pratique ?

@Ruxor: Merci, c'est très clair.

J'ai aussi trouvé <URL: https://arxiv.org/abs/2008.09016> qui démontre ce résultat (peut-être de la façon que tu suggères, je n'ai pas encore lu)

J'ai parcouru la partie « Sémantiques du calcul propositionnel intuitionniste » et je m'interrogeais sur de possibles sémantiques finies.

Je lis sur <URL: https://en.wikipedia.org/wiki/Intuitionistic_logic#Many-valued_logic> :
> Kurt Gödel's work involving many-valued logic showed in 1932 that intuitionistic logic is not a finite-valued logic.

Est-ce que ce résultat est quelque chose dont tu parles dans ton cours, ou qui serait compréhensible sur la base de tes transparents ?

Je profite de cette lecture pour vous souhaiter de joyeuses fêtes à vous et à votre poussinet, ainsi qu'une merveilleuse année 2025 !

Dans la catégorie « trivial mais illuminant », petite note pour les lecteurs intéressés qui auraient mis aussi longtemps que moi à le comprendre (⟵ bon OK je me justifie mais en fait je suis juste trop content de l'avoir compris pour ne pas le partager *quelque part*).

En fait, la sémantique de Kripke du calcul propositionnel est tout simplement un cas particulier de la sémantique topologique : celui où l'espace topologique est un ensemble partiellement ordonné avec sa topologie d'Alexandroff.

(J'imagine que @Ruxor ne le dit pas parce que ses élèves n'ont pas entendu parler de topologie générale.)

"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."

Oui, mais connaitre les détails de la théorie de Fourier n'est ni nécessaire ni suffisant pour "penser Fourier" dans les cas physiques où c'est utile. Connaitre les détails théoriques des méthodes d'optimisation n'est ni nécessaire ni suffisant pour les appliquer correctement quand on en a besoin sur un cas réel.
C'est comme la musique. On a besoin de faire des gammes pour bien apprendre à s'amuser en jouant, mais on n'a pas besoin des détails théoriques sur la propagation des ondes sonores. Ce n'est ni nécessaire, ni suffisant.

Il existe un monde (dans beaucoup d'universités anglo-saxonnes par ex) dans lequel on se confronte aux problèmes, on apprend alors les finesses d'usage des outils pour les résoudre, PUIS, pour ceux que ça intéresse, on va regarder le détail de la théorie.
Le faire "à la française" est également possible, mais le risque est de perdre la majorité des étudiants et de produire des gens qui ne se rappelleront que de morceaux de théorie, tout en étant infoutu de penser au bon outil en situation.

Quand tu dis que la possibilité de faire des fonctions récursives avec Quine + une machine universelle "permet de bien comprendre pourquoi on tombe si facilement sur des langages Turing-complets", tu penses à quoi ?
Je n'ai pas l'impression que ça explique particulièrement pourquoi des jeux comme Minecraft ou Magic: the Gathering sont Turing-complets vu qu'ils ne sont pas conçus pour avoir une machine universelle. Donc j'imagine que tu parles de vrais langages conçus dans un but de décrire des algorithmes, mais là je ne vois pas quel langage aurait été fait en cherchant à éviter le Turing-complétude (vu qu'un tel langage serait a priori interprété ou compilé en utilisant un langage générique donr on sait qu'il est Turing-complet).

Je n'aime pas les transparents moi non plus. Sur une conf assez courte où l'on veut faire passer quelques idées et quelques résultats, ça va. Mais sur des cours, je crois que pas grand monde n'aime ça. Le seul avantage est que c'est moins fatiguant pour le prof : plus facile que de faire défiler des transparents que de gratter au tableau.

J'aime bien les cours à l'américaine, ils écrivent en tout gros sur leurs tableaux https://www.youtube.com/watch?v=Tw1k46ywN6E
Leur cours est complémentaire aux supports, typiquement des bouquins de références.

Quand j'enseignais à la fac, je choisissais autant que possible les TD ou les projets. Je trouve que c'est là que j'ai une valeur ajoutée en temps qu'enseignant. Quand ce sont des transparents, je sais que je suis soporifique.

@Héhéhé : Vous trouverez très peu d'enseignement de Lean ou de Haskell en France en général par rapport à Coq et OCaml, tout simplement parce que les deux derniers sont développés à l'Inria. Il y a peut-être une part de chauvinisme/NIH contestable là-dedans, mais c'est aussi tout simplement qu'un certain nombre des enseignants-chercheurs qui enseignent ces cours travaillent avec ces outils dans leur recherche, voire les développent.

J'ai profité du mauvais temps d'hier pour lire un peu plus de ton cours, voici quelques remarques sur la partie call/cc (en espérant ne pas dire trop de bêtises).

---
En se basant uniquement sur tes transparents, il est très compliqué pour quelqu'un comme moi qui ne connaît pas Scheme de comprendre ce qu'est call/cc.

En revanche, <URL: http://www.madore.org/~david/computers/callcc.html> est beaucoup plus intelligible car elle le rapproche d'autres notions plus évocatrices pour des gens habitués aux langages de programmation "classiques".

(L'analogie (cf <URL: https://stackoverflow.com/a/46518215/943524>) avec un niveau spécial dans un jeu vidéo où la continuation serait un objet permettant de revenir au déroulement normal du jeu est intéressante, même si elle mérite d'être précisée pour montrer que ce n'est pas juste un appel de fonction avec un return.)

Une autre difficulté dans ton cours, c'est que tu présentes call/cc au milieu d'une partie liée au typage. Je ne connais rien au typage en général mais le fait que dans un langage typé doté de call/cc, la continuation puisse être de type A -> B *avec n'importe quel B* n'est pas quelque chose d'évident.

Ce que je comprends, c'est que dans ce cas on a le droit de typer la continuation ainsi car par construction cette fonction ne retourne jamais (de fait, le contexte dans lequel elle est appelée disparaît quand on l'invoque).

Mais moi, quand on me dit A -> B, je m'attends à avoir un objet qui prend un truc de type A et renvoie un truc de type B et la construction qui précède ressemble alors plus à une astuce pour mettre un type sur une construction non classique.
---

Pour résumer : je trouve la construction call/cc intéressante mais ça ne me semble pas évident de s'émerveiller sur sa traduction en terme de correspondance de CH si on n'est pas déjà bien familier avec le sujet. Et ça me semble être un sujet trop "niche" pour prendre le risque de perdre des gens qui découvrent avec.

Pourquoi avoir choisi Coq plutôt que Lean ?

L'informatique "théorique" est bien intégrée dans les cursus info traditionnels (je crois que même Epita a de la calculabilité et du lambda calcul au programme). Dans ma fac, on faisait de la déduction naturelle en L1, de la logique du 1er ordre en L2 (50h), de la calculabilité en L3 (lambda calcul simplement typé, machines de Turing). Pour la suite, ça dépendait des spécialités, mais on pouvait trouver du Coq ou de la compilation de langages fonctionnels en M1, et puis les choses plus pointues dans les M2 spécialisés.

En école d'ingénieur, c'était similaire, mais on allait plus vite parce que les élèves étaient meilleurs, et il y avait quand même un biais pour faire des choses plus utiles.

Grosso-modo, les élèves qui ne sont pas passé par une prépa ont du mal à rédiger des preuves mathématiques. Par contre, les "formalismes" style sémantiques à petit pas ne posent pas trop de problème : après tout, c'est juste des notations pour décrire des programmes.

> J'ai tout de même le sentiment qu'idéalement, les ressources pédagogiques autour de ces sujets devraient former un continuum entre l'informatique "pratique" et l'informatique théorique, mais que ce n'est pas le cas.

En général, les profs qui s'intéressent à la théorique ne s'intéressent pas trop à la pratique et réciproquement. Et les manuels de référence font rarement le lien.

Tout d'abord, félicitations pour ce cours !

Pour ma part, ça m'a motivé à m'intéresser un peu, enfin, à ce qu'est la calculabilité.

Je dois dire que je me suis aidé de plusieurs sources :
* Le livre The Nature of Computation <Url: https://nature-of-computation.org/>
* Tes transparents, qui ont le mérite d'être plus rigoureux que le livre ci-dessus, mais ceci peut aussi être un désavantage car le bouquin s'autorise plus de distance avec le formalisme pour faire passer certaines idées.
* Ce papier sur l'équivalence entre les différents modèles de calculabilité <Url: https://arxiv.org/abs/2010.15600>, car tout le monde dit qu'ils sont équivalents mais je ne trouvais pas de présentation satisfaisante sur ce point.

Étant un ancien élève de Télécom (enfin, je n'y ai fait qu'un an après l'X), le plan de ton cours m'a paru assez ambitieux par rapport à ce qu'on y faisait de mon temps et j'ai sauté pas mal de choses pour lesquelles je n'avais pas la disponibilité/motivation intellectuelle (j'y reviendrai peut-être).

Je peux témoigner qu'il n'est pas facile d'assimiler autant de choses en si peu de temps et je pense effectivement que tu pourrais retirer certaines parties qui ont posé plus de problèmes, quitte à les proposer en ressources complémentaires optionnelles.

Concernant le côté "à quoi ça sert ?", je ne sais moi-même pas vraiment y répondre. Je trouve qu'une question comme "Pourquoi les langages de programmation classique comportent-ils des constructions à risque comme while/goto et pourrait-on s'en passer ?" est fondamentale et devrait intéresser toute personne bossant dans l'informatique. Néanmoins, je constate en discutant avec des collègues que beaucoup de gens ne montrent aucun intérêt pour ce genre de questions.

J'ai tout de même le sentiment qu'idéalement, les ressources pédagogiques autour de ces sujets devraient former un continuum entre l'informatique "pratique" et l'informatique théorique, mais que ce n'est pas le cas.

> C'est clairement la sémantique des ouverts qui leur a le plus « parlé » […]. La sémantique de Tarski m'a semblé avoir été assez bien compris aussi

Tu voulais dire Kripke ?

> 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.

Est-ce que tu leur as directement parlé du combinateur Y (c'est mon impression d'après tes transparents), ou d'abord de la récursion plus naïve par simple auto-application avec « self self » pour faire les appels récursifs (dont tu parles très bien dans <URL:http://www.madore.org/~david/weblog/d.2023-12-01.2771.cours-lfi-2.html>) ?

Ça vaut ce que ça vaut (pas grand-chose), mais je peux donner mon expérience personnelle quand on m'a enseigné ça : la première fois qu'on m'a montré le combinateur Y, j'ai trouvé ça un peu obscur et miraculeux, alors que je comprenais beaucoup mieux la récursion naïve, mais je n'avais pas fait le lien. J'ai mis un temps fou à comprendre que c'est juste un moyen de faire de la récursion avec « self » au lieu de « self self », et surtout, que c'est bootstrappé via la récursion naïve. Je reste infoutu de connaître par cœur les combinateurs Y et Θ, mais maintenant je sais les retrouver à partir de `let curry f = let rec fixed = f fixed in fixed` et `let rec turing f = f (turing f)`.

Sur ce sujet, je recommande le cours de Xavier Leroy au collège de France de cette année.

https://www.college-de-france.fr/fr/agenda/cours/structures-de-controle-de-goto-aux-effets-algebriques

> 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).

Dommage, parce que comme tu le dis aussi, "ça sert vraiment" ! En plus, ce sont des constructions que l'on peut facilement programmer et rendre très concrètes grace à l'interaction avec l'ordinateur.

Personnellement, j'en suis un peu revenu de la théorie : j'en ai mangé pas mal en tant que prof et thésard, et je trouve que ça n'a pas été payant. Pour beaucoup d'élèves, les formalismes compliquent plus les choses qu'ils ne les éclairent, surtout quand ils sont introduits avant les concepts. Je pense que c'est plus naturel de jouer avec scheme ou ocaml, d'expérimenter avec le call/cc et les gestionnaires d'effet pendant quelques semaines, avant de chercher à écrire des règles de typage ou des sémantiques dénotationnelles.

C'est une spécificité assez française de promouvoir une rigueur poussée mais je me demande si c'est la bonne approche si le but est de former des ingénieur (par opposition à fournir des thésards dans les labos locaux).

Bon cela dit, ton cours a l'air super et tu as la chance d'avoir des étudiants qui sont demandeurs.