The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

<mailinglists AT robbertkrebbers.nl>
 wrote:
> On 01/13/2016 03:44 PM, Matthieu Sozeau wrote:
>>
>> You are right that the cbv strategy is doing normalization under
>> binders though, not weak reduction as advertised.
>
> Thanks for clarifying. But is this a bug or intended behavior?

The reference manual is correct but probably not phrased in a
non-ambiguous and extensive enough way.

  "the arguments of a function call are evaluated first, using a weak
   reduction (no reduction under the λ-abstractions)"

The arguments are indeed evaluated first without reduction under the
binders, i.e. using only weak-head reduction.

What is missing is that the initial term, which is not necessarily
closed, once a weak-head normal form is obtained using a roughly
standard weak-head cbv reduction strategy, i.e. once a value or a
neutral term E[x] with E an evaluation context is obtained, then the
reduction recursively continues under the binders of the value or
under the binders of the terms occurring in E, respectively.

Note that Coq's cbv is not compatible with cbv semantics in
Plotkin-Moggi's sense in the sense that it has the rule

(λx:T.t) E[y] → t[x:=E[y]]

where the neutral term E[y] is not a value, and this rule is an
instance of (call-by-name) β which is not an instance of Plotkin's
β_v.

So, the correct formulation of Coq's cbv should be "a call-by-value
strategy of reduction for call-by-name normalization".

Best,

Hugo

PS: Thomas Sibut-Pinote started to write a "print" function in
Coq. It could help to visualize what cbv is doing exactly.