uncbasic.txt -- basic predicates defined by unconditional axioms
uses: (nothing)

Unconditional-Axiom Variable-Only Predicates


1. Introduction

This file defines the most basic utility predicates and functions. which can
then be used in the definition of other predicates and functions.
The predicates defined here have just variable arguments and are defined
just from unconditional axioms, without use of any higher-order forms.

Terms for these predicates could include "basic", "arrangement", "form",
"format", "structure", "combination", "partition", etc.  They deal with
the form of expressions but not their actual values.  For now we will
refer to them as "basic" predicates.

Note that we do not attempt to define every possible variation of
function and predicate that might be useful.  Sometimes we define
a predicate or function simply because its pattern is interesting.
A later file defines families of predicates that allows defining essentially
all possible variations.

Choosing good names is probably the most difficult task in defining this
utility library.  An attempt has been made to let the names reflect grouping
and similarity between predicates, and to use consistent abbreviations.
Alternative names are given for some predicates.

Another area of difficulty is deciding the order of arguments.  Since some
of the higher-order functions assume that inputs occur before outputs,
there may be a case for defining variations of the same predicate with
different argument order.  The families of predicates defined elsewhere
allows arbitrary argument order.


2. Basic set predicates

predicate without arguments:

   (no_args).       ! possibly useful

set of expressions and sequences:

   (expr %).        ! set of all expressions
   (seq ($)).       ! set of all sequences

   ! Note that the set of atoms must be explicitly defined.
   ! (Definitions for atoms are found in other files.)

multiple expressions as arguments:

   (exprs2 %1 %2).      ! two expressions
   (exprs3 %1 %2 %3).     ! three expressions
   !...

   (exprs $).           ! arbitrary number of expressions

multiple sequences as arguments:

   (seqs2 ($1) ($2)).
   (seqs3 ($1) ($2) ($3)).
   !...

   ! Note that to do an arbitrary number of sequences requires a conditional
   ! definition:   (seqs ($1) ($2) ... ($n))  for arbitrary n

a null sequence "constant":

   (null ()).

   ! OK, there are no variables here, but this constant is nevertheless
   ! about "form".

set of non-null sequences:

   (nonnull (% $)).

set of sequences whose length is not 1:

   (not_len_1 ()).
   (not_len_1 (%1 %2 $)).

   ! define  ~len0, ~len1, ..., ~len9
   !         >len0, >len1, ...
   !                <len1, <len2, ...

sets of sequences of various length:

   (single (%1)).           ! sequence with just one element
   (pair (%1 %2)).
   (triple (%1 %2 %3)).
   !,,,

   ! A more general approach defined elsewhere will use a higher-order form
   ! to define predicates with names "len<n>seq", where <n> is a decimal
   ! number giving the length of the sequence.


3. Simple relations and functions

two expressions are identical:

   (== % %).          ! identical expressions

   ! used as a relational test and for variable "assignment"
   ! use = instead of == ?
   !    (may use = for some other purpose, such as equal values even though
   !     the expression representations may differ)

   ! will be generalized as follows:
   !   (== <expr1> ... <exprn>)     -- n >= 2
   !   (== (<expr1> ... <exprn>))   -- n >= 0

   (two_same % %).   ! -- same as ==
   (three_same % % %).
   !...

   (pair_same (% %)).
   (triple_same (% % %)).
   !...

decomposition of a sequence into its string of elements:

   (decompose_seq ($) $).   ! useful?   -- extension of "first" below

   (decompose_prefix ($1 $2) $1).
   !    "    _suffix ($1 $2) $2).

generalizing to arbitrary number of elements:

   (compose_seq $ ($)).

special cases of compose:

   (make_single % (%)).
   (make_pair %1 %2 (%1 %2)).
   (make_triple %1 %2 %3 (%1 %2 %3)).
   !...

another related pattern:

   (symmetric_decompose $1 ($1 $2) $2).
   ! -- this subsumes "decompose_seq" and "compose_seq"

functions involving the first element of a sequence:

   (first (% $) %).             ! first element of a sequence  ("head")
   (rmv_first (% $) ($)).       ! remove first element from sequence  ("tail")
   (ins_first ($) %x (%x $)).   ! insert new first element in front of sequence
   (repl_first (% $) %x (%x $)).  ! replace first element with new one 

The following "insert" function may be used instead of ins_first:

   (insert %x ($) (%x $)).      ! insert new front element
                                ! (note argument order)  

We also switch the input arguments to produce a "reverse" binary operator:

   (rev_op ($) %x (%x $)).

(This is used later in an example fold definition of reverse.)

Getting 2nd, 3rd, etc. elements from a sequence:

   (2nd (%1 % $) %).             ! get 2nd element in sequence
   (3rd (%1 %2 % $) %).          ! get 3rd element
   ...

-- could also define rmv_, ins_, and repl_ functions

corresponding functions involving last element of a sequence:

   (last ($ %) %).               ! last element of a sequence
   (rmv_last ($ %) ($)).         ! remove last element from sequence
   (ins_last ($) %x ($ %x)).     ! insert new last element at end of sequence
   (repl_last ($ %) %x ($ %x)).  ! replace last element with new one

The ins_last function will more commonly be called "append1":

   (append1 ($) % ($ %)).        ! append one element to a sequence 

   ! Could just call this "append", but that is often used in Prolog
   ! examples for our "concat" function, defined below.  We thus
   ! avoid using "append" in order to avoid confusion.

-- could also define functions on 2nd, 3rd, etc., from end of sequence

"functions" (relations) involving an arbitrary element of a sequence:

   (elem ($1 % $2) %).              ! any element of a sequence
   (rmv_elem ($1 % $2) ($1 $2)).     ! remove any element from sequence
   (ins_elem ($1 $2) %x ($1 %x $2)).  ! insert an element in a sequence
   (repl_elem ($1 % $2) %x ($1 %x $2)).  ! replace element in sequence

The classic "member" function is just "elem" with arguments reversed:

   (member % ($1 % $2)).            ! member of a sequence

two sequences share at least one element:

   (share ($1 % $2) ($3 % $4)).

   ! an alternative conditional definition:
   !   (share %seq1 %seq2)<
   !     (member % %seq1),
   !     (member % %seq2).

functions involving a matched element of a sequence:

   (rmv_elem ($1 % $2) % ($1 $2)).   ! remove specified element from sequence
   (repl_elem ($1 % $2) % %x ($1 %x $2)).  ! replace element in sequence

  ! We can use the same names here since the functions are distinguished by
  ! the extra argument that identifies the element to be removed or replaced.
  ! (Note that if there is more than one occurrence of element %, then the
  ! function nondeterministically picks one.)

   (ins_<elem ($1 % $2) % %x ($1 %x % $2)).  ! insert to the left of element
   (ins_>elem ($1 % $2) % %x ($1 % %x $2)).  ! insert to the right of element

   ! -- similar functions involving substrings are below

relations defining a subsequence of a sequence:

   (prefix ($1) ($1 $2)).    ! prefix of a sequence
   (suffix ($2) ($1 $2)).    ! suffix of a sequence
   (substr ($) ($1 $ $2)).   ! substring of a sequence

Note that for these subsequence relations, as well as the member relation,
we put the part before the whole.  In the earlier functions "first", "last",
and "elem" (a "nondeterministic function") we put the whole before the
part.  This convention is somewhat arbitrary and there may be good reason
to define variations on these predicates with different argument order.
The generalized family of arrangement predicates defined elsewhere will
provide for all alternatives.

concatenation of two sequences:

   (concat ($1) ($2) ($1 $2)).   ! concatenate two sequences
                                 ! -- often called "append" in Prolog examples

  ! will be generalized as follows (see <higher.txt>):
  !   (concat ($1) ... ($n) ($1 ... $n))     -- n >= 2
  !   (concat (($1) ... ($n)) ($1 ... $n))   -- n >= 0  ("flatten" function)

additional substring (nondeterministic) functions:
(compare with prefix, suffix, and substr above)

   (repl_prefix ($1 $2) ($1x) ($1x $2)).
   (repl_suffix ($1 $2) ($2x) ($1 $2x)).
       ! -- Note that inserting a prefix or suffix is equivalent to concat
       !    and removing a prefix/suffix leaves a suffix/prefix, respectively. 

   (ins_substr ($1 $2) ($x) ($1 $x $2)).
   (rmv_substr ($1 $ $2) ($1 $2)).
   (repl_substr ($1 $ $2) ($x) ($1 $x $2)).

functions involving matching a subsequence of a sequence:

   (repl_prefix ($1 $2) ($1) ($1x) ($1x $2)).    ! replace matched prefix
   (repl_suffix ($1 $2) ($2) ($2x) ($1 $2x)).    ! replace matched suffix

   (rmv_substr ($1 $ $2) ($) ($1 $2)).           ! remove matched substring
   (repl_substr ($1 $ $2) ($) ($x) ($1 $x $2)).  ! replace matched substring

   (ins_%>prefix ($1 $2) ($1) %x ($1 %x $2)).    ! insert expr after prefix
   (ins_%<suffix ($1 $2) ($2) %x ($1 %x $2)).    ! insert expr before suffix
   (ins_$>prefix ($1 $2) ($1) ($x) ($1 $x $2)).  ! insert string after prefix
   (ins_$<suffix ($1 $2) ($2) ($x) ($1 $x $2)).  ! insert string before suffix

   (ins_%<substr ($1 $ $2) ($) %x ($1 %x $ $2)).  ! insert expr before substr
   (ins_%>substr ($1 $ $2) ($) %x ($1 $ %x $2)).  ! insert expr after substr
   (ins_$<substr ($1 $ $2) ($) ($x) ($1 $x $ $2)).  ! insert str before substr
   (ins_$<substr ($1 $ $2) ($) ($x) ($1 $ $x $2)).  ! insert str before substr

select value from sequence based on first-element key:

   (key_select ($1 (%x $) $2) %x (%x $)).    ! select entire expr based on key
   (key_select% ($1 (%x %y $) $2) %x %y).    ! select 2nd expr based on key
      ! -- usually this predicate would be used with just a sequence of pairs
   (key_select$ ($1 (%x $) $2) %x ($)).      ! select tail of seq based on key

  ! Note that the member function can be used as a substitute here.


Rotation Predicates

arbitrary rotation of a sequence:

   (rotate ($1 $2) ($2 $1)).

rotate left or right by 1:

   (rotate1< (% $) ($ %)).       ! rotate left or forward
   (rotate1> ($ %) (% $)).       ! rotate right or backward

rotate to move matched element to first or last position:

   (rotate_first % ($1 % $2) (% $2 $1)).
   (rotate_last  % ($1 % $2) ($2 $1 %)).

other options:
-- rotate based on a matched subsequence
-- rotate based on matched first-element key