The Coq mailing list

["William J. Bowman" <wjb AT williamjbowman.com>]

On Mon, Dec 12, 2016 at 04:56:46PM -0500, Gabriel Scherer 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.
Ah, of course. Thanks!

--
William J. Bowman

Attachment: signature.asc
Description: PGP signature