! noteq.ax - utility predicates related to inequality of expressions ! -- Note that inequality is not built in, so we basicaly define inequality ! between expressions based on "explicitly declared" atoms. ! commutativity of /= (/= %1 %2)< (/= %2 %1). ! -- eliminates some axioms below ! "declaring" a set of atoms (atoms ` `0 `1 `char). ! defining inequality between distinct ["declared"] atoms (/= %1 %2)< (atoms \$a %1 \$b %2 \$c). ! -- (/= %2 %1) follows from commutativity axiom ! defining inequality between ["declared"] atom and a sequence (/= % (\$))< (atoms \$a % \$b). ! -- (/= (\$) %) likewise ! /= - inequality on sequences (/= () (% \$)). ! inequality between sequences of different length ! -- (/= (% \$) ()) follows (/= (%1 \$1) (%2 \$2))< ! inequality for unequal sub-expressions (/= %1 %2). (/= (% \$1) (% \$2))< ! skip identical prefixes (/= (\$1) (\$2)). ! From the above axioms we get inequality between distinct characters, ! character strings, and symbols. ! not_in - expression not in sequence (not_in %x ()). (not_in %x (% \$))< (/= %x %), (not_in %x (\$)). ! all_diff - all elements in a sequence are different (all_diff ()). (all_diff (% \$))< (all_diff (\$)), (not_in % (\$)). ! elim_dupl - eliminate duplicate elements from a sequence ! (elim_dupl ) !/ old: (elim_dupl %nodups %nodups)< (all_diff %nodups). (elim_dupl %dups' %nodups)< (elim_dupl %dups %nodups), (in % %nodups), (insert % %dups %dups'). ! duplicate another element ! The above definition constrains the order of the unduplicated elements. !\ ! An alternative definition below allows duplicates in any order. (elim_dupl () ()). (elim_dupl %dups' (% \$nodups))< ! adding 1st occurrence of an element (elim_dupl %dups (\$nodups)), (not_in % (\$nodups)), (insert % %dups %dups'). (elim_dupl %dups' %nodups)< ! adding repeat occurrence of an element (elim_dupl %dups %nodups), (in % %nodups), ! or (in % %dups), (insert % %dups %dups'). ! union - get union of two sets (with no duplicates in result) (union (\$set1) (\$set2) %union)< (elim_dupl (\$set1 \$set2) %union). ! union elements are nondeterministically in any order and w/o duplicates ! merge_sets - merge two sets sharing a common element (merge_sets (\$sets1 %setA \$sets2 %setB \$sets3) (\$sets1 \$sets2 \$sets3 %setAB))< (in %e %setA), ! same element is in both sets A & B (in %e %setB), (union %setA %setB %setAB). ! union the sets ! disjoint - two sets (sequences) are disjoint (no elements in common) (disjoint () (\$set)). (disjoint (% \$) (\$set))< (not_in % (\$set)), (disjoint (\$) (\$set)). ! *** use higher-order definition from /= ! disjoint_all - a set is disjoint wrt all sets in a sequence ! *** use higher-order form here! (disjoint_all %set ()). (disjoint_all %set (% \$))< (disjoint %set %), (disjoint_all %set (\$)). ! partition - a set of sets is a partition if sets are pairwise disjoint (partition ()). ! no sets is a partition (partition (%set \$sets))< (partition (\$sets)), (disjoint_all %set (\$sets)). ! new set disjoint wrt other sets ! Boolean functions involving inequality tests ! -- These return atoms `t or `f. ! ==? - test if two (comparable) expressions are identical or not (==? % % `t). ! expressions are identical (==? %1 %2 `f)< ! expressions have inequality defined between them (/= %1 %2). !/ possible extension: ! ==? - variation of ==? for a single >=2-element sequence argument: (==? (%a %b \$) %t/f)< (==? %a %b %t/f). ! -- any elements beyond the second are ignored !\ -- for now we will use the "1" higher-order form ! in? - test if expression is in a sequence (in? %expr %seq `t)< (in %expr %seq). (in? %expr %seq `f)< (not_in %expr %seq). ! in_set? - test whether expression is element of a finite set ! ((in_set? ) ) ((in_set? %set) %elem %t/f)< (finite_set %set %elems), (in? %elem %elems %t/f). ! -- This only works if finite set elements have inequality relation defined ! (A finite set of atoms probably would not.) ! prefix? - test whether first sequence is a prefix of the second (prefix? (\$pre) (\$pre \$suf) `t). ! is prefix (prefix? (\$pre %1 \$1) (\$pre) `f). ! not prefix - 2nd arg too short (prefix? (\$pre %1 \$1) (\$pre %2 \$2) `f)< ! not prefix - unequal expressions (/= %1 %2). ! not - Boolean 'not' function (not `f `t). (not `t `f). ! and - Boolean 'and' function (and `f `f `f). (and `f `t `f). (and `t `f `f). (and `t `t `t). ! or - Boolean 'or' function (or `f `f `f). (or `f `t `t). (or `t `f `t). (or `t `t `t). ! subset - a sequence [set] of elements is contained in another sequence [set] (subset () %seq). (subset (% \$) %seq)< (in % %seq), (subset (\$) %seq). ! or: (subset %elems %seq)< ((*1 in) %elem %seq). ! ~subset - a sequence [set] is not contained in another sequence [set] (~subset (\$1 % \$2) %seq)< ! not a subset if (not_in % %seq). ! any element not in sequence ! subset? - Boolean test for one sequence a subset of another (subset? %elems %seq `t)< (subset %elems %seq). (subset? %elems %seq `f)< (~subset %elems %seq). ! =sets? - test for two sets being "equal" (=sets? %set1 %set2 %t/f)< ! 2 sets equal if each is subset of other (subset? %set1 %set2 %t/f1), (subset? %set2 %set1 %t/f2), (and %t/f1 %t/f2 %t/f). ! -- Note that element duplications are ok and order doesn't matter. ! set_in - a set is in a sequence of sets (set_in %set (\$1 % \$2))< (=sets %set %). ! ~set_in - a set is not in a sequence of sets (~set_in %set ()). (~set_in %set (% \$))< (=sets? %set % `f), ! arg1 set not equal to each set in arg2 sequence (~set_in %set (\$)). ! subsset - a set of sets is a subset of another set of sets ! *** We use the notation "sset" for "set of sets". (subsset () %seq). (subsset (% \$) %seq)< (set_in % %seq), (subsset (\$) %seq). ! ~subsset - a set of sets is not a subset of another set of sets (~subsset (\$1 % \$2) %seq)< ! not a subsset if (~set_in % %seq). ! any set not in sset ! subsset? - Boolean test for one sset a subset of another sset (subsset? %sset1 %sset2 `t)< (subsset %sset1 %sset2). (subsset? %sset1 %sset2 `f)< (~subsset %sset1 %sset2). ! =ssets? - test for two sets-of-sets being equal (=ssets? %sset1 %sset2 %t/f)< ! each a subsset of the other? (subsset %sset1 %sset2 %t/f1), (subsset %sset2 %sset1 %t/f2), (and %t/f1 %t/f2 %t/f). ! *** Note that =ssets? is defined from =sets? the same way =sets? can be ! defined from ==?. A higher-order form could be used here!