The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

roconnor AT theorem.ca
 wrote:

> On Fri, 16 Dec 2005, Bruno Barras wrote:
>
>  
>
> > What about this ?
> >    
>
>  
>
> > Complexity is linear.
> >    
>
> What a promising solution.  I wasn't even close to thinking of anything
> like this.  How did you come up with it?
>
>  
I first tried something like in Laurent's post, but by merging 
neighbours pairwise to avoid computing the log of the length. The 
problem was that for lists of size 2^n+1, the last element would not 
grow before the last step, because the last always remains the last. So 
I imagined that the last element should always be merged with its 
neighbour. This was good since the element that is not merged would 
change at every step, thus avoiding the depth gap to increase.
Not a formal reasoning but it was enough to guide me towards a solution...
Indeed, it seems the elements at depth n+1 are all on the rightmost 
branches, so if you want the most constrained solution, just mirror the 
input list and the output tree. But I'm not yet sure of that.

I have no idea if this is a classical algorithm or not.

Bruno.