The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

I think the idea is that while this can lead to non-termination during the checking of the guard condition, if this succeeds then the resulting program is well-guarded, and so can not be used to derive a contradiction, which is the real point of the whole thing.

Potential non-termination on it's own is certainly not fun, but the increased convenience of the relaxed guard condition seems to be a good trade off. The real deal breaker is inconsistency, and AFAIK this non-termination does not allow it.

Best,

Cody

On Mon, Dec 12, 2016 at 4:33 PM, William J. Bowman <wjb AT williamjbowman.com> wrote:

The first reference shows the typing rule for fix that reduces the body of the recursive function before applying the guard condition. This has a similar effect to using convertibility in the guard condition, at least for the uses I had in mind.

However, it also points out that this breaks strong normalization. In fact, the example seems to cause a stack overflow when I run it in Coq, and would infinitely loop otherwise.

Why is this not considered a problem for Coq?

--
William J. Bowman

On Mon, Dec 12, 2016 at 02:36:15PM -0500, William J. Bowman wrote:
> Frédéric,
>
> Thank you for these references! I'll take a look and see if they resolve my issue.
>
> Do you (or others) know why the "official reference" in the Coq manual is so outdated?
>
> --
> William J. Bowman
>
> On Fri, Dec 09, 2016 at 09:33:10AM +0100, Frédéric Blanqui wrote:
> > Hello William.
> >
> > For more recent descriptions of the Coq termination checker, have a look at:
> >
> > - http://coq.inria.fr/files/adt-2fev10-barras.pdf
> >
> > - http://hal.archives-ouvertes.fr/hal-00651780
> >
> > - https://tel.archives-ouvertes.fr/tel-01054723/
> >
> > To which extent this is an accurate description of what is actually
> > currently implemented, I have no idea.
> >
> > Best regards,
> >
> > Frédéric.
> >
> > Le 12/08/2016 à 11:54 PM, William J. Bowman a écrit :
> > >I have been studying CIC and am trying to understand the termination checker for recursive functions,
> > >but am confused about whether certain equalities are syntactic equality or convertibility.
> > >
> > >I have read "Codifying guarded definitions with recursive schemes" by E. Giménez, and transliterated
> > >the definitions from that work into Figure 1 in the following PDF:
> > >   https://williamjbowman.com/downloads/guard-q.pdf
> > >At the top of Figure 1, the judgment "fix f:t.e terminates" holds when, among other things, t = Π (x : (D e' ...)). t'.
> > >That is, when e defines a function whose first argument inhabits an inductively defined type.
> > > From my reading of the aforementioned paper, I believe that this = means syntactic equality.
> > >However, the following line from Chapter 4 of the Coq manual leads me to believe = should mean
> > >convertible (or perhaps reducible-to):
> > >   "Each Ai should be a type (reducible to a term) starting with at least ki products ∀ y1:B1,… ∀ yki:Bki, A′i and Bki an is unductive [sic] type."
> > >
> > >There are several other cases where = is used and I'm not sure if it should mean syntactic equality or
> > >convertibility---cases I have labeled [Guard-AppRec] and [Guard-CaseSmaller] in Figure 1.
> > >In [Guard-AppRec], we know an application of the recursive function (f e) is valid if e = y e' ...,
> > >where y is a syntactically smaller variable guarded by a constructor.
> > >Again I wonder if this should be e ≡ y e' ..., i.e, e is convertible, not just not merely
> > >syntactically equal to, an application of a syntactically smaller variable etc.
> > >In [Guard-CaseSmaller], we have similar restrictions on the structure of the branches for the case
> > >analysis.
> > >
> > >In Figure 2, I define the guard condition using convertibility instead of syntactic equality in places
> > >I believe (hope) should be valid.
> > >
> > >Can anyone advise me on the correct definition of the guard condition?
> > >
> >