The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello Bas,

It is indeed folklore that the current guard condition of Coq breaks SN.
However, Coq's implementation (if no bugs) should be weakly normalizing,
which is usually enough for consistency.

It is not easy to design a syntactic guard condition that is flexible
enough in practice and preserves SN. Here again, a termination criterion
based on types could help.

Maxime.

On 02/28/16 19:15, Bas Spitters wrote:
> Is Coq strongly normalizing?
> 
> 
> The *implementation* of Coq is (or was) not SN. The issue is recorded
> here, I believe.
> https://coq.inria.fr/cocorico/CoqTerminationDiscussion
> 
> I am not sure whether this has been fully fixed yet.
> 
> 
> The Coq manual is incomplete, as it refers to Coquand's work on CoC
> for the SN proof of CIC, which can't be strictly right.
> https://coq.inria.fr/refman/Reference-Manual006.html
> I haven't chased the references yet, but this paper claims the result for 
> CIC:
> https://www.cs.rice.edu/research/technical-reports/TR11-01/
> 
> Does this seem correct? It would be probably be good to document this
> properly (in the FAQ, ref manual?).
> 
> Bas
>