atom.txt -- some basic definitions about atoms
uses:
   higher -- higher-order definitions  (Valid)
   finite -- finite-set definition  (finite_set)


1. Discussion

Atoms are the "leaves" of axiomatic language expressions.  In this section we
give some utilities that help to manage them.  Note that there is no built-in
predicate in axiomatic language called  (atom <atom>)  which defines the set
of atoms.  Even more important there is no built-in inequality between distinct
atoms.  It turns out that inequality between atoms can be easily defined so
long as one follows certain conventions described in this section.

Probably users of axiomatic language will rarely deal with atoms directly.
Instead users will write expressions involving symbols, as if symbols were
the atom leaves of the expression trees.  As described in subsequent files,
however, that is not the case:  Symbols are actually syntactic shorthand
for expressions that include the character string representation of the
symbol, and characters are syntactic shorthand for expressions that give
the bit pattern of the character using bit atoms.  But the user should not
have to deal with this underlying representation very often, and in fact,
a goal of this utility library is to provide high-level functions and
predicates that hide this low-level representation.  Users will probably
have little need to introduce new atoms.  It may just only be this library
that defines atoms.

To define an  (atom <atom>)  predicate for atoms being used and to define
inequality between distinct atoms, we adopt the convention of having users
"declare" each atom that is used using the following unconditional axiom:

!  (atom_defn <atom> <atom_name> [<atom_pred>]).

! example:
!    (atom_defn `char "char" char_atom).

Here <atom> is the new atom being defined, <atom_name> is the atom symbol,
with the leading `, as a character string, and the optional argument
<atom_pred> is a unique predicate name associated with this atom.
Note that if the atom predicate is omitted then the declaration axiom
would appear as:

!  (atom_defn <atom> <atom_name>)        -- <atom_pred> omitted here

From the atom declaration axiom we wish to generate the following valid
expressions:

!  (atom <atom>)               -- add to set of atoms
!  (atom <atom> <atom_name>)   -- associate atom with its char str name
!  (<atom_pred> <atom>)        -- (optional) assoc atom with predicate name

! example:
!    (atom `char)
!    (atom `char "`char")
!    (char_atom `char)

The (atom <atom>) predicate adds this atom to the set of declared atoms.
The (atom <atom> <atom_name>) predicate allows easy definition of inequality
between distinct atoms using the following axiom that is formally introduced
in the <notequal.txt> file:

!  (~== %atom1 %atom2)<
!    (atom %atom1 %atom1_name),
!    (atom %atom2 %atom2_name),
!    (~== %atom1_name %atom2_name).

This axiom asserts that if two atoms have distinct character string names
then the two atoms are considered distinct with an inequality relation
defined between them.  Obviously, the names gives to distinct atoms must be
distinct for this convention to work!  That's why our convention is to use
the actual atom symbol (with the leading `) as the atom name.  Note that
we must define inequality between characters and character strings first
before this general inequality between distinct atoms can be defined.
(It turns out this can be done by just defining inequality between the
two bit atoms, bit0 and bit1, along with other axioms found in file
<notequal.txt>.)

Alternative:  Instead of using a character string name, could use the
name without the leading ` as a symbol.  For example:

!   (atom_defn `char char char_atom)

This may be a littler easier to write; however, atoms of the form `%abc
and `$xyz cannot be represented by symbols %abc and $xyz and the atom `
does not have a viewable representation.  (Of course, such "symbols" could
be defined by explicit expression representation, but this detracts from the
convenience of having a symbol representation.)  Also, the character string
representation is "simpler" than a symbol.  Therefore we will use the
character string representation for the atom name as proposed here.

Another alternative would be to eliminate the leading ` character in the
character string, since all atoms start with `.  However, below we define
sets of atoms in a finite_set expression and we use the character string
from the set symbol (which does not have a leading `) as the atom name
string.  Thus a leading ` for an atom name marks the declaration of a
specific atom while a missing ` denotes a name for a set of atoms.

The third, optional, predicate that is generated from an "atom_defn" axiom
is an  (<atom_pred> <atom>)  expression which associates the atom with
a unique predicate name.  This expression is only generated if the <atom_pred>
symbol is present as the third argument of the atom_decl axiom.  The purpose
of this predicate is to simply give a symbolic name to the atom, which allows
the atom symbol itself to be "hidden", much as one might give a symbolic
name to a numeric constant.  With this predicate one can use the character
atom in axioms without having to use the atom symbol explicitly, such as
in the following example:

!    ... example axiom using %char_atom ...<
!         ...,
!         (char_atom %char_atom).

With this predicate, we are free to change the atom symbol for the character
atom in the atom_defn axiom without having to change axioms, such as this one,
where it is used.  (In some of the subsequent examples where this is used
it may be a toss-up how helpful this convention actually is, but at least it
is available.)


2. Axioms

In this section we give the actual axioms that generate the above expressions
from the atom_defn axiom.  We first define the optional unique predicate
which serves as the symbolic name for the atom:

   (%atom_pred %atom)<         ! -- definition of unique predicate for atom
     (atom_defn %atom %atom_name %atom_pred).
        ! -- This handles the optional case where <atom_pred> is present.

Now we generate the two forms of the (atom ...) predicate:

   (Valid
       (atom %atom)
       (atom %atom %atom_name))<
     (atom_defn %atom %atom_name $atom_pred).
        ! -- Note that <atom_pred> is optional and unused here.

See subsequent files for actual atom definitions and see file <notequal.txt>
for inequality definition.


3. Defining a set of atoms

This section defines a finite set of atoms all at once, using a form similar
to the "finite_set" definition in file <finite.txt>.  A set of atoms is
declared by the following expression:

!  (atom_set <set_name> (<atom0> ... <atomn-1>)).

! example:
!    (atom_set bit_atom (`bit0 `bit1)).     ! the set of two bit atoms

The atoms in an atom set should all be distinct from each other as well as
distinct from atoms in any other atom set or in any atom_defn declaration.

We generate the atom definition predicate from this set definition as follows:

   (atom_defn %atom %set_chstr)<
     (atom_set %set_name ($1 %atom $2)),
     (== %set_name (%symbol_atom %set_chstr)).

Note that the character string name for the atoms in this set is obtained
from the second expression of the set name symbol.  (See <symbol.txt>.)
This name applies to all atoms in the set.  From this atom_defn expression
we generate the following predicates (see <atom.txt>):

!  (atom <atom>)
!  (atom <atom> <set_chstr>)      -- same char str name for each atom in set

Instead of a predicate name for each individual atom, we generate a predicate
for the entire set of atoms by first asserting that this is a finite set
(see file <finite.txt>):

   (finite_set %set %atoms)<
     (atom_set %set %atoms).     ! an atom set is a finite set

From this finite set we generate a set predicate as follows:

!  (<set> <atom>)

An index associated with each set element would also be defined from the
finite_set expression.  An error (ERROR!) would be generated if the same
atom appeared more that once in the list of atoms.

Note that we can define an additional error message if a non-atom is
in the list of atoms:

!  (ERROR! "non-atom in definition of set of atoms")
!     < (atom_set %set ($1 ($seq) $2)).

In order to define inequality we must first define inequality between
the atoms of the atom set and then between atoms of different sets and
between atoms defined in sets and those defined individually in atom_defn
predicates.  The definition of inequality for atoms in the same set
is given in file <notequal.txt>, but we show it here too:

!  (~== %atom1 %atom2)<
!    (atom_set %set ($1 %atom1 $2 %atom2 $3)).

Now, so long as set names are distinct, which causes the <set_chstr> names
to be distinct, then an inequality relation will be defined between atoms
of different sets and between individually declared atoms.

Note that if an atom only appears in one atom set then an index associated
with that atom will be unique.


4. Set of expressions formed from declared atoms

The set of expressions formed from declared atoms is as follows:

   (declared %atom)<
     (atom %atom).     ! these atoms should have inequality defined

   (declared ()).
   (declared (% $))<
     (declared %),
     (declared ($)).

This set of expressions has the not-identical relation defined on them.
It would also be nice to have a special type of ordering relation
"<declared" defined on the complete set of declared expressions.

   *** to be defined here or in <order.txt>

-- First we need to define to define <declared for declared atoms.
   Such atoms would be ordered first by their character string atom_name
   (for individual atom declarations) and then by their order in
   an atom_set declaration.

-- Allow mixing non-declared atoms in the expressions?