Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9204131842.AA17015@easynet.crl.dec.com>
Date: Mon, 13 Apr 92 14:42:44 EDT
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 13-Apr-1992 1342" <leonard@com.dec.enet.ricks>
To: info-hol@edu.uidaho.cs.ted
Apparently-To: info-hol@ted.cs.uidaho.edu
Subject: Re: A wordn library.

Wordn will use other theories, some of which will be in other libraries.  If
we understand now what the library hierarchy will eventually be, we can try to
fit it now, and make eventual convergence much simpler.  For example, consider
organizing the wordn functions so they can someday be divided among a hierarchy
of libraries something like this:

  o fixed-length lists (implictly used in the current representation of words)
  o integers (signed num)
  o modular numbers (unsigned and signed)
  o radix<n> numerals (unsigned and signed)
  o rational numbers (unsigned and signed)
  o floating point numbers
  o fixed-length floating-point numbers
  o wordn (fixed-length lists of num)
    - wordn as booleans (bit-wise boolean operations)
    - wordn as modular num
    - wordn as modular int
    - wordn as radix<n> numerals (for packing and unpacking bytes in words?)
    - wordn as modular floating-point numbers

I've probably overlooked lots more.  If we can agree on a hierarchy to be our
goal, I'll organize my own work to fit, too.

Thinking this way, I realize that I included arithmetic shift right (a shift
that sign extends) with shift and rotate, and it should actually be grouped
with the arithmetic operations.  Also, I should have included arithmetic shift
left (a shift that checks for overflow). 

The boolean operations depend on yet another interpretation of words, and
probably represent a separate sub-theory.

Wordn arithmetic includes at least ADD, SUB, MUL, MUL (high half), DIV, and
EXP, each with and without overflow checking; and the comparison operations EQ,
NE, LT, LE, GT, and GE.  These are all needed for num, int, and fp.