! ho.ax.txt - higher-order forms to apply to other predicates
! (Some new predicates using those higher-order forms are defined.)
!---+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
!/
all_valid - all arguments are valid expressions
one_valid - at least one argument is a valid expression
valid - all arguments of conclusion expression are asserted as valid
axiom - an axiom is defined in a predicate
axioms - a set of axioms is defined in a predicate
((* <pred>) ..argseqs..) - predicate applies to each tuple of args from seqs
binary relation higher-order forms ...
def - define a synonym name for a predicate expression

*** h-o forms to generalize binary relations ...
heads - head elements of sequences in a sequence
((rev <binrel>) <arg1> <arg2>) - reverse args for a binary relation
head_fn - unary function to get head of a sequence
>len, >=len - reversed seq length comparison
((1* <binrel>) <arg1> <arg2s>) - rel applies to 1st arg and each arg2 elem
((*1 <br>) <arg1s> <arg2>) -          "         each arg1 elem and arg2
((** <br>) <arg1s> <arg2s>) -         "         each arg1/arg2 elem pair
((^1 <br>) <arg1s> <arg2>) - rel valid for at least one arg1 elem wrt arg2
((^* <br>) <arg1s> <arg2s>) - for each arg2 elem, at least 1 arg1 elem has rel
((1^ <br>) <arg1> <arg2s>) - rel valid for arg1 wrt at least one arg2
((*^ <br>) <arg1s> <arg2s>) - for each arg1 there is an arg2
((seq <br>) <seq>) - for each adj seq elems we have <ei> <br> <ei+1>
((seq* <br>) <seq>) - br applies between each ordered pair ei,ej from seq
   
*** h-o forms to generalize binary operations ...
(1* <binop>) - apply binop to arg 1 and arg 2 seq elems to get result seq 
(*1 <binop>) - apply binop to arg 1 seq elems and arg 2 to get result seq
distr1 - distribute arg 1 element as prepended heads of arg 2 seqs
distr - distribute arg 1 seq as prepended heads of arg 2 seqs
!\

! all_valid - all arguments are valid expressions

  (all_valid).
  (all_valid % $)< % , (all_valid $).

! one_valid - at least one argument is a valid expression

  (one_valid % $)< % .
  (one_valid % $)< (one_valid $).

! valid - all arguments of conclusion expression are asserted as valid

  % < (valid $1 % $2).     ! - could use 'in' here

! axiom - an axiom is defined in a predicate

  %conclu < (axiom %conclu $conds),
    (all_valid $conds).

! axioms - a set of axioms is defined in an axiom

  (axiom %conc $conds)<
    (axioms $1 (%conc $conds) $2).    

  ! *** Note that the 'axioms' predicate allows us to define axioms as "data"!

! * (map) - map a predicate to sequences of arguments
! - this only works where the predicate has a fixed number of arguments
!   (term for this??)

  ((* %pred) $nulls)<
    (copies () ($nulls)).
  !? also add this??  - ensures that nulls case matches possible arg count
    (%pred $args),
    (=len ($args) ($nulls)).    ! -- not really necessary

  ((* %pred) $argseqs')<
    ((* %pred) $argseqs),
    (%pred $args),
    (distr ($args) ($argseqs) ($argseqs')).
    ! *** Note that distr is a map of the prepend1 function!
    !     We thus need the form.ax distr def instead of ho.ax def below!
    !     (?? Should we have two distinct predicates here??)

! def - define a synonym name for a predicate expression
! (def %name %expr).

  (%name $args)<
    (def %name %expr),
    (%expr $args).

!---+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
! h-o forms to generalize binary relations ...

! heads - head elements of sequences in a sequence
! (1st arg is head elements of 2nd arg sequences)

  (def heads (* head)).

! ((rev <binrel>) <arg1> <arg2>) - reverse arg order for binary relation

  ((rev %binrel) %arg1 %arg2)<
    (%binrel %arg2 %arg1).
    
!/ examples:
  ((rev in) (a b) b)
  ((rev head) (a b c) a)
  ((rev last) c (a b c))
  ((rev tail) (b c) (a b c))
!\

! head_fn - unary function to get head of a sequence
! (This turns the head binary relation into a unary function.)

  (def head_fn (rev head)).

! >len, >=len - reversed arg 1, arg 2 sequence length comparison

  (def >len (rev <len)).
  (def >=len (rev <=len)).

! ((1* <binrel>) <arg1> <arg2s>) - rel applies to 1st arg and each arg2 elem

  ((1* %binrel) %arg1 ()).
  ((1* %binrel) %arg1 (%arg2 $arg2s))<
    (%binrel %arg1 %arg2),
    ((1* %binrel) %arg1 ($arg2s)).

!/ examples:
  ((1* in) x ((a x b) (c d x))   - arg1 elem in every arg2 seq
  ((1* head) a ((a b c) (a x)))   - same head elem in each arg2 seq
!\

! ((*1 <br>) <arg1s> <arg2>) - rel applies to each arg1 elem and arg2

  ((*1 %binrel) () %arg2).
  ((*1 %binrel) (%arg1 $arg1s) %arg2)<
    (%binrel %arg1 %arg2),
    ((*1 %binrel) ($arg1s) %arg2).

!/ examples:
  ((*1 in) (x y z) (a x b z c y)) - each arg1 elem in arg2 seq - all_in, subset
!\

! ((** <br>) <arg1s> <arg2s>) - rel applies to each arg1/arg2 elem pair
! ((*br <br>) ? - covered by 'map' above
  
  ((** %binrel) () %arg2s).
  ((** %binrel) (%1 $1) %arg2s)<
    ((1* %binrel) %1 %arg2s),
    ((** %binrel) ($1) %arg2s). 

!/ examples:
  ((** in) (b d) ((a b c d) (x d b y)))
!\

! ((^1 <br>) <arg1s> <arg2>) - rel valid for at least one arg1 elem wrt arg2

  ((^1 %binrel) %arg1 %arg2)<
    (in %1 %arg1),
    (%binrel %1 %arg2).

!/ examples:
  ((^1 in) (a b c d) (x c y))
!\

! ((^* <br>) <arg1s> <arg2s>) - for each arg2 elem, at least 1 arg1 elem has rel
!                               (not necessarily the same arg1)

  ((^* %binrel) ($1a %1 $1b) ())< 
    (%binrel %1 %2).            ! binary relation must have a domain?
  ((  ^* %binrel) %arg1 (%2 $2))<
    ((^1 %binrel) %arg1 %2),
    ((^* %binrel) %arg1 ($2)).
    
!/ examples:
  ((^* in) (c y) ((x y z) (a b c)))
!\

  ! *** Another possibly useful h-o <binrel> variation would be where
  !     at least one arg 1 elem has rel to each arg2 elem.
  !        ((^1 (1* <binrel>)) <arg1> <arg2>)   -- wrong?!?  -- fix!!!

! ((1^ <br>) <arg1> <arg2s>) - rel valid for arg1 wrt at least one arg2

  ((1^ %br) %arg1 %arg2s)<
    (in %2 %arg2s),
    (%br %arg1 %2).

!/ examples:
  ((1^ head) a ((u v) (a b c)))   - 'a' is head of one arg2 seq
!\

! ((*^ <br>) <arg1s> <arg2s>) - for each arg1 there is an arg2
!                               (not necessarily the same arg2)

  ((*^ %br) () ($2a %2 $2b))<
    (%br %1 %2).             ! binary relation must have a domain
  ((*^ %br) (%1 $1) %arg2s)<
    ((1^ %br) %1 %args2),
    ((*^ %br) ($1) %args2).

! binary relation folds into a sequence of elements ...
! (note that relation does not need to be reflexive)
! ((seq <br>) <seq>) - for each adj seq elems we have <ei> <br> <ei+1>

  ((seq %br) ())<
    (%br %1 %2).         ! binary relation must be defined
  ((seq %br) (%2))<
    (%br %1 %2).         ! singleton element must be right elem of a bin rel
  ((seq %br) (%1 %2 $))<
    (%br %1 %2),
    ((seq %br) (%2 $)).
  
! ((seq* <br>) <seq>) - br applies between each ordered pair ei,ej from seq

  ((seq* %br) ())<
    (%br %1 %2).
  ((seq* %br) (% $))<
    ((1* %br) % ($))<
    ((seq* %br) ($)).
    
!---+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
! *** h-o forms to generalize binary operations ***
! (<binop> <arg1> <arg2> <result>)

! (1* <binop>) - apply binop to arg 1 and arg 2 seq elems to get result seq 
! ((1* <binop>) <arg1> <arg2s> <results>)

  ((1* %binop) %1 () ()).
  ((1* %binop) %1 (%2 $2) (%r $r))<
    (%binop %1 %2 %r),
    ((1* %binop) %1 ($2) ($r)).

! (*1 <binop>) - apply binop to arg 1 seq elems and arg 2 to get result seq 
! ((*1 <binop>) <arg1s> <arg2> <results>)

  ((*1 %binop) () %2 ()).
  ((*1 %binop) (%1 $1) %2 (%r $r))<
    (%binop %1 %2 %r),
    ((*1 %binop) ($1) %2 ($r)).

! distr1 - distribute arg 1 element as prepended heads of arg 2 seqs

  (def distr1 (1* prepend1)).

! distr - distribute arg 1 seq as prepended heads of arg 2 seqs
! *** Note: we also have a non-h-o form.ax def since distr is used to
!     define the (* <pred>) higher-order map operation. 

  (def distr (* prepend1)).