The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

Well, you do not need to go all the way to classical functional 
relations to be able to build this function. You need only one niceo 
function : one that decides whether a function from cotree to conat 
terminates (that is a halting problem oracle). These are hard to find in 
nature. But if you are given one, it's quite easy to compute the 
"number" of leaves in your cotree.

That said, you cannot tell that to Coq, because it is not able to 
meta-reason on termination.

But still, it's rather easy a function to build, you only need to be 
able to look at the omega-th step. We could say it almost exists. Some 
people like to say it has a low turing degree.



Arnaud Spiwack

Edsko de Vries a écrit :
> Hi,
>
> I am a programmer at heart which is why I feel very comfortable with 
> proofs in Coq. Notions such as termination and productivity make sense 
> to me; domain-theoretic definitions of functions as least or greatest 
> fixed points -- I have to think about a lot more.
>
> Now, my "programmatic" (am I allowed say "constructive"?) intuition 
> usually serves me quite well. Simple example: when a function 
> "obviously does not terminate", it should not be possible to give an 
> inductive definition of the function (it would not be well-founded).
>
> My question is this: when a function is "obviously not productive", 
> does that mean it should not be possible to give an coinductive 
> definition of that function (it would be ill-specified in some sense, 
> although I'm not sure what the equivalent of "well-founded" is for 
> coinduction)?
>
> 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?
>
> 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