Re: [isabelle] nat_code Equation



Note that if you import HOL/Library/Code_Nat.thy, which declares a
binary code representation for type nat, then the implementation of
function nat from Code_Integer is *much* faster than either nat' or
nat_th.

- Brian

On Fri, Nov 30, 2012 at 7:51 AM, René Neumann <rene.neumann at in.tum.de> wrote:
> 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
>





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