The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Try

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

Eval compute in f 0.

(it doesn't actually loop with [let '_ := …] but that's a technicality)

It would be a dreadful idea to store the normal form in the kernel, anyway. The performance would be ruined.

And to answer Kirill's question: syntactical subterm checking is very restrictive. Therefore, Coq tries to relax it by doing some reduction. Since the body of a fix is normalising, we can reduce it and check subterm checking on the normal form of the body instead. That way, we can use auxiliary functions that effectively builds subterms in a fixed point definition (it happens often). The problem of this strategy is that some ill-formed calls can disappear like in this example.


Arnaud

On 10 February 2014 15:28, Matthieu Sozeau <matthieu.sozeau AT gmail.com> wrote:

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
>
>
>
>