Réactions
  1. bluestorm, Emily, et les chameaux
  2. L'innocence est un mythe : les programmes fonctionnels nécessairement impurs
  3. Histoire de minorité et d'informatique
  4. Détection automatique de bugs
  5. Cohérence des effets de bord
  6. Sécurité et interface utilisateur
  7. Génération de tests, compilateurs, et preuve formelle

L'innocence est un mythe : les programmes fonctionnels nécessairement impurs

(Gabriel Scherer (gasche) @ 2009-08-21 16:49:00)

Tut tut tut, deuxième réaction de bluestorm dans les bacs. Après ses aventures avec la petite Emily, notre héros nous revient en terrain familier et, par ce discours nouveau, introduit la jeunesse à une des dures réalités de la vie d’un guerrier fonctionnel, dans sa quête éternelle de la meilleure conception, chassant les belles factorisations… tak tak.

Mais je vais éviter de m’imposer davantage sur son billet de peur de le vexer, puisque j’ai déjà pris la liberté d’amender son titre originel tout meugnon.

—minh

Cette réaction n’est pas la deuxième sur ma liste : c’est la quatrième, et je l’ai choisie parce que c’est un sujet qui me tentait plus. C’est un papier sur les programmes et langages de programmation, qui repose sur un arrière-plan théorique complètement inaccessible (pour moi en tout cas), mais qui cache toutes ces difficultés et qui est orienté vers une certaine forme de pratique.

Le papier explore un fait qu’il considère comme « surprenant » : il existe des fonctions qui respectent la transparence référentielle, mais qu’on ne peut pas écrire dans un langage de programmation pur ; autrement dit, il parle de la programmation fonctionnelle qu’on ne peut faire que dans un langage (un peu) impératif. Il donne des exemples de ces fonctions, se demande à quoi elles peuvent bien servir, donne des cas d’utilisation et discute de leurs avantages et inconvénients par rapport aux fonctions écrites dans un langage pur, d’une part, et aux fonctions générales d’autre part.

Il aborde aussi de façon relativement tangente deux points que je trouve intéressants :

  1. parfois, pour qu’une fonction ait de bonne propriétés, il faut lui faire perdre une partie des informations qu’elle donne, en fournissant pour cela un travail supplémentaire ;

  2. l’écriture dans un style fonctionnel pur peut poser des problèmes de modularité.

When is a functional program not a functional program
Citeseer (PDF, PS), 7 pages
John Longley

Ce n’est pas un papier révolutionnaire dans le sens où les techniques présentées ne changeront pas fondamentalement votre vision de la programmation, mais ça reste une lecture agréable et à placer dans la catégorie "exercices mentaux de programmeurs ML".

Le reste de cette réaction est une explication plus détaillée et plus verbeuse de tous les points que j’ai évoqués jusqu’ici. C’est donc une paraphrase de l’article, avec des choses en moins, mais je pense que c’est plus accessible : ce qui dans l’article constitue une petite allusion d’une ligne (« the familiar recursive type », « in the obvious way », « in the usual sense »…) sera un peu plus détaillé et donc normalement plus accessible au lecteur qui ne connaît pas le sujet, même si je ne ferai sans doute pas de miracles. En pensant aux gens qui n’ont pas envie d’entrer trop dans les détails, j’ai retiré une partie de mes digressions et les ai mis en annexe ; ça casse un peu le flot naturel du discours, mais vous pouvez très bien ne pas les lire, ou les lire seulement à la fin si vous voulez des détails. C’est même ce que je vous conseille : lisez-les quand vous aurez terminé le corps de l’article et si vous en avez encore envie, c’est le plus simple.

Par contre, je donne des exercices dans ce billet. Si cela peut vous motiver, au milieu de mes explications à la noix vous trouverez des énoncés d’exercices pas tous évidents, qui pourront vous faire un petit challenge matinal en mangeant vos chocapics (ou pas).

Des fonctions fonctionnelles non pures

L’article se place dans le cadre de langages dont les fonctions peuvent "échouer", c’est à dire ne pas renvoyer de valeur : boucler à l’infini, renvoyer une erreur/exception, etc. C’est le cas de tous les langages Turing-complets,α donc tous les langages que l’on manipule en général. On dit dans ce cas que la fonction diverge, ou n’est pas définie. Le bon outil mathématique pour étudier les fonctions dans ces langages est le concept de fonction partielle : une fonction partielle de A vers B (où A et B sont des ensembles au sens mathématiques du terme) est une fonction qui renvoie, pour tout élément de A, soit un élément de B, soit ⊥, qui représente l’échec, la divergence. Si on évalue une fonction (informatique) en un argument où elle n’est pas définie, l’ensemble du calcul diverge : si par exemple l’évaluation de la fonction boucle à l’infini (ne termine pas), le reste du programme n’est jamais exécuté et l’ensemble boucle à l’infini.

α : la notion de Turing-complétude permet d’étudier l’expressivité d’un langage pour écrire des fonctions de type int -> int ; comme expliqué dans l’article, on peut voir les fonctions présentées ici comme une extension de la notion Turing-like de calcul aux autres types fonctionnels.

Ce point de vue explique aussi la prépondérance du type int dans l’article. Il utilise par exemple souvent des fonctions de type int -> int alors qu’une fonction int -> 'a aurait été plus générale et plus appropriée ; j’ai choisi de respecter ce choix, ne vous étonnez pas de voir des types inutilement restreints.

En deux mots, on considère les fonctions du langage qui sont fonctionnelles, c’est à dire qu’elles se comportent vraiment comme une fonction partielle mathématique : pour chaque valeur possible en argument, elles renvoient toujours la même valeur, ou divergent toujours. On les appelle aussi séquentiellement représentables (SR) parce qu’elles englobent toutes les fonctionnelles que l’on peut définir dans un langage séquentiel, où il n’y a qu’un seul fil d’exécution. Concrètement, les fonctionnelles et les SR désignent ici les mêmes fonctions, mais quand je parle de fonctionnelle j’insiste sur le comportement mathématique (une sortie par entrée au plus), et quand je parle de SR j’insiste sur la possibilité de les implémenter dans un langage SR. De plus, on pourrait imaginer d’autres classes d’expressivité où des fonctions restent fonctionnelles mais ne sont plus SR (cas traité en annxe). Ou l’inverse (cas de la plupart des langages impératifs).

Formellement, on peut voir les fonctions partielles de A dans B comme des applications de A dans (B + {⊥}), où (+) représente la somme disjointe de deux ensembles. On peut alors définir une traduction des valeurs du langage de programmation vers des objets mathématiques : les fonctions du langage deviennent des fonctions partielles, et les types deviennent des ensembles. On note [u] l’objet mathématique représenté par le terme u, et ['a] l’ensemble qui représente le type 'a.

Plutôt qu’étudier directement les fonctions du langage, on étudiera donc les fonctions mathématiques correspondantes. Il peut y avoir de nombreuses implémentations différentes d’une fonctionnelle, mais on les considèrera toutes comme équivalentes si elles donnent les mêmes résultats pour les mêmes arguments, donc dénotent la même fonction mathématique.

Avec la définition que j’ai donnée, qui est celle du papier, les fonctions prennent en paramètre non pas un terme quelconque du langage, mais une valeur.β Cela veut dire que les arguments doivent être évalués avant d’être passés aux fonctions, et on est donc dans un cadre d’évaluation stricte. On ne perd en fait aucune généralité, et si cela vous intéresse je parle un peu de l’évaluation paresseuse en annexe. En un mot, on peut représenter une valeur paresseuse de type t comme une valeur stricte de type unit -> t, donc cela reste dans le cadre de cette discussion.

β : par valeur on entend "terme qui s’évalue en lui-même" : valeurs immédiates (entiers, booléens), mais aussi structures et fonctions

L’intérêt de cette classe de fonction est apparent : si on sait qu’elles renvoient toujours le même résultat, on peut effectuer un grand nombre de transformations du code sans modifier sa signification, beaucoup plus que pour des fonctions qui n’ont pas cette propriété. Par exemple si un compilateur trouve le code f x + f x, où x est une valeur et f vérifie cette propriété, il peut le transformer en let y = f x in y + y. Cette optimisation correspond à une optimisation déjà effectuée par la plupart des compilateurs optimisants, la CSE (Common Subexpression Elimination) ; mais elle ne peut en générale être pratiquée que pour des expressions très simple (calculs numériques principalement) et pas pour les appels de fonctions, si leur résultat peut changer entre deux appels (certains compilateurs de langages impératifs, dont GCC, permettent cependant au programmeur d’annoter des fonctions pour préciser qu’elles sont fonctionnelles et peuvent être prises en compte par la CSE).

L’article repose en fait sur un deuxième article beaucoup plus long du même auteur, qui développe toute la partie théorique. J’ai essayé d’y jeter un coup d’oeil avant d’écrire cette réaction, et il est complètement indigeste. Exemples de mots clés : « full and faithful » (théorie des catégories), « presheaves » (algèbre), « hypercoherence » (?).

Exemple : fonction use

On s’intéresse à un type, que l’on notera (), qui a une seule valeur que l’on note u (type u = unit). On dénote () par un objet mathématique quelconque noté * : [u] = {*}.

Quels sont les éléments de [u -> u] ? Ces fonctions sont définies par leur valeur en le seul argument possible, *. On a donc deux possibilités :

  1. (* -> ⊥), la fonction qui diverge, que je noterai 0

  2. (* -> *), la fonction qui renvoie *, que je noterai 1

Cas (u -> u) -> u

Quels sont maintenant les éléments de [(u -> u) -> u] ? Quand on a en argument une fonction de type u -> u, on a trois possibilités :

  1. diverger dans tous les cas : c’est la fonction [bot] : f -> ⊥,
    par exemple let rec bot f : unit = bot f ;

  2. renvoyer () dans tous les cas : c’est la fonction [top] : f -> *,
    par exemple let top _ = () ;

  3. évaluer l’argument en () puis renvoyer () : c’est la fonction [mid] : f -> f(*), par exemple let mid f = f ()

    argument retour
    0
    1 *

    En effet, si on évalue 0(*), le calcul diverge (puisque 0 diverge), donc mid(0) est ⊥.

Il y a une quatrième fonction dans l’ensemble des fonctions partielles [u -> u] -> [u], c’est neg, qui termine pour 0 et diverge pour 1. Cette fonction n’est pas représentable,γ car elle correspond en fait au théorème de l’arrêt : elle permettrait de "savoir" sans diverger si son argument diverge, ce qui est impossible dans tout langage Turing-complet. J’ai développé ce point en annexe.

γ : donc n’appartient pas à [(u -> u) -> u]

Cas ((u -> u) -> u) -> bool

Nous arrivons maintenant au coeur du sujet. Quelles sont les fonctions représentables de ((u -> u) -> u) -> bool ? Ce sont les fonctions qui prennent bot, mid et top en paramètre et qui renvoient true ou false, ou divergent.

Quand on a un paramètre de (u -> u) -> u, on peut :

Pour toutes ces fonctions, le choix du booléen b n’a pas d’importance : que ce soit true ou false, ça ne diverge pas et c’est tout ce qu’on en tire.

On peut cependant imaginer une autre fonction que l’on appellera use :

bot
mid true
top false

(on peut inverser true et false ici, ça ne change pas grand chose)

Cette fonction permettrait de différentier mid et top, bien qu’elles renvoient les même résultats sur la valeur où elles sont toutes les deux définies. On ne peut pas la coder dans un langage fonctionnel pur. On peut cependant l’écrire en Caml, en se basant sur l’observation suivante : il faut renvoyer true si et seulement si la fonction "utilise" la fonction u -> u qui lui est passée en paramètre.

let use f =
   let used = ref false in
   f (fun () -> used := true);
   !used

Le code utilise un effet de bord, mais la fonction est bien fonctionnelle et appartient donc à la classe SR.

Exercice (plutôt facile)
Coder use en utilisant des exceptions à la place des références.

Cet exercice, ainsi que les suivants, demande d’écrire une fonction. Vous pouvez le faire dans le langage que vous voulez. L’auteur de l’article le ferait sans doute en SML (mais tous mes exercices ne trouvent pas leur solution dans l’article), je l’ai fait en OCaml, mais vous pouvez le faire dans le langage que votre choix. Tout me va, du moment que vous savez différencier les fonctionnalités "pures" du langage des autres (qu’il ne faut pas utiliser sauf quand c’est explicitement demandé), et que vous restez dans un cadre séquentiel. Pour les exercices qui parlent d’exceptions, il est sous-entendu qu’elles ont la sémantique des exceptions ML : si votre langage n’en a pas, faites comme si, un pseudocode suffit. Si vous ne les connaissez pas, j’en ai fait un résumé rapide en annexe.

Fonction modulo

La fonction modulo est un exemple qu’on sent un peu plus utile de fonction SR qui n’est pas représentable dans un langage fonctionnel pur. En deux mots, modulo surveille l’utilisation d’une des fonctions qui lui est passée en paramètre, c’est à dire les arguments qu’elle reçoit au court de ses appels, et les résultats qu’elle renvoie.

Plus précisément, modulo prend une fonction q : (int -> int) -> int (comme "questions") et une fonction r : int -> int (comme "réponses"). Imaginez que l’on donne la fonction r en paramètre à la fonction q, qui doit renvoyer un entier. Les deux fonctions (comme toutes les fonctions de l’article) sont supposées fonctionnelles, donc les moyens d’action de q pour fournir son résultat sont limités : il doit poser des questions à r et, selon les réponses, décider du résultat. Il peut poser une questions, plusieurs, aucunes (c’est alors une fonction constante), poser un nombre différent de questions selon les réponses qu’il a déjà reçues, etc. On définit modulo ainsi : il renvoie l’ensemble des questions posées par q, ainsi que les réponses que r a données.

Il est facile de coder modulo en utilisant des références :

let modulo q r =
  let li = ref [] in
  let traced_r x =
    let y = r x in
    li := (x, y) :: !li;
    y in
  ignore (q traced_r);
  !li

Il y a cependant un problème : cette fonction n’est pas SR ! En effet, elle produit des résultats différents pour fun r -> r 1 + r 3 et fun r -> r 3 + r 1, qui ont pourtant le même représentant dans [int -> int] : le résultat varie selon l’ordre dans lequel les questions ont été posées (d’abord 3, après 1, ou l’inverse). Pour la même raison, on ne s’intéresse pas au nombre d’appels de chaque argument, mais juste à la présence d’au moins un appel avec cet argument.

Il est cependant facile de résoudre ce problème : au lieu d’une liste de résultats on renvoie un ensemble de résultats, en utilisant un type dédié, ou en supprimant les doublons et triant la liste :

let modulo q r =
  let li = ref [] in
  let traced_r x =
    let y = r x in
    if not (List.mem_assoc x !li) then
      li := (x, y) :: !li;
    y in
  ignore (q traced_r);
  List.sort (fun (a, _) (b, _) -> a - b) !li

Cette fonction est maintenant SR. Pourquoi ? On pourrait imaginer que deux implémentations d’une même fonction partielle, qui ne posent pas les mêmes questions. En réalité, ça n’est pas possible : si la première fonction demande un entier n que la deuxième ne demande pas, il suffit de donner une fonction (SR) qui est définie partout sauf en n pour que les deux fonctions produisent des résultats différents (car la première diverge), donc elles ne correspondent pas à la même fonction mathématique.

(moins facile) Écrire modulo en utilisant des exceptions (et sans références).

On arrive maintenant au premier point tangent. Pour rendre notre fonction SR on a du lui retirer des informations, en fournissant du travail supplémentaire. L’auteur de l’article le remarque bien et utilise une formulation poétique : « one sometimes has to do stupid extra work in order to behave functionally ». Cette idée (fournir du travail supplémentaire pour garantir de bonnes propriétés) n’est pas du tout spécifique à ce papier, et je l’ai rencontré dans des situations variées. Par exemple, dans l’excellent CTM, Peter Van Roy différencie la programmation concurrente déterministe de la concurrence non-déterministe. Il doit parfois brider certaines de ses opérations pour rester dans le cadre déterministe : ça limite un peu (voire beaucoup dans certains cas) l’expressivité, mais apporte des avantages considérables en terme de raisonnement sur les programmes, recherche des erreurs, optimisations potentielles, etc.

(moins facile) D’après l’auteur, « indeed it is easy to see how use can be defined from modulo in pure functional ML ». Définir use à partir de modulo.

(difficile) En fait, l’expressivité de modulo est équivalente à celle de use : définir modulo à partir de use. Comme précédemment, il ne faut utiliser aucune autre fonctionnalité impure. Indice : l’implémentation (ou en tout cas la mienne) est nettement moins efficace que les précédentes.

L’auteur présente rapidement quelques fonctions SR qui ne sont pas définissables à partir de use ou modulo, mais sans expliciter leur définitionε ni justifier cette non-définissabilité. Il évoque même une SR universelle, qui permettrait d’exprimer toutes les autres, bien que très peu efficace.

ε : si quelqu’un comprend la signification du deuxième paramètre de la fonction E de l’article, je suis preneur ; je croyais l’avoir trouvée en lisant le paper la première fois, mais je m’étais peut-être trompé, et en tout cas ne l’ai pas retrouvée au moment de la présente rédaction.

Cas d’utilisation

L’auteur présente ensuite deux applications pratiques des fonctions SR. Elles restent de l’ordre du jouet, parce qu’il explique ensuite qu’on peut toujours faire mieux, soit en abandonnant la contrainte de comportement fonctionnel, soit en enrichissant l’interface des fonctions considérées, mais ça reste assez amusant à voir.

Prédicat de recherche

On définit une fonction search :

int -> ((int -> int) -> bool) -> (int -> int) list`

search n pred doit fournir la liste des permutations de [1 .. n] (représentées comme des fonctions int -> int) qui vérifient le prédicat pred.

L’implémentation naïve parcourt l’espace de recherche, qui est de taille !n. Il est possible de couper de grandes parties de l’espace de recherche en utilisant la fonction modulo sur les permutations qui ne vérifient pas le prédicat : si le prédicat ne demande que les trois premières valeurs (en 1, 2 et 3) d’une permutation avant de renvoyer une réponse négative, il est inutile de tester toutes les permutations ayant les mêmes images en 1, 2 et 3 : la réponse sera forcément négative aussi. On a donc éliminé (n - 3)! candidats potentiels.

La définition de search est assez générale pour être appliquée à des problèmes de programmation par contrainte classique, comme le problèmes des huits reines, et l’optimisation utilisant modulo la rend, d’après l’auteur, raisonnablement efficace.

Il est bien sûr possible de faire le même genre de choses en restant dans le cadre des fonctions pures : il suffit de modifier l’interface de search pour que le prédicat renvoie de lui-même les informations sur les appels qu’il a effectué.ζ Plus généralement, on peut visiblement imiter l’effet des fonctions SR impures dans un langage pur, en ajoutant des informations aux valeurs de retour des fonctions appelées. Ce n’est cependant pas toujours possible, par exemple si le prédicat est fourni par une bibliothèque externe sur laquelle le programmeur n’a pas de contrôle.

ζ : (int -> int) -> bool * (int * int) list

Plus généralement, et c’est le second point tangent, l’idée d’enrichir l’interface va en fait à l’encontre des principes habituels de génie logiciel : il faudrait modifier la fonction pour révéler une partie plus importante de son implémentation interne, dans le but d’un usage particulier, ce qui nuit d’une part à la modularité (il faut modifier l’interface d’une fonction fondamentale dans la perspective d’une utilisation spécifique qui peut être très loin dans la chaîne de dépendances), d’autre part à l’encapsulation (on demande à une fonction d’exposer plus d’information sur son implémentation interne). Cette pratique n’est tout simplement pas praticable à grande échelle : si l’on essayait d’exposer toutes les informations potentiellement utilisables par ce genre de pratiques rendues explicites, cela reviendrait essentiellement à rendre publique l’implémentation complète de la fonction.

C’est une question que j’ai trouvé intéressante parce que d’autres outils de la programmation fonctionnelle pure, comme les monades, peuvent soulèver des problèmes similaires. Les fonctions SR sont ici des outils précieux parce qu’elles permettent d’accéder à des informations sur une fonction sans alourdir son interface. Comme dit l’auteur, elles servent en quelque sorte à "rendre la boîte noire moins opaque".

Intégration d’une fonction

Le deuxième exemple est aussi assez joli. Supposez que l’on représente un nombre réel (entre 0 et 1 par exemple) comme un flux paresseux de nombres entiers (ses décimales) : type real = int * (unit -> real).

On cherche à écrire une fonction qui intègre une fonction real -> real entre 0 et 1, à une précision donnée (le nombre de décimales exactes du résultat, passé en paramètre). On commence par demander la valeur de la fonction en 0 à une précision suffisante (au moins autant de décimales que ce qui est demandé pour le résultat final), mais on utilise une variante de modulo pour connaître le nombre k de décimales demandées par la fonction avant de renvoyer un résultat. On sait que, si on se contente de cette précision, tous les nombres réels qui ont les mêmes k premières décimales (ici tous les nombres inférieurs à 10-k) renverront le même résultat. On peut donc approximer l’intégrale de la fonction sur tout cette intervalle avec la précision désirée, et recommencer le processus en commençant à 10-k au lieu de 0. L’algorithme termine en un nombre fini d’étapes (l’auteur en fait la preuve), et c’est une manière astucieuse de faire de très bonnes approximations.

Conclusion

Je donnerai la solution des exercices dans un prochain billet. En attendant, n’hésitez pas à poser vos questions, proposer vos solutions, ou simplement donner votre avis en commentaires ; ils sont là pour ça !

Les commentaires risquent donc de contenir des (fragments de) solutions. Prenez garde à ne pas vous gâcher le plaisir de chercher accidentellement.

Par ailleurs. je suis tout aussi intéressé par des commentaires généraux sur la réaction : avez-vous trouvé ça intéressant ? Trop détaillé ? Pas assez détaillé ? Qu’est-ce qu’il faut changer ? Je n’ai pas encore complètement décidé de la forme que ces réactions devraient avoir, et si vous avez des conseils/demandes, c’est avec plaisir.


Appendices

Il y a quelque chose de curieux dans la définition de la relation [ ] (qui est celle de l’auteur) : on ne prend en compte pour définir les éléments de ['a -> 'b] que leur action sur les éléments définissables (tels qu’on peut écrire un bout de code qui fait exactement ça) de type 'a. Ça me dérange un peu, sachant qu’on pourrait éventuellement passer à une fonction une valeur qui n’est pas définissable à l’intérieur du langage, mais qui fait appel à une bibliothèque logicielle codée dans un autre langage. Dans ce cas il faudrait considérer l’action sur toutes les fonctionnelles, et pas seulement les fonctionnelles définissables.

Exceptions en ML

Je décris ici les expressions en OCaml, mais l’important c’est la sémantique (ce que ça fait), pas la syntaxe (comment ça s’écrit). Le but c’est que vous sachiez un peu précisément ce que vous pouvez utiliser pour les exercices qui demandent d’utiliser des exceptions : un pseudo-code suffit, mais il faut comprendre ce que vous avez le droit de faire ou pas.

L’idée de base est qu’une expression, quand elle est lancée (raise) interromp complètement le calcul qui l’entoure, sauf si elle est rattrappée par un bloc try .. with. Par exemple :

let exists predicate array =
  try
    for i = 0 to Array.length array - 1 do
      if predicate array.(i)
      then raise Exit
    done;
    false
  with Exit -> true

Le bloc try <expr> with <cases> évalue l’expression <expr>, renvoie sa valeur si aucune exception n’est levée pendant l’évaluation, et sinon réagit selon les cases <cases> (c’est un filtrage de motif, mais c’est un détail) : si l’un des cas correspond à l’expression lancée, elle est arrêtée et la branche correspondante est suivie. Ici, on teste toutes les valeurs d’un tableau, en lançant une exception si l’une d’entre elle vérifie une condition, et on renvoie "faux" sinon. En dehors de la boucle, on rattrappe l’exception en renvoyant "vrai". Cela teste l’existence d’un élément vérifiant le prédicat, en arrêtant immédiatement le parcours du tableau dans ce cas (un peu comme les instructions de contrôle break ou return des langages impératifs).

On peut aussi utiliser des exceptions qui transmettent des valeurs. Pour cela il faut déclarer une nouvelle exception (Exit est prédéfinie) :

 exception Mon_exception of mon_type

mon_type est le type des valeurs transmises par l’exception. Par exemple :

exception Position_invalide of (int * int)

... raise Position_invalide (1, 2) ...

match .. with
  Position_invalide (x, y) ->
    printf "erreur : position invalide (%d, %d)" x y

Et les langages paresseux ?

Dans un langage paresseux, les fonctions ne prennent pas des valeurs, mais des termes quelconques que la fonction évaluera éventuellement elle-même si elle en a besoin. Toute la différence pour ce qui nous concerne repose sur le fait qu’on ne sait pas encore si les paramètres vont diverger ou pas (alors qu’en évaluation stricte, on est sûr qu’ils ne divergent pas). Au lieu de fonctions de ['a] dans ['b] + {⊥}, on doit donc modéliser avec des fonctions de ['a] + {⊥} dans ['b] + {⊥}.

Un terme paresseux t est donc un terme "par encore évalué". Il suffit de le représenter dans un langage strict par le terme fun () -> t, qui n’est pas encore évalué non plus.

Plus formellement : au lieu du type 'a, on considère que le paramètre est de type u -> 'a. En effet, [u -> 'a] = {*} -> 'a + {⊥} est isomorphe à 'a + {⊥}. Donc dans un langage strict [(u -> 'a) -> 'b] = ['a]+{⊥} -> ['b]+{⊥}.

On ne gagne donc aucune expressivité en passant à un langage paresseux. Cette étude les concerne tout autant que les langages stricts, modulo une traduction des types. Les fonctions u -> u étudiées sont juste des termes de type u dans un langage paresseux, (u -> u) -> u donne u -> u, et le dernier type est (u -> u) -> bool.

Dans un cadre paresseux, mid est la fonction qui force l’évaluation de son argument. En haskell on écrirait par exemple :

mid f = seq f ()

Impossibilité de neg

L’auteur ne donne pas plus de précisions, mais il n’est pas du tout clair que la fonction neg : 0 -> * | 1 -> ⊥ conduise au problème de l’arrêt. Dans cette section je donne une preuve faite de mes blanches mains, mais elle est un peu compliquée (je me plonge dans une classe de fonctions plus riche), donc si vous en avez une plus simple je suis intéressé.

Le problème de l’arrêt est la question suivante : « peut-on décider sans l’exécuter de si un programme va terminer ou boucler à l’infini ? ». Plus précisément, « existe-t-il un programme qui prend un programme P en paramètre, et renvoie vrai‘ si P bouclerait à linfini s’il était exécuté, et faux sinon ? ». On sait depuis le début du siècle précédent (donc avant l’apparition du premier ordinateur) que la réponse est « Non ».

La preuve de ce « Non » est assez simple (c’est en fait un remake d’une preuve très connue en mathématiques, l’argument diagonal) : imaginons qu’il existe un tel programme H (comme Halting problem). On définit le programme B (comme "Boum") suivant :

B(P) =
  si H(P(P)), boucler à l'infini
  sinon, terminer

B prend un programme, l’applique sur lui-même (le truc pas tordu déjà) et inverse sa divergence : si le programe diverge, B s’arrête, si le programme s’arrête B diverge. On peut maintenant poser la question qui tue : quel est le comportement de B(B) ?

Boum. On est arrivé à une contradiction, donc on est parti de quelque chose de faux. La seule supposition qu’on a faite pour en arriver là est l’existence de P, donc c’est ce qui est faux : P n’existe pas.

On peut réutiliser cette preuve pour déduire de nombreuses choses sur ce qu’on sait des programmes. Il suffit de "réduire" le problème au problème d’arrêt, en montrant en gros que « monsieur, si on savait répondre à votre question, on pourrait résoudre le problème d’arrêt, you fool ».

Cas présent

Dans le cas présent, on s’intéresse à la fonction neg qui s’arrête si on lui donne 0 (la fonction divergente), et diverge si on lui donne 1. On sent bien qu’il y a un lien avec le problème de l’arrêt, le fait d’inverser les divergences, mais ça ne va pas forcément plus loin : cette fonction ne permet pas de savoir directement si l’argument diverge puisque, une fois sur deux, elle ne répond rien du tout (⊥). Par exempe la fonction voisine 0 -> ⊥ | 1 -> * existe évidemment (c’est mid) et ça n’a rien à voir avec le théorème d’arrêt.

Concrètement, dans notre cadre la fonction d’arrêt est la fonction suivante :

halt 0 = true
halt 1 = false

Peut-on écrire halt à partir de neg ? Dans SR ça n’a pas l’air commode : si on donne 0 à neg, le calcul termine et on peut renvoyer true, mais si on donne 1 on est coincé dans une boucle infinie et on ne peut pas renvoyer false.

Je m’en tire en sortant de SR, en rajoutant une primitive de parallélisme : on ajoute la primitive par : (α -> β) -> (α -> β) -> (α -> β), qui exécute en parallèle les deux fonctions passées en paramètre : quand on lui donne une valeur, elle demande à la première fonction et à la deuxième simultanément, et elle renvoie le résultat de la première des deux à terminer ; si les deux divergent, elle diverge.

Cette primitive existe : il suffit de se placer dans un langage avec multi-threading et un ordonnancement équitable, et d’exécuter les deux fonctions dans des threads séparés, ou plus simplement encore de formaliser l’exécution d’un programme comme une machine procédant étape par étape, et d’alterner une étape d’exécution de chaque fonction à tour de rôle. Cela permet d’accéder à une autre classe d’expressivité des fonctions ; si l’on définit par convenablement, on peut rester dans un cadre déterministe (il suffit de s’assurer que si on lui donne deux fonctions qui terminent, elle ne choisira pas parfois l’une, parfois l’autre mais toujours la même), par contre on sort du cadre des "fonctionnelles", car deux implémentations dénotant une même fonction mathématique pourront donner des résultats différents (si l’une est beaucoup plus lente que l’autre, elle sera moins choisie par par).

(plutôt facile, si vous avez fait le reste) Écrire halt en utilisant par, neg et sans fonctionnalités impures.

Donc, dans le cadre bien réel des "fonctions SR auxquelles ont a ajouté du parallélisme", on ne peut pas écrire neg puisqu’elle permettrait d’écrire halt. Si on ne peut pas écrire neg après avoir ajouté par, on ne pourra sûrement pas l’écrire sans ajouter par (puisqu’on peut écrire moins de chose), donc [neg] n’appartient pas à [(u -> u) -> u].