The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

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?