Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: "William M. Farmer" <farmer@linus.mitre.org>
Date: Tue, 16 May 1995 14:05:32 -0400
Message-Id: <199505161805.OAA18758@apollonius.mitre.org>
To: info-hol@leopard.cs.byu.edu
Subject: Re: Sequences

In IMPS, a sequence over a sort A is represented as a partial function
from the natural numbers N to A.  The "length" of a sequence s is
defined as the unique n : N such that, for all m : N, m < n iff s(m)
is defined.  A sequence s is "finite" if length(s) is defined and
"infinite" if s is total on N.  (A sequence is "improper" if it is
neither finite nor infinite, i.e., if it has gaps in its domain.)
Operators like car, cdr, cons, and append are defined for all
sequences in the obvious way, and nil is the empty function.

Similarly, a matrix over a sort A can be represented as a partial
function from N x N to A.  The "row-length" of a matrix s is defined
as the unique n : N such that, for all m1,m2 : N, m1 < n iff s(m1,m2)
is defined.  The "column-length" is defined in the same way.  A matrix
s is "finite" if both row-length(s) and column-length(s) are defined
and "infinite" if s is total on N x N. The basic matrix operations,
including multiplication, are easy to define.

These representations work very well in a logic -- like the IMPS logic
-- which provides support for partial higher-order functions.

Bill Farmer