Journal Haskell -- Évaluation paresseuse

Posté par Guillaum (site web personnel) le 03 mai 2016 à 12:31. Licence CC By‑SA.

Étiquettes :

mai

2016

Sommaire

Opérateur à court-circuit
Visualisation
Fun et brain melting

Bonjour,

Je voulais vous parler d'évaluation paresseuse, en me servant comme support du langage Haskell.

L'évaluation paresseuse c'est juste le summum de la procrastination, reporter à demain (ou jamais) ce que tu n'as pas besoin de faire aujourd'hui. En haskell, une fonction n'est évaluée que si la valeur de retour est nécessaire pour évaluer immédiatement un autre résultat.

Je ne vous parlerai pas des avantages ou inconvénient de cela, mais je vais plutôt donner des exemples que je trouve amusant.

Opérateur à court-circuit

Dans tous les langages de programmation il y a des opérateurs à court-circuit, comme le && / and. Exemple en Python :

resultat = longCalculA(argA) and longCalculB(argB)

longCalculB ne sera effectué que si longCalculA renvoie True. Dans ce cas là, le résultat de and est défini par le résultat de longCalculB. Mais si longCalculA renvoie False, alors le résultat de longCalculB n'est pas nécessaire, et il ne sera donc pas calculé.

Cet opérateur and est un cas particulier du langage Python et il est impossible de l’implémenter en Python pur. Essayons :

def myAnd(a, b):
    if a == False:
        return False
    else:
        return b

resultat = myAnd(longCalculA(argA), longCalculB(argB))

Bien que le résultat sera le même, les deux fonctions longCalculA et longCalculB seront appelées avant l'appel à myAnd, et donc une perte d'efficacité très claire.

En Haskell :

myAnd a b = if a == False
            then False
            else b

resultat = myAnd (longCalculA argA) (longCalculB argB)

Ici les calculs ne sont pas effectués tant que ce n'est pas nécessaire. Ainsi pour connaitre le resultat, il faut regarder la valeur de longCalculA (et donc effectuer le calcul), mais si celui-ci est False, alors la valeur de b importe peu et le calcul ne sera jamais effectué.

Visualisation

Pour les besoins de cet exemple j'ai crée une fonction longId qui met du temps (~ une seconde) à renvoyer la valeur passée en paramètre, j'ajoute les temps en commentaire sur chaque ligne :

*Long> print (longId 10) -- 1s
10
*Long> print (longId "Hello") -- 1s
"Hello"

On va s'amuser un peu avec, que se passe-il si on applique la fonction longId sur tous les éléments de 1 à 10 :

*Long> print (map longId [1..10]) -- 10 secondes
[1,2,3,4,5,6,7,8,9,10]

En fait, de façon amusante, les chiffres apparaissent les uns après les autres, un par seconde. En fait la fonction print consomme les éléments du résultat un par un et est capable de les afficher quand ils arrivent.

Cependant, combien de temps prend le calcul de la longueur de la liste ?

*Long> print (length (map longId [1..10])) -- instantané
10

C'est instantané, car il n'est pas nécessaire d'évaluer les cellules de la liste pour connaitre la longueur.

Autres exemples, avec la fonction elem qui teset si un élément est dans la liste :

*Long> print (elem 1 (map longId [1..10])) -- 1s
True
*Long> print (elem 5 (map longId [1..10])) -- 5s
True
*Long> print (elem 10 (map longId [1..10])) -- 10s
True

Les éléments de la liste qui ne sont pas testés ne sont pas calculés.

Nous allons pousser un peu plus grâce à l'outil :sprint du shell ghci. Celui-ci permet de voir les valeurs évaluées et celles qui ne le sont pas encore.

Nous allons partir d'une liste toute simple :

*Long> let l = map longId [1..10] :: [Int]

(Pour des raisons techniques je force le type de la liste à une liste d'entiers [Int]).

Comment est évalué l ?:

*Long> :sprint l
l = _

Ici _ signifie que ce n'est pas évalué.

Prenons maintenant les 3 premiers éléments de la liste, sans les afficher.

*Long> print (length (take 3 l)) -- instantané
3
*Long> :sprint l
l = _ : _ : _ : _

Ici on obtient une suite de cellules de liste, liées ensemble par (:). Il y a 4 éléments, les 3 premiers et la suite de la liste. Notez que les éléments ne sont pas évalués.

Nous allons commencer à en évaluer quelques-un, le premier et le dernier.

*Long> print (head l) -- 1s
1
*Long> :sprint l
l = 1 : _ : _ : _

*Long> print (last l) -- 1s
10
*Long> :sprint l
l = [1,_,_,_,_,_,_,_,_,10]
*Long>

L'évaluation du premier élément apparaît dans sprint, le _ est remplacé par 1. L'évaluation du dernier élément force l'évaluation de toutes les cellules de la liste (mais pas de leur contenu) ainsi que du contenu de la dernière cellule. Les deux évaluations n'ont prise chacune qu'une seule seconde, temps nécessaire pour évaluer la première ou dernière cellule.

Nous allons conclure :

*Long> print (sum l) -- 8 secondes
55
*Long> :sprint l
l = [1,2,3,4,5,6,7,8,9,10]

Notez que cela ne prend que 8 secondes, puisque la première et dernière cellule sont déjà évaluées.

Fun et brain melting

Nous allons nous intéresser à une fonction totalement inutile qui calcul une normalisation d'une liste de nombre en divisant les éléments de la liste par la somme des éléments de cette liste, soit :

*Main> f [1,2,3,4]
[0.1,0.2,0.3,0.4]

(ici la somme fait 10).

Une façon simple d'écrire cette fonction est la suivante :

f l = let s = sum l
      in map (/s) l

En premier lieu on calcule la somme de la liste avec s = sum l et on applique la division par s, (/s) sur chaque élément de la liste avec la fonction map.

La liste est parcourue deux fois, une fois pour faire la somme, et une fois pour faire la division de chaque élément. Ne pourrait-on pas faire cela en un seul parcours pour s'amuser ?

Pour cela nous allons introduire une nouvelle fonction g qui fait deux choses : elle calcule le résultat et elle renvoie la somme. Cependant elle prend la somme utilisée pour la division en paramètre. Exemple :

*Main> g 10 [1,2,3,4]
([0.1,0.2,0.3,0.4],10.0)
*Main> g 100 [1,2,3,4]
([1.0e-2,2.0e-2,3.0e-2,4.0e-2],10.0)

Dans le premier exemple, la somme passée est 10 et le résultat est le bon. Dans le second cas, la somme passée est 100, donc la liste de résultats a des valeurs 10 fois trop petites, mais par contre la somme retournée est bien 10.

Je laisse l'écriture de la fonction g en tant qu'exercice au lecteur, elle n'est pas importante. Écrivons maintenant f :

f l = let s = sum l
          (res, s') = g s l
      in res

Ici nous calculons la somme grâce à s = sum l, nous appelons la fonction g en lui passant la somme et la liste et nous récupérons le résultat et la somme s' calculée par g, pour enfin renvoyer le résultat let ... in res. La liste est toujours parcourue deux fois (dans sum et dans g).

Ici s et s' représentent la même valeur, la somme de la liste. On pourrait même envisager de remplacer l'un par l'autre :

f l = let s = sum l
          (res, s') = g s' l
      in res

Et ici le calcul de s ne sert plus à rien… :

f l = let (res, s') = g s' l
      in res

Alors pourquoi cela fonctionne, sachant que s' est autant un paramètre de g qu'un résultat ? La fonction g va se contenter de crée une liste qui contient :

Mais elle contient les fonctions non évaluées. Ainsi la valeur de s n'est pas nécessaire pour construire la liste. Bien que pas encore calculée, elle peut être utilisée dans des expressions à condition que son calcul ne dépende pas du résultat de ces expressions. Une fois que g se termine, la valeur de s est bien définie, et donc l'évaluation des cellules de la liste de résultat de g peut être effectuée.

Bref, moi je trouve cela marrant. Et vous ?

# pour implémenter : enrober dans une fonction

Posté par Dreammm le 03 mai 2016 à 13:53. Évalué à 9.
Le problème pour implémenter l'évaluation paresseuse, c'est … l'évaluation immédiate, plus exactement des paramètres quand on évalue une fonction/méthode.

C'est possible de circonvenir la chose en enrobant une valeur dans une fonction.
Cela suppose la possibilité d'utiliser une fonction comme un paramètre d'une autre fonction, ce qui commence à se généraliser dans pas mal de langage.

On appelle cela un thunk
Exemple en javascript :
```
// let a=…, let b=…
function thunk_a(){return a}
function thunk_b(){return b}

function myAnd(a,b) { // a and b are thunks
  let valA = a()
  if valA then
    return valA
  else
    return b()
}
```
C'est moche et lourdingue, mais ça fait ce qui était demandé.

La même chose en bien mieux, par Larry Wall : Laziness is a virtue

Soyez des feignasses !
- [^] # Re: pour implémenter : enrober dans une fonction
  
  Posté par Guillaum (site web personnel) le 03 mai 2016 à 15:16. Évalué à 2.
  
  Ce que j'aime en haskell c'est le coté simple de la syntaxe à ce niveau, tu n'as pas à te préoccuper de qui va évaluer ton thunk, où qu'il soit évalué plusieurs fois.. Tu peux écrire une fonction qui marche sur n'importe quelle type de donnée que ce soit une donnée lazy ou pas.
  
  Alors il est certain que cela a des défauts par certains cotés.
  - [^] # Re: pour implémenter : enrober dans une fonction
    
    Posté par Kaane le 04 mai 2016 à 00:07. Évalué à 0.
    
    Ce que j'aime en haskell c'est le coté simple de la syntaxe à ce niveau, tu n'as pas à te préoccuper de qui va évaluer ton thunk, où qu'il soit évalué plusieurs fois.
    
    Je te rassure en javascript on arrive à des résultats similaire avec des iterators.
    - [^] # Re: pour implémenter : enrober dans une fonction
      
      Posté par barmic le 04 mai 2016 à 09:24. Évalué à 3.
      
      Et bientôt avec les générateurs
      
      Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)
    - [^] # Re: pour implémenter : enrober dans une fonction
      
      Posté par Guillaum (site web personnel) le 04 mai 2016 à 09:31. Évalué à 2.
      
      C'est marrant comment les seuls réponses que j'ai eu c'est "Je peux le faire en C / Javascript / Brainfuck".
      
      J'ai vraiment du rater mon discours parce que je trouve le dernier point vraiment intéressant, mais il n'est pas discuté. Dommage.
      
      Alors simplement que je ne meurs pas idiot, comment on peut faire l’exemple de structure de contrôle custom et l’exemple de parcours de liste en une fois en javascript ? A ma connaissance l'un est difficile / pas élégant / pas safe et l'autre est impossible, mais je me trompe surement.
      - [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par cimcim le 04 mai 2016 à 10:19. Évalué à 0.
        
        Bon, comme dit dans mon autre commentaire, je ne connais pas Haskell, je risque donc de dire des énormités, merci de m'en excuser (et de m'expliquer, c'est comme ça qu'on progresse !)
        
        Mais je ne comprend pas comment ça peut fonctionner, aussi bien en interne (comment haskell gère des résultats non évalués) que ton bout de code final
        
        f l = let (res, s') = g s' l in res
        
        Ici, le s' que tu passes en argument , il vient d'où ?
        (car si je comprend bien,
        
        (res, s') = g s' l
        
        c'est l'évaluation de la fonction g, avec comme argument s' et l, retournant res et s'.)
        
        Le 2e point que je ne capte pas, c'est :
        
        La fonction g va se contenter de crée une liste qui contient :
        [L0/s,L1/s,…]
        Mais elle contient les fonctions non évaluées.
        
        La liste d'origine est donc parcourue pour créer la 2nde liste, contenant les fonctions non évaluées. Mais pour évaluer les résultats, la 2nde liste devra aussi être parcourue, non ?
        
        [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par Guillaum (site web personnel) le 04 mai 2016 à 11:37. Évalué à 4.
        
        Je viens de réaliser une explication d'une heure et j'ai fais un raccourcis clavier à la con sur mon navigateur et j'ai tout perdu… Je me déteste.
        
        Ici, le s' que tu passes en argument , il vient d'où ?
        
        C'est autant un argument qu'un résultat. On peut s’intéresser à un cas très simple :
        
        blork = let l = 1:l in l
        
        Ici (:) représente l'ajout en tête d'une valeur sur une liste tel que 1:2:[3,4] == [1,2,3,4]
        
        On peut appeler la fonction blork avec une valeur et voir son comportement :
        
        blork -- équivalent à l -- équivalent à 1:l -- équivalent à 1:1:l -- équivalent à 1:1:1:l
        
        J'ai crée une liste infinie de 1 avec une expression qui s'auto-référence. L'évaluation paresseuse fait que la liste ne sera jamais évaluée, seul les éléments nécessaires le seront. Si je demande avec take 2 les deux premiers éléments, il peux s’arrêter à 1:1:l sans évaluer la suite.
        
        La liste d'origine est donc parcourue pour créer la 2nde liste, contenant les fonctions non évaluées. Mais pour évaluer les résultats, la 2nde liste devra aussi être parcourue, non ?
        
        Oui. Mais de toute façon tu feras surement un traitement sur cette seconde liste, pour l'afficher par exemple. Les résultats seront évalués à ce moment. Il y a ce site que j'aime beaucoup qui permet d'observer les évaluations.
        
        [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par cimcim le 04 mai 2016 à 11:56. Évalué à 0.
        
        OK, je vois mieux.
        
        C'est autant un argument qu'un résultat.
        
        Du coup, je rapproche ça à un pointeur (oui, je suis développeur c principalement…) avec le contenu de s' mis à jour dans g
        
        Merci pour ton temps et tes explications !
        
        [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par Guillaum (site web personnel) le 04 mai 2016 à 12:58. Évalué à 2.
        
        Du coup, je rapproche ça à un pointeur (oui, je suis développeur c principalement…) avec le contenu de s' mis à jour dans g
        
        Oui mais avec quelques subtilités. Principalement l'ordonnancement des opérations est garantie. En gros tu est certain que une utilisation de s' te retourne la somme complète, et pas une somme partielle en milieu de route.
        
        [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par Thomas Douillard le 05 mai 2016 à 12:56. Évalué à 2.
        
        C'est mieux de détester la personne qui n'a pas implémenté https://linuxfr.org/suivi/sauvegarde-auto-des-commentaires-en-redaction :)
        
        [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par Benoît Sibaud (site web personnel) le 05 mai 2016 à 14:16. Évalué à 9. Dernière modification le 05 mai 2016 à 14:16.
        
        Le code étant libre et public, c'est mieux de détester tous ceux qui n'ont pas implémenté la fonctionnalité alors qu'ils auraient pu. Ah non en fait ce n'est pas mieux. Le mieux serait d'utiliser son émotion comme énergie positive pour créer la fonctionnalité, la soumettre et en tirer gloire, bonne fortune et karma positif sur 3,14 générations.
        
        [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par Thomas Douillard le 05 mai 2016 à 14:29. Évalué à 2.
        
        Chut ne dis rien ça casse l'effet /o\
        
        [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par barmic le 06 mai 2016 à 23:13. Évalué à 4.
        
        J'ai crée une liste infinie de 1 avec une expression qui s'auto-référence. L'évaluation paresseuse fait que la liste ne sera jamais évaluée, seul les éléments nécessaires le seront.
        
        J'ai déjà eu des surprises assez marrante avec des traitements paresseux (chacun son humour…).
        Je pars d'une collection d'entiers et j'associe des traitements (paresseux) à chacun de ses éléments et tous les traitements que j'appliquais étaient bien paresseux… Donc jamais réalisés. Il faut forcément sortir de la paresse à un moment. C'est des choses dont il faut faire attention.
        
        Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)
        
        [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par Aluminium95 le 08 mai 2016 à 09:17. Évalué à 7.
        
        Il faut forcément sortir de la paresse à un moment.
        
        En effet, il faut faire attention, mais la majorité du temps on ne se rend pas compte au niveau sémantique de l'évaluation paresseuse. Si le code ne fait pas ce que l'on pense, et que les calculs ne sont pas faits, c'est qu'on utilise jamais la valeur à calculer. Cela pose uniquement problème quand trouver la valeur est moins important que faire le calcul, par exemple avec des effets de bords cachés (mais normalement c'est déconseillé en Haskell).
        
        La majorité des problèmes viennent de code qui n'évaluent pas tout de suite la valeur, et qui accumulent des instructions, alors que calculer la valeur prend un espace mémoire constant : par exemple, faire une séquence de modifications sur un entier se fait en espace constant, alors que sous certaines conditions, cela se fera en espace linéaire si on évalue paresseusement.
      - [^] # Re: pour implémenter : enrober dans une fonction
        
        Posté par Thomas Douillard le 05 mai 2016 à 12:53. Évalué à 2.
        
        Fais pas attention, tu réponds à khane<.
# astuce

Posté par max22 le 03 mai 2016 à 15:58. Évalué à 1.
Je ne sais pas si tu as utilisé ça, mais pour avoir automatiquement le temps d'évaluation dans ghci il suffit de faire
```
:set +s
```
Sinon merci d'avoir fait découvrir sprint, ça a l'air super cool.
- [^] # Re: astuce
  
  Posté par Guillaum (site web personnel) le 03 mai 2016 à 16:01. Évalué à 2.
  Au départ c'est ce que je voulais faire, mais +s ne prend que le temps cpu en compte ;) Et comme ma fonction longId est un threadDelay, cela ne marche pas ;(
```
longID x = unsafePerformIO (threadDelay 1000000 >> return x)
```
# valeur vs pointeur

Posté par cimcim le 03 mai 2016 à 17:53. Évalué à 1.
Je ne connais pas Haskell, mais l'évaluation ou non des paramètres d'une fonction, ça me fait penser à un passage d'argument par valeur ou par pointeur/réference…

En c:
```
int resultat( int longCalculA, int longCalculB )
{
    if( !longCalculA )
        return longCalculA;
    else
        return longCalculB;
}

void main()
{
    resultat( longCalculA(), longCalculB() );
}
```
exécutera les 2 fonctions pour pouvoir passer leur valeurs de retour en arguments.

Alors qu'en passant les adresses des fonctions en arguments:
```
int resultat( int (*longCalculA)(), int (*longCalculB)() )
{
    int a = longCalculA();
    if( !a )
        return a;
    else
        return longCalculB();
}

void main()
{
    resultat( &longCalculA, &longCalculB );
}
```
Seul longCalculA() sera exécuté si il retourne 0.
- [^] # Re: valeur vs pointeur
  
  Posté par Guillaum (site web personnel) le 03 mai 2016 à 18:09. Évalué à 4.
  Tu es forcé de explicitement gérer toi même ces fonctions.
  
  Si par exemple tu veux faire quelque chose du genre :
```
void main()
{
       a(&longCalculA, &longCalculB);
       b(&longCalculA, &longCalculC);
       c(&longCalculB, &longCalculC);
}
```
  Sans connaitre le contenu de a, b et c, tu ne peux avoir aucune certitude sur le nombre d'appel aux fonctions longCalculA, longCalculB.
  - [^] # Re: valeur vs pointeur
    
    Posté par cimcim le 03 mai 2016 à 18:24. Évalué à 2.
    
    Exact, j'étais parti dans l'idée que a(), b() et c() étaient des fonctions écrites soi même dont on maitrisait le contenu.
# (oups)

Posté par feth le 03 mai 2016 à 22:11. Évalué à 0. Dernière modification le 03 mai 2016 à 22:14.

ce commentaire a été dépublié par son auteur qui n'avait pas bien lu le journal
# Dernier cas

Posté par Anthony Jaguenaud le 04 mai 2016 à 11:37. Évalué à 2.
Je n’arrive pas à reproduire ce que tu décris. J’ai fait mes tests dans l’interpréteur ghci :
```
Prelude> let g s l =  ((map (/s) l),sum l)
Prelude> let f l = let (res,s) = g s l in res
Prelude> f [1,2]
*** Exception: <<loop>>
Prelude> let r = f [1,2]
Prelude> l
*** Exception: <<loop>>
```
Par contre :
```
Prelude> let f l = let (res,s) = g (sum l) l in res
Prelude>  f [1,2]
[0.3333333333333333,0.6666666666666666]
Prelude>
```
Je me demande si ce n’est pas ton implémentation de g qui ferait que ça marche ?
- [^] # Re: Dernier cas
  
  Posté par Guillaum (site web personnel) le 04 mai 2016 à 11:45. Évalué à 2.
  Oui, l’implémentation doit être faite avec attention pour ne pas boucler.
```
let g s l =  ((map (/s) l),sum l)
```
  Je n'arrive pas à reproduire ta boucle en copiant ton implémentation de g. Es-tu certain que c'est bien celle que tu utilises ?
  
  Voici mon implémentation de g :
```
g s (x:[]) = ([x / s], x)              -- cas 0
g s (x:xs) = let (res, s') = g s xs    -- cas 1
             in ((x / s) : res, s' + x)
```
  Ici, dans le cas 0, je traite la liste d'un seul élément. Le résultat c'est [x / s] et la somme pour un unique élément c'est x.
  
  Dans le cas 1, je traite la liste de plus d'un élément. Je réalise d'abord un appel récursif g s xs pour récupérer le résultat res sur la sous liste et la somme s' sur la sous liste. Puis je renvois le résultat courant (x / s) : res) et la somme mise à jours s' + x.
  - [^] # Re: Dernier cas
    
    Posté par Anthony Jaguenaud le 04 mai 2016 à 15:05. Évalué à 2.
    En fait, c’est un problème d’interpréteur… en prenant le même code dans un fichier : linuxfr.hs
```
Prelude> :l linuxfr.hs
[1 of 1] Compiling Main             ( linuxfr.hs, interpreted )
Ok, modules loaded: Main.
*Main> f [1,2]
[0.3333333333333333,0.6666666666666666]
*Main> f [1..10]
[1.818181818181818e-2,3.636363636363636e-2,5.454545454545454e-2,7.272727272727272e-2,9.090909090909091e-2,0.10909090909090909,0.12727272727272726,0.14545454545454545,0.16363636363636364,0.18181818181818182]
*Main>
```
    Quand je définie tout dans l’interpréteur ça ne marche pas… bon, ce n’est pas grave. Merci pour la démonstration.
    
    Source :
```
g s l =  ((map (/s) l),sum l)

f l = let (res,s) = g s l in res

main = putStrLn $ show $ f [1,2]
```
# Visualiser les réductions

Posté par max22 le 05 mai 2016 à 12:09. Évalué à 2.

Pour bien comprendre la fin, j'ai pris un papier et un crayon. mais est-ce que ça existe un truc qui permet de visualiser les étapes de l'exécution du code ?
- [^] # Re: Visualiser les réductions
  
  Posté par Guillaum (site web personnel) le 06 mai 2016 à 23:28. Évalué à 4.
  
  C'est le mieux que je connaisse pour l'instant :
  
  http://chrisuehlinger.com/LambdaBubblePop/
# Programmation Dynamique

Posté par Aluminium95 le 10 mai 2016 à 21:55. Évalué à 1.
Un autre aspect amusant de l'évaluation paresseuse en Haskell c'est la facilité avec laquelle on peut faire de la programmation dynamique. L'idée est d'utiliser un tableau en haskell, via le module Data.Array, qui possède une fonction array avec un type compliqué, mais qui est simplement là pour construire un tableau à partir de bornes et d'une liste d'association indice-valeur.
```
unTableau :: Array Int Int
unTableau = array (0,10) [ (i,i) | i <- [0..10] ]
```
Imaginons qu'une suite double soit définie par la récurrence $u_j^{n+1} = a u_{j+1}^n + b u_j^n + c u_{j-1}^n$ avec
, et une condition initiale donnée. Alors un moyen très simple de calculer la matrice représentant les valeurs de la suite est le suivant :
```
calculSuite u0 = tableau
    where
        tableau = array ((0,0),(nMax,mMax)) [ ( (j,n), u j n ) | i <- [0..nMax], j <- [0..mMax] ]
        u 0 _ = 1
        u j 0 = u0 ! j
        u j n = if j == nMax then 
                   0
                else
                   a * (tableau ! (j+1,n-1)) + b * (tableau ! (j,n-1)) + c * (tableau ! (j-1,n-1))
```
Ce qu'il faut remarquer c'est que la fonction qui calcule les valeurs du tableau … accède au tableau !
Si les dépendances sont cycliques, le code ne termine pas, mais si on a montré qu'on peut effectivement faire le calcul, alors tout se passe bien. On remarque que mettre dans un tableau les valeurs correspond à enregistrer les appels à une fonction dans un tableau pour ne pas avoir à calculer plusieurs fois le même sous-arbre lors des appels récursifs.

Un avantage par rapport à un code manuel, est de ne pas avoir à gérer comment remplir le tableau : l'ordre d'évaluation est « automatique », alors que dans certain programmes dynamiques, il est pénible à mettre en place (ou du moins il faut réfléchir, et imbriquer plusieurs boucles).

Un désavantage est justement que quelqu'un qui lit le code doit avoir quelque part montré que les appels sont « cohérents » et que le programme ne va pas simplement boucler, ce qui force à mettre plus de documentation à disposition.
- [^] # Re: Programmation Dynamique
  
  Posté par barmic le 11 mai 2016 à 00:31. Évalué à 3.
  
  facilité avec laquelle
  
  Ah ! Ah ! Note que cette facilité s'accompagne d'une démonstration de ton code… :-)
  
  Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)
  - [^] # Re: Programmation Dynamique
    
    Posté par Aluminium95 le 12 mai 2016 à 13:11. Évalué à 3.
    Note que cette facilité s'accompagne d'une démonstration de ton code
    
    Que le code soit impératif en python ou bien utilise des concepts plus avancés, il faut toujours expliquer ce qu'il fait non ? Ne serait-ce que parce que les gens qui le lisent ne sont pas forcément bien concentrés, ou juste pour éviter toute ambigüité possible sur le sens de ce qui est écrit.
    
    En python, j'aurais donné certainement des explications très similaires, pour un code qui ferait la chose suivante :
    1. Construire une matrice de la bonne taille initialisée à None
    2. Définir les valeurs connues dans la matrice
    3. Faire une ou plusieurs boucles (ici deux) pour remplir la matrice en utilisant une récurrence dont on doit prouver qu'elle n'utilisera jamais des valeurs non initialisées (ie: on ne tombe pas sur None).
    Dans ce cas, la démonstration est la même en haskell si on résume de la même manière :
    1. Construire une matrice de la bonne taille initialisée avec les fonctions de calculs
    2. Définir la fonction de calcul d'une case en fonction des valeurs du tableau
    3. Prouver que les valeurs utilisées pour calculer une case n'ont pas de dépendances cycliques, ce qui correspond à donner un ordre d’initialisation valide en python
    La grosse différence est qu'une fois qu'on a une preuve, les détails de l'implémentation ne sont pas présents en haskell. Par exemple, on peut vouloir remplir la matrice diagonale par diagonale. Pour ce faire, il faut réfléchir à comment on fait les diagonales, ne pas se tromper sur les indices, bien parcourir tout le monde etc … Alors que c'est totalement inutile en haskell. Et cela est d'autant plus vrai que la dimension du tableau augmente, et donc que les procédures de calculs font intervenir de plus en plus de boucles imbriquées avec des invariants de plus en plus complexes.
    - [^] # Re: Programmation Dynamique
      
      Posté par kantien le 12 mai 2016 à 16:16. Évalué à 1.
      D'autant que sur un tel code, la définition de la fonction suit le schéma de la preuve par récurrence qui justifie son bon fonctionnement (c'est le principe même des langages fonctionnels, et des structures récursives).
      
      Exemple en OCaml sur le calcul de la hauteur d'un arbre binaire :
      
      type 'a btree = Empty | Btree of'a tree * a * 'a tree let rec depth t = match t with (* arbre vide, ou preuve de P(0) i.e on initialise la récurrence *) | Empty -> 0 (* arbre à deux branches, ou preuve de P(n) => P(n+1) *) | Btree(left, _, right) -> (max_int (depth left) (depth right)) + 1 depth (Btree(Empty, 1, Btree(Empty, 0, Empty))) - : int = 2
      
      Dans ton cas, c'était une récurrence double et à la lecture du code il n'est pas difficile de se convaincre qu'il est correct. Sur des cas plus complexes, cela demande plus de réflexion, mais en fonctionnel cela reste plus simple.
      
      Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
      - [^] # Re: Programmation Dynamique
        
        Posté par Aluminium95 le 13 mai 2016 à 09:57. Évalué à 1.
        
        En effet, on peut même remarquer que si on retire la partie « tableau » (qui sert en fait à faire de la mémoïsation), on se retrouve avec une bête fonction récursive classique. Pour reprendre l'exemple donné :
        
        u u0 0 _ = 1 u u0 j 0 = u0 ! j u u0 j n = if j == nMax then 0 else a * (u u0 (j+1) (n-1)) + b * (u u0 j (n-1)) + c * (u u0 (j-1) (n-1))
        
        Remarque: pour continuer à pouvoir utiliser u0 simplement, on le passe en argument de la fonction.
        
        L'avantage d'utiliser un tableau est en fait celui de la Réification, on ne traite plus une méthode de calcul mais des valeurs. Par exemple si on veut tracer les courbes qui correspondent à la suite pour un n fixé, un nombre énorme de calculs seront refait plusieurs fois, alors qu'en ayant enregistré toutes les étapes intermédiaires, on ne refait jamais deux fois le même calcul, et le tableau se calcule en temps linéaire par rapport à sa taille.
        
        [^] # Re: Programmation Dynamique
        
        Posté par kantien le 26 mai 2016 à 00:18. Évalué à 1. Dernière modification le 26 mai 2016 à 00:19.
        
        L'avantage d'utiliser un tableau est en fait celui de la Réification, on ne traite plus une méthode de calcul mais des valeurs. Par exemple si on veut tracer les courbes qui correspondent à la suite pour un n fixé, un nombre énorme de calculs seront refait plusieurs fois, alors qu'en ayant enregistré toutes les étapes intermédiaires, on ne refait jamais deux fois le même calcul, et le tableau se calcule en temps linéaire par rapport à sa taille.
        
        Oui, c'est une manière comme une autre d'allouer sur le tas (en l'occurrence ici dans une matrice) ce qui autrement resterait dans la pile d'appel à chaque calcul de la fonction, ce qui revient à faire de la mémoïsation.
        
        À l'inverse, dans certain cas, on peut vouloir éviter ce genre d'allocation pour gagner du temps de calcul lorsque l'on n'a pas besoin de réutiliser ultérieurement les données produites (traitement en flux) :
        transformation CPS et réification de la pile d'appel
        éviter les allocations en utilisant le paradigme Continuation Passing Style
        
        Pour le rapport avec la preuve de la correction d'algorithme et la théorie de la démonstration, voir par exemple le livre Categorical semantics of linear logic aux pages 11-13 sur l'élimination des coupures.
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: Programmation Dynamique
        
        Posté par Aluminium95 le 27 mai 2016 à 10:14. Évalué à 1.
        
        Je n'ai pas bien saisi en quoi le livre explique le lien entre le « CPS » et l'élimination des coupures. En fait, il explique « juste » l'élimination des coupures (ce qui est intéressant), mais il faut travailler un peu pour l'appliquer à la programmation. Par exemple, il faut savoir s'il existe un équivalent pour le lambda calcul typé, et si la règle de coupure y est aussi admissible : à ce moment là avec la correspondance de curry-howarrd on arrive à appliquer ce résultat. Ou alors j'ai loupé quelque chose en lisant un peu trop vite.
        
        Du coup, si tu avais un lien vers ce genre de documents je serais ravi !
        
        [^] # Re: Programmation Dynamique
        
        Posté par kantien le 27 mai 2016 à 14:26. Évalué à 1. Dernière modification le 27 mai 2016 à 14:29.
        
        Effectivement, le livre n'explique pas le lien entre CPS et élimination des coupures : celui-ci est plutôt le fruit d'une réflexion personnelle en faisant un raisonnement par analogie via la correspondance de Curry-Howard. Cela étant, c'est plus une réflexion informelle qu'autre chose et il se peut que je pousse l'analogie au-delà de ses limites acceptables (ce n'est pas mon domaine de spécialisation, je ne suis pas informaticien théoricien).
        
        Je vais détailler le schéma de pensée qui m'a amené à cette conclusion. Que dit la règle des coupures en théorie de la démonstration ? Elle généralise le principe du modus ponens : si A alors B, or A donc B. La forme générale de la règle des coupures est donné en bas de la page 11 dans le livre sus-cité : si j'ai deux séquents dans lesquels une même proposition A se trouve dans les prémisses de l'un et dans les conclusions de l'autre, alors je peux produire un séquent dans lequel celle-ci a disparue en fusionnant les prémisses et les conclusions. En haut de la page 12, cette règle est exprimée sous la forme particulière du modus ponens : si j'ai une preuve P1 qui a pour conclusion la proposition A, puis une preuve P2 dont la conclusion est la proposition B et dont A fait partie des prémisses, alors je peux produire une preuve P3 de la proposition B dans laquelle A ne fait plus partie des prémisses. Ensuite, la règle d'élimination des coupures affirme qu'il est également possible de produire une preuve P4 de la proposition B directement sans faire intervenir la preuve P1 qui produit la conclusion A ni la preuve P2 qui produit la proposition B lorsqu'elle a la proposition A dans ses prémisses.
        
        Maintenant passons dans le monde des programmes via la correspondance de Curry-Howard. Cette dernière nous dit que chacune des preuves Pi correspond à un programme et les formules qu'elles manipulent sont les types des objets des programmes. Ainsi la preuve P1 produit un objet de type A qui est consommé par la preuve P2 pour produire un objet de type B ce qui, par coupure, fournit un programme P3 qui produit un objet de type B mais qui dans son exécution (par son recours à P1) doit allouer sur le tas un objet de type A (qui sera à terme désallouer par le ramasse-miette) : le modus ponens est la règle de typage de l'application de fonction :
        
        let app (f:'a->'b) (x:'a):'b = f x;; val app : ('a -> 'b) -> 'a -> 'b = <fun>
        
        Mais, la règle d'élimination des coupures nous dit qu'il est possible d'écrire un programme P4 qui se passe totalement de cette allocation. Prenons maintenant l'exemple donné par Pierre Chambart dans l'article de blog chez OCamlPro pour calculer le minimum et le maximum d'une liste :
        
        let rec fold_left f init l = match l with | [] -> init | h :: t -> let acc = f init h in fold_left f acc t let keep_min_max (min, max) v = let min = if v < min then v else min in let max = if v > max then v else max in min, max let find_min_max l = match l with | [] -> invalid_arg "find_min_max" | h :: t -> fold_left keep_min_max (h, h) t
        
        Les types de ces trois fonctions sont :
        
        val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a = <fun> val keep_min_max : 'a * 'a -> 'a -> 'a * 'a = <fun> val find_min_max : 'a list -> 'a * 'a = <fun>
        
        Icikeep_min_max joue le rôle de la preuve P1 (c'est un lemme qui est responsable d'allocation) et fold_left joue le rôle de la coupure qui produit la preuve P3 à savoir find_min_max. Puis dans la suite de l'article, en transformant son code via CPS, il produit la preuve P4 sans coupure find_min_max_k2 qui se passe d'allocation et qui aura la même fonction que la fonction find_min_max initiale si on lui passe comme continuation la fonction identité fun x -> x.
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: Programmation Dynamique
        
        Posté par Aluminium95 le 28 mai 2016 à 10:44. Évalué à 1.
        
        D'accord, si je comprend bien, passer une continuation c'est éviter de faire la preuve maintenant, et la passer en argument du reste de la preuve pour l'instancier quand on en a besoin (ce qui se passe aux branches des preuves généralement).
        
        Mais j'ai alors un problème, parce que le principe du modus-ponens est tout de même dans le calcul des séquents classique sans coupures : on a une règle (gauche)
        
        G, B |- D G,A |- B,D -------------------------- =>-gauche G, A => B |- D
        
        Ce n'est pas exactement une coupure, mais cela fait bien deux évaluations et donc conserve la nécessité de garder une pile d'appel pour l'évaluation. Par exemple cette règle semble nécessaire pour prouver ((A=>B)=>A)=>(A=>A))

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.