higher.txt -- definition of the most-basic higher-order constructions
uses:
   uncbasic -- unconditional basic predicates
   cbasic -- conditional basic predicates (inserts, zero_or_more)
   -- Many basic predicates are not used in the definition of higher-order
      forms but as predicates to apply the forms to.


This section defines the most-basic of higher-order constructions, which can
then be used as tools to define predicates and functions.  A higher-order
definition is one in which a predicate or function name is used as a
parameter, or an entire predicate is a parameter.  The higher-order
definitions of this file are as follows:


1. Generalizing 1-Argument Conclusion and Condition Predicates

generalize a 1-argument "conclusion" predicate to multiple arguments:

! format:  (generalize_conclu1 <pred>).
! -- Writing  (<pred> <arg1> .. <argn>)  as a conclusion produces
!       (<pred> <arg1>) ... (<pred> <argn>)
!    as valid expressions.  (see Valid below)

   (%pred %)<
     (generalize_conclu1 %pred),   ! predicate is declared for generalization
     (%pred $1 % $2).              ! multiple args supplied to 1-arg pred

We use this generalization declaration to define the following conclusion
predicate forms which allow for multiple arguments in a sequence:

!  ((gen <pred>) (<arg1> .. <argn>))     -- multiple args in a sequence
!  ((gen <pred>) (<arg> .. <arg>) ... (<arg> .. <arg>))   -- >1 multi-args
!  ((gen (gen <pred>)) ((<arg>..<arg>) .. (<arg>..<arg>))) -- generalize again!
!   ...

These expressions would be used as conclusions to generate (<pred> <arg>)
valid expressions.  We define this generalization as follows:

   (%pred $args)<
     (generalize_conclu1 %pred),
     ((gen %pred) ($args)).

   ! -- this allows multiple arguments to be incorporated within a sequence

   (generalize_conclu1 (gen %pred))<
     (generalize_conclu1 %pred).

   ! -- if <pred> is generalized, then <pred>* is generalized, etc.!

   ! -- Could factor out the shared condition (generalize_conclu1 %pred)
   !    from the three axioms.  (See Axset_w_shared_conds below.)
 
!{
   In file hosym.txt we see take advantage of symbol representation to
   define a more concise representation where a higher-order generalized
   predicate (gen <pred>) is represented by appending an asterisk to the
   symbol name: <pred>*.

     (<pred>* (<arg1> .. <argn>)     -- multiple args in a sequence
     (<pred>* (<arg> .. <arg>) ... (<arg> .. <arg>))   -- >1 multi-args
     (<pred>** ((<arg> .. <arg>) ... (<arg> .. <arg>)))  -- generalize again!
     ...
!} 

application below:  Valid

A similar higher-order form is to generalize a 1-argument "condition"
predicate to multiple arguments:

! format:  (generalize_cond1 <pred>).
! -- Given valid expressions
!       (<pred> <arg1>), ..., (<pred> <argn>)
!    we get a single valid expression:
!       (<pred> <arg1> .. <argn>)
!    (see valid below)

   (%pred)<
     (generalize_cond1 %pred).    ! predicate is declared for generalization
   (%pred $ %)<
     (generalize_cond1 %pred),
     (%pred $),
     (%pred %).

As with generalize_conclu1, we define the following condition predicate
forms which allow for multiple arguments in a sequence:

!  ((gen <pred>) (<arg1> .. <argn>))     -- multiple args in a sequence
!  ((gen <pred>) (<arg> .. <arg>) ... (<arg> .. <arg>))   -- >1 multi-args
!  ((gen (gen <pred>)) ((<arg>..<arg>) .. (<arg>..<arg>))) -- generalize again!
!   ...

These expressions effectively combine multiple (<pred> <arg>) into a single
valid expression.  We define this generalization as follows:

   ((gen %pred) ($args))<
     (generalize_cond1 %pred),
     (%pred $args).

   ! -- this allows multiple arguments to be incorporated within a sequence

   (generalize_cond1 (gen %pred))<
     (generalize_cond1 %pred).

!{
   Similarly, file hosym.txt uses defines generalization with an
   asterisk suffix:

      (<pred>* (<arg1> .. <argn>)     -- multiple args in a sequence
      (<pred>* (<arg> .. <arg>) ... (<arg> .. <arg>))   -- >1 multi-args
      (<pred>** ((<arg> .. <arg>) ... (<arg> .. <arg>)))  -- generalize again!
      ...

      -- these would be used as conditions
!} 

application below:  valid

Note that we can generalize the generalize_cond1 predicate since it is a
conclusion predicate:

   (generalize_conclu1 generalize_cond1).

   ! -- Should both of these have capitalized first letters to correspond
   !    to the conclusion predicate convention described below?  -- probably  

now apply to basic predicates in previous files!:

   (generalize_cond1 expr seq
        null single pair triple
        pair_same triple_same).

   (generalize_cond1 palindrome).


2. Valid Expressions as Data

Generating a valid expression from an expression:

   % < (Valid %).

We adopt the convention of using an uppercase letter to start this symbol
to mark this as conclusion predicate that is used to generate other
valid expressions.  Note the extra space needed after the first %
since %< together would form a single symbol.

We generalize this conclusion predicate using the above higher-order form:

   (generalize_conclu1 Valid).

This gives us the more useful higher-order tool for defining multiple
valid expressions from one expression:

!  (Valid <expr1> .. <exprn>)    -- all exprs are made valid
 
!  example:  (Valid (father Sue Tom) (father Bill Tom) (father Jane Bill)).
!  This expression generates the separate valid expressions,
!     (Valid (father Sue Tom))
!     (Valid (father Bill Tom))
!     (Valid (father Jane Bill))
!  from which we would get the valid expressions:
!     (father Sue Tom)
!     (father Bill Tom)
!     (father Jane Bill)

Note that these two axioms are an alternative to the single axiom
generating multiple valid expressions from one expression:

!  % < (Valid $1 % $2).

The use of the higher-order form allows a simpler Valid definition while
simultaneously generating useful extensions such as
!  ((gen Valid) (<expr> .. <expr>)).
or
!  (Valid* (<expr> .. <expr>)).
(see hosym.txt)

Now we define a related "condition" predicate that asserts that its one
argument is a valid expression:

   (valid %)< % .

This predicate name starts with a lowercase letter since it would be used
as a condition predicate.  Note the extra space needed after the second %.

We generalize this condition predicate using the above higher-order form:

   (generalize_cond1 valid).

From these two axioms we get single valid expressions that combine multiple
valid expressions as follows:

!  (valid (number (s 0)) (number 0) (plus (s 0) 0 (s 0)))

The alternative to using this higher-order form is the following definition,

!  (valid).
!  (valid % $)< % , (valid $).

which is less elegant.

Note that we could use the same symbol "valid" for both the conclusion
predicate "Valid" as well as for the condition predicate, since they
serve different purposes, but it probably enhances clarity to keep
different symbols.

The generalized "valid" condition predicate asserts that all of the
expressions in its list are valid.  That is, their conjunction is valid.
It is also useful to define the disjunction of valid expressions.

The "one_valid" predicate asserts that at least one expression in its
argument list is valid:

   (one_valid $1 % $2)< % .

  ! example:  (parent %x %y)< (one_valid (mother %x %y) (father %x %y)).


3. Representing Axioms as Data

Defining an axiom in a single expression:
!  format:  (Axiom_ <conclu> ..<conds>..)

   %conclu < (Axiom_ %conclu $conds), (valid $conds).

  ! example:  (Axiom_ (sort %1 %2) (permutation %1 %2) (ordered %2)).

Generating the Axiom_ expression as a conclusion predicate results in
valid expressions being generated if the conditions are valid.
We capitalize the first letter in keeping with the convention above.

We create an alternative version of this predicate that represents the
axiom in an expression sequence:

   (Axiom_ $)< (Axiom ($)).

Note the relation of Axiom_ to Axiom.  We may adopt this as a symbolic
higher-order form for other multi-argument predicates.

The 1-argument Axiom conclusion predicate can now be generalized:

   (generalize_conclu1 Axiom).

This generalization allows us to define a set of axioms in a single expression:

! example:  (Axiom ((length () 0))
!                  ((length (% $) (s %n)) (length ($) %n))).
!    -- The individual axioms are generated and from these the
!       valid expressions are generated.

! *** An alternative to this is given in <hosym.txt>.


4. Common Conditions in Axioms of a Definition

Sometimes the same condition or conditions is used for all axioms for a
given definition.  We can extract the common conditions using the following
higher-order form:

!  form:  (Axset_w_shared_conds
!            (<conclu> ..<conds>..)
!            ...
!            (<conclu> ..<conds>..)
!            (..<shared_conds>..)
!         ).

Here the shared conditions ..<shared_conds>.. are to be added to each
axiom in the list.  The definition of this higher-order form is as follows:

   (Axiom_ %conclu $conds $shared_conds)<
     (Axset_w_shared_conds
       $axioms1
       (%conclu $conds)
       $axioms2
       ($shared_conds)
     ).

Note that we could consider using this higher-order form for the "valid"
higher-order definition above,

!  (Axset_w_shared_conds
!    ((%pred))
!    ((%pred % $) (%pred $) (%pred %))
!    ((generalize_cond1 %pred))
!  ).

The problem is that we need the "valid" definition first in order to
have the "Axiom_" conclusion predicate.  Thus using this higher-order
form to define "valid" results in a circular definition.


5. Generalizing a binary relation

Given a binary relation (<binrel> <arg1> <arg2>), we want to generalize it
to (<binrel> <arg1> .. <argn>), n>=2, and to (<binrel> (<arg1> .. <argn>)),
n>=0.  There are two ways to define this generalization: (1) let the
relation apply between consecutive pairs, <arg1> <rel> <arg2> <rel> ...
<rel> <argn>, or (2) let the relation apply between any pair of elements:
<argi> <rel> <argj>, 1 <= i < j <= n.  Both definitions would work for
the identity relation == or for an ordering relation such as < or <=.
Only the first definition would work for a "successor" relation on
natural numbers and the second definition would be best for a generalization
of the inequality relation /=.

The axioms for the first definition generalization are as follows:

   (%rel ())<
     (generalize_binrel %rel).

   (Valid
       (%rel (%arg1))
       (%rel (%arg2)))<
     (generalize_binrel %rel),
     (%rel %arg1 %arg2).
     ! -- Note that we constrain the single expression to be one of the
     !    arguments (either first or second!) of the binary relation.
     !    Consider for example succ on non-negative integers and pred
     !    on non-positive integers.  Both must allow 0 as a single argument.

better defn?:
   (%rel (%arg))<
     (generalize_binrel %rel),
     (one_valid
         (%rel %arg %arg')
         (%rel %arg' %arg)).
         ! -- this seems a little nicer

   (%rel ($args %arg %arg'))<
     (generalize_binrel %rel),
     (%rel ($args %arg)),
     (%rel (%arg %arg')).

   (%rel %arg1 %arg2 $args)<
     (generalize_binrel %rel),
     (%rel (%arg1 %arg2 $args)).

   ! -- could factor out the shared conditions here

In place of the explicit generalization for == we can define:

   (generalize_binrel ==).

The axioms for the second definition are given in <higher2.txt>.


6. Some Utilities for More Concise Axiom Definitions

optional trailing argument for a predicate:

   (Valid
       (%pred $args)
       (%pred $args %opt_arg))<
     (Opt_arg %pred $args %opt_arg).

  ! examples from <symbol.txt> and <atom.txt>:
  !    (Opt_arg symbol_atom `symbol symbol).
  !       ->  (symbol_atom `symbol)
  !       ->  (symbol_atom `symbol symbol)
  !    (Opt_arg atom <atom> <atom_name>)
  !       ->  (atom <atom>)
  !       ->  (atom <atom> <atom_name>)

Asserting that a binary relation is symmetric:

   (%op %arg1 %arg2)<
     (Symmetric %op),
     (%op %arg2 %arg1).

  ! example:  (symmetric /=).

a better definition for 2-operand operation with possible addition parameters:

   (%op %arg1 %arg2 $params)<
     (Symmetric %op),
     (%op %arg2 %arg1 $params).

     ! This can be used for unifyx and no_unifyx!
     ! (Note that we can delete the previous axiom since this new one
     ! subsumes it.)

Defining one predicate from another:
!  (Pred_defn <newpredname> <oldpredname(or expr)>)

   (%newpred $args)<
     (Pred_defn %newpred %oldpred),
     (%oldpred $args).

-- examples from <cbasic.txt> (see "map" below):

   (Pred_defn seq_of_seqs (map seq)).
   (Pred_defn seq_of_nulls (map null)).
   (Pred_defn seq_of_singles (map single)).
   (Pred_defn seq_of_pairs (map pair)).
   (Pred_defn seq_of_triples (map triple)).

Another version that allows one to constrain the arguments:
!  (Pred_defn_w_args <newpredname> <oldpredname> ..args..)

   (%newpred $args)<
     (Pred_defn_w_args %newpred %oldpred $args),
     (%oldpred $args).

-- examples from <metaAL.txt>:

 ! (Pred_defn_w_args encode_axiom *:encode
 !      (%conclu $conds) (%xconclu $xconds)).
     ! -- args force sequence of one or more exprs

 ! (Pred_defn encode_axset *:encode_axiom).


7. Extracting common predicate name from axiom conclusions

definition format:

!  (Axioms_for_pred <pred_name>
!    <axiom>
!    ...
!    <axiom>
!  ).

axiom for definition:

   (Axiom_ ((%pred_name $conc_args) $conds)<
     (Axioms_for_pred %pred_name
       $axioms1
       (($conc_args) $conds)
       $axioms2
     ).

example:

!  (axioms_for_pred seq_of_seqs
!     ((()))
!     (((($) $seqs)) (seq_of_seqs ($seqs)))
!  ).

! replaces:

!    (seq_of_seqs ()).
!    (seq_of_seqs (($) $seqs))<
!      (seq_of_seqs ($seqs)).

!    -- The above higher-order definition is not an improvement!

!{ alternative syntax that eliminates pair of parentheses around each axiom:

     (axioms_for_pred seq_of_seqs
        (()) .
        ((($) $seqs)) < (seq_of_seqs ($seqs)) .
     ).      -- this is a little more readable than the above example

     *** need to give axiom definition for this form

  better for this problem to use mapping function here anyway:

     (seq ($)).
     (*:seq <seq_of_seqs>)

  *** also combine this form with shared conditions form?
!}


!{
***. Extracting Common Predicate Name and Common Arguments

If all the conditions have the same predicate name and possibly the same
leading arguments, as the conclusion expressions, then we can factor out
the common sub-expressions as follows:

! form:  (Factored_defn <pred> ..<args>..
!           <axiom w leading <pred> ..<args>.. removed from conclu & conds>
!           "
!        ).

definition:

   (Axiom_ (%pred $args $conclu_args) (
      (

***  doing just %pred requires a "distr%1$*" predicate
     doing %pred and $args requires "distr$1$*"

For now we will omit this.

-- see <higher2.txt> for other alternatives


***. extracting common predicate name from conclusions and conditions
(assuming all expressions have same predicate name)

definition format

   (axioms_for_pred' <pred_name>
     <axiom>
     ...
     <axiom>
   ).

axiom for definition:

   (axiom $axiom)<
     (axioms_for_pred' %pred_name
       $axioms1
       %axiom
       $axioms2
     ),
     (distr1* %pred_name %axiom ($axiom)).

     (distr1* %expr () ()).
     (distr1* %expr (($seq) $seqs) ((%expr $seq) $seqs'))<
       (distr1* %expr ($seqs) ($seqs')).

example:

   (axioms_for_pred seq_of_seqs
     (((()))
      (((($) $seqs)) (($seqs)))
     )
   ).
!}


8. String Variable Either Set by Predicate or is Null

Defining an optional string variable value.  A string variable is either set
by a predicate or has a null value.
!  (opt_str_var <pred> <str_var>)

   (opt_str_var %pred $)< %pred.
      ! string var (usually) in predicate is set by predicate value
   (opt_str_var %expr).
      ! string var following predicate expr is forced to have a null value!

  *** need an example of this!

This predicate is an alternative to the condition

   (one_valid
      <pred>
      (null (<svar>)))

  -- not a big savings


9. Map functions and relations to sequences of arguments:

! form for condition exprs:
!    ((map <pred>) <seq of arg1s> ... <seq of argns>)
! -- the length of each argument sequence is the same

axiom definition:

  ((map %rel) $nulls)<             ! empty sequences of arguments
    (zero_or_more () ($nulls)).    ! note that number of nulls is unrestricted
  ((map %rel) $argseqs')<
    ((map %rel) $argseqs),
    (%rel $args),
    ((inserts ($args) ($argseqs) ($argseqs')).

  ! examples:  ((map day) (Saturday Tuesday Tuesday))
  !                from (day <day>) relation
  !            ((map concat) ((a b) ())
  !                          ((c) (u v))
  !                          ((a b c) (u v)))

  ! note that we are also generating ((map <anything>) () ... ())

File <hosym.txt> replaces (map <rel>) with the modified symbol *:<rel>.

Note that this map form is more general than the map of Haskell, which
maps a function to a list of arguments to produce a list of results.
For example, this map operation also does what the Haskell zipWith operation
does, which is to apply a binary operator to pairs of elements obtained
from two argument lists to yield a list of results.

Note that the following "named_set_closure" predicate is just a special case
of map:

closure of elements from a named set:
!  (named_set_closure <set_name> <seq of elements from set>)

   (named_set_closure %set_name ()).
   (named_set_closure %set_name ($elems %elem))<
     (named_set_closure %set_name ($elems)),
     (%set_name %elem).

   ! -- better relation name needed

! -- This could be considered obsolete since it is replaced by map.

A similar predicate that concatenates sequences from a set is as follows:

concatenation closure from a named set:
!  (named_set_concat <set_name> <concat of sequences from set>)

   (named_set_concat %set_name ()).
   (named_set_concat %set_name ($seqs $seq))<
     (named_set_concat %set_name ($seqs)),
     (%set_name ($seq)).

! example:  defining the set of all sequences of even length:

   (even_len %seq)<
     (named_set_concat pair %seq).   ! sequence of pairs concatenated!

Another mapped form that simplifies some of the above definitions is the
following which defines a new predicate as the mapped version of an existing
predicate:

! mapped predicate definition
!   (mapped_pred <new_mapped_pred> <orig_pred>)

   (%new_pred $args)<
     (mapped_pred %new_pred %orig_pred),
     ((map %orig_pred) $args).

examples:    (compare with Pred_defn examples above)

   (mapped_pred seq_of_seqs seq).
   (mapped_pred seq_of_nulls null).
   (mapped_pred seq_of_singles single).
   (mapped_pred seq_of_pairs pair).
   (mapped_pred seq_of_triples triple).


10. Fold

Here we apply or "fold" a binary operator <op> into a list.  The fold-right
("foldr") operation has the following form:

!  ((foldr <op> <identr>) <list of values>)

The <identr> value is the "right identity" for the binary operator.
That is, <x> <op> <identr> == <x> for all <x>.  This higher-order operation
evaluates the follow expression given a list of values (<x1> <x2> .. <xn>):

! foldr:   (<x1> <op> (<x2> <op> (... (<xn> <op> <identr>)...)))

Note that if the list is null then the result is <identr>.
The fold-left operation ("foldl") is analogous and uses the "left identity":

! foldl:   ((...((<identl> <op> <x1>) <op> <x2>) ...) <op> <xn>)

For associative operators, such as plus and concat, the left and right
identities are the same (0 and (), respectively, for plus and concat),
and the results for foldl and foldr are the same.

The definition of foldr is as follows:

   ((foldr %op %id) () %id).
   ((foldr %op %id) (% $) %x')<
     ((foldr %op %id) ($) %x),
     (%op % %x %x').

The foldl operation is analogous:

   ((foldl %op %id) () %id).
   ((foldl %op %id) ($ %) %x')<
     ((foldl %op %id) ($) %x),
     (%op %x % %x').
 
An interesting alternative definition of foldl (using a tail string variable)
is as follows:

   ((foldl %op %id) () %id).
   ((foldl %op %id) (% $) %x)<
     (%op %id % %idx),
     ((foldl %op %idx) ($) %x). 

!{
Some examples of fold are as follows:

   (Pred_defn concat (foldr concat ())).    ! generalization of concat

   (Pred_defn sum (foldr plus 0)).          ! add numbers in a list

   (Pred_defn reverse (foldl rev_op ())).   ! defining reverse using fold!
!}


11. scanl -- a Haskell operator

The "scan from left" operation scanl is found in Haskell and is like foldl
except that it returns a list that saves all the intermediate values.
An example of its format is as follows:

!  ((scanl <op> <id>) (<x1> <x2> .. <xn>)
!       (<id> <id<op>x1> <id<op>x1<op>x2> .. <id<op>x1<op>x2<op>..<op>xn>))

The definition of scanl is as follows:

   ((scanl %op %id) () (%id)).
   ((scanl %op %id) ($ %) ($' %'))<
     ((scanl %op %id) ($) ($')),
     (last ($') %x), 
     (%op %x % %').


12. eval -- evaluating an expression

The "eval" operation allows predicates to be evaluated as nested expressions.
The axioms are as follows:

   (eval (quote %expr) %expr).      ! "quote" returns expr unchanged 
        ! -- the ` atom might be a better "quote" marker
   (eval (%fn $args) %result)< 
     ((map eval) ($args) ($results)), 
     (%fn $results %result). 

These axioms turn some of the previously-defined predicates into functions
which can be applied in a LISP-like manner: 

   (eval (append (quote (a b c)) 
                 (reverse (quote (e d))) 
         ) %value)

When this expression is used as a condition, the variable %value will get
instantiated to the expression (a b c d e).

Axioms in later files will extend eval to evaluate decimal digit symbols
to the numbers they represent.