The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

For a fix, can I ask Coq to give me the version of its body for which the guard conditions were checked?

Is it the same as doing "Eval compute in (fix ...)"?

I understand that this version may be excessively bloated (beyond the limits of human understanding) due to all the unfoldings.

Instead of blindly normalizing the body of a fixpoint, can Coq proceed lazily, only normalizing subterms of the body where the guard condition fails?

Suppose that Coq stored only the versions (of bodies of fix) on which guard checks were done, and discarded whatever the user wrote.

Would Coq then be strongly normalizing?

Another useful meta-theoretic property of interest is that all typing judgments are closed under definitional equality.

Thus, it seems that Coq's kernel (not what user writes) cannot accept 

"fix F (n : nat) := 0" and reject "fix F (n : nat) := let x := F n in 0", as long as reductions are allowed inside bodies of fixpoints.

Do we also need to ban reductions inside bodies of fixpoints?

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Mon, Dec 12, 2016 at 4:56 PM, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

My understanding of what happens is that it breaks *strong*
normalization, in the sense that there exist reduction strategies that
loop, but it preserves *weak* normalization, namely the fact that
there exists a reduction path to a value -- and thus consistency.
Indeed, in the checking rule

Gamma, F : T |- M : T
M -beta*-> M'
M' \in Guard^F_k
-------------------------
Gamma |- (Fix F_k : T := M) : T

there *exists* a reduction path M -> M', and my understanding is that
reusing this specific reduction path each time you unfold the fixpoint
is a normalizing strategy.

Indeed in this specific example we have:

Coq < Fixpoint F (n : nat) := let x := F n in 0.
F is defined
F is recursively defined (decreasing on 1st argument)

Coq < Eval cbv in (F 1).
Stack overflow.

Coq < Eval cbn in (F 1).
     = 0
     : nat

On Mon, Dec 12, 2016 at 4:48 PM, William J. Bowman
<wjb AT williamjbowman.com> wrote:
> On Mon, Dec 12, 2016 at 04:44:05PM -0500, roux cody wrote:
>> I think the idea is that while this can lead to non-termination during the
>> checking of the guard condition, if this succeeds then the resulting
>> program is well-guarded,
> Is the example program non-terminating at run-time or when checking the guard condition? To me, it
> seems it would terminate when checking the guard condition, but fail to terminate at run-time.
> For reference, the example I'm referring to is:
>   Fixpoint F n := let x = (F n) in 0.
>
> Since let x = (F n) in 0 reduces to 0, and 0 is well-guarded, so is the Fixpoint (according to the
> algorithm described in the slides). But F will not terminate at run-time.
>
> I agree that it is less concerning since I cannot see how it would allow deriving contradiction.
>
> --
> William J. Bowman