The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Fri, Dec 16, 2005 at 09:44:05AM -0500, 
roconnor AT theorem.ca
 wrote:
> On Fri, 16 Dec 2005, Lionel Elie Mamane wrote:
>> On Fri, Dec 16, 2005 at 07:38:20AM -0500, 
>> roconnor AT theorem.ca
>>  wrote:

>>> Does anyone know of a nice way of converting a list into a complete
>>> binary tree using structural recursion such that the order is
>>> preserved?

>> Theoretically, here's how I'd do it.

> I didn't follow it entirely,

The key observation is that there are 2*m elements at depth p and the
rest at depth p-1. I'm calling i the position in the list. As a list
of bits (heaviest first) it is the path to the position of that
element for the 2*m first ones and then the position is m, m+1, m+2,
... n. "Path" where 0 = left and 1 = right.

> but it doesn't seem like O(n).  Am I wrong?

No, it is a \theta (n * log(n)).

But with in-place modification of the tree, it can be made O(n):
Instead of restarting each time at the root and following the path
indexed by the bits of "i", one can find the next spot far faster: Go
up in the tree until you had a "0" in the path you just followed and
go right there. A single "insertion" is \theta(log n), but over the
whole algorithm execution, you take every edge in the graph (the tree)
at most twice: Once down and once up.

Hmm... Maybe one can do it even without in-place tree
modification. Yes, I think so. The algo I wrote fills in the tree
left-to-right; I construct the tree to its full depth since the
start, top-down. If you do it bottom-up, you'll get something
O(n). So, instead of constructing the empty skeleton

     /\
    /\ .
   /\ .
  /\ .
 /\ .
.  .

Just to place the first element, construct just

 /\
.  .

and construct its father node only when going up "beyond the root"
(you will go up only one position beyond the root). Then no in-place
modification necessary and still O(n).

Yeah, this should work.


A much more hackish idea is:

let rest = (ref l) in
let get () = match !rest with h :: t -> h;;

and then construct first the left tree, then the right tree
(recursively) just calling "get()" when you get to the leaves to know
what to put there:

let rec aux offset = 
 if length(offset) = p and (List.rev offset) < 2*m
 then Leaf get()
 else if length(offset) = p-1 and (List.rev 0::offset) >= 2*m
 then Leaf get()
 else
  let left  = (aux 0::offset) in
  let right = (aux 1::offset) in
  Node left right

(This can be massaged into something O(n) by passing the length of the
offset around instead of calculating it and not using lists for
offsets but lists where insertion at the end works well and thus
getting rid of the List.rev. Note that confusing numbers and sequences
of bits will work well in Coq: that's what binint does, isn't it?)

Hey, maybe this can even be massaged into something nice:

let rec aux offset = 
 if (length(offset) = p and (List.rev offset) < 2*m) or
    (length(offset) = p-1 and (List.rev 0::offset) >= 2*m)
 then function (h :: t) as l -> Leaf h, t
 else fun l ->
  let left,  l0 = (aux 0::offset l) in
  let right, l1 = (aux 1::offset l0) in
  Node left right, l1

-- 
Lionel