The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Thorsten,

The theoretical reason I don’t like co-inductive types is that they require some notion of an infinite term in the meta-language. This leads to all sorts of issues in formalizing the meta-theory of a system. But maybe you know how to get around these issues? A translation like you suggest, that defines co-inductive types in terms of constructs already in the system, would be a great help in this direction.

I will admit that I don’t quite understand everything you said in complete detail, but it sounds at a high level like you are basically saying that positive functors have greatest fixed-points, for the usual reason of being continuous. I buy this. But I at least would be interested to see more of the details of how to actually do this in type theory.

For instance, I imagine that directly formalizing the terminal coalgebra of a positive functor would lead to some trickiness with universes, and same thing with taking the omega-limit of a type functor. I could be wrong, but if not, you would probably have to do this part on paper, defining a translation from a given positive functor to the type of its terminal coalgebra. It would be especially neat if this somehow yielded the results you gave in the examples you mentioned; i.e., if you could run it on the stream type and get nat functions, and if you could run it on the colist type and get the nat -> maybe A type you described.

As for W-types, I thought they were well-founded? I.e., inductive, and not co-inductive?

-Eddy

On Dec 10, 2015, at 8:31 AM, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

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.