The Coq mailing list

[Milad Niqui <milad AT cs.kun.nl>]

Venanzio Capretta wrote:
> My question was specifically about the type Tree defined using lists.
> I think this example is an argument in favor of the "coinductive types 
> as final coalgebras" definition against the "guarded by constructors" 
> conception.

Dear Venanzio,

I completely agree. A similar function that you can not define because
of guardedness conidtion is the stream of natural numbers:

 nats = Cons O (map S nats)

Here --- similar to your function --- nats is guarded by map and not by
Cons. But at least this example can easily be made guarded, while yours
needs a modification of the datatype using a dependent type (which for
example is not allowed in Haskell).


> It seems to me that implementing the coinductive principle stating that 
> there is a unique morphism from any coalgebra to the inductive type 
> would be much easier than extendin the definition of "guarded by 
> constructors".
>
> Maybe this could be a suggestion for future versions of Coq.

Did you mean "there is a unique morphism from any coalgebra to the
/coinductive/ type" ? Or do you really mean inductive types are enough?

I think extending the definition of guardedness condition in a way that
the recursive calls can be guarded by the Fix operator is enough (e.g.
the map functions is actually a fixpoint). It seems to me that this will
solve the problem for all coalgebra maps that can be obtained by the
dual of the course of value recursion scheme (so by composing the
coalgbera with the iterator of an initial algebra); although it still
doesn't solve the problem for partial functions that are not
syntactically productive.

Another question: with your suggestion, can we still encode all
coinductive types, including impredicatvie ones?  And is there
a criteria that says for which functors on the category \omega-sets
(the model for impredicative CIC) the final coalgebra exist?

Regards,


--
Milad Niqui

Computing Science Department,                tel:+31 24 365 2631
University of Nijmegen,                      fax:+31 24 365 2525
P.O.B. 9010,                                 email: 
milad AT cs.kun.nl
6500 GL Nijmegen,                            http://www.cs.kun.nl/~milad
The Netherlands.
==============================================================================================
The University of Nijmegen will be named Radboud University Nijmegen as 
of September 1st, 2004