Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 15 May 1995 16:51:29 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA174571312; Mon, 15 May 1995 09:21:53 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from catseye.idbsu.edu by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA174541311; Mon, 15 May 1995 09:21:51 -0600 Received: by catseye.idbsu.edu (1.38.193.4/16.2) id AA03361; Mon, 15 May 1995 09:25:36 -0600 Date: Mon, 15 May 1995 09:25:36 -0600 From: Randall Holmes To: info-hol-request@leopard.cs.byu.edu, info-hol@leopard.cs.byu.edu Subject: Re: Sequences Message-ID: <"swan.cl.cam.:261540:950515155304"@cl.cam.ac.uk> I think that non-well-founded set theory in the style of Aczel would provide a natural treatment of lists of both finite and infinite length. In ZFC- + AFA (Aczel's anti-foundation axiom), with a base type A already chosen, define "A list" as the maximal (not minimal!) class with distinguished element nil such that C = {nil} u (AxC). This class would contain both finite and infinite lists. reference: Peter Aczel, _Non well founded sets_, CSLI lecture notes #14, 1988. I think that there are other reasonable approaches as well. The opinions expressed | --Sincerely, M. Randall Holmes above are not the official | Math. Dept., Boise State Univ. opinions of any person | holmes@math.idbsu.edu or institution. | http://math.idbsu.edu/faculty/holmes.html