Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 24 May 1995 18:06:28 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA245991735;
          Wed, 24 May 1995 10:08:55 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA245901685;
          Wed, 24 May 1995 10:08:05 -0600
Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Wed, 24 May 1995 16:52:46 +0100
X-Mailer: exmh version 1.6 4/21/95
To: Rob Arthan <rda@win.icl.co.uk>, chou@cs.ucla.edu
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: Finite+Infinite Sequences
X-Uri: <URL:http://www.cl.cam.ac.uk/users/lcp>
X-Face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> 
        E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 
        13swsz`i*9}*8fy}.au9jo.
In-Reply-To: Your message of Wed, 24 May 1995 11:48:20 -0000. <9505241048.17337.0@win.icl.co.uk>
Date: Wed, 24 May 1995 16:52:38 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:038700:950524155248"@cl.cam.ac.uk>

> I don't see how you get this to do the job, in the context of the earlier
> discussion. Wouldn't the final coalgebra have to correspond to
> finite sequences + infinite sequences, where the index sets of the infinite
> sequences range over arbitrary ordinals, not just the natural numbers
> (as required, I think, in the original posting on this topic)?
> If that is the case, then the final coalgebra will be "too big" to be a
> set in ZF set theory and certainly won't be something you can define in HOL.

There are natural constructions such that the final coalgebra of the functor 
is just its greatest fixed point.  The fixed points are up to equality, not 
isomorphism.  A nice bonus is that the least fixed point (which contains only 
the finite lists) is a subset of the greatest fixed point -- no embedding is 
required, and there is no artificial joining of two distinct sets.

The following papers of mine describe the necessary constructions.

For HOL:  Co-induction and Co-recursion in Higher-Order Logic
    URL	   http://www.cl.cam.ac.uk/Research/Reports/TR304-lcp-coinduction.ps.gz

For ZF:   A Concrete Final Coalgebra Theorem for ZF Set Theory
    URL    http://www.cl.cam.ac.uk/Research/Reports/TR334-lcp-final.coalgebra.dvi.gz

They contain a bit of informal motivation.  The paper

    @TechReport{greiner92,
      author = 	 "John Greiner",
      title = 	 "Programming with Inductive and Co-Inductive Types",
      institution =  CMU,
      number =	 "CMU-CS-92-109",
      year = 	 1992}

also contains some useful discussion.
							Larry Paulson