Re: [isabelle] nat_code Equation



Just for the fun, a simple test:

fun nat' :: "int ⇒ nat ⇒ nat" where
  "nat' k accu = (if k ≤ 0 then accu else nat' (k - 1) (Suc accu))"

fun nat_th :: "int ⇒ nat" where
  "nat_th k = (if k ≤ 0 then 0 else Suc (nat_th (k - 1)))"

ML {*
  val y : IntInf.int = 70000000;

  (* Tail-recursive approach *)
  val t = Time.now ();
  val _ = @{code nat'} y (@{code nat} 0);
  val nat_tail = Time.- (Time.now (), t);

  (* René Thiemann's approach *)
  val t = Time.now ();
  val _ = @{code nat_th} y;
  val nat_th = Time.- (Time.now() , t);

  (* approach from Code_Integer *)
  val t = Time.now ();
  val _ = @{code nat} y;
  val nat = Time.- (Time.now(), t);
*}
Results:

val nat_tail = 9.403: Time.time
val nat_th = 28.333: Time.time
val nat = 9.594: Time.time

Here the difference between nat_tail and nat is neglegible. When running
the above multiple times, sometimes 'nat_tail' is a little better, other
times 'nat' is.

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.