The Coq mailing list

["William J. Bowman" <wjb AT williamjbowman.com>]

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

Attachment: signature.asc
Description: PGP signature