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