The Coq mailing list

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

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

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 :

> Hello,
>
> 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
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club