The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

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