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; Sun, 14 May 1995 07:23:41 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA179431703; Sun, 14 May 1995 00:08:23 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA179401698; Sun, 14 May 1995 00:08:18 -0600 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26735-3>; Sun, 14 May 1995 08:07:15 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8081>; Sun, 14 May 1995 08:07:13 +0200 From: Konrad Slind To: info-hol@leopard.cs.byu.edu, chou@cs.ucla.edu In-Reply-To: <9505140457.AA18615@maui.cs.ucla.edu> (chou@cs.ucla.edu) Subject: Re: Sequences Message-Id: <95May14.080713met_dst.8081@sunbroy14.informatik.tu-muenchen.de> Date: Sun, 14 May 1995 08:07:06 +0200 Ching Tsun asks: > Finite sequences can be represented by lists; infinite sequences can > be represented by functions with domain :num. But has anyone > developed a theory of sequences that can deal with both finite and > infinite sequences? Tobias Nipkow and I developed something like this for IO/automata in Isabelle. As was discussed earlier on info-hol, define an "option" type 'a option = None | Some of 'a. Then a general sequence has type num -> 'a option and a finite sequence is defined to end with an infinite number of consecutive Nones. So far so good, but filtering of sequences by a predicate can raise the problem of defining equivalence of sequences modulo "gaps" (basically consecutive Nones should all collapse), which gets somewhat complicated. Some details can be found in the papers (with IO Automata in the title) accessible through Tobias' home page: http://hpbroy3.informatik.tu-muenchen.de/MITARBEITER/nipkow/nipkow.html Konrad.