The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.fr>]

Hi,

> Hello!
>
> AFAIKS it is not difficult to calculate an upper bound O(f) for the 
> time
> complexity from Coq's function definitions. It is a kind of counting
> reduction steps. It is roughly done by T as follows:
...
> T(fix f (args) { struct s } := e)
>  := T(e with recursive calls of f replaced by a constant) * depth(s).
>  (* where depth(s) counts the `inductive depth of s', e.g.
>     forall n:nat, depth(n) := n.
>     forall t:binary_tree A, depth(t) := binary_tree_depth(t)
>
>     Note, that s becomes an argument to the complexity function.
>     *)
> >
Are you sure you do not make some implicit linearity assumptions ?
Would your idea apply to Ackermann's function ?

Also (but this is a minor point)  it would not work for inductive types 
which are not datatypes because you cannot define a finite depth then. 
Take :

Inductive ord : Set :=
OO : ord
| SO : ord -> ord
| lim : (nat->ord) -> ord.

> Where can I find Paul Zimmermann's LUO? Well, I will try Google.

I would not know a better pointer :-). He is at LORIA (INRIA-Nancy) 
now. But since his PhD was in Rocquencourt, you can look at

http://algo.inria.fr/libraries/software.html#luo

(I did not check further recently).

Cheers,


Benjamin