Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199505172107.RAA20400@circe.mitre.org>
To: Tom Melham <tfm@dcs.gla.ac.uk>
Cc: guttman@linus.mitre.org, farmer@linus.mitre.org, 
    info-hol@leopard.cs.byu.edu
Subject: Re: Sequences
In-Reply-To: Your message of "Wed, 17 May 1995 10:27:48 BST." <199505171122.HAA20125@linus.mitre.org>
Date: Wed, 17 May 1995 17:07:40 -0400
From: "Joshua D. Guttman" <guttman@linus.mitre.org>

Tom Melham wrote:  

>  So, can anyone exhibit a nice abstract characterization 
>  of infinite+finite sequences?  As usual, we want the
>  characterizing theorems to be:
>  
>    * abstract (doesn't explicitly refer to the representation)
>    * independent
>    * complete
>  

One might start out as follows: 

1.  If s is a finite/infinite sequence, then it must make sense to ask
    what its i-th term is.  So there must be some operator -- I'll
    think of it as a partial function, but you can of course cash that
    out in your favorite way in your favorite logic -- of type:

	Seq_ap : 'a Seq -> N -.-> 'a 

    where I'm using -.-> to mean partial fn.  
    
    For s to be a finite/infinite sequence, then (Seq_ap s) must have
    either an initial segment of N or else all of N as its domain.
    Using the notation #(t) to mean that t has a value, we can state
    that as:

(*)	forall i,j:N . i<j and #(Seq_ap s j) implies #(Seq_ap s i)

    The sequence is finite if also forsome i:N . not(#(Seq_ap s i)).
    CAR and CDR are also easily defined; car is \s . (Seq_ap s 0).  The
    cdr of s is s' iff 

	Seq_ap s' = \i Seq_ap s (1+i). 

2.  One also needs an identity criterion, to determine when two of
    these beasts are the same (if I can express it that way; I suppose
    that *two* of them are never the same).  And this principle has to
    be the relevant version of extensionality:  

(**)	(forall i:N . Seq_ap s_1 i =~= Seq_ap s_2 i) implies s_1 = s_2

    where =~= expresses Imps's "quasi-equal", i.e. s =~= t means 

	#(s) or #(t) implies s=t.

    This means that s and t have the same value or lack thereof.

3.  Finally, though, there is the question of what finite/infinite
    sequences exist.  At this point, it seems to me, there is no
    longer any point in pretending to do the treatment of
    finite/infinite sequences in an abstract,
    representation-independent way.  For, we need to ensure that all
    the uncountably many sequences that should exist really do exist,
    and the easiest way to do so is to make use of the
    function-existence principles that any suitable logic must
    provide:

	forall f : N -.-> 'a 
	  (forall i,j:N . i<j and #(f j) implies #(f i))
          implies 
	  forsome s . Seq_ap s = f.  
	  
    Extensionality (**) ensures that any two such s are equal.  

    So, it seems to me, we may as well dispense with the attempt to
    hide the nature of finite/infinite sequences using Seq_ap.  We can
    stipulate that finite/infinite sequences simply are functions of
    type N -.-> 'a such that (*) holds.  Then we can discard Seq_ap;
    it is simply \f i . f(i).  Similarly, cdr may now be defined
    explicitly as \f i . f(1+i).

So it seems to me that "partial fn satisfying (*)" is as abstract a
characterization of the notion as it really makes sense to give.  

	Josh