Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Check time and space consumption

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Check time and space consumption


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page