Upsilon, termine (ou pas) ?

**SpiceGuid** · 16/04/2010, 22h26

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** · 17/04/2010, 07h11

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** · 17/04/2010, 16h18

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

Envoyé par bluestorm

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** · 17/04/2010, 21h14

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** · 18/04/2010, 17h41

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.