Section 27 Want more of a challenge? View in iconic form (experimental)

---

       # MATH introduce sets and set membership
[hear] (intro element);

[hear] (define element /
         ? x /
         ? lst /
         not /
         = (list-find-helper (lst) (x) (? y 0) 1) 0);

[hear] (element 2 (vector 8 9 2));

[hear] (element 8 (vector 8 9 2));

[hear] (element 9 (vector 8 9 2));

[hear] (element 4 (vector 6 1 4 9));

[hear] (element 1 (vector 6 1 4 9));

[hear] (element 6 (vector 6 1 4 9));

[hear] (element 1 (vector 8 1 0 3 5));

[hear] (element 3 (vector 8 1 0 3 5));

[hear] (element 0 (vector 8 1 0 3 5));

[hear] (element 3 (vector 4 0 3 7 9));

[hear] (element 0 (vector 4 0 3 7 9));

[hear] (element 9 (vector 4 0 3 7 9));

[hear] (element 3 (vector 4 1 3 9));

[hear] (element 9 (vector 4 1 3 9));

[hear] (element 4 (vector 4 1 3 9));

[hear] (not / element 8 (vector 4 1 0 9));

[hear] (not / element 8 (vector 6 4 0 7 5));

[hear] (not / element 1 (vector 0 7));

[hear] (not / element 4 (vector 1 3 2 5));

[hear] (not / element 8 (vector 3 7 2 5));

       # rules for set equality
[hear] (define set-subset /
         ? x /
         ? y /
         if (> (list-length / x) 0)
          (and (element (head / x) (y))
               (set-subset (tail / x) (y)))
          (true));

[hear] (define set= /
         ? x /
         ? y /
         and (set-subset (x) (y)) (set-subset (y) (x)));

[hear] (set= (vector 1 5 9) (vector 5 1 9));

[hear] (set= (vector 1 5 9) (vector 9 1 5));

[hear] (not / set= (vector 1 5 9) (vector 1 5));

       # let's go leave ourselves wide open to Russell's paradox
       # ... by using characteristic functions
       # ... since it doesn't really matter for communication purposes
       # ... and so far this is just used / tested with sets of integers really
[hear] (element 5 (all (? x / = (+ (x) 10) 15)));

[hear] (element 3 (all (? x / = (* (x) 3) (+ (x) 6))));

[hear] (define empty-set / vector);

[hear] (element 0 (natural-set));

[hear] (forall
          (? x /
           => (element (x) (natural-set))
              (element (+ (x) 1) (natural-set))));

[hear] (element 1 (natural-set));

[hear] (element 2 (natural-set));

[hear] (element 3 (natural-set));

[hear] (element 4 (natural-set));

[hear] (element 5 (natural-set));

[hear] (element 6 (natural-set));

[hear] (element 7 (natural-set));

[hear] (element 8 (natural-set));

[hear] (element 9 (natural-set));

[hear] (define boolean-set / vector (true) (false));

[hear] (element (true) (boolean-set));

[hear] (element (false) (boolean-set));

       # actually, to simplify semantics elsewhere, true and false
       # are now just 0 and 1 so they are not distinct from ints
[hear] (define even-natural-set /
         all /
         ? x /
         exists /
         ? y /
         and (element (y) (natural-set))
             (= (* 2 (y)) (x)));

[hear] (element 0 (natural-set));

[hear] (element 0 (even-natural-set));

[hear] (element 1 (natural-set));

[hear] (not / element 1 (even-natural-set));

[hear] (element 2 (natural-set));

[hear] (element 2 (even-natural-set));

[hear] (element 3 (natural-set));

[hear] (not / element 3 (even-natural-set));

[hear] (element 4 (natural-set));

[hear] (element 4 (even-natural-set));

[hear] (element 5 (natural-set));

[hear] (not / element 5 (even-natural-set));

[hear] (element 6 (natural-set));

[hear] (element 6 (even-natural-set));