symbol.txt -- defn of symbol representation, symbol atom, and symbol predicates
uses:
   higher.txt
   atom.txt
   char.txt


1. The Symbol Syntax Extension

!{
This file describes the axiomatic language syntax extension for symbols.
In ordinary pure Prolog a symbol is a primitive, indivisible, atomic
element.  In axiomatic language, however, atoms are symbols beginning
with the backquote  character `: `abc, `+, etc.  A symbol that does not
begin with ` % $ ' " ( ) is syntactic shorthand for an expression
consisting of a special prefix atom  `symbol  followed by the symbol
as a character string:

   abc  ==  (`symbol "abc")
   +    ==  (`symbol "+")
   3174  ==  (`symbol "3174")
   _%$`'"  ==  (`symbol "_%$`'""")

Note that these relationships are all generated as valid expression
instances of the identity relation:

   (== % %).           ! axiom for the identity relation

  generated valid expressions:

     (== abc (`symbol "abc"))
     (== (`symbol "+") +)         -- order doesn't matter
     (== 3174 (`symbol "3174")
     (== (`symbol "_%$`'""") _%$`'")

This expression representation for symbols allows for defining decimal
numbers, some higher-order definitions, and inequality between symbols,
which is not built-in.

Recall that a character string in single quotes within a sequence is
equivalent to writing the character symbols separately within the sequence,

   (... 'abc' ...)  ==  (... 'a' 'b' 'c' ...)  

and that a character string in double quotes represents a sequence of those
characters:

   "abc"  ==  ('abc')  ==  ('a' 'b' 'c')

See file <char.txt> for the expression representation for character symbols.
!}


2. Axiom Definition for Symbols

This section gives the few axioms needed for symbol definition.  We first want
to define our symbol atom using the following atom declaration (see file
<atom.txt>):

   (atom_defn `symbol "`symbol" symbol_atom).

This axiom generates the following predicate expressions

!  (atom `symbol)
!  (atom `symbol "`symbol")
!  (symbol_atom `symbol)

These expressions define the atom used for symbols and associate it with a
character string name, which is used in the <notequal.txt> file to define
inequality between distinct atoms.  Note that by using the symbol_atom
predicate, this file is the only file that needs to know what the symbol
atom actually is.

The set of symbols is defined by the following axiom:

   (symbol (%symatom %charstr))<
     (symbol_atom %symatom),
     (char_str %charstr).

Here we use the "symbol_atom" to avoid having to explicitly use the atom
`symbol.  (Maybe this is more trouble than its worth?!)


3. Some Basic Symbol Predicates

Appending a character string to the end of a symbol:
!  (sym_append <sym> <char_str> <sym+char_str>)
(actually we allow any expression to be appended)

Inserting character string at the front of a symbol:
!  (sym_insert <char_str> <sym> <char_str+sym>)

Concatenating two symbols:
!  (sym_concat <sym1> <sym2> <sym1+sym2>)

These predicates are defined in the following axiom:

   (Valid
       (sym_append (%symatom ($sym)) ($chars) (%symatom ($sym $chars)))
       (sym_insert ($chars) (%symatom ($sym)) (%symatom ($chars $sym)))
       (sym_concat (%symatom ($sym1)) (%symatom ($sym2))
                     (%symatom ($sym1 $sym2))))<
     (symbol_atom %symatom).    ! we "hide" the actual value of this atom!

It is also helpful to extract the character string from a symbol and to
map a character string to a symbol:

   (Valid
       (sym>chstr (%symatom %chstr) %chstr)
       (chstr>sym %chstr (%symatom %chstr)))<
     (symbol_atom %symatom).

Note that these predicates are just inverses of each other; however, we
define both since they may be used as functions.  (Perhaps better names would
be "sym_chstr" and "chstr_sym"?)


4. Ordering of Symbols

The default ordering relation < is only defined for "values" -- expressions
that represent real data elements such as numbers or characters, and symbols
are, in general, not values.  However, it may be useful to have a special
ordering relation "<symbol" that can apply to arbitrary symbols and
expressions formed from them.

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