The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Cedric,

 

the docs for vm_compute state that it uses “call by value” semantics. Isn’t this equivalent to eager?

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Cedric Auger
Sent: Monday, November 02, 2015 2:27 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Time analysis

 

Keep in mind, also that Coq semantics does not take into account whether evaluation is lazy or eager.

If you want to extract code to Haskell or OCaml, execution time behaviour can largely differ.

 

2015-11-02 9:14 GMT+01:00 Tillmann Weisser <tweisser AT laas.fr>:

Dear Coq-Club,

I want to do a time analysis of a function in my code. However, I don't really know how to do this. Here is my problem:

Given 3 types A, B and C and converting functions g: A -> B and h: B -> C. I want to analyse the function f:= h o g.  In particular I'm interested in the question which part of f (i.e. g or h)  takes most of the time.

Let now a be of type A. I ran the commands

Time Eval vm_compute in (f a).
Time Eval vm_compute in (g a).
Let b:= Eval vm_compute in (g a).
Time Eval vm_compute in (h b).

However, the evaluation of (h b) is as slow as the evaluation of (f a), whereas the evaluation of (g a) is a little bit faster than the others. (The times of (g a) and (h b) do not sum up to the time of (f a).) What can I conclude from that? Is there a better way to analyse f?

Thanks for your help in advance!
 Tillmann

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928