Skip to Content.
Sympa Menu

coq-club - Re: Reduction strategies

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Reduction strategies


chronological Thread 
  • From: Pierre Casteran <casteran AT labri.u-bordeaux.fr>
  • To: coq-club AT inria.fr, casteran AT labri.u-bordeaux.fr
  • Subject: Re: Reduction strategies
  • Date: Fri, 29 Jun 2001 08:30:33 +0200
  • Organization: LaBRI

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





Archive powered by MhonArc 2.6.16.

Top of Page