overview.txt -- overview of library of utility axioms


1. Organization

This file gives an overview of the library of utility axioms given in
multiple source files.  These source files have a two digit prefix which
defines a sequence on the source files.  (Note that these numbers are not
always sequential since there may be future insertions and re-arranging.)
The order of axiom definition is basically bottom-up.  We define the most
primitive functions and relations first and then define functions and
relations that use previously defined functions and relations.
The source files group the axioms into related categories, such as the
following:

   basic -- fundamental predicates involving the form of expressions
   higher -- higher-order functions and predicates
   symbol -- axioms relating to symbol representation
   char -- axioms relating to characters
   atom -- axioms relating to atoms
   count -- 
   length --
   natnum --
   ...

This library of axioms is effectively concatenated to form a single set
of axioms, which then define a set of valid expressions.  (Note that the
order of concatenation does not matter as far as the language is concerned --
the source file ordering is just for human understanding and organization.)
Comments on how to improve the organization would be most welcome.


2. Syntax

See the LOPSTR 2000 paper and other recent notes for a definition of
axiomatic language syntax.  The standard syntax is that a comment begins
with an exclamation point ! and extends to the end of a line.  We define
an exception to that rule by allowing a ! to be a symbol character after
the first one, as shown in the following example:

   (abc! %! w)!    -- 1st two ! are part of symbol, third starts a comment

An extension to the comment syntax is that a line beginning with !{ starts
a block of comment lines which continues until there is a line beginning
with !}:

!{    -- start of comment block

   ... comment lines ...

!}    -- end of comment block

We also adopt a syntax convention for these axiom source files that a line
which is non-blank in its first column is also a comment (and thus axioms
must start after the first column):

this is a comment

   (member % ($1 % $2)).    -- not a comment

   ! -- this needs ! to start comment

another comment

Note also that certain other axiom syntax characters, such as < . , are
usable for symbols when they don't occur in the proper position as
axiom expression delimiters.  Thus, it is necessary to put an extra
space between symbols occurring as top-level conclusion and condition
expressions and the subsequent delimiter character:

   % < abc .

Another possible syntax enhancement that is not mentioned elsewhere is to
allow a block of text to occur within an expression.  If a line ends with
with a double quote character immediately followed by a symbol and then
arbitrary blanks and an optional comment, but no closing double quote,
then the next zero or more lines represent a block of text intended as
data, followed by a line starting with zero or more blanks, then the
same symbol followed immediately by a double quote.  (The purpose of
the symbol is to provide a distinctive end-of-block marker.  Is there
a better way to handle this???)  The block of text becomes a sequence
of zero or more expressions, each expression representing a line of text
and is a sequence of zero or more characters.  An example of this is as
follows:

   (abc () "block
This is the first line of a block of text.
... another line ...  
Last line of block of text.
    block" xyz)

The expression defined here is equivalent to

   (abc ()
    ("This is the first line of a block of text."
     "... another line ..."  
     "Last line of block of text.")
    xyz)

This may be useful for some meta-language applications.


3. Disclaimer

This software is available "as is" with no technical support or guarantee
of fitness for any purpose.  This is purely research software that has not
been tested or validated for any production use. 


4. Copyright

These axiomatic language source files and other files on this website are
Copyright Walter W. Wilson 2001 (or earlier years for some papers).