! 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!