The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 29/12/2021 22:32, Jason Gross wrote:
> Maybe we can get one of the authors to comment?

Not an author nor a MetaCoq dev, but I share enough office with them to
comment a bit on that.

From what I gather, strong normalization of CIC is a bit overrated. In
practice, it seems that the important proofs (notably decidability of
type-checking and consistency) can be restricted to only depend on
normalization of the "standard" reduction, that is the (weak) head
reduction. Obviously we have to reduce under contexts so variables can
appear everywhere, so weak head really means head reduction a.k.a.
call-by-name.

The Coq examples that violate SN do so for a reduction that is not the
call-by-name one, but instead the call-by-value reduction. One could
(and probably should) argue that CIC is fundamentally call-by-name,
hence trying to normalize a term with the wrong reduction has a little
evil flavour. There is no doubt that there is a bit of bad faith in the
previous statement and we should strive for a SN language, but it's
probably not as bad as it sounds.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature