! form.ax.txt - utility spec ax for "form" predicates
! These predicates deal with the structure of expressions, not really content.
!---+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
!/

===== sets =====
(<set> <elem>)
expr - element is an arbitary expression (which doesn't constrain an expr var)
seq - element is a sequence
- note that there can be no "atom" predicate in basic axiomatic language
singleton - element is sequence of one element
pair - element is sequence of two elements
twins - element is sequence of two of the same element
triple - element is sequence of three elements
- predicates for larger tuples may incorporate a decimal num in the pred name

===== binrel - binary relations =====
  (<binrel> <arg1> <arg2>)
== - the two arguments are identical
in - 1st arg is element in 2nd arg sequence
head (first) - 1st arg is head element of 2nd arg sequence
last - 2nd arg is last element of 1st arg sequence
tail - 2nd arg is tail of 1st arg sequence (everything but head)
ftail (front_tail) - 1st argument is everything but last elem of 2nd arg seq
prefix - 1st arg is prefix of 2nd arg sequence
suffix - 2nd arg is suffix of 1st arg sequence
substr - 1st arg is substring of 2nd arg sequence
subseq - 1st arg is ordered subset of 2nd arg seq elems (may have dups)
rotate - swap prefix/suffix of a sequence
reverse - 2nd arg sequence is reverse of 1st arg sequence
=len - both sequence arguments have the same length
<len - arg sequence lengths are ordered
<=len - <= ordering for arg sequence lengths
/=len - sequence lengths are unequal
partition - 2nd arg is a partition of 1st arg seq into non-null sequences
  ?? Should we have a partition_null pred that has empty seq partitions??
partition1 - partition 1st arg into singleton seqs for arg 2
partition2 - partition 1st arg into pair seqs for 2nd arg
powerset - arg 2 holds powerset sequences for arg 1 sequence
powerset_len - arg 2 holds powerset seqs for arg 1 seq, ordered first by len
copies - arg 2 sequence is zero or more copies of arg 1 expr
perm - 2nd arg sequence is a permutation of 1st arg sequence
transpose - transpose sequence of equal-length non-null sequences

===== binop - binary operations (functions) that yield a result =====
  (<binop> <arg1> <arg2> <result>)
  === also includes ternary relations ===
k-tuples - get all k-tuples from arg 2 element sequence, with k = arg 1 len
append1 - append one element to end of a sequence
prepend1 - prepend one element to front of a sequence
concat - concatenate two sequences
insert - insert expr at arbitrary position in sequence
distr - distribute arg 1 seq as prepended heads of arg 2 seqs

!\

! ===== sets =====
! (<set> <elem>)

! expr - element is an arbitary expression (which doesn't constrain an expr var)

  (expr %).

! seq - element is a sequence

  (seq ($)).
  ! - note that there can be no atom predicate in basic axiomatic language
  
! singleton - element is sequence of one element

  (singleton (%)).

! pair - element is sequence of two elements

  (pair (%1 %2)).

! twins - element is sequence of two of the same element

  (twins (% %)).

! triple - element is sequence of three elements

  (triple (%1 %2 %3)).

  ! - predicates for larger tuples may incorporate a decimal number in the name
  ! - =len gives tuples of specified length, with length given by other arg


! ===== binrel - binary relations =====
! (<binrel> <arg1> <arg2>)

! == (id) - the two arguments are identical

  (== % %).

! in (member) - 1st arg is element in 2nd arg sequence

  (in % ($1 % $2)).

! head (first) - 1st arg is head element of 2nd arg sequence

  (head % (% $)).

! last - 2nd arg is last element of 1st arg sequence

  (last ($ %) %).     ! - arg order? - this is a nice complement of head pred

! tail - 2nd arg is tail of 1st arg sequence (everything but head)

  (tail (% $) ($)).

! ftail (front_tail) - 1st argument is everything but last elem of 2nd arg seq
! -- better name needed!

  (ftail ($) ($ %)).
  
! prefix - 1st arg is prefix of 2nd arg sequence

  (prefix ($p) ($p $)).

! suffix - 2nd arg is suffix of 1st arg sequence

  (suffix ($ $s) ($s)).

! substr - 1st arg is (continguous) substring of 2nd arg sequence

  (substr ($) ($1 $ $2)).
  ! This can be used to get successive ordered pairs from a sequence

! subseq - 1st arg sequence is ordered subset of 2nd arg seq elems

  (subseq () ()).
  (valid (subseq ($sub) (% $seq))     ! some arg 2 elems omitted from arg 1
         (subseq (% $sub) (% $seq)))<
    (subseq ($sub) ($seq)).

! rotate - swap prefix/suffix of a sequence

  (rotate ($1 $2) ($2 $1)).

! reverse - 2nd arg sequence is reverse of 1st arg sequence

  (reverse () ()).
  (reverse ($ %) (% $r))<
    (reverse ($) ($r)).

! =len - both sequence arguments have the same length

  (=len () ()).
  (=len (%1 $1) (%2 $2))<
    (=len ($1) ($2)).

! <len - arg sequence lengths are ordered

  (<len () (% $)).
  (<len (%1 $1) (%2 $2))<
    (<len ($1) ($2)).

! <=len - <= ordering for arg sequence lengths

  (<=len () ($)).
  (<=len (%1 $1) (%2 $2))<
    (<=len ($2) ($2)).
	 
!/ or ...
  (<=len ($1) ($2))< (one_valid (<len ($1) ($2)) (=len ($1) ($2))).
!\

! /=len - sequence lengths are unequal

  (/=len %1 %2)< (one_valid (<len %1 %2) (<len %2 %1)).


! partition - 2nd arg is ordered partition of 1st arg seq into non-null seqs

  (partition () ()).      ! empty arg 1 sequence has empty partition
  (partition (% $) ((%) $prtn))<     ! added elem may be new partition
    (partition ($) ($prtn)).
  (partition (% $) ((% $p) $prtn))<  ! ... or may go into 1st partition
    (partition ($) (($p) $prtn)).

  ! ?? Should we have a partition_null pred that allows empty seq partitions??
  
! partition1 - partition 1st arg into singleton seqs for 2nd arg

  (partition1 () ()).
  (partition1 (% $) ((%) $prtn))<
    (partition1 ($) ($prtn)).
    
! partition2 - partition 1st arg into pair seqs for 2nd arg
! (if 1st arg seq has odd length, last partition set element is singleton)

  (parrition2 () ()).         ! even # arg 1 elements
  (partition2 (%) ((%))).     ! odd # arg 1 elements
  (partition2 (%1 %2 $) ((%1 %2) $prtn))<
    (partition2 ($) ($prtn)).

! powerset - arg 2 holds power set sequences for arg 1 sequence
! (element order is preserved)

  (powerset () (()).
  (powerset (% $) ($pow $%pow))<
    (powerset ($) ($pow)),
    ((1* prepend1) % ($pow) ($%pow)).
!or (distr1 % ($pow) ($%pow)).

  ! - ordering of power set:
  !  (powerset () (()))
  !  (powerset (a) (() (a)))
  !  (powerset (a b) (() (b) (a) (a b)))
  !  (powerset (a b c) (() (c) (b) (b c) (a) (a c) (a b) (a b c)))
  !          ...
  !  - last element cycles fastest
  !
  ! - other orderings - by increasing lengths, 1st cycles fastest?

[! powerset_len - arg 2 holds powerset seqs for arg 1 seq, ordered first by len]
! powerset_len arg 2 holds power set sequence for arg 1 elements
! (powersets are ordered first by length, then by element order)

  (powerset_len %elems %pset)<       ! powerset subsets ordered by length 0..k
    (powerset_lenX %elems %elems %pset).   ! k is len of elem seq
  ! - note that first powerset is () and last is entire seq of elems
  
  (powerset_lenX () ($elems) (())).   ! zero-len powerset subset is just ()
  (powerset_lenX (%l $l) %elems ($psubs $ktups))<  ! pwrset subsets thru len k+1 
    (powerset_lenX ($l) %elems ($psubs)),    ! powerset subsets thru len k
    (k-tuples (%l $l) %elems ($ktups)).     ! len k+1 tuples from elems set

! copies - arg 2 sequence is zero or more copies of arg 1 expression

  (copies % ()).
  (copies % (% $))<
    (copies % ($)).

! perm - 2nd arg sequence is a permutation of 1st arg sequence

  (perm () ()).
  (perm (% $) ($1 % $2))<
    (perm ($) ($1 $2)).
  
! transpose - transpose sequence of equal-length non-null sequences
! ?? generalize to null or non-equal-length sequences?  - not for now

  (transpose %nulls ())<     ! unknown # rows, 0 columns
    (copies () %nulls).
  (transpose %rows' (%col $cols))<  ! insert new col at front of rows
    (transpose %rows ($cols)),
    (distr %col %rows %rows').


! ===== binop - binary operations (functions) that yield a result =====
!       -- can also be ternary relations --
! (<binop> <arg1> <arg2> <result>)

! k-tuples - get all k-tuples from arg 2 elem seq, with k = arg 1 len
! - tuples are ordered by element sequence order

  (k-tuples () ($e) (())).       ! only 1 0-len tuple for any elem seq
  (k-tuples ($l) ($e) (($e)))<   ! only 1 k-tuple from k-elem seqtup
    (=len ($l) ($e)).            !  -- needed??
  (k-tuples %l %e ())<           ! no k-tuples longer than elem seq
    (>len %l %e).
  (k-tuples (%l $l) (%e $e) ($etups $tups))<  ! %e k-tups + $e k-tups
    (k-tuples ($l) ($e) ($k--tups)),    ! get k-- tuples from $e elems
    ((1* prepend) %e ($k--tups) ($etups)),  ! prepend %e to get %e k-tups
    (k-tuples (%l $l) ($e) ($tups)).     ! get k-tups without leading %e
    ! - Note that tuples have element order

!/ example axiom instances:

  (k-tuples () () (())).
  (k-tuples () (%e0) (())).
  (k-tuples () (%e1 %e0) (())).
  (k-tuples () (%e2 %e1 %e0) (())).
          ...
  (k-tuples () () (())).
  (k-tuples (%l0) (%e0) ((%e0))).
  (k-tuples (%l1 %l0) (%e1 %e0) ((%e1 %e0))).
  (k-tuples (%l2 %l1 %l0) (%e2 %e1 %e0) ((%e2 %e1 %e0)))
           ...
  (k-tuples (%l0) () ()).
  (k-tuples (%l1 %l0) () ()).
  (k-tuples (%l1 %l0) (%e0) ()).
          ...

  (k-tuples (%l0) (%e0) ((%e0)))<  - $etups = '(%e0)' $tups = ''
    (k-tuples () () (()),
    ((1* prepend) %e0 (()) ((%e0))),
    (k-tuples (%l0) () (())).

  (k-tuples (%l0) (%e1 %e0) ((%e1) (%e0)))<  - $etups = '(%e1)' 2tups = '(%e0)'
    (k-tuples () (%e0) (())),
    ((1* prepend) %e1 (()) ((%e1))),
    (k-tuples (%l0) (%e0) ((%e0%))).

  (k-tuples (%l0) (%e2 %e1 %e0) ((%e2) (%e1) (%e0)))<
         - $etups = '(%e2)' $tups = '(%e1) (%e0)'
    (k-tuples () (%e1 %e0) (())),
    ((1* prepend) %e2 (()) ((%e2))),
    (k-tuples (%l0) (%e1 %e0) ((%e1) (%e0))).
            ...

  (k-tuples (%l1 %l0) (%e1 %e0) ((%e1 %e0)))<
         - $etups = '(%e1 %e0)' $tups = ''
    (k-tuples (%l0) (%e0) ((%e0))),
    ((1* prepend) %e1 ((%e0)) ((%e1 %e0))),
    (k-tuples (%l1 %l0) (%e0) ()).

  (k-tuples (%l1 %l0) (%e2 %e1 %e0) ((%e2 %e1) (%e2 %e0) (%e1 %e0)))<
         - $etups = '(%e2 %e1) (%e2 %e0)' $tups = '(%e1 %e0)'
    (k-tuples (%l0) (%e1 %e0) ((%e1) (%e0))),
    ((1* prepend) %e2 ((%e1) (%e0)) ((%e2 %e1) (%e2 %e0))),
    (k-tuples (%l1 %l0) (%e1 %e0) ((%e1 %e0))).

  (k-tuples (%l1 %l0) (%e2 %e1 %e0)
              ((%e3 %e2) (%e3 %e1) (%e3 %e0)     - ($etups
               (%e2 %e1) (%e2 %e0) (%e1 %e0)))<     $tups)
    (k-tuples (%l0) (%e2 %e1 %e0) ((%e2) (%e1) (%e0))),
    ((1* prepend) %e3 ((%e2) (%e1) (%e0)) ((%e3 %e2) (%e3 %e1) (%e3 %e0))),
    (k-tuples (%l1 %l0) (%e2 %e1 %e0) ((%e2 %e1) (%e2 %e0) (%e1 %e0))).
            ...
!\

! append1 - append one element to end of a sequence

  (append1 ($) % ($ %)).
  
! prepend1 - prepend one element to front of a sequence

  (prepend1 % ($) (% $)).
  
! concat - concatenate two sequences

  (concat ($1) ($2) ($1 $2))

! insert - insert expr at arbitrary position in sequence

  (insert %x ($1 $2) ($1 %x $2)).

! distr - distribute arg 1 seq as prepended heads of arg 2 seqs

  (distr () () ()).
  (distr (%h $h) (($) $seqs) ((%h $) $seqs'))<
    (distr ($h) ($seqs) ($seqs')).