Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by nene.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 24 May 1995 12:44:23 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA153422652; Wed, 24 May 1995 04:50:52 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from relay1.pipex.net by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA153362564; Wed, 24 May 1995 04:49:24 -0600 Received: from Q.icl.co.uk by flow.pipex.net with SMTP (PP); Wed, 24 May 1995 11:47:57 +0100 Received: from norman.win.icl.co.uk (norman.win01.icl.co.uk) by Q.icl.co.uk (4.1/icl-2.12-server) id AA19108; Wed, 24 May 95 11:51:57 BST From: Rob Arthan Date: Wed, 24 May 95 11:48:20 BST Message-Id: <9505241048.17337.0@win.icl.co.uk> To: info-hol@leopard.cs.byu.edu Subject: Finite+Infinite Sequences Larry Paulson writes: > By far the simplest, abstract characterization of infinite+finite sequences > (over A) is as the final coalgebra of the functor 1 + (A * -), that is, the > functor F such that F(Z) = 1 + (A*Z) for all Z. 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. Regards, Rob Arthan (rda@win.icl.co.uk)