The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

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