The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi all,

  Termination is checked on a beta-let-hnf of the term (BTW, we don’t know it 
is normalizing yet…), 
and the term in the kernel is this hnf (right?). So we’re not loosing SN in 
the kernel actually, 
even though it looks like only cbn reduction is strongly normalizing due to 
this “feature” if 
I’m not mistaken. For example: 

For

Fixpoint f (x:nat) : nat := let '_ := f x in 0.

and

Fixpoint f (x:nat) : nat := match f x with _ => 0 end.

the hnf of the elaborated term is 0. While

Fixpoint f (x:nat) : nat := match f x with 0 => 0 | S n => 0 end.

is not accepted as the match is kept by the elaboration.

Best,
— Matthieu
        
On 10 févr. 2014, at 14:16, Kirill Taran 
<kirill.t256 AT gmail.com>
 wrote:

> Arnaud, Frederic,
> 
> Thanks for elaborations.
> 
> > Fixpoint f (x:nat) : nat := let '_ := f x in 0.
> Why it is allowed? Doesn't argument have to decrease on recursive call?
> 
> Sincerely,
> Kirill Taran
> 
> 
> On Mon, Feb 10, 2014 at 2:45 PM, Arnaud Spiwack 
> <aspiwack AT lix.polytechnique.fr>
>  wrote:
> To elaborate on Frédéric's answer, termination is a technique to prove 
> consistency. It goes like that:
>       • If there is a closed proof of ⊥, then we can find a closed proof of 
> ⊥ in normal form
>       • Closed normal-form proofs start with an introduction rule
>       • ⊥ has no introduction rule
> Note that we only need weak normalisation. In fact, we can settle with 
> something weaker (like a semantic proof of cut elimination, which doesn't 
> imply the existence of a set of terminating rewriting rules, I believe 
> Olivier Hermant's PhD thesis was on the subject of such proofs). Strong 
> normalisation, whereby every rewriting strategy terminates, is a much 
> stronger result (at least in principle as there is a conjecture, originally 
> by Klop I believe, that every weakly normalising PTS is strongly 
> normalising, there are some thoughts on this conjecture in Denis 
> Cousineau's PhD thesis). Proof theorists tend to favour strong 
> normalisation result over consistency.
> 
> This is what makes the fact that Coq accepts the following definition
> 
> Fixpoint f (x:nat) : nat := let '_ := f x in 0.
> 
> a (long standing) minor bug: it makes Coq only weakly normalising (which is 
> a bug), but it doesn't threaten consistency (which prevents it from being a 
> serious bug).
> 
> 
> 
> On 10 February 2014 10:34, Frédéric Blanqui 
> <frederic.blanqui AT inria.fr>
>  wrote:
> Hi.
> 
> I would answer that it depends. Guillaume provides an example of looping 
> function in False. Then, of course, you can build a proof of False. But 
> what if f is in nat? Then problems may arise if you can prove that 0=1. 
> Define for instance f by  f x = S (f x). So, I am not sure that 
> non-termination always leads to inconsistency, especially if you restrict 
> type dependencies to terminating terms (but it is not decidable...). See 
> for instance the works of Constable et al on partial functions in 
> constructive type theory, and the NuPRL proof assistant.
> 
> Best regards,
> 
> Frédéric.
> 
> Le 08/02/2014 12:19, Guillaume Melquiond a écrit :
> 
> On 08/02/2014 12:05, Kirill Taran wrote:
> 
> Is it true that if we had possibility to write non-terminating programs
> (suppose we don't use non-terminating term in types, so type check
> terminates) then we would have possibility to prove everything?
> 
> Fixpoint f (x : unit) : False := f x.
> Goal False. exact (f tt). Qed.
> 
> Best regards,
> 
> Guillaume
> 
> 
> 
>