The Coq mailing list

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

> Example: suppose we define coinductive trees as
>
>  CoInductive cotree : Set :=
>    | coleaf : cotree
>    | cobranch : cotree -> cotree -> cotree.
>
> Consider a function to count the number of leaves in a tree
>
>  leaves : cotree -> conat
>
> (the domain is conat because there might be infinitely many leaves).  
> This function is "obviously not productive": there are infinitely  
> large trees that don't have any leaves but simply keep on branching  
> forever. For trees like this, the expected answer is zero (there are  
> no leaves in the tree) or possibly infinity (one might argue that  
> that is a valid interpretation) but for either answer the function  
> would have to be sure that the tree is infinite and does not have  
> any leaves; it needs to traverse the entire tree before it can be  
> sure and so cannot produce (even part of) the answer in finite time.  
> Hence, this function is not productive.
>
> However, what does that mean? Does 'leaves' exist in some  
> mathematical world that I simply cannot encode in Coq, or is it  
> somehow inhererently ill-specified?

What should leaves return for infinite tree which only contains  
cobranch? You could say 0 because it doesn't contain any coleafs but  
there is no way to find this out in finite time. With other words this  
function is not constructively definable.

In classical mathematics the word function is used to refer to a  
relation R which is left-unique and right total. Constructively,  
classical right-total means that forall t:tree,not (forall n:conat,  
not R t n). left-uniqueness has to be stated upto bisimulation.

Cheers,
Thorsten

> Thanks,
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.