coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frederic Blanqui <frederic.blanqui AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Guard Condition
- Date: Thu, 14 Apr 2011 09:18:57 +0800
Dear Christian,
please find more information about the current Coq termination checker in Bruno Barras presentation on http://coq.inria.fr/adt/egalite-terminaison .
Frederic.
Le 13/04/2011 04:50, Christian Doczkal a écrit :
Dear Georges Gonthier, dear Coq-Club
First of all, thank you for your quick reply. The paper [1], to which I
was referring, defines a syntactic "guarded by destructors" condition
for fix. As far as I can tell, this condition does not handle the case
of div/mod. However, there appears to be an extended version in the form
of an LIP research report that I was unable to obtain.
I found a later paper from Giménez [2], where termination of fix is
ensured by typing conditions. The paper employs guarded types and an
order relation on types. The motivating example in this paper is a
structurally recursive version of div.
Now I'm curious whether Coq uses a type based approach for termination
checking as proposed in [2] or a syntactic condition closer to [1],
extended to cover div/mod. The Coq manual only references [1].
I would be thankful for any clarification.
- [Coq-Club] Guard Condition, Christian Doczkal
- RE: [Coq-Club] Guard Condition,
Georges Gonthier
- Re: [Coq-Club] Guard Condition,
Gert Smolka
- RE: [Coq-Club] Guard Condition, Georges Gonthier
- RE: [Coq-Club] Guard Condition,
Christian Doczkal
- Re: [Coq-Club] Guard Condition, Frederic Blanqui
- Re: [Coq-Club] Guard Condition,
Gert Smolka
- RE: [Coq-Club] Guard Condition,
Georges Gonthier
Archive powered by MhonArc 2.6.16.