The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

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