coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Stefan Karrmann <sk AT mathematik.uni-ulm.de>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Check time and space consumption
- Date: Sun, 20 Feb 2005 00:34:41 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [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.