The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

On 12 February 2014 00:57, Greg Morrisett <greg AT eecs.harvard.edu> wrote:

On Feb 11, 2014, at 6:54 PM, Mitchell Wand <wand AT ccs.neu.edu> wrote:

> Is this a CBN vs. CBV issue?

Yes.  I'd argue that if termination checking is allowing for:

  Fixpoint f (x:nat) : nat := let z := f(x) in 0

then the language isn't confluent,

Well, this is quite unlikely to compromise confluence (hell, deactivating termination checking altogether shouldn't compromise confluence). So I don't think this is a problem. But remember: it's really a bug. If the termination checking of Coq changes for something more flexible/robust like sized types, someday, this term will be rejected. And so, you should reject it as well (with the power of you miiiiiind!), and not be too bothered about it.

 

and so it's easy to run into
problems when reduction is done one way, and extraction + evaluation
is done another.

But I suspect Pierre was smart enough to cover the bases here
and it's not really a problem.  I was just hoping someone knew
what, exactly, is going on.

Actually, extraction has a bunch of optimisations (mostly a bit of partial evaluation plus some commutative cuts, if I remember correctly). It's certainly not trivial that the extracted code does the same thing as the Coq code, but surely, this is still easier than understanding why you can erase proof of acc which are the structural argument of a fixed point.