The Coq mailing list

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

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?

-- 
William J. Bowman
Northeastern University
College of Computer and Information Science

Attachment: signature.asc
Description: PGP signature