The Coq mailing list

[Pierre Casteran <casteran AT labri.u-bordeaux.fr>]

Pierre Casteran wrote:
> 
Hello again.
 Perhaps my question took its origin in the Call by Value Languages
evaluations (Scheme, ML), in which "evaluation" means "computing some
term into some value", and this process doesn't compute inside lambda-
abstraction (that's the key of using thunks for delaying evaluations).

 Is Coq's Eval a command for "evaluation" whith this meaning (and i
don't 
understand Coq's answer to my "Eval Cbv" command), or rather
a command for getting normal forms (in this case my question loses its
interest
but the last paragraph of page 110 is hard to understand, and the name
of the
command : "Eval" may be quite confusing (should be "Normalize" better
?).


Best regards

Pierre



> Hello,
> 
>  In the reference manual (V7, p 110) it is said that with the Cbv flag,
> only
> weak reductions are performed (no reductions under a lambda abstraction
> for the
> arguments of a function call).
> 
> Isn't the following dialogue in contradiction with this assertion ?
> 
> Definition nop := [f:nat->nat]f.
> Definition twice := [f:nat->nat ; n : nat](f (f n)).
> Definition plus_3 := [i:nat](S (S (S i))).
> 
> Eval Cbv Beta Delta [plus_3 twice] in (nop [n:nat](twice plus_3 (S n))).
>  = (nop [n:nat](S (S (S (S (S (S (S n))))))))
> 
> Because of the abstraction on n, i expected to get as answer
> the original term unchanged. Perhaps am I missing something ?
> 
> Pierre
> 
> --
> Pierre Casteran,
> LaBRI, Universite Bordeaux-I      |
> 351 Cours de la Liberation        |
> F-33405 TALENCE Cedex             |
> France                            |
> tel : (+ 33) 5 56 84 69 31
> fax : (+ 33) 5 56 84 66 69
> email: Pierre . Casteran @ labri . u-bordeaux . fr  (but whithout white
> space)
> www: http://dept-info.labri.u-bordeaux.fr/~casteran

-- 
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |   
351 Cours de la Liberation        |   
F-33405 TALENCE Cedex             |   
France                            |   
tel : (+ 33) 5 56 84 69 31
fax : (+ 33) 5 56 84 66 69
email: Pierre . Casteran @ labri . u-bordeaux . fr  (but whithout white
space)
www: http://dept-info.labri.u-bordeaux.fr/~casteran