Discussion :

[SpiceGuid]

J'ai un type tas binaire :

Code OCaml :

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

1
2
3
4
type 'a heap =
	'a non_empty_heap option
and 'a non_empty_heap =
	{left: 'a heap; item: 'a; right: 'a heap}

Et j'ai besoin de ce récurseur où h est un tas binaire et f une fonction bien fondée (qui termine) :

Code OCaml :

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

1
2
3
4
5
6
let rec upsilon f h =
	match h with 
	| {left=None;right=t} | {right=None;left=t} -> 
		t 
	| {left=Some l;right=Some r} ->
		f (upsilon f) l h r

Il y a une certaine ressemblance entre ma fonction upsilon et le récurseur Y.
Toutefois je n'arrive pas à en tirer la conclusion :

• upsilon termine toujours ?
• ou bien la terminaison de upsilon est indécidable ?

edit: comme ça peut paraître un peu abstrait je vous donne du code plus concret

Code OCaml :

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

1
2
3
4
5
6
7
let heap_remove_max h =
	let f k l h r = 				 
		if l.item > r.item then 
			Some{l with right = k {h with left=l.right}} 
		else 
			Some{r with left  = k {h with right=r.left}}
	in upsilon f h

[gasche]

Qu'entends-tu par le fait que `f` termine ? f prend une fonction d'ordre supérieur en paramètre, qu'elle appelle. La terminaison de f est donc liée à celle de ce paramètre : f termine si et seulement si on lui donne une fonction qui termine en paramètre ?

Le problème ici est que `upsilon` appelle `f` et `f` appelle `upsilon`. La terminaison de `upsilon f` dépend de la fonction `f` :
- elle ne termine pas toujours :

Code :

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

upsilon (fun k _l h _r -> k h)

- elle termine toujours si `f` rappelle `upsilon` uniquement sur `l` et `r`, qui sont des sous-termes inductif directs de `h` : c'est un critère simple de terminaison (analogue à celui de Coq sur les inductifs), mais assez limitant en pratique puisque ton exemple d'utilisation n'en fait pas partie

La terminaison pour un f particulier est indécidable :

Code :

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

1
2
3
let f k l h r =
  k (if is_sum_of_two_primes (2 * next_int_to_try ())
     then h else r)

Pour information, j'ai déjà rencontré ce type d'itérateurs, où tu passes à la fonction locale l'itérateur. Par exemple, en ce moment je travaille pas mal sur des graphes, et j'utilise la fonction générale d'itération "dps" suivante (je l'ai un peu nettoyée pour retirer les parties spécifiques à l'application) :

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
exception Cycle of node
let do_nothing _ = ()
let dps ?(acyclic=true) ?(seen=do_nothing) unseen = 
  let visiting = Table.create () in
  let visited = Table.create () in
  let rec visit node = 
      if Table.mem visited node then
        seen node
      else
        if Table.mem visiting node then
          if acyclic then raise (Cycle node) else ()
        else
          begin 
            Table.set visiting node;
            unseen visit node;
            Table.set visited node;
          end in
  visit;;
 
let top_down unseen =
  dps
    (fun visit t ->
       unseen t;
       List.iter visit (edges t))

[SpiceGuid]

(ou du moins je n'ai plus qu'à trouver un autre itérateur qui supporte les rotations)

Pour information, j'ai déjà rencontré ce type d'itérateurs, où tu passes à la fonction locale l'itérateur. Par exemple, en ce moment je travaille pas mal sur des graphes

Pour information mon type arbre binaire tournoi est tiré de La lettre de Caml n°5.

Je vais sans doute aussi travailler sur les graphes, mais implantés à la façon Martin Erwig.

[gasche]

ou du moins je n'ai plus qu'à trouver un autre itérateur qui supporte les rotations

Pas si facile, mais je propose celui là :

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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
 
  type step = [ `Left | `Right ]
  and heap_pointer = step list
  and heap_skeleton = heap_pointer * heap_pointer * heap_pointer
 
  type productive_step = [ `On_left of step | `On_right of step ]
  and non_empty_skeleton = productive_step * heap_skeleton
 
  let normalize_skeleton = function
    | `On_left s, (l, i, r) -> (s::l, i, r)
    | `On_right s, (l, i, r) -> (l, i, s::r)
 
  let productive_skeleton = function
    | (s::l, i, r) -> `On_left s, (l, i, r)
    | (l, i, s::r) -> `On_right s, (l, i, r)
    | ([], _i, []) -> failwith "productive_skeleton"
 
  let fill_skeleton h (l, i, r) =
    let get = function
      | None -> failwith "skeleton points too far"
      | Some h -> h in
    let follow =
      let step h = 
        let h = get h in function
          | `Left -> h.left
          | `Right -> h.right in
      List.fold_left step in
    {left = follow h l;
     item = (get (follow h i)).item;
     right = follow h r}
 
  let rec digamma f h =
    match h with 
      | {left=None; right=t} | {left=t; right=None} -> 
	  t 
      | {left=Some l; right=Some r} ->
          let recur (skel : non_empty_skeleton) =
            digamma f (fill_skeleton (Some h) (normalize_skeleton skel)) in
	  f recur l h.item r
 
  let heap_remove_max h =
    let f k l _i r = 				 
      if l.item > r.item then 
        Some{l with right = k (`On_left `Left, ([`Right], [], [`Right]))}
      else 
        Some{r with left  = k (`On_right `Right, ([`Left], [], [`Left]))}
    in digamma f h

On note les symétries de la fonction, qui sont assez marrantes.

[SpiceGuid]

Alors là, visiblement, tu as fait un gros effort

J'y reviendrai quand j'aborderai le problème de façon plus globale, à savoir comment adapter les paramorphismes aux arbres qui font des rotations.
Pour le moment je vais faire autre chose de plus simple pour me reposer la tête.
De toute façon il va me falloir au moins 6 mois pour comprendre si oui on non tu viens de me donner une solution générale.

[Cacophrene]

Bonjour !

<HS>

De toute façon il va me falloir au moins 6 mois pour comprendre si oui on non tu viens de me donner une solution générale.

Moi c'est le temps qu'il me faudra pour comprendre le thème de ce fil. En tout cas je soupçonne que ce doit être bigrement intéressant.
</HS>

Cordialement,
Cacophrène

[SpiceGuid]

Rappel: Le code est celui d'un tas tournoi (un tas capable de restituer l'ordre d'insertion) tiré de La lettre de Caml n°5 de Laurent Chéno.
Je l'ai juste un peu rafraichi pour éliminer les vilaines exceptions.

Code OCaml :

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
type 'a heap =
   'a non_empty_heap option
and 'a non_empty_heap =
   {left: 'a heap; item: 'a; right: 'a heap}

let rec remove_max h =
   match h with
   | {left=None;right=t} | {right=None;left=t} -> 
      t 
   | {left=Some l;item=x;right=Some r} ->
      if l.item > r.item then
         Some {l with right=remove_max {h with left=l.right} }
      else
         Some {r with left=remove_max {h with right=r.left} }

Ce qui me gêne est surligné en rouge :

• d'abord ça n'est pas optimal en espace, un nouveau noeud est alloué dans le simple but d'être détruit par remove_max.
• ensuite il est particulièrement difficile (je n'ai pas vraiment examiné la proposition de bluestorm, trop compliquée à mon goût) de factoriser la récursion dans ce code car on y perd le critère inductif

Mon idée est plutôt la suivante :

• on recode le remove_max à l'aide d'un merge
• ce merge est un bi-catamorphisme (comme la fusion de deux listes triées)
• on n'a plus de créations de noeuds inutiles

Code OCaml :

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
let rec merge ha hb =
   match ha,hb with
   | None,h | h,None -> 
      h
   | Some a,Some b ->
      Some (
      if a.item > b.item then
      	{a with right = merge a.right hb} 
      else 
      	{b with left = merge ha b.left}) 

let remove_max h =
   merge h.left h.right

edit
La notion de bi-catamorphisme illustrée par la fusion de deux listes triées :

Code OCaml :

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
(* A Bi-Catamorphism example *)

let rec bifold l1 l2 case =
   match l1,l2 with
   | [],_ -> case#nil1 l2
   | _,[] -> case#nil2 l1 
   | h1::t1,h2::t2 ->
         if case#cond h1 h2
         then case#cons1 h1 (bifold t1 l2 case)
         else case#cons2 h2 (bifold l1 t2 case)

let merge l1 l2 =
   bifold l1 l2 (
      object
         method nil1 l2 = l2
         method nil2 l1 = l1
         method cond h1 h2 = h1 < h2 
         method cons1 h t = h::t
         method cons2 h t = h::t
      end )

merge [1;3;6;8;9] [2;4;7];;