David Madore's WebLog: Où j'apprends aussi l'informatique en l'enseignant

Ce que j'aime surtout dans le fait d'enseigner, c'est qu'on apprend souvent soi-même plein de choses sur le sujet qu'on enseigne, surtout la première fois, et surtout si on crée soi-même le programme du cours : on croyait bien savoir les choses de loin, mais être obligé de les regarder de près pour les enseigner oblige souvent à se rendre compte qu'il y avait une subtilité là où on ne le savait pas (ou qu'on avait oubliée) ; ça peut éventuellement conduire à une panique zut, l'approche que je croyais avoir tracée pour ce cours ne marche pas ! comment est-ce que je vais m'en sortir ?, mais souvent on en ressort bien plus compétent qu'avant : même si la subtilité qu'on a découverte, finalement, n'est pas enseignée, l'enseignant sera quand même meilleur (ceci étant, les personnes à qui on enseigne la première fois risquent de moins goûter l'expérience, et il faut parfois quelques années pour que la découverte de surprises se tarisse et que l'enseignant soit rôdé).

Pour prendre un exemple passé précis, en enseignant mon cours de théories des jeux (notez le pluriel à théories !) à Télécom — dont les notes sont ici si ça intéresse quelqu'un — je me suis rendu compte d'une subtilité importante dont je n'avais pas du tout pris conscience avant : quand on parle de stratégie dans un jeu (à information parfaite), on peut soit s'intéresser aux stratégies qui, pour prescrire un coup à jouer, dépendent seulement de la configuration actuelle du jeu (appelons-les stratégies positionnelles), soit de celles, plus générales, qui dépendent de tout l'historique de la confrontation jusqu'à ce point (appelons-les stratégies historiques) ; or, même si la règle du jeu ne dépend que de la configuration actuelle et pas de l'historique qui a mené à cette configuration, ce n'est pas du tout évident a priori qu'une stratégie gagnante dans le sens plus général (historique) soit forcément traduisible en une stratégie gagnante dans le sens plus restreint (positionnel) ; et j'avais un peu paniqué, parce que j'avais construit mon cours autour de la démonstration de l'existence d'une stratégie gagnante dans un sens via la théorie des jeux de Gale-Stewart (qui sont intrinsèquement « historiques »), alors que j'en avais besoin ensuite au sens plus fort (« positionnel ») pour la théorie de Sprague-Grundy. J'ai réussi à m'en sortir (j'ai écrit des notes expliquant correctement le lien, voir la section 3.5 du PDF lié ci-dessus), en cours je demande aux élèves d'admettre ce point en les renvoyant au poly s'ils ne veulent pas l'admettre, donc finalement je n'enseigne pas vraiment cette subtilité, mais j'ai été content d'en prendre conscience, et je suis étonné qu'il soit si peu évoqué, ou si mal expliqué, dans la littérature scientifique sur le sujet.

Même en donnant un cours d'analyse (dont je n'étais, cette fois, pas le responsable ni le créateur, mais simple intervenant) j'ai appris un certain nombre de choses sur le sujet, voyez par exemple ce billet passé pour quelque chose que j'ai appris au détour d'un exercice. Et en donnant un cours d'initiation à la géométrie algébrique, je me rends surtout compte… que c'est très difficile d'enseigner la géométrie algébrique et que je ne sais même pas produire une définition d'un morphisme entre variétés quasiprojectives (l'objet fondamental du domaine, quoi) qui ne soit pas abominable dans sa complication.

Bref. Cette année, comme je l'ai raconté ici et là, j'inaugure un cours intitulé Logique et Fondements de l'Informatique où je dois parler de calculabilité, λ-calcul, logique, typage, isomorphisme de Curry-Howard, ce genre de choses (un programme à vrai dire assez ambitieux, mais on m'a donné comme consigne de profiter de la création de la filière MPI en prépa pour viser quelque chose d'assez sérieux). Des choses, à cheval entre mathématiques et informatique théorique, qui me plaisent beaucoup (sur la calculabilité voyez par exemple ce long billet) et sur lesquelles je pensais ne pas avoir grand-chose à apprendre… Famous last words!

(La suite de ce billet est essentiellement un brain dump de quelques unes des choses que j'ai apprises, réapprises, ou mieux comprises en préparant ce cours jusqu'à présent. Noter que ça ne veut pas dire que je vais les enseigner ! Ou du moins pas forcément sous cette forme. Comme les petits bouts de ce billet, de longueur très inégales, sont assez indépendants, je les ai séparés par des fleurons : si on n'aime pas ce que je raconte à un endroit donné, on peut sauter jusqu'au fleuron suivant.)

❦

Il y a des choses que j'ai apprises en marge de la préparation de ce cours, sans que ça ait vraiment d'impact dessus. Par exemple, comment on fabrique des modèles du lambda-calcul non typé (pour ceux qui veulent en savoir plus là-dessus, j'ai bien aimé l'article From computation to foundations via functions and application: The λ-calculus and its webbed models de Chantal Berline, et notamment la partie sur les K-modèles, qui m'ont semblé les plus parlants de tout cette histoire : de façon très sommaire, on représente un terme par l'ensemble de tous les types qu'on peut lui attribuer dans un certain système de typage dont les types ne sont pas disjoints ; en plus ça semble avoir un rapport avec la réalisabilité, ce qui n'est pas déplaisant) : ce n'est pas spécialement une difficulté que j'ai rencontrée, juste quelque chose que j'ai appris au passage.

❦

Il y a aussi des choses que je pensais savoir sans vraiment y avoir suffisamment réfléchi. Notamment, comment fonctionne au juste le combinateur de point fixe Y de Curry. J'avais déjà appris il y a longtemps que dans un langage fonctionnel non typé on peut faire des appels récursifs sans faire d'appels récursifs, par exemple (en Scheme) :

(define proto-fibonacci
  (lambda (self)
    (lambda (n) 
      (if (<= n 1) n
	  (+ ((self self) (- n 1)) ((self self) (- n 2)))))))
(define fibonacci (proto-fibonacci proto-fibonacci))

— code la fonction définie récursivement[#] par F(n)=n si n≤1 et F(n) = F(n−1) + F(n−2) sinon, sans jamais que la fonction fasse appel à elle-même dans sa définition (c'est, en fait, l'astuce de Quine — qui n'est pas due à Quine, c'est Hofstadter qui lui a donné ce nom-là, mais à Cantor, Gödel, Turing et Kleene — et sur laquelle j'avais écrit une page alors que mes élèves actuels n'étaient même pas nés). L'astuce (de Quine qui n'est pas de Quine), donc, c'est qu'on passe la fonction proto-fibonacci en argument à la fonction proto-fibonacci, et quand elle a besoin de faire appel à elle-même, elle applique son argument (self) en prenant bien soin de lui passer une copie de lui-même, d'où le self self dans ce code.

[#] Oui, je sais que la suite de Fibonacci est un très mauvais exemple de récursion parce qu'en vrai il ne faut pas la coder de façon récursive, c'est épouvantable pour la complexité ; mais c'est un exemple facile à lire, donc je le reprends avec cet avertissement qu'il ne faut pas faire comme ça pour autre chose que pour illustrer les appels récursifs.

Vous noterez bien, donc, qu'il n'y a pas d'appels récursifs dans ce code. La même astuce de Quine permet de faire un programme qui s'écrit lui-même même si le langage ne permet pas de faire référence à lui-même (voyez ma vieille page liée ci-dessus pour tous les détails), à Gödel de fabriquer un énoncé qui dit je suis indémontrable, etc. Ici ça sert à ce qu'une fonction s'appelle elle-même même si le langage ne permettait pas les appels récursifs comme construction spéciale (par exemple en λ-calcul, il n'y a pas de construction récursive).

Ici on est dans un langage fonctionnel donc on peut juste appeler une fonction passé en argument, mais dans un langage non fonctionnel capable d'écrire un interpréteur de lui-même, on pourrait quand même simuler les appels récursifs en lançant l'interpréteur (sur une représentation du code de la fonction !) à chaque fois qu'il est écrit self self dans le code ci-dessus, ce qui est la façon la plus mind-blowing de faire de la récursion, et je ne m'étais pas rendu compte de ça avant de commencer à préparer ce cours.

Mais ce que je n'avais pas bien compris c'est que c'est justement cette transformation qu'automatise le combinateur Y, à partir d'une version de la fonction à récurrer dans laquelle les appels récursifs sont écrits comme des appels à une fonction passée en argument :

(define y-combinator
  (lambda (func)
    ((lambda (self) (func (self self))) (lambda (self) (func (self self))))))
(define pre-fibonacci
  (lambda (fib)
    (lambda (n) 
      (if (<= n 1) n
	  (+ (fib (- n 1)) (fib (- n 2)))))))
(define fibonacci (y-combinator pre-fibonacci))

…sauf qu'en fait ce code ne fonctionne pas : il fonctionnerait dans un Scheme à évaluation paresseuse, mais Scheme n'est pas à évaluation paresseuse, donc il part dans une boucle infinie. Mais on peut réparer ça avec une variante du combinateur Y parfois appelée le combinateur Z (qui a une η-expansion de plus sur la partie « bouclante ») :

(define z-combinator
  (lambda (func)
    ((lambda (self) (func (lambda (val) ((self self) val))))
     (lambda (self) (func (lambda (val) ((self self) val)))))))
(define pre-fibonacci
  (lambda (fib)
    (lambda (n) 
      (if (<= n 1) n
	  (+ (fib (- n 1)) (fib (- n 2)))))))
(define fibonacci (z-combinator pre-fibonacci))

— cette fois ce code marche (le lambda supplémentaire ajouté sert à retarder l'évaluation, mais sinon, bien sûr, (lambda (val) ((self self) val)) se comporte comme (self self)).

J'avoue que j'ai été assez Éclairé en écrivant ce code. Pourquoi on ne m'a pas raconté tout ça quand j'étais petit ? Ah, en fait, on a dû me le raconter : c'est certainement écrit quelque part dans le Wizard Book (d'ailleurs je suis sûr qu'il y a un interpréteur de Scheme paresseux dans le Wizard Book). Il y a tout le savoir informatique du monde dans le Wizard Book.

Bon, mais voilà le problème : mes élèves n'ont pas lu le Wizard Book (et ce n'est pas vraiment le sujet de mon cours ; c'est sans doute dommage, parce que le Wizard Book est extraordinairement instructif et enrichissant[#2], mais on ne peut pas tout enseigner) ; et d'ailleurs ils ne connaissent pas le Scheme. Certes, je peux recoder ce truc en Python (qu'ils sont censés connaître pour une certaine définition de connaître) :

z_combinator = lambda func: (lambda slf: func(lambda val: (slf(slf))(val)))(lambda slf: func(lambda val: (slf(slf))(val)))
pre_fibonacci = lambda fib: lambda n: n if n<=1 else fib(n-1)+fib(n-2)
fibonacci = z_combinator(pre_fibonacci)

— ça marche, mais ce n'est pas comme ça qu'on est censé écrire du Python et, de fait, c'est assez illisible. Donc je ne sais pas si je vais réussir à Éclairer mes élèves de cette manière.

[#2] À défaut, on peut regarder cette vidéo (sur l'écriture d'un interpréteur Scheme en Scheme) en guise de succédané du Wizard Book.

Mes élèves ont fait du OCaml, mais en OCaml la traduction évidente de ce truc ne type pas (et pour le coup, je compte bien leur expliquer pourquoi : le λ-calcul simplement typé est fortement normalisant, donc ne permet pas de faire de boucles infinies). Sauf si on introduit un type récursif ad hoc pour y arriver quand même : j'écris ça explicitement, parce que je me suis un peu gratté la tête pour trouver le bon type : dans la première version, ça donne :

type 'b loopy = Loop of ('b loopy -> 'b)
let proto_fibonacci = fun (Loop slf) -> fun n -> if n<=1 then n else slf (Loop slf)(n-1) + slf (Loop slf)(n-2)
let fibonacci = proto_fibonacci (Loop proto_fibonacci) ;;

ou bien, en introduisant le combinateur Z :

type 'b loopy = Loop of ('b loopy -> 'b)
let y_combinator = fun fnc -> (fun (Loop slf) -> fnc(slf (Loop slf))) (Loop (fun (Loop slf) -> fnc(slf (Loop slf))))
let z_combinator = fun fnc -> (fun (Loop slf) -> fnc(fun vl -> slf (Loop slf) vl))
                                (Loop (fun (Loop slf) -> fnc(fun vl -> slf (Loop slf) vl)))
let pre_fibonacci = fun fib -> fun n -> if n<=1 then n else fib(n-1)+fib(n-2)
let fibonacci = z_combinator pre_fibonacci ;;

Mais le type récursif n'est pas évident à expliquer, et puis franchement ce code n'est pas super lisible, donc je ne crois pas que j'en parlerai.

Ajout (2023-12-09) : On me fait remarquer que OCaml a une option -rectypes qui permet d'autoriser les cycles dans la définition des types sans passer par un constructeur explicite (notamment, en pratique, ça permet d'implémenter le λ-calcul non typé). Avec cette option, on peut faire marcher le code précédent en retirant la ligne de définition du type et chaque occurrence du constructeur Loop :

(* For use with -rectypes option *)
let y_combinator = fun fnc -> (fun slf -> fnc(slf slf)) (fun slf -> fnc(slf slf))
let z_combinator = fun fnc -> (fun slf -> fnc(fun vl -> slf slf vl))
                                (fun slf -> fnc(fun vl -> slf slf vl))
let pre_fibonacci = fun fib -> fun n -> if n<=1 then n else fib(n-1)+fib(n-2)
let fibonacci = z_combinator pre_fibonacci ;;

Il s'agit donc d'une traduction à peu près exacte du code Scheme au-dessus. [Fin ajout.]

En Haskell, comme l'évaluation est paresseuse, le combinateur Y marche :

data Loopy b = Loop (Loopy b -> b)
y_combinator = \fnc -> (\ (Loop slf) -> fnc(slf (Loop slf))) (Loop (\ (Loop slf) -> fnc(slf (Loop slf))))
pre_fibonacci = \fib -> \n -> if n<=1 then n else fib(n-1)+fib(n-2)
fibonacci = y_combinator pre_fibonacci

Bon là évidemment il y a des fans de Haskell qui me diront que ce n'est pas ça La Bonne Façon d'écrire le truc en Haskell, mais plutôt quelque chose comme

fiblist = y_combinator (\l -> [0,1] ++ zipWith (+) l (tail l))

qui génère la liste (infinie) des nombres de Fibonacci, où la fonction \l -> [0,1] ++ zipWith (+) l (tail l) prend une liste l et l'ajoute terme à terme avec la même liste moins son premier terme, puis insère 0 et 1 au début, et la fonction y_combinator cherche le point fixe de ça ; c'est tout de même assez avec l'évaluation paresseuse (et ici avec le combinateur Y et pas Z), c'est qu'on arrive à trouver un point fixe sur une liste infinie comme ça, sans même passer par une fonction, et ensuite on peut demander à Haskell take 20 fiblist et il sort les 20 premiers nombres de Fibonacci. Bon mais mon exemple a un but pédagogique, quand même, parce que si je veux faire ça en Haskell je n'ai pas besoin d'écrire explicitement le combinateur Y, je peux directement faire la récursion en Haskell :

fiblist = [0,1] ++ zipWith (+) fiblist (tail fiblist)

marche directement sans avoir besoin de définir y_combinator ou quoi que ce soit d'autre. Mais mon propos était d'illustrer comment le combinateur Y (ou Z dans les langages pas paresseux) peut servir à coder les appels récursifs même s'ils ne sont pas dans le langage. (Et puis mes élèves ne connaissent probablement pas Haskell. Là aussi, c'est dommage, mais il faut bien faire avec.)

❦

Tout de même une connexion avec la correspondance de Curry-Howard : considérons la démonstration fallacieuse suivante (paradoxe de Curry) :

Je veux démontrer que les poules ont des dents.

Je tiens l'affirmation suivante : Si j'ai raison, alors les poules ont des dents.

Clairement, si j'ai raison (c'est-à-dire, si cette affirmation est vraie), alors les poules ont des dents.

Mais c'était justement mon affirmation : donc j'ai raison.

Donc, par ce qui vient d'être démontré, les poules ont des dents. ∎

Le contenu formel de cette « démonstration » est le suivant : si j'appelle A le fait que j'aie raison (en affirmant si j'ai raison alors les poules ont des dents) et B l'énoncé les poules ont des dents : l'énoncé A est construit de manière à ce que A :⇔ (A⇒B) (c'est là qu'est le paradoxe : dans la supposition implicite qu'on peut construire[#3] un tel A) ; le raisonnement (qui est valable dès lors qu'on dispose d'un tel A) est :

Supposons temporairement A. Alors (par l'équivalence A ⇔ (A⇒B)) on a A⇒B. Donc B. (Fin de la supposition.)

Ce qu'on vient de dire montre A⇒B. Donc (par l'équivalence A ⇔ (A⇒B)) on a A.

Donc on a prouvé A⇒B et A. Donc B. ∎

[#3] Ce n'est pas l'autoréférence qui est problématique (l'astuce de Quine évoquée plus haut permet justement l'autoréférence syntaxique) : ce qui est problématique c'est la manipulation de la vérité (A dit si A est vrai, alors B est vrai) à partir d'une (auto)référence syntaxique : c'est un théorème de Tarski qui dit en substance qu'on ne peut pas définir la vérité (d'un énoncé syntaxique, et dans le système considéré). Voyez cette entrée passée (et encore plus précisément ce passage de celle-ci où je parle du problème sous le nom d'uniformisation).

Maintenant, preuves et programmes se correspondent par la correspondance de Curry-Howard. Si je passe cette preuve à la moulinette de Curry-Howard, elle se traduit par le programme suivant : disons que je dispose d'un type a qui soit interconvertible avec a→b, je vais alors fabriquer un terme de type b de la manière suivante : je fabrique d'abord une fonction a→b en prenant un argument s de type a, en le convertissant en une fonction a→b et appliquant celle-ci à s lui-même : ceci renvoie un résultat de type b, donc j'ai codé une fonction a→b ; et maintenant que j'ai une fonction a→b, elle se convertit en une valeur de type a, et je peux appliquer l'une à l'autre pour obtenir la valeur de type b promise. Or en Haskell, mon type récursif data Loopy b = Loop (Loopy b -> b) me donne justement le type a (en l'occurrence Loopy b) interconvertible avec a→b. Donc je peux formaliser ainsi l'algorithme que je viens de décrire (le Loop slf est ce qui s'appelait s dans la version en français que je viens de donner : le constructeur Loop sert à convertir un a→b en un a) :

data Loopy b = Loop (Loopy b -> b)
(\ (Loop slf) -> slf (Loop slf)) (Loop (\ (Loop slf) -> slf (Loop slf)))

— ce truc a pour type b pour n'importe quel b (et c'est normal : c'est juste une boucle infinie) ; et écrit avec le combinateur Y c'est juste y_combinator (\x -> x). Moralité de l'histoire : le combinateur Y, qui permet la récursion côté informatique, permet les preuves circulaires de n'importe quelle conclusion, et notamment transforme l'affirmation tout à fait raisonnable si les poules avaient des dents, alors les poules auraient des dents en les poules ont des dents. (Et c'est pour éviter ce paradoxe logique que Coq, notamment, ne permet pas de créer des types récursifs comme le Loopy ci-dessus.)

Pardon, je digresse, mais le propos de cette digression est justement d'illustrer le genre de réflexions que l'enseignement m'oblige à avoir (et comme je ne peux pas vraiment montrer tous ces exemples en cours, je les dumpe sur mon blog) ; d'ailleurs, je me demande si ça ne fait pas partie de ces sujets qu'on ne peut pas vraiment comprendre sans les redécouvrir soi-même, si possible justement en les enseignant à quelqu'un (qui, à son tour, ne les comprendra qu'une fois qu'il aura, etc. ; cherchez à appliquer un combinateur Y à ce problème !).

❦

Bon, tout ça c'était des choses que je savais plus ou moins mais je n'avais jamais correctement pris le temps d'expliciter dans ma tête. Une chose plus technique dont je ne m'étais pas rendu compte, cependant : comme la démonstration « standard » de l'équivalence entre λ-calcul et fonctions générales récursives passe par le combinateur Y, qui est faiblement normalisable mais pas fortement normalisable[#4], on n'obtient qu'une représentation faible dans le λ-calcul ; ce n'est pas évident, par exemple, que le fait qu'un terme soit fortement normalisable soit indécidable. C'est néanmoins vrai, et on peut représenter toute fonction générale récursive par un terme fortement normalisable (et même par un terme du λI-calcul), mais ce n'est pas du tout évident de trouver des références, sauf le livre de Barendregt qui est assez illisible. J'ai néanmoins trouvé un truc sur le sujet (que je n'ai pas eu le temps de lire, parce que ça s'écarte trop de mon cours) : Paweł Urzyczyn, A simple proof of the undecidability of strong normalisation (2003) (il cite diverses références antérieures). Bon, c'est un peu agaçant que la démonstration très jolie avec le combinateur Y tombe court de ce qu'on voudrait au mieux, mais le monde est ainsi fait. En tout cas, je ne savais pas ça.

[#4] Et pourquoi pas le combinateur Z, alors, que j'ai employé avec succès ci-dessus pour remplacer le combinateur Y en Scheme, Python et OCaml ? Parce qu'il n'est pas non plus fortement normalisable ! (Aucun combinateur de point fixe ne peut être fortement normalisable.) Les langages que je viens de citer n'évaluent pas à l'intérieur des fonctions lorsque celles-ci sont définies, c'est ce qui l'empêche de boucler. Mais si on a affaire au λ-calcul avec une β-réduction non spécifiée (ou disons, intérieure gauche) jusqu'à tomber sur une forme normale, là, comme ça, je ne sais pas représenter une fonction générale récursive quelconque.

❦

Autre exemple d'un point technique qui m'avait échappé : j'étais vaguement persuadé que l'élimination des coupures dans les démonstrations en calcul des séquents était exactement la même chose, par Curry-Howard, que la normalisation des termes du λ-calcul simplement typé. En fait, les choses sont un chouïa plus compliquées, comme on me l'a signalé en réponse à cette question : déjà, la complexité de la recherche d'une démonstration sans coupure et de la normalisation du λ-calcul simplement typé n'est pas la même ; on peut quand même obtenir l'élimination des coupures à partir de la normalisation du λ.c.s.t., mais ce qui correspond trivialement à cette dernière par Curry-Howard, c'est l'élimination des détours en déduction naturelle, pas l'élimination des coupures en calcul des séquents, et si ces choses ne sont pas très éloignées, il y a des petites crottes de ragondin partout. (À vrai dire, je n'avais jamais bien prêté attention à la différence entre déduction naturelle et calcul des séquents, surtout qu'il y a moyen de présenter la déduction naturelle sous la même forme que le calcul des séquents, et je pensais que la distinction devenait complètement insignifiante ; si vous êtes embrouillés comme moi, les articles Wikipédia sur les deux styles ne sont pas mal foutus, je trouve.)

Ajout (2023-12-06) : Je dois ajouter à ce sous-sujet le résumé de quelque chose que j'ai fini par comprendre après la publication de ce billet. Mettons qu'on ait une démonstration sans détour dans le style déduction naturelle (correspondant, disons, à un certain λ-terme normal), qu'on veut convertir en démonstration sans coupure dans le style calcul des séquents. Le point crucial est de considérer les applications successives yx₁x₂⋯x_r (à lire comme (⋯((yx₁)x₂)⋯x_r)), avec r maximal, dans le λ-terme, où y est nécessairement une variable (il ne peut pas être une abstraction parce que le terme est supposé normal, ni une application parce que ce serait juste sortir un nouveau x ; cf. le concept de forme normale de tête), disons que y est de type σ₁→σ₂→⋯→σ_r→τ : en déduction naturelle, ce terme correspond à r applications successives de la règle d'élimination du ‘⇒’, en partant de y et sur les variables x₁,x₂,…,x_r dans cet ordre (si je descends dans l'arbre) ; en calcul des séquents, on va convertir ça en une démonstration avec des règles « ⇒ gauche » successives qui justifient la conclusion τ à partir de prémisses successivement réduites (si je remonte dans l'arbre) de σ₁→σ₂→⋯→σ_r→τ à σ₂→⋯→σ_r→τ, …, σ_r→τ et finalement τ. Le point crucial dans cette histoire est que l'utilisation de x₁,x₂,…,x_r est inversée en calcul des séquents par rapport à la déduction naturelle : en quelque sorte, en déduction naturelle, on applique successivement y à x₁, puis x₂, …, puis x_r, alors qu'en calcul des séquents on prépare un contexte de type successivement τ, σ_r→τ, …, σ₁→σ₂→⋯→σ_r→τ, dans lequel on « branche » finalement y ; ou, si on veut, on prépare une liste d'arguments d'abord [], puis [x_r], …, [x₁,x₂,…,x_r] qu'on donne enfin à manger à y. Cette idée (que j'ai sans doute très mal expliquée) est rendue précise par le λ̅-calcul (lambda-bar-calcul) de Herbelin qui fournit une variante du λ-calcul qui est au calcul des séquents normal ce que le λ-calcul normal est à la déduction naturelle (ces transparents d'un exposé de Pierre-Louis Curien peuvent aussi aider à comprendre ça, et diverses généralisation notamment à la logique classique).

❦

J'évoque un dernier point que je pense avoir mieux compris en préparant un exercice pour mon cours : la représentation des couples par des fonctions d'ordre supérieur, et le problème de typage que ça pose.

Je veux dire : dans un langage de programmation fonctionnel non typé (ou disons, dynamiquement typé), même si les couples n'étaient pas disponibles comme construction de base, on pourrait les fabriquer de la manière suivante : pour représenter un couple (x,y), je vais utiliser la fonction (p) qui prend en entrée une autre fonction f (de deux arguments, si besoin est de préciser) et qui renvoie f appliquée à ces deux arguments. Ceci est une façon de stocker les couples, en fait, dans la clôture associée à la fonction p ; pour extraire x il suffit d'appliquer la fonction p représentant le couple à la fonction f de deux arguments qui renvoie le premier (ce qui va donc renvoyer f du couple, c'est-à-dire la première composante), et symétriquement pour extraire y. Voici à quoi ça ressemble en Scheme :

;; Define pairing and projection functions by storing values in a closure
(define pairing (lambda (x y) (lambda (f) (f x y))))
(define proj1 (lambda (p) (p (lambda (x y) x))))
(define proj2 (lambda (p) (p (lambda (x y) y))))
;; Conversion from and to native pairs
(define fromnative (lambda (z) (pairing (car z) (cdr z))))
(define tonative (lambda (p) (p cons)))
(define tonative_alt (lambda (p) (cons (proj1 p) (proj2 p))))
;; Tests:
(proj1 (pairing "coucou" 42))  ;; Returns "coucou"
(proj2 (pairing "coucou" 42))  ;; Returns 42
(tonative (pairing "coucou" 42))  ;; Returns ("coucou" . 42)
(tonative_alt (pairing "coucou" 42))  ;; Returns ("coucou" . 42)

— et en Python (même si, de nouveau, on n'est pas du tout censé coder en Python de la sorte, le fait est que ça marche) :

# Define pairing and projection functions by storing values in a closure
pairing = lambda x,y: lambda f: f(x,y)
proj1 = lambda p: p(lambda x,y: x)
proj2 = lambda p: p(lambda x,y: y)
# Conversion from and to native pairs
fromnative = lambda z: pairing(z[0], z[1])
tonative = lambda p: p(lambda x,y: (x,y))
tonative_alt = lambda p: (proj1(p), proj2(p))
# Tests:
proj1(pairing('coucou', 42))  # Returns 'coucou'
proj2(pairing('coucou', 42))  # Returns 42
tonative(pairing('coucou', 42))  # Returns ('coucou', 42)
tonative_alt(pairing('coucou', 42))  # Returns ('coucou', 42)

Je pense que cette façon de faire est assez standard[#5] : j'avais dû l'apprendre dans le Wizard Book ou dans un texte quelconque sur le λ-calcul non typé (et d'ailleurs, c'est la représentation standard des couples en Unlambda, si on veut). Mais le Wizard Book ne parle pas du tout de typage !

[#5] Bien sûr, personne ne va vouloir coder les couples comme ça, parce que tous les langages ont une construction plus simple de couples, mais c'est important de savoir qu'on peut stocker des valeurs dans les clôtures par ce genre de procédé. Notamment, ça permet de rendre la valeur inaccessible autrement que par les méthodes qu'on fournit pour y accéder, puisque le contenu d'une clôture est complètement opaque et inaccessible une fois qu'elle est scellée.

Or maintenant le code écrit ci-dessus dans des langages non typés (enfin, dynamiquement typés) que sont Scheme et Python a un correspondant évident et naturel dans les langages (statiquement) typés que sont OCaml et Haskell, et le voici, d'abord en OCaml :

(* Define pairing and projection functions by storing values in a closure *)
let pairing = fun x -> fun y -> fun f -> f x y
let proj1 = fun p -> p (fun x -> fun y -> x)
let proj2 = fun p -> p (fun x -> fun y -> y)
(* Conversion from and to native pairs *)
let fromnative = fun (x,y) -> pairing x y
let tonative = fun p -> p (fun x -> fun y -> (x,y))
let tonative_alt = fun p -> (proj1 p, proj2 p)
;;
(* This works as expected: *)
proj1 (pairing "coucou" 42) ;;  (* Returns "coucou" *)
proj2 (pairing "coucou" 42) ;;  (* Returns 42 *)
tonative (pairing "coucou" 42) ;;  (* Returns ("coucou", 42) *)
(* But this doesn't: *)
tonative_alt (pairing "coucou" 42) ;;  (* Type error! *)

— et en Haskell :

-- Define pairing and projection functions by storing values in a closure
let pairing = \x -> \y -> \f -> f x y
let proj1 = \p -> p (\x -> \y -> x)
let proj2 = \p -> p (\x -> \y -> y)
-- Conversion from and to native pairs
let fromnative = \ (x,y) -> pairing x y
let tonative = \p -> p (\x -> \y -> (x,y))
let tonative_alt = \p -> (proj1 p, proj2 p)
-- This works as expected:
proj1 (pairing "coucou" 42)  -- Returns "coucou"
proj2 (pairing "coucou" 42)  -- Returns 42
tonative (pairing "coucou" 42)  -- Returns ("coucou",42)
-- But this doesn't:
tonative_alt (pairing "coucou" 42)  -- Type error!

Et là, badaboum, la fonction tonative_alt, qui est manifestement complètement équivalente à tonative en Scheme ou Python, ne marche pas correctement, elle cause une erreur de typage. Erreur d'autant plus bizarre que tonative_alt (pairing 1729 42) marche correctement (que ce soit en OCaml ou en Haskell) mais si les types des deux arguments sont différents, non ! Mais comment diable est-il possible que la fonction proj1 fonctionne correctement et que la fonction proj2 fonctionne correctement, mais qu'essayer de faire la fonction qui à p associe (proj1 p, proj2 p) ne marche pas ?

Mon explication du phénomène (qui n'est peut-être pas complète) est la suivante :

Le type du résultat de la fonction pairing appliquée à deux arguments de types a et b est (∀c) (a→b→c)→c (c'est-à-dire que si on lui passe une fonction f de type a→b→c, elle renvoie la valeur de f appliquée à x et y, de type c, et ce, pour n'importe quel type c) : c'est une fonction polymorphe (en c). Mais du coup, la fonction tonative qui convertit un couple sous cette forme en couple natif (appelons a×b le type des couples natifs) devrait être : (∀a,b) ((∀c) (a→b→c)→c) → a×b. Notez bien le placement du quantificateur universel sur c : alors que sur a et b la fonction tonative est polymorphe (elle peut opérer sur n'importe quels types a et b), sur c c'est l'argument de tonative qui devrait être polymorphe, i.e., tonative veut recevoir une fonction polymorphe en argument, ce n'est pas du tout la même chose que, par exemple, (∀a,b,c) ((a→b→c)→c) → a×b qui voudrait dire que la fonction accepte une fonction de type (a→b→c)→c pour n'importe quels a,b,c, là elle veut que la fonction qu'on lui passe soit polymorphe. Et de fait, pour calculer proj1 p et proj2 p on va utiliser p avec pour type (a→b→a)→a et (a→b→b)→b respectivement. Or le système de polymorphisme à la Hindley-Milner, utilisé par OCaml et Haskell (sans extensions), est incapable d'exprimer un tel type : donc le type se fait réduire en quelque chose qu'il est capable d'exprimer, et notamment quand on écrit (proj1 p, proj2 p) la fonction p n'est pas polymorphe, elle doit renvoyer le même type les deux fois, donc les deux composantes du couple sont obligées d'être de même type, alors que c'est clairement juste une insuffisance du système de typage.

Tout ça c'est des choses que je savais (de l'autre côté de Curry-Howard, c'est essentiellement dire que la conjonction logique A∧B peut s'écrire ∀(C:Prop).(A⇒B⇒C)⇒C, d'ailleurs), mais j'ignorais que ça pouvait se produire sur un exemple si simple, si parlant et potentiellement si utile.

En fait, le compilateur Haskell GHC a des extensions (-XRankNTypes -XExplicitForAll) qui permettent de faire marcher le code ci-dessus (notez bien que je ne fais qu'ajouter des annotations de type) :

{-# LANGUAGE RankNTypes, ExplicitForAll #-}
-- Define pairing and projection functions by storing values in a closure
let pairing = \x -> \y -> \f -> f x y
let proj1 :: (forall c. (a->b->c)->c)->a ; proj1 = \p -> p (\x -> \y -> x)
let proj2 :: (forall c. (a->b->c)->c)->b ; proj2 = \p -> p (\x -> \y -> y)
-- Conversion from and to native pairs
let fromnative = \ (x,y) -> pairing x y
let tonative :: (forall c. (a->b->c)->c)->(a,b) ; tonative = \p -> p (\x -> \y -> (x,y))
let tonative_alt :: (forall c. (a->b->c)->c)->(a,b) ; tonative_alt = \p -> (proj1 p, proj2 p)
-- This works as expected:
proj1 (pairing "coucou" 42)  -- Returns "coucou"
proj2 (pairing "coucou" 42)  -- Returns 42
tonative (pairing "coucou" 42)  -- Returns ("coucou",42)
-- And now this works as well:
tonative_alt (pairing "coucou" 42)  -- Returns ("coucou",42)

— mais le fait d'utiliser ce genre d'extensions rend l'inférence de type beaucoup plus difficile (indécidable, je suppose, vu que c'est essentiellement le système F).

❦

Ajout (2023-12-02) : Même si, pour le coup, ça n'a rien à voir avec la préparation de mon cours, comme c'est quelque chose de très intéressant à l'interface entre maths et informatique théorique que j'ai apprise au même moment, je profite de ce billet pour attirer l'attention sur cette question que j'ai posée sur le StackExchange d'informatique théorique, et qui a reçu une super réponse d'Emil Jeřábek (il a répondu à plein de mes questions, lui, et c'est toujours un plaisir de lire ses explications), sur ce qu'on peut faire avec un oracle générique par opposition à un oracle aléatoire (les explications sont dans la question, mais je renvoie aussi à ce vieux billet pour une tentative de vulgarisation(?)) : la morale de l'histoire c'est que, du point de vue complexité comme calculabilité, les oracles génériques n'apportent vraiment rien d'utile (encore moins que les oracles aléatoires) ; et on peut tirer une intéressante fausse preuve de P≠NP (dont je n'arrive honnêtement pas à savoir s'il faut la considérer comme purement bidon ou comme au moins un argument informel pour P≠NP).

❦

Ajout (2023-12-03) : Tant que j'y suis, je fais aussi la pub pour cette question sur MathOverflow où je demande quel est précisément le rapport entre, d'une part, la correspondance de Curry-Howard, et, d'autre part, la réalisabilité, parce que c'est une question que je me suis assez naturellement posée en réfléchissant à ce cours (même si je ne compte pas y parler de réalisabilité).

❦

Voilà, j'arrête là le brain dump qui avait plus comme objet de me permettre de retrouver ces réflexions ultérieurement que de les expliquer à d'autres (mais si ce qui précède vous a aidé à mieux comprendre quelque chose, tant mieux). L'ennui, de mon côté, c'est qu'à chaque fois que je découvre/recomprends un truc comme ça, je passe pas mal d'heures dessus à m'assurer que j'ai bien compris ce que j'ai compris (voire, à le raconter sur mon blog, pour sauvegarder l'Univers dans lequel je suis et l'empêcher de changer sous mes pieds), or j'ai un nouveau cours à donner mardi et je ne suis pas prêt du tout du tout du tout.

(Si je décide de parler du call/cc dans ce cours, et c'est probable pour faire le lien entre logique intuitionniste et classique, je vais certainement redécouvrir aussi plein de choses que j'avais oubliées ou seulement à moitié comprises.)

PS : En plus des transparents du cours que j'ai déjà liés, il y a une feuille d'exercices corrigés ici (pour l'un comme pour l'autre, vous pouvez me signaler des erreurs que vous trouvez, il y en a certainement plein vu le niveau de hâte avec lequel j'écris).