! ho.ax.txt - specification axioms for higher-order forms
! (Many of these are FP-style higher-order functional forms.
! See [Backus 1978: Can programming be liberated from ..."])
! uses: form.ax
!/
   fp function format in AL:

      (_f _arg _result)    -- always 1-argument function

   functional forms are used to combine functions into larger functions.
   In these axiomatic language functional higher-order forms, the functions
   have zero-or-more input arguments and 1 result output arg:

     (_f _iarg0 .. _iargn-1 _res)

index:
 (all_valid .. _ve ..) -   e xpressions in list are valid exprs
 (one_valid .. _e _ve _e ..) - at least one expression in list is valid
 (valid .. _e ..) - generate multiple valid exprs from a single expr
 (axiom _conc .._cond ..) - define an axiom in a single expression
 (axioms .. _ax ..) - define multiple axioms from a single expression
 (ax _ax_ `< _cond_) - define multiple axioms with shared conditions
 (def _name _expr) - define a name for a predicate/function expression
 (* _p)  - apply pred to seq of tuples formed from argument sequences
 ((_f_) _iargs_ _res) - l-to-r fn composition on >=0 input args giving result
 dup  - duplicate the first input arg in a function composition
 swap  - swap the first two input args in a function composition

=== h-o forms for binary relations/functions:
 ((bun _b) _args_) - apply bin rel/fn to a pair of args (make rel/fn unary)
 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
 ((.* _binrel) _arg1 _arg2s) - rel aplies to 1st arg and each arg2 elem
 ((*. _br) _arg1s _arg2) -        "       to each arg1 elem and arg2
 ((.* _binfn) _arg1 _arg2s _ress) - apply fn to 1st arg and each arg2 elem
 ((*. _bf) _arg1s _arg2 _ress) -         "   to each arg1 elem and arg2
 ((** _br) _arg1s _arg2s) - apply rel to each arg1/arg2 elem pair
 ((^. _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
 ((seq _br) _seq) - for adjacent seq elems we have _ei _br _ei+1
 ((seq* _br) _seq) - br applies between each ordered pair ei,ej from seq
!\
!---+----1----+----2----+----3----+----4----+----5----+----6---+----7----+----8

! all_valid - combine valid expressions into single expression

  (all_valid).
  (all_valid % $)< % , (all_valid $).
     ! -- all expressions in list are valid

! one_valid - assert that at least one expression in list is valid

  (one_valid $1 % $2)< % .
     ! -- (at least) one expression in list is a valid expr

! valid - generate multiple valid expressions from a single expression

  % < (valid $1 % $2).

! axiom - represent an axiom in a single expression
! (axiom <conclu> <cond1> .. <condn>)

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

! axioms - generate a set of axioms from a single expression

  (axioms $axiom)< (axiom_set $1 ($axiom) $2).

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

! ax - define multiple axioms with shared conditions
! (ax (<conc> <cond> .. <cond>) .. (<conc> <cond> .. <cond>)
!     `< <cond> .. <cond>)      -- shared conditions

  (axiom %conclu $conds $shared_conds))<
    (ax $ax1 (%conclu $conds) $ax2 `< $shared_conds).
    ! -- no shared condition can be a `< atom  

  ! examples? - application?

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

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

! ((* _p) .. _argseq ..) - map pred to arg tuples from seqs

  ((* %pred) $nulls)<
    (copies () ($nulls)).
  ((* %pred) $argseqs')<
    (%pred $args),
    ((* %pred) $argseqs),
    (distr ($args) ($argseqs) ($argseqs')).

  ! *** Note that distr is a map of the prepend1 function!
  !     (But that means we need distr in order to define distr!
  !      So we will use the form.ax definition.)

  ! - This also works to map a function to sequences of input arguments,
  !   yielding a sequence of results.

  ! Alternative to be defined!:
  !   Define convention where * is appended or prepended to the predicate
  !   name symbol to denote this mapping operation!  - to be defined


! ((_f_) _iarg_ _res)  - composition of fns on >=0 input args giving result
!  - functions are evaluated in left-to-right order

  (() %arg %arg).  ! empty function seq is identity fn with 1 input arg
  ((%f $f) $iarg1 $iarg %res)<
    (%f $iarg1 %res1),       ! appl of first fn on its inputs
    (($f) %res1 $iarg %res).  ! appl of rest of fn seq

! dup - duplicate the first input arg in a function composition

  ((dup $f) %iarg0 $args)<
    (($f) %iarg0 %iarg0 $args).
 
 swap  - swap the first two input args in a function composition

  ((swap $f) %iarg0 %iarg1 %args)<
    (($f) %iarg1 %iarg0 $args).
    

!---+----1----+----2----+----3----+----4----+----5----+----6---+----7----+----8
! =========== higher-order forms for binary relations & functions ===========

! ((bun _b) _args_) - apply bin rel/fn to a pair of args (make rel/fn unary)

  ((bun %br) (%arg1 %arg2))<   ! binary relation becomes unary
    (%br %arg1 %arg2).

  ((bun %bf) (%iarg1 %iarg2) %res)<  ! binary fn (binop) becomes unary
    (%bf %iarg1 %iarg2 %res).

! 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))
!\

! ((rev _binfn) _arg1 _arg2 _res) - reverse arg order for binary function

  ((rev %binfn) %arg1 %arg2 %res)<
    (%binfn %arg2 %arg1 %res).

!/ examples:
  ((rev append1) c (a b) (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)).

! ((.* _binrel) _arg1 _arg2s) - rel applies to 1st arg and each arg2 elem

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

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

! ((*. _br) _arg1s _arg2) - rel applies to each arg1 elem and arg2

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

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

! ((.* _binfn) _arg1 _arg2s _ress) - apply fn to 1st arg and each arg2 elem

  ((.* %binfn) %arg1 () ()).
  ((.* %binfn) %arg1 (%arg2 $arg2s) (%res $ress)<   ! return seq of results
    (%binfn %arg1 %arg2 %res),    ! bin fn maps two input args to a result
    ((.* %binfn) %arg1 ($arg2s) ($ress).

!/ example:
  ((.* append1) (a b) (x y) ((a b x) (a b y)))
!\

! ((*. _bf) _arg1s _arg2 _ress) - apply fn to each arg1 elem and arg2

  ((*. %bf) () %arg2 ()).
  ((*. %bf) (%arg1 $arg1s) %arg2 (%res $ress))<   ! return seq of results
    (%bf %arg1 %arg2 %res
    ((*. %bf) ($arg1s) %arg2 ($ress).

!/ examples:
  ((*. prepend) (1 2) (u v) ((1 u v) (2 u v)))
!\

! ((** _br) _arg1s _arg2s) - rel applies to each arg1/arg2 elem pair
! ((*br _br) ? - covered by 'map' above
   ??? - probably easily defined from other h-o forms!
  
  ((** %br) () %arg2s).
  ((** %br) (%1 $1) %arg2s)<
    ((.* %br) %1 %arg2s),
    ((** %br) ($1) %arg2s). 

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

! ((^. _br) _arg1s _arg2) - rel valid for at least one arg1 elem wrt arg2

  ((^. %br) %arg1s %arg2)<
    (in %1 %arg1s),
    (%br %1 %arg2).

!/ examples:
  ((^. 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 elem)

  ((^* %br) ($1a %1 $1b) ())< 
    (%br %1 %2).            ! binary relation must have a domain?
  (  (^* %br) %arg1s (%2 $2))<
    ((^. %br) %arg1s %2),
    ((^* %br) %arg1s ($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.
  !        ((^. (.* <binrel>)) <arg1> <arg2>)   -- wrong?!?  -- fix!!!

! ((.^ _br) _arg1 _arg2s) - rel valid for arg1 wrt at least one arg2

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

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

! ((*^ _br) _arg1s _arg2s) - for each arg1 there is an arg2 elem
!                            (not necessarily the same arg2 elem)

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

! binary relation folds into a sequence of elements ...
! (note that relation does not need to be reflexive)
! ((seq _br) _seq) - for each adjacent 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) (% $))<
    ((.* %br) % ($))<
    ((seq* %br) ($)).



! ================ old: =================



! constr - apply sequence of functions to same argument giving seq of results

  ((constr) %arg ()).
  ((constr %f $f) %arg (%res $res))<
    (%f %arg %res),
    ((constr $f) %arg ($res)).

! filter - apply boolean pred to each element of sequence, keeping true values
! ((filter <pred>) <seq> <seq'>) - <seq'> is subset of <seq> where <pred> is `t
! (<pred> <expr> <`t/`f>) - true/false predicate on an expression

  ((filter %pred) () ()).
  ((filter %pred) (%elem $elems) (%elem $elems'))<
    (%pred %elem `t),
    ((filter %pred) ($elems) ($elems')).
  ((filter %pred) (%elem $elems) ($elems'))<
    (%pred %elem `f),
    ((filter %pred) ($elems) ($elems')).

   ! -- use higher-order form for the shared condition?

!/ old:

  (filter %pred () ()).
  (filter %pred (%elem $elems) (%elem $elems'))<
    (%pred %elem `t),
    (filter %pred ($elems) ($elems')).
  (filter %pred (%elem $elems) ($elems'))<
    (%pred %elem `f),
    (filter %pred ($elems) ($elems')).

! or ...

  (filter ($pred) () ()).             ! pred may include "constant" args
  (filter ($pred) (%elem $elems) (%elem $elems'))<
    ($pred %elem `t),
    (filter ($pred) ($elems) ($elems')).
  (filter ($pred) (%elem $elems) ($elems'))<
    ($pred %elem `f),
    (filter ($pred) ($elems) ($elems')).

   ! -- $pred may represent boolean function plus some "constant" parameters

! -- Is there another string-vs-expr var notation that is nicer here???
!\

! repeat - repeat 0 or more function applications

  ((repeat %f) % %).             ! 0 evaluations is identity function
  ((repeat %f) %arg %result')<   ! n+1 evaluations
    ((repeat %f) %arg %result),    ! n evaluations
    (%f %result %result').         ! one more evaluation

! partial - turn multi-argument function into a single argument function
!   by including the initial arguments as part of the function
! ("partial evaluation")

  ((partial %f $initial_args) %last_arg %res)<
    (%f $initial_args %last_arg %res).

! min - get element from sequence with minimum function result value
! - function result is a natural number

  ((min %fnat) (%elem) %elem).     ! if just one value, that's the min
  ((min %fnat) (% $) %)<           ! first element is new minimum
    (%fnat % %n0),
    ((min %fnat) ($) %min),
    (%fnat %min %n1),
    (<=num %n0 %n1).
  ((min %fnat) (% $) %min)<        ! first element is not new minimum
    (%fnat % %n0),
    ((min %fnat) ($) %min),
    (%fnat %min %n1),
    (<=num %n1 %n0).
  ! -- Note that definition is ambiguous if new element value same as min.
  !    Thus the function nondeterministically picks any minimum element.

 ! -- use higher-order form for the common conditions:

   (ax (((min %fnat) (% $) %) (<=num %n0 %n1))
       (((min %fnat) (% $) %min) (<=num %n1 %n0))
    `< (%fnat % n0)
       ((min %fnat) ($) %min)
       (%fnat %min %n1)
   ).

! define_func - define a name for a (single-argument) function expression

  (%name %arg %res)<
    (define_func %name %fn_expr),
    (%fn_expr %arg %res).

!/


! generalize - generalize certain associative binary operators with an identity
! -- We generalize operator to >2 arguments and to a sequence of >=0 args.

  (%binop %arg1 %arg2 $args %arg' %result')<     ! >2 arguments
    (generalize %binop %id),
    (%binop %arg1 %arg2 $args %result),          ! >=2 arguments
    (%binop %result %arg' %result').             ! adding an argument

  (%binop () %id)<                     ! empty argument sequence
    (generalize %binop %id).
  (%binop ($args %arg) %result')<      ! adding arg to sequence
    (generalize %binop %id),
    (%binop ($args) %result),
    (%binop %result %arg %result').

! move these to their original function definitions?:

  (generalize concat ()).
  (generalize plus 0).
  (generalize times (s 0)).
  (generalize and `t).
  (generalize or `f).


! Binary operator and binary relation higher-order forms:


! .* - apply first arg to sequence of second args to get sequence of results
! ((.* <binop> <arg1> <arg2-seq> <result-seq>)

  ((.* %binop) %arg1 () ()).
  ((.* %binop) %arg1 (%arg2 $args2) (%res $res))<
    (%binop %arg1 %arg2 %res),
    ((.* %binop) %arg1 ($args2) ($res)).

! - also apply to binary relation:

  ((.* %binrel) %arg1 ()).
  ((.* %binrel) %arg1 (%arg2 $args2))<
    (%binrel %arg1 %arg2),
    (.* %binrel) %arg1 ($args2)).

! *. - apply sequence of first args to second arg to get sequence of results
! ((*. <binop>) <arg1-seq> <arg2> <result-seq>)

  ((*. %binop) () %arg2 ()).
  ((*. %binop) (%arg1 $args1) %arg2 (%res $res))<
    (%binop %arg1 %arg2 %res),
    ((*. %binop) ($args1) %arg2 ($res)).

! - also apply to binary relation:

  ((*. %binrel) () %arg2).
  ((*. %binrel) (%arg1 $args1) %arg2)<
    (%binrel %arg1 %arg2),
    ((*. %binrel) ($args1) %arg2).

! _ - concatenate the (sequences) of a fn result sequence into a single sequence
! ((_ <fn>) <arg1> ... <argn> <result-seq>)
!    -- number of function input args is arbitrary but last elem must be result

  ((_ %fn) $args %result*)<
    (%fn $args %result),          ! get function result
    (concat %result %result*).    ! concatenate result subsequences

! .*_ - apply .* to binary operator and concatenate the results
! ((.*_ <binop>) <arg1> <arg2-seq> <concatenated results>)

  ((.*_ %binop) %arg1 %arg2s %concatenated_results)<
    ((_ (.* %binop) %arg1 %arg2s %concatenated_results).

    ! ??? This is probably not needed!

! **_ - binary operator cartesian product in flat sequence
! ((**_ <binop>) <a> <b>
!      (<a0xb0> <a0xb1> .. <a0xbn> <a1xb0> .. <a1xbn> ... <amxb0> .. <amxbn>))
!   -- note that the 2nd argument cycles faster

  ((**_ %binop) %args1 %args2 %results)<
    ((_ (*. (.* %binop))) %args1 %args2 %results).
 
! filter.* - filter second arg sequence for a Boolean binary operator
! ((filter.* <boolbinOp>) <arg1> <arg2s> <t-args2s>)

  ((filter.* %binop) %arg1 () ()).
  ((filter.* %binop) %arg1 (%arg2 $arg2s) ($arg2s'))<
    (%binop %arg1 %arg2 `f),        ! result is false - arg2 not included
    ((filter.* %binop) %arg1 ($arg2s) ($arg2s')).
  ((filter.* %binop) %arg1 (%arg2 $arg2s) (%arg2 $arg2s'))<
    (%binop %arg1 %arg2 `t),        ! result is true - arg2 is included
    ((filter.* %binop) %arg1 ($arg2s) ($arg2s')).


! finite_set - define a finite set in a single expression

  (%set %elem)< (finite_set %set ($1 %elem $2)).

 ! example:
 !   (finite_set day (Sun Mon Tue Wed Thu Fri Sat)).


! eval - Lisp-like expression evaluation (from paper)

  (eval (quote %expr) %expr).      ! value is unevaluated expression
  (eval %dec_sym %value)<          ! value of decimal number symbol
    (dec_sym %dec_sym %value).
  (eval (%fn $args) %result)<      ! evaluate function on arguments
    (eval* ($args) ($results)),    ! evaluate argument expressions
    (%fn $results %result).        ! evaluate function on argument results
       ! -- this works for functions that yield a single result at end of list