Discussion :

[gasche]

Salut,

résumé : pour des besoins personnels, j'ai changé du code dans la bibliothèque standard Map. Comme je connais mal l'algorithmique de cette structure de donnée (des arbres de données équilibrés), et que je sais que certains d'entre vous sont très au courant, je viens vous raconter ma vie, montrer du code, et je voudrais votre avis.


Dans le contexte du projet Batteries, je travaille en ce moment sur une factorisation des modules Map.Make (Map fonctorielles) et PMap (map polymorphiques).

Les fonctions de ces modules utilisent deux informations, la fonction de comparaison et l'arbre (la structure de donnée sous-jacente). Map a la fonction de comparaison comme constante, et accède directement à l'arbre, et PMap prend en argument un record contenant un champ pour l'arbre et un champ pour la fonction et, bien sûr, renvoie des valeurs de la même forme.

Pour factoriser, je regroupe les implémentations des fonctions dans un module concret qui prend et renvoie directement l'arbre, mais aussi, quand c'est nécessaire, la fonction de comparaison. Ensuite j'ai deux "écorces", une pour Map.Make et une pour PMap, qui passent les paramètres qu'il faut, construise et déconstruisent les données qu'il faut.

L'état actuel du module :
http://github.com/gasche/batteries-i.../src/batMap.ml

L'intérêt est qu'il est ensuite facile de s'assurer que Map et PMap proposent les mêmes fonctionnalités, et de transmettre à l'un les améliorations de l'autre. J'espère aussi me débarasser du hack "on révèle l'implémentation des Map stdlib en cassant le typage" utilisé jusqu'à présent pour ajouter des fonctions au module Map.Make (issu de la bibliothèque standard).

Dans le module Concrete, certaines fonctions ont besoin de l'opération de comparaison, typiquement la fonction "find", et d'autres n'en ont pas besoin, typiquement la fonction "iter". On pourrait croire que c'est arbitraire, mais il y a en fait une logique interne claire à cette distinction : si la fonction a besoin de trouver un chemin dans l'abre en fonction d'une clé, il lui faut comparer, sinon elle ne devrait pas en avoir besoin. iter ne cherche aucune clé en particulier, elle itère sur toutes les clés. De même, min_binding qui renvoie la plus petite clé n'en a pas besoin, il lui suffit de descendre tout à gauche dans l'arbre.

Dans le but de porter la fonction "split" ajoutée dans le module standard Map depuis la 3.12, je m'intéresse à la fonction auxiliaire "join" qu'elle utilise. Dans map.ml (de la distribution OCaml) :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
    (* Same as create and bal, but no assumptions are made on the
       relative heights of l and r. *)
    let rec join l v d r =
      match (l, r) with
        (Empty, _) -> add v d r
      | (_, Empty) -> add v d l
      | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
          if lh > rh + 2 then bal ll lv ld (join lr v d r) else
          if rh > lh + 2 then bal (join l v d rl) rv rd rr else
          create l v d r

Join sert à réunir une branche gauche, une branche droite, et au milieu une clé et une valeur, mais dans un cas où on ne sait pas si les deux branches sont déséquilibrées. Si c'est le cas, il faut ré-équilibrer l'arbre en utilisant l'opération `bal`.

Mon soucis avec cette implémentation est qu'elle utilise, dans le cas où l'une des branches est vide, la fonction `add`. C'est la fonction générique d'ajout d'un élément dans l'arbre, et elle demande (dans mon implémentation) la fonction de comparaison. Si je reprends cette implémentation, je dois donc demander pour `join` une fonction de comparaison :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
  let rec join cmp l v d r =
    match (l, r) with
        (Empty, _) -> add v d cmp r
      | (_, Empty) -> add v d cmp l
      | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
          if lh > rh + 2 then bal ll lv ld (join cmp lr v d r) else
          if rh > lh + 2 then bal (join cmp l v d rl) rv rd rr else
          create l v d r

Ce n'est pas très grave mais ça casse la séparation globale "besoin de cmp ou pas ?". join utilise cmp alors qu'elle n'a besoin de trouver la position d'aucun élément en particulier. En effet, on sait en fait que la clé `v` est plus petite que toutes les clés de la branche droite, et plus grande que toutes celles de la branche gauche. Il suffirait donc d'écrire :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
 
  (* beware : those two functions assume that the added k is *strictly*
     smaller (or bigger) than all the present keys in the tree; it
     does not test for equality with the current min (or max) key.
     
     Indeed, they are only used during the "join" operation which
     respects this precondition.
  *)
  let rec add_min_binding k v = function
    | Empty -> singleton k v
    | Node (l, x, d, r, h) ->
      bal (add_min_binding k v l) x d r
 
  let rec add_max_binding k v = function
    | Empty -> singleton k v
    | Node (l, x, d, r, h) ->
      bal l x d (add_max_binding k v r)
 
  (* Same as create and bal, but no assumptions are made on the
     relative heights of l and r. *)
  let rec join l v d r =
    match (l, r) with
        (Empty, _) -> add_min_binding v d r
      | (_, Empty) -> add_max_binding v d l
      | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) ->
          if lh > rh + 2 then bal ll lv ld (join lr v d r) else
          if rh > lh + 2 then bal (join l v d rl) rv rd rr else
          create l v d r

Qu'en pensez-vous ? Est-ce que le code vous paraît correct ?

PS : il y aurait un énorme hack qui marcherait dans mon cas, qui serait de garder les appels à add en leur passant une "fausse" fonction de comparaison, qui vaudrait toujours 1 ou toujours -1 selon que l'on veut ajouter le minimum ou le maximum. Mais c'est moche, c'est fragile et je ne l'aime pas.

PPS : si l'implémentation vous semble conclusive, je l'enverrai peut-être sur le bug-tracker Caml, parce que comme la fonction de comparaison est user-defined et potentiellement coûteuse ça pourrait les intéresser d'avoir une implémentation qui en minimise les appels.

[Cacophrene]

Bonjour bluestorm,

Si j'ai bien suivi, la fonction join est ennuyeuse parce qu'elle est dans une situation intermédiaire (floue) entre les deux affirmations "je n'ai pas besoin de cmp" et "j'ai besoin de cmp", toutes deux dictées par la nature des opérations effectuées (tu as donné l'exemple de find versus iter). Comme je n'ai pas les connaissances suffisantes pour te donner une réponse algorithmique, je vais te donner une réponse pragmatique.

J'imagine que, vu de l'extérieur, le type map reste abstrait. Cela veut dire que tes fonctions sont les seules à savoir ce qui se raconte en coulisses. Partant de là, tu peux très bien exploiter localement une propriété non généralisable si, évidemment, elle est vraie dans le contexte où tu l'appliques, et à plus forte raison et si elle facilite la maintenabilité du code, sa symétrie, son efficacité, ou toutes ces choses (et d'autres) à la fois (et tu fais bien de le signaler par un commentaire).

Cordialement,

PS : je n'aime pas non plus le hack dont tu parles, je vois ça comme une solution détournée pour éviter de choisir entre "j'ai besoin de cmp" et "je peux affirmer ceci". Au final ça revient quand même à utiliser une fonction de comparaison, ça fait perdre du temps pour rien, et on ne va pas au bout de la démarche.

[SpiceGuid]

Le code de join que tu cites est extrait de stdlib, celui de OCaml-Reins est à peu près identique.
join est un smart-constructor, il fabrique un nouveau noeud, il n'a pas besoin de la fonction cmp qui sert aux accesseurs pour une position ou un intervalle.

Comme tu l'as justement deviné, les accesseurs min_binding et max_binding suggèrent les deux constructeurs add_min_binding et add_max_binding dont join a besoin.
Il est tout à fait normal qu'en factorisant tu sois obligé d'améliorer le code existant.

Indeed, they are only used during the "join" operation which
respects this precondition.

Personnellement je dis qu'une précondition est required tandis qu'une postcondition ou un invariant sont respected

Si tu veux un filter rapide tu auras également besoin du constructeur concat.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
  let concat ta tb =
    match ta,tb with
    | None,t | t,None -> t
    | _,Some b ->
        let m,t = delete_min b in
        Some (join ta m t)

  let rec filter f = function
    | None -> None
    | Some n ->
        if f n.item then
          Some (join (filter f n.left) n (filter f n.right))
        else        
          concat (filter f n.left) (filter f n.right)

[gasche]

Tu es l'auteur de Ocaml-Reins ? Je n'avais jamais fait le rapprochement (ou alors oublié). Je vais voir de temps en temps cette bibliothèque, mais j'ai effectivement oublié de la consulter dans ce cas.

Personnellement je dis qu'une précondition est required tandis qu'une postcondition ou un invariant sont respected.

Oui, mais là je parle de la fonction appelante, donc le contexte est justement inversé : elle "respecte" la précondition dans le sens où dans son contexte, la préconditie est remplie. De même, si elle utilisait le résultat d'une fonction en supposant des invariants sur ces résultats, on pourrait dire qu'elle "requiert" une postcondition. Mais dans ce cadre, "fulfills" serait peut-être plus adapté.

Je dois dire que j'ai été un peu impatient, et que j'ai finalement posté une "issue" sur le bugtracker Caml avant d'avoir un avis définitif ici. M'enfin, le fait que tu ne soies pas tombé de ton siège en lisant mon code m'assure que je n'ai pas fait de bourde énorme.

[SpiceGuid]

Je ne suis pas l'auteur de OCaml-Reins.

Par contre je suis bien l'auteur de OCaml-Idaho (qui est classé très loin derrière Macaque).

le fait que tu ne soies pas tombé de ton siège en lisant mon code m'assure que je n'ai pas fait de bourde énorme.

Merci de ta confiance, c'est toujours bon pour le moral

[TropMDR]

Bah pour être sûr, il ne te reste plus qu'à modifier http://coq.inria.fr/coq/stdlib/Coq.FSets.FMapAVL.html :-D

[gasche]

Je n'ai pas encore un niveau en Coq suffisant pour être à l'aise avec le code de la bibliothèque standard, qui contient des choses nettement plus avancées que le simple intro/induction/apply.

Ceci dit, ta suggestion me semble une très bonne idée dans l'absolu (pouvoir vérifier formellement l'absence de bug, c'est une bénédiction; si on pouvait faire comme ça partout...), et n'est pas si irréaliste puisque alex_pi s'en est chargé.

[TropMDR]

Je n'ai pas encore un niveau en Coq suffisant pour être à l'aise avec le code de la bibliothèque standard, qui contient des choses nettement plus avancées que le simple intro/induction/apply.

Si jamais tu veux t'y mettre, je te conseille très fortement Software Foundations de Pierce. C'est excellent.

Ceci dit, ta suggestion me semble une très bonne idée dans l'absolu (pouvoir vérifier formellement l'absence de bug, c'est une bénédiction; si on pouvait faire comme ça partout...), et n'est pas si irréaliste puisque alex_pi s'en est chargé.