cbasic.txt -- some basic predicates using conditional axioms
uses:
   uncbasic (member)  (references to insert, append1, concat, make_pair)


Basic Predicates Defined from Condition Axioms 

This file defines basic predicates and functions that require conditional
axioms but do not use higher-order definitions.  (Typically these are
recursive definitions.)  This file is a continuation of the file
<uncbasic.txt>, which defines basic predicates using unconditional
axioms.  See that file for more background.


1. Sequences of an element type
-- these will be given higher-order definitions in <higher2.txt>

sequence of sequences:

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

 ! higher-order definition is better:
 ! (see <higher1.txt> and <higher2.txt>)

 ! could name this  *:seq  to match higher-order definition
 
 !  (Pred_defn seq_of_seqs *:seq).      ! better
    ! -- or just use *:seq or (map seq) when needed

sequence of null sequences:

   (seq_of_nulls ()).               ! or *:null
   (seq_of_nulls (() $nulls))<
     (seq_of_nulls ($nulls)).

  ! or could just use closure:
  !   (seq_of_nulls %nulls)<
  !     (closure () %nulls).

  ! (Pred_defn seq_of_nulls *:null).    ! better
     ! -- or just use *:null when needed

sequence of singleton sequences (one element in sequence)

   (seq_of_singles ()).
   (seq_of_singles ((%) $seqs))<
     (seq_of_singles ($seqs)).

  ! (Pred_defn seq_of_singles *:single).

sequence of pairs:

   (seq_of_pairs ()).
   (seq_of_pairs ((%1 %2) $pairs))<
     (seq_of_pairs ($pairs)).

  ! (Pred_defn seq_of_pairs *:pair).

sequence of triples:

  ! (Pred_defn seq_of_triples *:triple).

-- generalize to sequence of k-tuples

set of sequences of even length:

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

set of sequences of odd length:

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

-- higher-order definitions for these predicates are found in file <higher.txt>


2. Closure of an expression or sequence

zero or more copies (closure) of a constant expression:

   (closure % ()).
   (closure % (% $))<
     (closure % ($)).

 ! -- sometimes also called "zero_or_more":

   (zero_or_more % ()).
   (zero_or_more % (% $))<
     (zero_or_more % ($)).

one or more copies of an expression:

   (closure+ % (% $))<
     (closure % ($)).

   ! alternative definition that may be more declarative?:
   !   (closure+ % %seq+)<
   !     (closure % %seq+),
   !     (nonnull %seq+).

closure of a string:

   (closure_str ($) ()).
   (closure_str ($) ($ $$))<
     (closure_str ($) ($$)).

closure+ of a string:

   (closure_str+ ($) ($ $$))<
     (closure_str ($) ($$)).

closure of the finite set of elements in a sequence:

   (set_closure ($set) ()).        ! 0 or more elements from sequence
   (set_closure %set ($ %))<
     (set_closure %set ($)),
     (member % %set).       ! -- or could just replace %set with ($1 % $2)

   (set_closure+ ($set) (% $))<    ! 1 or more elements from sequence
     (set_closure ($set) (% $)).

! See <higher.txt> for closure of named sets of the form  (<set> <elem>) .

! seq>  -- map seq to itself or map seq of 1 element to closure seq
! *** this is a very specialized function -- only used for map generalization?

   (seq> ($) ($)).       ! map sequence to itself
   (seq> (%) ($))<       ! or map 1-elem seq to closure of element
     (closure % ($)).    ! (zero or more occurrences of %)


3. Generalization of binary relations and binary operators

generalization of identity relation ==:
!  (== (<expr1> ... <exprn>))   -- n >= 0
!  (== <expr1> ... <exprn>)     -- n >= 2
(a generic higher-order definition is found in <higher2.txt>)

   (== ()).               ! 0 or more expressions in a sequence
   (== (%)).
   (== (% % $))<
     (== (% $)).

   ! -- Note that this defines the set of all sequences whose elements are
   !    the same:

   (same_expr_seq %seq)<         ! better than the above definition
     (zero_or_more % %seq).

   (== %1 %2 $)<          ! 2 or more expressions at the top level
     (== (%1 %2 $)).

generalization of concatenation:
!  (concat (($1) ... ($n)) ($1 ... $n))      n >= 0
!  (concat ($1) ... ($n) ($1 ... $n))        n >= 2
(a generic higher-order definition is found in <higher2.txt>)

   (concat () ()).                   ! 0 or more arguments in a sequence
   (concat ($seqs %seq) %result')<   ! ("flattening" a sequence of sequences)
     (concat ($seqs) %result),
     (concat %result %seq %result').

   (concat %1 %2 $ %result),         ! 2 or more arguments at top level
     (concat (%1 %2 $) %result).

  ! This same generalization can be applied to other binary operators.

generalization of append1:
!  (append1 ($seq) %1 ... %n ($seq %1 ... %n))
-- multiple elements are appended in one step

   (append1 ($seq) ($seq)).
   (append1 %seq $args % ($seq' %))<
     (append1 %seq $args ($seq')).

generalization of insert:
!  (insert %1 ... %n ($seq) (%1 .. %n $seq))   -- insert multiple exprs

   (insert ($seq) ($seq)).
   (insert % $args %seq (% $seq'))<
     (insert $args %seq ($seq')).


4. Pairwise application of some binary operators
   (insert,append1,concat,make_pair)
-- these can also be defined by mapping the binary operators

pairwise insert elements at front of sequences:
!  (inserts <elems> <seqs> <seqs w elems at front>)  #<elems> = #<seqs>
!  or call it  *:insert

   (inserts () () ()).
   (inserts (%elem $elems) (($seq) $seqs) ((%elem $seq) $seqs'))<
     (inserts ($elems) ($seqs) ($seqs')).

  ! Note that this function is a mapping of the insert function:  *:insert
  ! However, we need this function in order to define the mapping
  ! (see <higher.txt>), so we must define it explicitly here.

pairwise append elements to ends of sequences:
! -- mapping of append1:  *:append1

   (append1s () () ()).
   (append1s (($seq) $seqs) (%elem $elems) ((%seq %elem) $seqs'))<
     (append1s ($seqs) ($elems) ($seqs')).

pairwise concat sequences to sequences:
! -- mapping of concat:  *:concat

   (concats () () ()).
   (concats (($1) $1s) (($2) $2s) (($1 $2) $seqs))<
     (concats ($1s) ($2s) ($seqs)).

pairwise forming of pairs:
! -- mapping of make_pair:  *:make_pair

   (make_pairs () () ()).
   (make_pairs ((%1) $1) ((%2) $2) ((%1 %2) $pairs))<
     (make_pairs ($1) ($2) ($pairs)).


5. Distribution of values over sequences of values
-- applying binary operators insert, append1, concat, make_pair

distribute one element over front of multiple sequences and vice versa:
! (related to insert)
! (distr%1$* <elem> <seqs> <seqs w elem at front>)
! (distr%*$1 <elems> <seq> <seqs w elems at front>)

   (distr%1$* %elem () ()).           ! one element, multiple sequences
   (distr%1$* %elem (($seq) $seqs) ((%elem $seq) $seqs'))<
     (distr%1$* %elem ($seqs) ($seqs')).

   (distr%*$1 () ($seq) ()).          ! multiple element, one sequence
   (distr%*$1 (%elem $elems) ($seq) ((%elem $seq) $seqs'))<
     (distr%*$1 ($elems) ($seq) ($seqs')).

   ! Perhaps define these distr_ predicates using a higher-order form?

distribute one element over end of multiple sequences and vice versa:
! (related to append1)
! (distr$1%* <seq> <elems> <seq w elems at end>)
! (distr$*%1 <seqs> <elem> <seqs w elem at end>)

   (distr$1%* ($seq) () ()).          ! one sequence, multiple elements
   (distr$1%* ($seq) (%elem $elems) (($seq %elem) $seqs'))<
     (distr$1%* ($seq) ($elems) ($seqs')).

   (distr$*%1 () %elem ()).           ! multiple sequences, one element
   (distr$*%1 (($seq) $seqs) %elem (($seq %elem) $seqs'))<
     (distr$*%1 ($seqs) %elem ($seqs')).

distribute one prefix over multiple suffixes and vice versa:
! (related to concat)
! (distr$1$* <prefix> <suffixes> <prefix+suffixes>)
! (distr$*$1 <prefixes> <suffix> <prefixes+suffix>)

   (distr$1$* ($pre) () ()).         ! one prefix, multiple suffixes
   (distr$1$* ($pre) (($suf) $sufs) (($pre $suf) $seqs))<
     (distr$1$* ($pre) ($sufs) ($seqs)).

   (distr$*$1 () ($suf) ()).         ! multiple prefixes, one suffix
   (distr$*$1 (($pre) $pres) ($suf) (($pre $suf) $seqs))<
     (distr$1$* ($pres) ($suf) ($seqs)).

distribute one element over a sequence to form pairs and vice versa:
! (related to make_pair)
! (distr%1%* <elem1> <elem2s> <pairs>)
! (distr%*%1 <elem1s> <elem2> <pairs>)

   (distr%1%* %elem1 () ()).         ! one element 1, multiple element 2s
   (distr%1%* %elem1 (%elem2 $elem2s) ((%elem1 %elem2) $pairs))<
     (distr%1%* %elem1 ($elem2s) ($pairs)).

   (distr%1%* () %elem2 ()).         ! multiple element 1s, one element 2
   (distr%1%* (%elem1 $elem1s) %elem2 ((%elem1 %elem2) $pairs))<
     (distr%1%* ($elem1s) %elem2 ($pairs)).


6. Cartesian product of sequences of values
-- using binary operators insert, append1, concat, make_pair

! Cartesian product of new head elements with sequences:
! (product%$ <elems> <seqs> <seqs w elems at front -- all combinations>)
! -- The cartesion product consists of the following:
!    (((<elem1> ..seq1..) ... (<elem1> ..seqn..))
!     ...
!     ((<elemm> ..seq1..) ... (<elemm> ..seqn..)))
! Note that product sequences are grouped first by the elements and then
! by sequences.  Is other order of interest?
! What about flattened sequence of products?
! (related to insert)

   (product%$ () %seqs ())<
     (seq_of_seqs %seqs),
   (product%$ (%elem $elems) %seqs (%prod $prods))<
     (product%$ ($elems) %seqs ($prods)),
     (distr%1$* %elem %seqs %prod).

! Cartesian product of sequences with new last elements:
! (product$% <seqs> <elems> <seqs w elems at end -- all combinations>)
!    (((..seq1.. <elem1>) ... (..seq1.. <elemn>))
!     ...
!     ((..seqm.. <elem1>) ... (..seqm.. <elemn>)))
! (related to append1)

   (product$% () ($elems) ())<
   (product$% (%seq $seqs) %elems (%prod $prods))<
     (product$% ($seqs) %elems ($prods)),
     (distr$1%* %seq %elems %prod).

! Cartesian product of prefixes with suffixes
! (related to concat)

   (product$$ () %sufs ())<
     (seq_of_seqs %sufs).
   (product$$ (%pre $pres) %sufs (%prod $prods))<
     (product$$ ($pres) %sufs ($prods)),
     (distr$1$* %pre $sufs %prod).

! Cartesian product of elements with elements to form pairs
! (related to make_pair)

   (product%% () ($elem2s) ()).
   (product%% (%elem1 $elem1s) %elem2s (%prod $prods))<
     (product%% ($elem1s) %elem2s ($prods)),
     (distr%1%* %elem1 %elem2s %prod).


7. Tupling, transposition, and interleaving

Generalization of make_pairs: create tuples from sequences:
(also mapping of "compose_seq") 
!  (make_tuples (x11 .. x1n) ... (xk1 .. xkn) ((x11 .. xk1) ... (x1n .. xkn)))
!  -- all sequences have the same length

   (make_tuples %nulls)<           ! result of tupling no arguments
     (closure () %nulls).
   (make_tuples %seq $seqs %tuples')<
     (make_tuples $seqs %tuples),
     (inserts %seq %tuples %tuples').

transpose a sequence of sequences:
(similar to tuple)

   (transpose ($seqs) %seq')<
     (make_tuples $seqs %seq').

   ! Note that transposing a null sequence produces a sequence of an
   ! arbitrary number of nulls.

interleave the elements in two sequences:
(the sequence lengths are n,n or n+1,n)

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

   ! Note that one can think of this predicate as a function that takes a
   ! sequence and splits it into its even and odd elements, counting from 0.
   ! (Different argument order may be desirable here.)
   ! old:  (split_seq <seq> <even elems> <odd elems>)   -- same as interleave
   !       (split_seq <seq> (<even elems> <odd elems>))   -- this good too
   !           -- go both ways here  (merge_seq )

generalization of interleave:
!  (interleave <seq1> ... <seqk> <interleaved seq>)
!  -- sequence lengths are n+1,..,n+1,n,..,n

   (interleave $seqs1 $nulls ($exprs1))<
     (seq_of_singles ($seqs1)),     ! 1-expr sequences
     (seq_of_nulls ($nulls)),       ! null sequences
     (concat ($seqs1) ($exprs1)).   ! flatten 1-expr seqs to get exprs
   (interleave $seqs' ($exprsx $exprs))<
     (interleave $seqs ($exprs)),
     (inserts ($exprsx) ($seqs) ($seqs')).


8. Basic predicates involving sequence element order

Reverse, palindrome, and permutation are involved more in the content of
sequences rather than just combining and partitioning them.

reverse of a sequence:

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

split a sequence with the prefix reversed:
!  (rev_prefix <seq> <suffix> <rev_prefix>)

   (rev_prefix ($prefix $suffix) ($suffix) %rev_prefix)<
     (reverse ($prefix) %rev_prefix).

   ! -- an argument permutation of "rev_acc" (reverse accumulator)
   !    (except that this definition is not O(n)!)

palindrome:

   (palindrome %)<
     (reverse % %).

permutation of a sequence:

   (permutation () ()).
   (permutation ($1 % $2) ($3 % $4))<
     (permutation ($1 $2) ($3 $4)).