Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: t.forster@pmms.cam.ac.uk, info-hol@leopard.cs.byu.edu
Cc: chou@cs.ucla.edu, tfm@dcs.gla.ac.uk
In-Reply-To: <m0sAzCP-0003V2C@emu.pmms.cam.ac.uk> (message from Thomas Forster on Mon, 15 May 1995 14:24:00 +0200)
Subject: Re: Sequences
Message-Id: <95May15.162352met_dst.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Mon, 15 May 1995 16:23:45 +0200


> Surely a finite-or-infinite list can be a function from an initial
> substructure of :num to widgets.  Could perhaps be done more cutely i
> suppose but aren't we meant to be engineers?  Won't that do?

I'm not exactly sure what Thomas is saying, but if he is saying: "just
add a predicate on the domain (num) whenever it is necessary", then that
is also OK. Paul Loewenstein's infinite-state automata theory (found in
contrib) takes this approach. The following is a quotation from his
paper, "A Formal Theory of Simulations Between Infinite Automata" (in
Formal Methods in System Design, Vol. 3 No. 1,2, August 1993):

   "Infinite sequences of values are denoted as functions from a natural
    number to the value at each instant.  ... We shall also use finite
    sequences , which will usually be prefixes of infintie
    sequences. Rather than define the concept of a finite sequence
    directly, and the operators to concatenate finite and infinite
    sequences, we instead refer to a finite number of elements of an
    infinite sequence. This allows fewer definitions, simpler formulas,
    and less tedious reasoning."

Note the last sentence, although I would like to see a comparison study
of the two approaches.

Konrad.