hosym.txt -- higher-order forms using symbol enhancement
uses:
   higher (Pred_defn, Axset_w_shared_conds)
   symbol (symbol_atom, sym_append, sym_insert)

This section gives additional higher-order language constructions which can
be used as tools to define new predicates and functions.  The higher-order
constructions of this section make use of symbol representation to define
generalizations of predicates by adding prefix or suffix characters or
by constructing new symbols according to patterns.


1. Map functions and relations to sequences of arguments:

This section defines an alternative to

!  ((map <rel>) <seq of arg1s> ... <seq of argns>)

where (map <rel>) is replaced by the modified symbol *:<rel>, as follows:

!  (*:pred <seq of arg1s> ... <seq of argns>)

Note that these would be used as condition expressions.
The axiom is as follows:
axiom definition:

  (Pred_defn %*:rel (map %rel))<
    (sym_insert "*:" %rel %*:rel).   ! relation symbol can be anything here!?

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

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

some examples of basic predicates defined using this higher-order form:

   (Pred_defn seq_of_seqs *:seq).
   (Pred_defn seq_of_nulls *:null).
   (Pred_defn seq_of_singles *:single).
   (Pred_defn seq_of_pairs *:pair).
   (Pred_defn seq_of_triples *:triple).
   ...
   (Pred_defn inserts *:insert).
      -- redundant since inserts had to be defined in order to define map!
   (Pred_defn append1s *:append1).
   (Pred_defn concats *:concat).
   (Pred_defn make_pairs *:make_pair).

Note that is is just as easy to write *:seq, *:null, etc., instead of using
the new predicate definitions seq_of_seqs, seq_of_nulls, etc.


2. Generalizing conclusion and condition unary predicates

This section defines symbolic representation for the generalization of unary
conclusion and condition predicates that were defined in file <higher.txt>.
From a unary conclusion generalization definition of the form

!  (generalize_conclu1 <pred>)

where <pred> is a unary predicate of the form

!  (<pred> <arg>)

we write the following generalizations:

!  (<pred> <arg1> .. <argn>)     -- multiple args for the predication
!  ((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!
!   ...

from which (<pred> <arg>) expressions are generated.

In this file we replace the expression (gen <pred>) with a symbol consisting
of the predicate name with an asterisk appended:

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

These symbols are an alternative to writing (gen <pred>) in conclusion
expressions.  The axioms are as follows:

   ((gen %pred) %arg)<
     (generalize_conclu1 %pred),
     (%pred* %arg),
     (sym_append %pred "*" %pred*).

   ! -- (gen <pred>) is generated from <pred>*

   (generalize_conclu1 %pred*)<
     (generalize_conclu1 %pred),
     (sym_append %pred "*" %pred*).

   ! -- (generalize_conclu1 <pred>*) is generated from
   !    (generalize_conclu1 <pred>)

Alternatively, we can abstract out the shared conditions, as follows:

   (Axset_w_shared_conds
     (((gen %pred) %arg)
      (%pred* %arg)                       ! generate (gen <pred>) from <pred>*
     )
     ((generalize_conclu1 %pred*)         ! <pred>* also generalized!
     )
     ((generalize_conclu1 %pred)          ! shared conditions
      (sym_append %pred "*" %pred*)
     )
   ).

example:  Valid

As with conclusion predicates, a unary condition predicate can be generalize
to allow for multiple arguments.  From the generalization definition

!  (generalize_cond1 <pred>)

where <pred> is a unary predicate of the form

!  (<pred> <arg>)

we get the following generalizations:

!  (<pred> <arg1> .. <argn>)     -- multiple args for the predication
!  ((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!
!   ...

which represent combined (<pred> <arg>) expressions.

In this file we replace the expression (gen <pred>) with a symbol consisting
of the predicate name with an asterisk appended:

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

These symbols are an alternative to writing (gen <pred>) in condition
expressions.  The axioms are as follows:

   (%pred* %arg)<
     (generalize_cond1 %pred),
     ((gen %pred) %arg),
     (sym_append %pred "*" %pred*).

   ! -- <pred>* is generated from (gen <pred>)

   (generalize_cond1 %pred*)<
     (generalize_cond1 %pred),
     (sym_append %pred "*" %pred*).

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

Alternatively, we can abstract out the shared conditions, as follows:

   (Axset_w_shared_conds
     ((%pred* %arg)                   ! generate <pred>* from (gen <pred>)
      ((gen %pred) %arg)
     )
     ((generalize_cond1 %pred*)       ! <pred>* also generalized!
     )
     ((generalize_cond1 %pred)        ! shared conditions
      (sym_append %pred "*" %pred*)
     )
   ).

example:  valid

Note that the (*:valid ...) mapping could be used here, except that the
numbers of multiple arguments in each sequence would have to be the same.
The mapping form clearly does not make good sense here.