The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

Hi Gert,

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

Actually Andreas Abel and myself proved termination (even though only for 
simple types). See our JFP 02 paper  "A Predicative Analysis of Structural 
Recursion" (http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf).

>  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 Lf? Or in Peter Aczel 1977?

Martin-Loef''s W-type is universal for strictly positive definitions. I am 
not sure when W-types appeared first, they certainly feature in the 1980 
Sambin/Martin-Loef book. 

Cheers,
Thorsten

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