coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Making a List into a Tree with Structural Recursion

From: kahl AT cas.mcmaster.ca
To: bruno.barras AT inria.fr
Cc: roconnor AT theorem.ca, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Making a List into a Tree with Structural Recursion
Date: 16 Dec 2005 14:27:30 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

>
> >>Complexity is linear.
> >>
[...]
> I have no idea if this is a classical algorithm or not.

The merge sort in Ralf Hinze's collection of sorting algorithms in Haskell

http://www.informatik.uni-bonn.de/~ralf/software.html#sort

relies on an O(n) tree construction like that,
and may have further references/explanations.

Wolfram

[Coq-Club] Making a List into a Tree with Structural Recursion, roconnor
- Re: [Coq-Club] Making a List into a Tree with Structural Recursion, Lionel Elie Mamane
  - Re: [Coq-Club] Making a List into a Tree with Structural Recursion, roconnor
    - Re: [Coq-Club] Making a List into a Tree with Structural Recursion, Lionel Elie Mamane
- Re: [Coq-Club] Making a List into a Tree with Structural Recursion, roconnor
  - Re: [Coq-Club] Making a List into a Tree with Structural Recursion, roconnor
    - Re: [Coq-Club] Making a List into a Tree with Structural Recursion, Bruno Barras
      - Re: [Coq-Club] Making a List into a Tree with Structural Recursion, roconnor
        
        Re: [Coq-Club] Making a List into a Tree with Structural Recursion, Bruno Barras
        
        Re: [Coq-Club] Making a List into a Tree with Structural Recursion, kahl
    - Re: [Coq-Club] Making a List into a Tree with Structural Recursion, Thery Laurent
      - Re: [Coq-Club] Making a List into a Tree with Structural Recursion, roconnor