Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Rob Arthan <rda@win.icl.co.uk>
Date: Mon, 22 May 95 16:16:51 BST
Message-Id: <9505221516.9213.0@win.icl.co.uk>
To: tfm@dcs.gla.ac.uk
Subject: Re: Sequences
Cc: info-hol@leopard.cs.byu.edu

Tom Melham writes:

> 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

I suspect that what's expected is a characterisation via some universal
mapping property (like the recursion principle for lists). The
following is the best I can think of. I'm sorry that it's a bit
technical and for any glitches in my HOL syntax.

To state the characterisation, I need the following function:

    Prefix n [] = []
/\  Prefix n (Cons x t) = if n = 0 then [] else Cons x (Prefix(n-1) t)


Thus Prefix N L is the list comprising the leading N elements of L, if
L has at least N elements and is just L otherwise. Loosely speaking,
I'm going to characterise the desired set of sequences as being anything
that permits a prefix operation for each n, producing lists of
length n, but allowing for the possibility of objects whose prefixes
just grow for ever as the length increases.

If 'a SEQ is to be the type containing the finite and infinite
sequences over 'a, then a characterising property of 'a SEQ can be
written (I claim) as follows:

?L : num -> 'a SEQ -> 'a LIST .
    (!i . Prefix (i) o L (i + 1) = L(i))
/\
    !A : num -> 'b -> 'a LIST .
        (!i . Prefix (i) o A (i + 1) = A(i))
    =>	?! h : 'b ->  'a SEQ . !i . A(i) = L(i) o h

This is the assertion that 'a SEQ is an example of what is called an
inverse limit. See the P.S. below for more information (and a
construction for 'a SEQ based on this characterisation).

Against Tom's more objective criteria I would
score this characterisation as follows:

1. Abstract: It certainly makes no mention of the internal structure of the
representation, so, in that sense, it is abstract.

2. Independent: well actually, I suspect the first conjunct under
the existential quantifier might follow from the second, but what
I've written is the usual way of describing this sort of property.

3. Complete: such a characterisation is guaranteed to characterise
the thing 'a SEQ by a standard argument. (If X and Y are two candidates
for 'a SEQ satisfying the characterisation then the existence part
gives functions f:X->Y and g:Y->X and the uniqueness part shows that
g o f and f o g are the identity functions on X and Y respectively.
So X and Y are in 1-1 correspondence.)

But I have to add:

4. Useful: probably not! To check out the formulation, I proved
in ProofPower-HOL that it holds of:

	'a SEQ = ('a LIST) + (num -> 'a)

and, I must confess, that the defining properties of lists and disjoint
union make reasoning with this definition pretty straightforward, and
I'm not sure that I'd often want to use what I've proposed as a
characterisation instead of them.

As to whether this is "nice", I suspect that's rather in the
eye of the beholder.  I would be interested if anyone can come up
with anything "nicer" - the problem with these dual things is that
the universal algebra which the HOL treatment of recursive types
is based on doesn't work too well when you turn all the
functions round.

Rob Arthan (rda@win.icl.co.uk)

========================================================================

P.S. Further Explanation: Consider a diagram of sets and functions like:

     X_0 <---- X _1 <---- X_2 <---- ....
           f_0        f_1       f_2

Such a thing is called an inverse system.  A cone over the inverse
system is defined to be a structure comprising a set
A together with maps a_i:A -> X_i such that the following diagram
commutes (i.e., a_0 = f_0 o a_1, a_1 = f_1 o a_2, etc.):

     X_0 <---- X_1 <---- X_2 <---- ....
           f_0        f_1       f_2
     / \       / \       / \
      |         |         |
  a_0 |     a_1 |     a_2 |
      |         |         |

      A    =    A    =    A   =  ....

An inverse limit (L, l_i) for the inverse system, is a cone such that
if (A, a_i) is any other cone, then there is a unique function h : A ->
L such that each a_i factors as:

	a_i = l_i o h

My proposed characterisation of 'a SEQ is then the assertion that 'a
SEQ is the inverse limit of the inverse system in which each X_i is
'a LIST and each function f_i is Prefix(i):


    'a LIST <-------'a LIST  <------'a LIST <------ .....    (*)
             Prefix(0)        Prefix(1)

There is a standard recipe (in set theory) for constructing inverse
limits. You form the product, P say, of all the X_i and then take the
subset L of P comprising those (x_0, x_1, ...) in which for each i
f_i(x_(i+1))  = x_i. The inverse limit then comprises (L, l_i) where
each l_i is the restriction to L of the projection of P onto its i-th
factor.

It's not too hard too see that for the above inverse system, this
construction of the inverse limit gives the desired set of finite and
infinite sequences of elements of 'a. What happens is that a
member (x_0, x_1, ...) of the inverse limit will either stabilise at
some stage, say x_i = x_j for all j > i, or the x_i will keep getting
longer. The former case corresponds to a finite sequence (given by the
stable value x_i), the latter case corresponds to an infinite sequence
(whose j-th term is the common j-th value of all the x_i which have
length greater than j). (Note that for each i, x_i has length
at most i, since x_i = Prefix(i) x_(i+1).)

The standard set theoretic recipe gives us a construction for
the finite and infinite sequences which one could use in HOL.
It would be:

	{f : num -> 'a LIST | !i . Prefix(i)(f(i+1)) = f(i)}


In set theory, but not so readily in HOL, one can understand this
construction (or something very like it) as being dual to a
construction of the set of lists over a set. Given a set, X say, let
X^n be the cartesian product of n copies of X (i.e., lists over X of
length exactly n), and let Y_n say be the union of X^0, X^1, ...  X^n.
(i.e., lists over X of length no greater than n). Now, in the i-th term
of the inverse limit (*) above, the lists of length greater than i play
no part in the construction of the limit. Thus the finite and 
infinite sequences are given as the inverse limit of an inverse
system:

   Y_0 <---- Y_1 <---- Y_2 <---- ...
        g_0       g_1        g_2

in which each g_i is the restriction of Prefix(i) to Y_i and, dually,
the set of lists over X is the direct limit of a direct system:

   Y_0 ----> Y_1 ----> Y_2 ----> ...
       f_0       f_1       f_2


where each f_i is just the inclusion of Y_i in Y_(i+1). (Direct systems
and direct limits are just like inverse systems and inverse limits but
with all the function arrows pointing in the opposite direction. In
this case, since each f_i is an inclusion mapping, the direct limit
amounts to no more than the union of the Y_i).