The Coq mailing list

[Mitchell Wand <wand AT ccs.neu.edu>]

Is this a CBN vs. CBV issue?

On Tue, Feb 11, 2014 at 6:50 PM, Greg Morrisett <greg AT eecs.harvard.edu> wrote:

I guess I'm just worried that the termination checking may
do one thing, and the extraction another, and this could
result in some OCaml term that diverges.

-Greg

On Feb 11, 2014, at 10:30 AM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

> Greg,
>
> There are some optimizations in extraction plugin, which work on intermediate "MiniML" AST inside plugin. But I don't remember do these optimizations normalize terms or just scan let body for occurence of let variables.
>
> Sincerely,
> Kirill Taran
>
>
> On Mon, Feb 10, 2014 at 10:29 PM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:
> On 10/02/2014 19:16, Greg Morrisett wrote:
> I'm curious about the interaction of this feature with extraction.
> In the example you gave:
>
> Fixpoint f (x:nat) : nat := let y := f x in 0.
>
> extraction to Ocaml yields:
>
>    let rec f x = 0
>
> This suggests that the body of a recursive function is
> normalized before extraction.  But this example:
>
>    Fixpoint g (x:nat) : nat :=
>      let z1 := x * x in
>      let z2 := z1 * z1 in
>      let z3 := z2 * z2 in
>      let z4 := g z3 * g z3 in
>      z3 * z3.
>
> yields the following Ocaml:
>
>    let rec g x =
>      let z1 = mult x x in
>      let z2 = mult z1 z1 in
>      let z3 = mult z2 z2 in
>      mult z3 z3
>
> so obviously, something more clever is happening.
>
> I don't see any difference between your two examples: in both cases, unused let-bindings seem to be removed from the extracted code. Am I missing something?
>
> Best regards,
>
> Guillaume
>