The Coq mailing list

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

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