! atom.ax.txt - atom "declarations" and "non-identicallity" predicates!
!/
  - The non-identicallity of distinct atoms and of atoms & sequences makes
    use of the bit-expression inequality operator '<>' in bit.ax which
    applies to distinct character strings.
  - Defining atom inequality is helpful since axiomatic language has no
    built-in predicate.  (Actually, we can do ok with just bit expr
    inequality, but I suspect the increased generality will come in handy.)
  - A "declaration" of an atom associates it with its symbol char string
    (but note that this is not a built-in feature of axiomatic language!).
  uses form.ax, ho.ax, bit.ax

  ***** Is there ever a reason for *NOT* "declaring" an atom??? *****
  -- Perhaps you don't want some special atoms to be included in
     "arbitrary data" collections!
  
  We also define predicates based on the inequality of atoms.

!/ predicate index:
 (atom _atom _atomcstr) - "declaration" of an atom (linked to it symbol ch str)
 (atom _atom) - set of declared atoms
 (atoms (_atom_) (_atomsym_)) - "declare" groups of atoms in one expr
 (~== _atom0 _atom1) - distinct declared atoms are non-identical
 (~== _atom _seq), (~== _seq _atom) - declared atoms and seqs are non-identical
 // old ...  -- no longer applicable --
  - *** Note that ~== has already been defined for bit expr inequality.
  - This means all the inequality predicates of bit.ax are now generalizd!
 \\

--- basic negative predicates defined from non-identical exprs:
  ~in - element not-in a sequence (based on bit inequality)
  ~in> - element not in domain of finite map
  distinct - all elements of a sequence are bit-distinguishable
  dup_elim - eliminate duplicate elements from a sequence (=> bit distinct)
  sort - 2nd arg is ordering of first arg elements, given <= relation
  all_in - all arg 1 elements are 'in' arg 2 sequence
z  some_in - at least one arg 1 elem is 'in' arg 2 sequence
  none_in - no arg 1 elem is 'in' arg 2 sequence
z  some_/in - at least one arg 1 elem is not-in arg 2 sequence
  subset - arg 1 is subset of arg 2
z  ~subset - arg 1 is not subset of arg 2

===== negative (expr-distinguishable) binary relations =====
 ~pre - arg 1 sequence is not a prefix of arg 2 sequence
 ~suf - arg 2 sequence is not a suffix of arg 1 sequence

 ===== bit-distinguishable binary operations ...
 add_elem - append an element to a set if not already there
 union - union of set-seqs of bit distinguishable elements
intersect - intersection of set-seqs of bit distinguishable elements
difference - difference of set-seqs of bit distinguishable elements

--- tbd:
  (merge <seq1> <seq2> <merged>)  - merge ordered sequences (given bit ordering)
  (merge_op <<op> <=op> <seq1> <seq2> <merged>)  - merge given ordering ops
  (sort <seq> <ordered_seq>)   - sort a sequence of elements based on bit <
  (sort_op <<op> <=op> <seq> <ordered_seq>)  - sort given ordering ops
  (par_sort (<keys> ..data..) (<keys'> ..data'..))  - parallel-sort data seqs

  (in_ <x> <seq>)  - expr in sequence, but only one solution
    - [only_]one_in or unique_in

  (prefix (..x..) <x> (..))  - bit expr prefix up to <x>
  (remove <expr> <seq> <seq-expr>)   - remove 1st occurrence of expr from seq
  (dup_elim <seq> <seq'>)  - elim duplicate exprs in seq, keeping first occur
  (dup_elim_front <seq> <seq'>)  - elim dupl exprs in seq, keeping last occur

  ((subst %ex? %ex') <ex> <ex'>)  - replace <ex> with <ex'> if == <ex?>
  ((replace %ex? %ex') <ex> <ex'>)  - replace <ex> with <ex'> if matches <ex?>
  (replace_head <seq> <h?> <h!> <seq'>)  - replace head of sequence if match

for eval.ax:
  not_member < /in
  char_string < charseq
  -- also see eval.ax utilities:
    member?, ==?, prefix?, <num?, <=num?, /=num? - do Boolean tests
    and, or, not - Boolean operations
 



----+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8

! (atom _atom _atomcstr) - atom with its symbol char str minus leading ` 
!  - this valid expr exists for all "declared" atoms
!    (Atom is associated with its symbol name as a char string.)

! (atom _atom) - a "declared" atom
!  - this valid expr derives from the atom declaration expr

  (atom %atom)< (atom %atom %atomcstr).   ! atom has been declared

! (atoms (_atom_) (_atomcstr_)) - used to declare multiple atoms in one expr
!  - _atom_ and _atomcstr_ sequences have same length so atoms and cstrs
!     are paired 1-to-1

  (atoms (`  `0  `1 )
         ("" "0" "1")).    ! "declaration" of "used" atoms so far

  (atom %atom %atomcstr)< (atoms ($prea  %atom     $sufa)     ! atom group
                                 ($preas %atomcstr $sufas))<  ! char strings
     (*=l (($prea) ($sufa)) (($preas) ($sufas))).
        ! - corresponding prefixes & suffixes are equal length!

! ~== - inequality between distinct atoms and between atoms & sequences
! - we use the bit expression inequality predicate <>
! - Note that identical exprs, including identical atoms, always have the
!   (== % %) relation.

  (~== %atom0 %atom1)<              ! two distinct atoms are non-identical
    (atom %atom0 %atomcstr0),
    (atom %atom1 %atomcstr1),
    (<> %atomcstr0 %atomcstr1).     ! bit inequality gives cstr inequality

  (val (~== %atom ($)) (~== ($) %atom))<   ! atom & sequence are non-identical
    (atom %atom).



! ======= negative predicates based on non-identical expressions (~==)

! ~in - expr not-in a sequence

  (~in %x ()).
  (~in %x (% $))< (~== %x %), (/in %x ($)).
 !or
  (def ~in /~==).

! ~in> - expr x' not in domain of finite map (..(x y)..)

  (~in> %x' ()).
  (~in> %x' ((%x %y) $x>y))<
    (~== %x' %x),
    (~in> %x' ($x>y)).

! distinct - all exprs of a sequence are distinct

z (def distinct (seq* ~==)).  ! non-identical rel applies between all ex pairs
Z!or

  (distinct ()).     ! empty sequence has no identical elements
  (distinct (%x $x))<
    (~in %x ($x)),       ! new x is distinct from rest of sequence
    (distinct ($x))      ! rest of sequence is also distinct

! dup_elim - eliminate duplicate exprs from a sequence (keeping 1st occurrence)

! (dup_elim _seq _seq_w_no_duplications)  - keeping 1st occurrence
! - Note that we keep the original element order.

  (dup_elim () ()).
  (dup_elim ($seq %x1) ($seqnd %x1))<   ! 1st occur of a new elem
      ! - appended to both orig seq and seq with no dups
    (~in %x1 ($seqnd)),            ! (1st occurrence of x1)
    (dup_elim ($seq) ($seqnd)).    ! seq dups have already been eliminated
  (dup_elim ($seq %x) %seqnd)<     ! expr has already occurred
      ! - appended to orig seq but not to seq with no dups
    (in %x ($seqnd)),              ! (expr has already occurred)
    (dup_elim ($seq) %seqnd).

!/ tbd:
! all_in - all arg 1 elements are 'in' arg 2 sequence

  (def all_in /in).

!z some_in - at least one arg 1 elem is 'in' arg 2 sequence

!z  (def some_in (^1 in)).

! none_in - no arg 1 elem is 'in' arg 2 sequence

  (def none_in (*1 /in)).

!z some_~in - at least one arg 1 elem is not-in arg 2 sequence

!z  (def some_~in (^1 /in)).

! subset - arg 1 is subset of arg 2 (synonym of all_in)
! (All arg 1 elements are in arg 2 - duplicates ok.)
! (Both substr and subseq imply subset, but not the inverse.)

  (def subset all_in).

  ! -- Do we need this since it is identical to all_in??

!z ~subset - arg 1 is not subset of arg 2 (synonym of some_/in)
!z (At least one arg 1 element is not in arg 2.)

!z  (def ~subset some_~in).

  ! -- Do we need this, too??
!\

!/
! ======== negative (bit-distinguishable) binary relations ========

! ~pre - arg 1 sequence is not a prefix of arg 2 sequence

  (~pre (%x $x) ()).
  (~pre (%x $x) (%h $t))<
    (~== %x %h).
  (~pre (%x $x) (%h $t))<
    (~pre ($x) ($t)).

! ~suf - arg 2 sequence is not a suffix of arg 1 sequence

  (~suf () ($x %x)).
  (~suf ($f %l) ($x %x))<
    (~== %l %x).
  (~suf ($f %l) ($x %x))<
    (~suf ($f) ($x)).

! ======== bit-distinguishable binary operations ========

! add_elem - append an element to a sequence set if not already there

  (add_elem ($set) %x ($set))<     ! already there - not added
    (in %x ($set)).
  (add_elem ($set) %x ($set %x))<   ! not already there - added
    (~in %x ($set)).
  ! - equivalent to (union %set (%x) %set') except arg 1 set dups not eliminated

! union - union of set-seqs of bit distinguishable elements
! (Arguments may have duplications, but result does not.  Result element
!  order is order of arg 1 set, then arg 2 set.)

  (union ($set1) ($set2) %union)<
    (dup_elim ($set1 $set2) %union).
  ! -- note that union order is 1st occurrence in arg 1, then arg 2

! intersection - intersection of set-seqs of bit distinguishable elements
! (arguments may have duplications, but result does not)
! (order of intersection is arg 1 order)

  (intersection () ($set2) ()).
  (intersection ($set1 %1) %set2 %iset')<
    (intersection ($set1) %set2 %iset),
    (in %1 %set2),               ! new element also in set 2
    (add_elem %iset %1 %iset').  ! append shared elem if not already there
  (intersection ($set1 %1) %set2 %iset)<
    (intersection ($set1) %set2 %iset),
    (~in %1 %set2).          ! new element not in set 2, so not in intersection

! difference - difference of set-seqs of bit distinguishable elements
! (arguments may have duplications, but result does not)
! (order of difference is arg 1 order)

  (difference () ($set2) ()).
  (difference ($set1 %1) %set2 %dset')<
    (difference ($set1) %set2 %dset),
    (~in %1 %set2),              ! new element not in set 2
    (add_elem %dset %1 %dset').  ! append difference elem if not already there
  (difference ($set1 %1) %set2 %dset)<
    (difference ($set1) %set2 %dset),
    (in %1 %set2).            ! new element is in set 2, so not in difference

! *** "Bag" operations could be interesting!


!/ ====== to be done:


! --- Merge sort based on bit ordering ---

! merge - merge ordered sequences into ordered sequence (based on <,<=)

  (merge () () ()).         ! merge of empty sequences gives empty seq
  (merge (% $) () (% $)).   ! if one seq empty, merge is just the other
  (merge () (% $) (% $)).
  (merge (%1 $1) (%2 $2) (%1 $))<   ! choosing head of 1st seq
    (<= %1 %2),
    (merge ($1) (%2 $2) ($)).
  (merge (%1 $1) (%2 $2) (%2 $))<   ! choosing head of 2nd seq
    (< %2 %1),
    (merge (%1 $1) ($2) ($)).
  ! Note that if heads identical, 1st sequence head gets chosen.

! merge_op - merge ordered seqs into ordered seq (using specified ops)

  (merge_op %< %= () () ()).        ! merge of empty sequences gives empty seq
  (merge_op %< %= (% $) () (% $)).  ! if one seq empty, merge is just the other
  (merge_op %< %= () (% $) (% $)).
  (merge_op %< %= (%1 $1) (%2 $2) (%1 $))<  ! choosing head of 1st seq
    (one_valid (%< %1 %2) (%= %1 %2)),      ! (1st head < or equivalent to 2nd)
    (merge_op %< %= ($1) (%2 $2) ($)).
  (merge_op %< %= (%1 $1) (%2 $2) (%2 $))<  ! choosing head of 2nd seq
    (< %2 %1),                              ! (2nd head < 1st)
    (merge_op %< %= (%1 $1) ($2) ($)).
  ! Note that if heads equivalent, 1st sequence head gets chosen.

! sort - (merge) sort a sequence based on bit ordering

  (sort () ()).
  (sort (%) (%)).
  (sort (%0 %1 $) %sorted)<
    (split (%0 %1 $) %half1 %half2),    ! split seq into halves
    (sort %half1 %sorted1),             ! sort each half
    (sort %half2 %sorted2),
    (merge %sorted1 %sorted2 %sorted).  ! merge the sorted halves

! sort_op - (merge) sort a sequence based on specified <,= ordering operations

  (sort_op %< %= () ()).
  (sort_op %< %= (%) (%)).
  (sort_op %< %= (%0 %1 $) %sorted)<
    (split (%0 %1 $) %half1 %half2),     ! split seq into halves
    (sort_op %< %= %half1 %sorted1),     ! sort each half
    (sort_op %< %= %half2 %sorted2),
    (merge_op %< %= %sorted1 %sorted2 %sorted).  ! merge the sorted halves

! par_sort - parallel sort data sequences based on sort of keys

  (par_sort %null_seqs %null_seqs)<   ! if key/data seqs null, nothing done
    (null_seqs %null_seqs).
  (par_sort (%keys $data) (%keys' $data'))<  ! seqs are non-empty
    (transpose (%keys $data) %seqs),     ! merge keys and data into sequences
    (sort_op <1 =1 %seqs %seqs'),        ! sort sequences based on keys
    (transpose %seqs' (%keys' $data')).  ! get sorted keys and data sequences

! prefix -- function returns sequence prefix up to a terminating expression
! - no solution if terminating prefix not present

  (prefix (%x $) %x ()).       ! terminating expr at front of sequence
  (prefix (% $1) %x (% $2))<
    (/= % %x),                 ! prefix consists of non-%x expressions
    (prefix ($1) %x ($2)).

! prefix? -- test if one string is a prefix of another, returning true/false
!   -- see eval.ax

! remove - remove first occurrence of an expression from a sequence
! - no solution if expression not present

  (remove %x (%x $) ($)).
  (remove %x (% $) (% $'))<
    (/= %x %),
    (remove %x ($) ($')).

! dup_elim - eliminate duplicate exprs in a sequence, keeping first occurrence

  (dup_elim %seq %unique)<
    (reverse %seq %seq_rev),
    (dup_elim_front %seq_rev %unique_rev),
    (reverse %unique_rev %unique).

! dup_elim_front - elim duplicate exprs from front of seq, keeping last occur

  (dup_elim_front () ()).
  (dup_elim_front (% $) ($'))<   ! dupl expr not included
    (in_ % ($)),                 ! head expr occurs in seq tail
    (dup_elim_front ($) ($')).
  (dup_elim_front (% $) (% $'))<  ! unique expr is included
    (/in % ($)),                 ! head expr does not occur in seq tail
    (dup_elim_front ($) ($')).

! subset - a sequence is a subset of another
! (The subset may have multiple occurrences of an element.)

  (subset () ($set)).      ! empty set is a subset
  (subset (% $) %set)<     ! adding element to subset
    (in_ % %set),          ! new element is set member (single solution)
    (subset ($) %set).

! /subset - sequence is not a subset of another

  (/subset (%x $) %set)<
    (/in %x %set).          ! element not member of set
  (/subset (% $) %set)<
    (in_ % %set),           ! (we want just a single solution)
    (/subset ($) %set).


! replace - replace an expression if matched to another
! ((replace %ex? %ex') <ex> <ex'>)   - replace <ex> with <ex'> if == <ex?>
! - note that substitution parameters are incorporated into predicate name expr

  ((replace %ex? %ex') %ex? %ex').   ! arg expr is matched, replacement done

  ((replace %ex? %ex') %ex %ex)<     ! no match, no replacement
    (/= %ex? %ex).

! replace_head - replace head of sequence if match
! (replace_head <seq> <h?> <h'> <seq'>) - replace head of sequence if match

  (replace_head (%h1 $tail) %h? %h' (%h2 $tail))<
    ((replace %h? %h') %h1 %h2).
                                                              322,1         Bot
!\
                                                              303,1         93%