The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

All coinductive types can be reduced to functions over the natural numbers and inductive types in an extensional setting (e.g. HoTT).

The reason is that all strictly positive functors are omega-continuous (I.e. they preserve omega-limits) and hence there is an encoding of the terminal coalgebra as an omega-limit. In the case of streams that is equivalent to the functions over Nat while n the case of colists the representation is equivalent to functions from Nat into Maybe A with the condition that if f(I)=nothing then f(i+1)=nothing. 

There is also an explicit encoding of all strictly positive types using only W-types which you find in our container papers, e.g. 

@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},
}

What are the theoretical reasons for not liking conductive types?

Thorsten

 

From: Eddy Westbrook <westbrook AT kestrel.edu>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Thursday, 10 December 2015 16:21
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Co-inductive Streams vs. Functions

I have actually thought a lot recently about modeling non-terminating systems, and have mostly come to a similar conclusion as you, that (nat-> A) equivalent to (Stream A), and that the former does not require co-inductive types (which I don't like for a number of theoretical and practical reasons).

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

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.