The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

 Hi Pierre,

thanks for pointing me to the trees with functional fields.
This provides me with a shorter example for my problem:

Inductive tree := L : tree | N : (nat -> tree) -> tree.
Fixpoint depth t n := match t with L => 0 | N f => depth (f n) n end.

While my intuition tells me that this recursion terminates,
my concern was that in general such recursions do not
terminate.  And in fact, this is case, as Coq'Art shows
with an example in Section 14.1.2.2.  The cure is the
positivity constraint for inductive definitions introduced
in 14.1.2.2.  It is only because of the positivity constraint
that recursion through functional fields terminates.

The informal explanation of recursion through functional fields
on page 171

"Defining recursive functions over inductive types where some
constructors have functions as arguments is a natural generalization
of other kinds of structural recursive definitions.  The images of
functions that appear as arguments of the constructors are naturally
subterms of the whole term.  When these images are in the inductive
type, it is natural to allow recursive calls on these images."

could be extended like this:

"To make sure that such recursions in fact terminate, Coq enforces
the positivity constraint as described in 14.1.2.2."

This brings me to my next question:
- Where do recursion through functional fields and
the positvity constraint come from?
- Did they already exist before Coq?
In Martin Löf? Or in Peter Aczel 1977?

Best,
Gert

Am 18.09.2010 18:12, schrieb Pierre Casteran:

> The explanation can be found p 171:
>
> "Defining recursive functions over inductive types where some
> constructors have functions as arguments is a natural generalization
> of other kinds of structural recursive definitions.  The images of
> functions that appear as arguments of the constructors are naturally
> subterms of the whole term.  When these images are in the inductive
> type, it is natural to allow recursive calls on these images."
>
> This explanation was given in a section about inductive types
> with functional fields, which is the case of Acc (with the function
> you called g).
>
> Pierre