The Coq mailing list

[roconnor AT theorem.ca]

On Sun, 25 Oct 2009, Yves Bertot wrote:

> Having only one principal argument for guarded recursion is not the problem, 
> I believe.  In my opinion, the problem is that when analyzing an internal fix 
> construct, only the principal argument is used to pass legitimate guarded 
> variables to the body of the fix construct.   This can be seen in Coq 
> sources, file kernel/inductive.ml
> It is beyond my competence to change this file and be sure that it does not 
> break consistency.

Thanks for looking at this.  I suspected that was the problem, but it is 
hard or impossible to find a description of the guardedness
specification.

> concerning Russell's initial problem, it is possible to workaround it, by 
> collecting the values of recursive calls on the second list in a first pass, 
> putting them in a list, and retrieving them during the second recursive 
> traversal.
> This may be unsatisfactory for efficiency reasons, but I believe it works. 
> Here is my proposal.

Thanks for this.  I was beginning to think of something along these lines, 
but I hadn't worked out the details yet.

In my actual problem I found a way of eliminating the recursive call to 
elements of my second list by using information that can be found in the 
first list.  However this solution is really specific to my actual problem 
and won't work in general like your solution does.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''