Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Co-recursion question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Co-recursion question


chronological Thread 
  • From: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
  • To: Jeffrey Harris <janglernpl AT gmail.com>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Co-recursion question
  • Date: Sun, 25 Oct 2009 22:09:07 +0000
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.





Archive powered by MhonArc 2.6.16.

Top of Page