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 :
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 ;
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.
Les types et valeurs de base du langage sont traduits par les
ensembles et éléments correspondants : [nat] = N, [bool] = {true,
false}, [1] = 1, etc.
On définit ['a -> 'b] comme l’ensemble des fonctions partielles de
['a] dans ['b] qui sont implémentables dans notre langage de
programmation
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 :
(* -> ⊥), la fonction qui diverge, que je noterai 0
(* -> *), 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 :
diverger dans tous les cas : c’est la fonction [bot] : f -> ⊥,
par exemple let rec bot f : unit = bot f ;
renvoyer () dans tous les cas : c’est la fonction [top] : f -> *,
par exemple let top _ = () ;
évaluer l’argument en () puis renvoyer () : c’est la fonction
[mid] : f -> f(*), par exemple let mid f = f ()
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 :
diverger dans tous les cas ;
évaluer en 0, puis renvoyer un booléen b :
| paramètre | retour
|
| bot | ⊥
|
| mid | ⊥
|
| top | b
|
évaluer en 1, puis renvoyer un booléen b :
renvoyer un booléen b dans tous les cas
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 :
(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
Récapitulatif des exercices
- Écrire
use avec des exceptions (lien)
- Écrire
modulo avec des exceptions (lien)
- Écrire
use à partir de modulo (lien)
- Écrire
modulo à partir de use (lien)
- (en annexe)
Écrire
halt avec neg et par (lien)
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) ?
si B(B) s’arrête, alors par définition B(B) diverge
si B(B) diverge, alors par définition B(B) s’arrête
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].
![[Atom]](http://media1.huoc.org/feed.png){kind=small}
![[Mail]](http://media1.huoc.org/mail.png){kind=small}
![[Twitter]](http://media1.huoc.org/twitter.png){kind=small}
![[Atom]](http://media1.huoc.org/smallfeed.png){kind=small}
tout en haut de la page.α
