The Coq mailing list

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

Hi Jeffrey,

the answer is no, because in extensional Type Theory coinductive types  
can be encoded using inductive types. And as far as the strength of  
the theory is concerned there is no difference between extensional and  
intensional Type Theory. For me detail see our paper

@Article{alti:cont-tcs,
 author =        {Michael Abott and Thorsten Altenkirch and Neil Ghani},
 title =         {Containers - Constructing Strictly Positive Types},
 journal =       {Theoretical Computer Science},
 year =          {2005},
 volume =        {342},
 pages =         {3--27},
 month =         {September},
 note =  {Applied Semantics: Selected Topics},
}
available from my webpage http://www.cs.nott.ac.uk/~txa/publ/cont-tcs.pdf

In section 4 we show how to derive M-types from W-types and this is  
enough because all strictly positive types can be constructed from W-  
and M-types. The basic idea can be concisely expressed in the language  
of category theory: every signature functor is \omega-continous hence  
its terminal coalgebra can be constructed as an \omega-limit and  
'omega-limits are easily definable within Type Theory.

Cheers,
Thorsten

On 25 Oct 2009, at 00:14, Jeffrey Harris wrote:

> Hello!
>
> I apologize for the imprecise phrasing, but does anyone know if the  
> ability to do coinduction/corecursion in Coq expands the class of  
> definable functions on inductive types? For instance, is there any  
> function from nat->nat which is definable in Coq, but would not be  
> definable without the use of coinduction/corecursion? (So, perhaps,  
> a composition of functions f1:nat->stream and f2:stream->nat).
>
> Thanks,
> Jeffrey


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.