The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

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(match e0 with | p1 => e1 | ... | p_n => e_n end)
 := T(e0) + max { T(e_i) + i | 1 <= i <= n }.
    (* I assume that the (simple) pattern match takes one unit of time or
    reduction step, respectivly. *)

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.
    *)

Lower bounds and space complexity can calculated in a similar way. How can
we handle cofix definitions?
The calculation of space complexity should have an extra branch for tail
recursive functions.

Benjamin Werner (Sun, Feb 20, 2005 at 10:42:42PM +0100):
> Hallo,
> 
> Coq does not provide tools for checking complexity of programs. It 
> should be interesting to see what external complexity checking tools 
> could do with code coming from coq (I thought about doing this with 
> Paul Zimmermann's LUO - lambda epsilon omega but never completed this).

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

> If you want to state internally results about the complexity, this is a 
> little difficult (see the discussion about extentional equality) but 
> not unfeasible (see Constable et. al.' s approach for instance).


> I general, it should be noted that allthough all coq programs 
> terminate, they can take a very very long time; in other words, they 
> cover all practical complexity classes.
> 
> Cheers,
> Benjamin
> 
> Le 20 févr. 05, à 00:34, Stefan Karrmann a écrit :
> >functions which are defined and accepted in Coq terminates. Can the system
> >check space and time upper bounds, i.e. O(f) bounds?
> >
> >Take for example the addition of the Coq 8 library:
> >(** Addition *)
> >
> >Fixpoint plus (n m:nat) {struct n} : nat :=
> >  match n with
> >  | O => m
> >  | S p => S (plus p m)
> >  end.
> >
> >We have:
> >   (plus n m) in time O(n)
> >and:
> >   (plus n m) in space O(n + m)
> >   (* the result has this length *)
> >
> >How can this be checked in or by Coq?

Regards,
-- 
Stefan Karrmann