coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benjamin Werner <benjamin.werner AT polytechnique.fr>
- To: sk AT mathematik.uni-ulm.de
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Check time and space consumption
- Date: Sun, 20 Feb 2005 22:42:42 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] Check time and space consumption, Stefan Karrmann
- Re: [Coq-Club] Check time and space consumption, Benjamin Werner
- Re: [Coq-Club] Check time and space consumption,
Stefan Karrmann
- Re: [Coq-Club] Check time and space consumption, Benjamin Werner
- Re: [Coq-Club] Check time and space consumption,
Stefan Karrmann
- Re: [Coq-Club] Check time and space consumption, Benjamin Werner
Archive powered by MhonArc 2.6.16.