Commit db1170ec by Stefan Israelsson Tampe

### set theory works better

parent 447a85c3
 ... ... @@ -87,49 +87,6 @@ using that predicate (with-lassoc-operators code ...) c(B + Ac) = A/B cc(B + Ac) = c(A/B) Which shows that c is nit idemptent for ordered sets, e.g. the current system works for c, cc orders , but not for ccc orders. For a full solution one need to track orders in the complement channel as well as the non complement channel. It looks like we must store either A/B or (A/B)c = B u Ac and do this properly. 1) Q = A/B u C/D = Q Qc = (A/B)c n (C/D)c = = (B u Ac) n (D u Cc) = U + Vc, U = B/C u D/A U u Qc = Qc (Q/U)c = Qc => Q/U = Q => stored pair Q,U 2) Q = A/B n C/D = AnC Qc = (A/B)c u (C/D)c = (Ac u B) u (Cc u D) = (B u D) u (AnC)c Qc = U + Vc, U = B u D => stored pair Q,U 3) Q = A/B u (C/D)c = A/B u Cc u D = (A/B u D) u Cc = Q u Cc Qc = C / (ABc u D) = C (Ac u B) n Dc = C(B u Ac) BC / (A+D) = BCAcDc = BCAc CAc /(A+D) = CAcAcDc = CAc BCAc + CAc 4) Q = A/B n (C/D)c = A/B n(D u Cc) = Q=A(D u Cc) Qc = (B u Ac) u (C n Dc) = U + Vc, U = B u C => stored pair Q,U 5) Q = (A/B)c u (C/D)c = B u D u (AnC)c AnC / (B u D) 6) Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before |# (define advanced-set-printer #t) ... ... @@ -199,7 +156,8 @@ Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before (begin code ...)))) (define-tool make-complementable-set make-complementable-set-mac (smember ∅ union intersection difference tripple equiv? set-size set? (smember ∅ union intersection difference tripple equiv? equiv4? set-size set? make-one) (define Ω (make-set- ∅ ∅ ∅ #t #t)) ... ... @@ -219,87 +177,113 @@ Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before (if pred Ω ∅) x)) x)) (_ x))) (define (u2 f ff) (lambda x (match x ((a b) (if (or (cset? a) (cset? b)) (f a b) (ff a b))) (x (apply f x))))) (define (u1 f ff) (lambda (a) (if (set? a) (f a) (ff a)))) (define (empty? x) (eq? x ∅)) (define uSSo (u2 (case-lambda (() ∅) ((x) (union x)) ((x y) ((x) (if (cset? x) x (union x))) ((x y) (match (list x y) ;;; (A⊔Bᶜ)∪(C⊔Dᶜ) = (A∪C)⊔(B∩D)ᶜ = X⊔Yᶜ, Y∖X=Y. (((? empty?) _) (uSSo y)) ((_ (? empty?)) (uSSo x)) (((\$ a1 b1 c1 #t) (\$ a2 b2 c2 #t)) (ifΩ (make-set (union a1 a2) (union (difference b1 a2) (difference b2 a1)) (intersection c1 c2) #t))) (let ((a (union a1 a2))) (make-set a (union (difference b1 a2) (difference b2 a1)) (difference (intersection c1 c2) a) #t)))) (((\$ a1 b1 c1 #t) (\$ a2 b2 c2 #f)) (ifΩ (make-set (union a1 a2) (union (difference b1 a2) (difference b2 a1)) (difference c1 c2) #t))) (let ((a (union a1 a2))) (make-set a (union (difference b1 a2) (difference b2 a1)) (difference c1 c2 a) #t)))) (((\$ a1 b1 c1 #f) (\$ a2 b2 c2 #t)) (ifΩ (make-set (union a1 a2) (union (difference b1 a2) (difference b2 a1)) (difference c2 c1) #t))) (let ((a (union a1 a2))) (make-set a (union (difference b1 a2) (difference b2 a1)) (difference c2 c1 a) #t)))) (((\$ a1 b1 c1 #f) (\$ a2 b2 c2 #f)) (ifΩ (let ((a (union a1 a2) )) (make-set a (union (difference b1 a2) (difference b2 a1)) (difference (union c1 c2) a) #f)))) (let ((a (union a1 a2))) (make-set a (union (difference b1 a2) (difference b2 a1)) (difference (union c1 c2) a) #f)))) ;;; (A⊔Bᶜ)∪C = (A∪C)⊔(B∖C)ᶜ = X⊔Yᶜ, Y∖X=Y. (((\$ a b #t) c) (((\$ ) c) (uSSo x (make-set ∅ ∅ (union c) #f))) (((\$ a b #f) c) (uSSo x (make-set ∅ ∅ (union c) #f))) ((a (\$ c d #t)) (uSSo y (make-set ∅ ∅ (union c) #f))) ((c (\$ a b #f)) (uSSo y (make-set ∅ ∅ (union c) #f))) ((c (\$ )) (uSSo (make-set ∅ ∅ (union c) #f) y)) ;; A∪C ((a c) (union a c)))) ((x y . l) (uSSo x (apply uSSo y l))))) (uSSo x (apply uSSo y l)))) union)) (define uSS (u2 (case-lambda (() ∅) ((x) (union x)) ((x) (if (cset? x) x (union x))) ((x y) (match (list x y) (((? empty?) x) (uSSo x)) ((x (? empty?)) (uSSo x)) (((\$ a1 b1 c1 #t) (\$ a2 b2 c2 #t)) (ifΩ (make-set (union a1 a2) ∅ (intersection c1 c2) #t))) (let ((a (union a1 a2))) (make-set a ∅ (difference (intersection c1 c2) a) #t)))) (((\$ a1 b1 c1 #f) (\$ a2 b2 c2 #f)) (ifΩ (ifΩ (let ((a (union a1 a2))) (make-set a ... ... @@ -309,46 +293,44 @@ Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before (((\$ a1 b1 c1 #f) (\$ a2 b2 c2 #t)) (ifΩ (make-set (union a1 a2) ∅ (difference c2 c1) #t))) (let ((a (union a1 a2))) (make-set a ∅ (difference c2 c1 a) #t)))) (((\$ a1 b1 c1 #t) (\$ a2 b2 c2 #f)) (ifΩ (make-set (union a1 a2) ∅ (difference c1 c2) #t))) (let ((a (union a1 a2))) (make-set a ∅ (difference c1 c2 a) #t)))) (((\$ a b #t) c) (((\$ _ _ _ _) c) (uSS x (make-set ∅ ∅ (union c) #f))) (((\$ a b #f) c) (uSS x (make-set ∅ ∅ (union c) #f))) ((a (\$ c d #t)) (uSS (make-set ∅ ∅ (union a) #f) y)) ((c (\$ _ _ _ _)) (uSS (make-set ∅ ∅ (union c) #f) y)) ((a (\$ c d #f)) (uSS (make-set ∅ ∅ (union a) #f) y)) ((a c) (union a c)))) ((x y . l) (uSS x (apply uSS y l))))) (uSS x (apply uSS y l)))) union)) (define nSSo (u2 (case-lambda (() Ω) ((x) (union x)) ((x) (if (cset? x) x (union x))) ((x y) (match (list x y) ;;;(A⊔Bᶜ)∩(C⊔Dᶜ) = ∅ ⊔ (B∪D)ᶜ = X⊔Yᶜ, Y∖X=Y (((\$ a1 b1 c1 #f) (\$ a2 b2 c2 #f)) (ifΩ (let ((i1 (intersection a1 c2)) ... ... @@ -390,14 +372,15 @@ Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before (((\$ a1 b1 c1 #t) (\$ a2 b2 c2 #t)) (ifΩ (let ((i1 (difference a1 c2)) (i2 (difference a2 c1))) (let* ((i1 (difference a1 c2)) (i2 (difference a2 c1)) (a (union (intersection a1 a2) i1 i2))) (make-set (union (intersection a1 a2) i1 i2) a (difference (difference (union b1 (addition a1 a2) b2) i1) i2) (union c1 c2) (difference (union c1 c2) a) #t)))) (((\$ _ _ _ _) c) ... ... @@ -410,14 +393,21 @@ Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before (intersection a b)))) ((x y . l) (nSS x (apply nSS y l))))) (nSS x (apply nSS y l)))) intersection)) (define nSS (u2 (case-lambda (() Ω) ((x) (union x)) ((x) (if (cset? x) x (union x))) ((x y) (match (list x y) (((? empty?) x) ∅) ((x (? empty?)) ∅) (((\$ a1 b1 c1 #f) (\$ a2 b2 c2 #f)) (ifΩ (let ((i1 (intersection a1 c2)) ... ... @@ -453,75 +443,84 @@ Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before (((\$ a1 b1 c1 #t) (\$ a2 b2 c2 #t)) (ifΩ (let ((i1 (difference a1 c2)) (i2 (difference a2 c1))) (let* ((i1 (difference a1 c2)) (i2 (difference a2 c1)) (a (union (intersection a1 a2) i1 i2))) (make-set (union (intersection a1 a2) i1 i2) a ∅ (union c1 c2) (difference (union c1 c2) a) #t)))) (((\$ _ _ _ _) c) (nSSo x (make-set ∅ ∅ (union c) #f))) (nSS x (make-set ∅ ∅ (union c) #f))) ((c (\$ _ _ _ _)) (nSSo (make-set ∅ ∅ (union c) #f) y)) (nSS (make-set ∅ ∅ (union c) #f) y)) ((a b) (intersection a b)))) ((x y . l) (nSSo x (apply nSSo y l))))) (nSS x (apply nSS y l)))) intersection)) (define cS (lambda (x) (match x ((\$ a b c #t) (ifΩ (let ((aa (intersection b c))) (make-set aa (union a (difference b c)) (difference c a aa) #f)))) (define (cS x) (match x ((\$ a b c #t) (ifΩ (let ((aa (intersection b c))) (make-set aa (union a (difference b c)) (difference c a aa) #f)))) ((\$ a b c #f) (ifΩ (let ((aa (difference b c))) (make-set aa (union a (intersection b c)) (difference (union a c) aa) #t)))) ((\$ a b c #f) (ifΩ (make-set (difference b c) (union a (intersection b c)) (union a c) #t))) (x (cond ((eq? x ∅) Ω) ((eq? x Ω) ∅) (else (ifΩ (make-set ∅ ∅ (union x) #t))))))) (x (cond ((eq? x ∅) Ω) ((eq? x Ω) ∅) (else (ifΩ (make-set ∅ ∅ (union x) #t)))))))) (define ∖SS (u2 (case-lambda ((a) a) ((a) (uSS a)) ((a b) (nSS a (cS b))) ((a b . l) (apply ∖SS (∖SS a b) l)))) (apply ∖SS (∖SS a b) l))) difference)) (define ∖SSo (u2 (case-lambda ((a) a) ((a) (uSS a)) ((a b) (nSSo a (cS b))) ((a b . l) (apply ∖SSo (∖SSo a b) l)))) (apply ∖SSo (∖SSo a b) l))) difference)) (define ⊕SS (u2 (case-lambda (() ∅) ((a) a) ((a) (uSS a)) ;; A ⊕ B = A∖B ∪ B∖A ((a b) (let ((a (make-one a)) ... ... @@ -529,12 +528,14 @@ Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before (uSS (∖SS a b) (∖SS b a)))) ((a b . l) (let ((a (make-one a))) (⊕SS a (apply ⊕SS b l)))))) (⊕SS a (apply ⊕SS b l))))) addition)) (define ⊕SSo (u2 (case-lambda (() ∅) ((a) (union a)) ((a) (uSS a)) ;; A ⊕ B = A∖B ∪ B∖A ((a b) (let ((a (make-one a)) ... ... @@ -542,12 +543,17 @@ Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before (uSSo (∖SSo a b) (∖SSo b a)))) ((a b . l) (let ((a (make-one a))) (⊕SSo a (apply ⊕SSo b l)))))) (⊕SSo a (apply ⊕SSo b l))))) addition)) (define (≡SS x y) (match (list x y) (((\$ x1 y1 z1) (\$ x2 y2 z2)) (and (equiv? x1 x2) (equiv? y1 y2) (eq? z1 z2))) (((\$ a1 b1 c1 p1) (\$ a2 b2 c2 p2)) (and (eq? p1 p2) (if p1 (equiv? c1 c2) (equiv4? a1 c1 a2 c2)))) ((_ (\$ )) (≡SS (make-set ∅ ∅ x #f) y)) (((\$ ) _) ... ... @@ -555,10 +561,10 @@ Q = (A/B)c n (C/D)c = (B u Ac) n (C u Dc) = .. as before ((x y) (equiv? x y)))) (define (⊆SS x y) (≡SS (nSS x y) (uSS x ∅))) (≡SS (nSS x y) (uSS x))) (define (⊂SS x y) (and (not (≡SS x y)) (≡SS (nSS x y) (uSS x ∅)))) (and (not (≡SS x y)) (≡SS (nSS x y) (uSS x)))) (define (->set x) (match (ifΩ x) ... ...
 ... ... @@ -4,7 +4,8 @@ #:use-module (srfi srfi-9) #:use-module (srfi srfi-9 gnu) #:export ( set? set-hash set-n make-set-from-assoc make-set-from-assoc-mac set-size)) make-set-from-assoc make-set-from-assoc-mac set-size set-hash)) #| This takes an assoc like library and transforms it to an ordered/undordered ... ... @@ -132,13 +133,12 @@ Output: set operations and iteratables (define-tool make-set-from-assoc make-set-from-assoc-mac (null assoc acons delete hash mk-kv kv? kv-key kv-val sizefkn value? order? equal? ar->l l->ar) value? order? equal? ar->l l->ar) (define ∅ (make-set '() null 0 0 (list set->kvlist))) (define size 10000000000000) (define size (@@ (ice-9 set vhashx) *size*)) (define (l-serie app) (define mt null) (let lp ((app app)) ... ... @@ -163,6 +163,7 @@ Output: set operations and iteratables (if (set? x) x (let ((kv (mk-kv x))) (hash kv size) (make-set (l->ar (list kv)) (acons kv null) 1 (hash kv size) (list set->kvlist))))) ... ... @@ -240,6 +241,44 @@ Output: set operations and iteratables #f) #f)))) (define (≡4 x1 x2 y1 y2) (match (list (make-one x1) (make-one x2) (make-one y1) (make-one y2)) (((\$ lx1 mx1 nx1 hx1) (\$ lx2 mx2 nx2 hx2) (\$ ly1 my1 ny1 hy1) (\$ ly2 my2 ny2 hy2)) (if (= (logxor hx1 hx2) (logxor hy1 hy2)) (if (= (+ nx1 nx2) (+ ny1 ny2)) (let () (define (try lx1 mx1) (let lp ((lx1 (l-serie lx1))) (if (pair? lx1) (let ((kv (car lx1))) (if kv (let ((kvx (assoc kv mx1))) (if kvx (let ((kvy1 (assoc kv my1))) (if kvy1 (if (equal? kvx kvy1) (lp (cdr lx1)) #f) (let ((kvy2 (assoc kv my2))) (if kvy2 (if (equal? kvx kvy2) (lp (cdr lx1)) #f) #f)))) (lp (cdr lx1)))) (lp (cdr lx1)))) #t))) (and (try lx1 mx1) (try lx2 mx2))) #f) #f)))) (define (o≡ x y) (match (list (make-one x) (make-one y)) (((\$ lx mx nx hx) (\$ ly my ny hy)) ... ... @@ -302,6 +341,84 @@ Output: set operations and iteratables #f) #f))))) (define (o≡4 x1 x2 y1 y2) (match (list (make-one x1) (make-one x2) (make-one y1) (make-one y2)) (((\$ lx1 mx1 nx1 hx1) (\$ lx2 mx2 nx2 hx2) (\$ ly1 my1 ny1 hy1) (\$ ly2 my2 ny2 hy2)) (let () (define (do-the-iteration) (define (assocx kv) (let ((kvx (assoc kv mx1))) (if kvx kvx (assoc kv mx2)))) (define (assocy kv) (let ((kvx (assoc kv my1))) (if kvx kvx (assoc kv my2)))) (let lp ((lx (l-serie (make-append lx1 lx2))) (ly (l-serie (make-append ly1 ly2)))) (if (pair? lx) (let ((kvx (car lx))) (if kvx (begin (let ((kvxx (assocx kvx))) (if kvxx (if (order? kvxx) (set! kvx kvxx) (let ((kvy (assocy kvxx))) (if kvy (if (order? kvy) (set! kvx kvxx) (lp (cdr lx) ly)) #f))) (lp (cdr lx) ly))) (let lp2 ((ly ly)) (if (pair? ly) (let ((kvy (car ly))) (begin (let ((kvyy (assocy kvy))) (if kvyy (if (order? kvyy) (set! kvy kvyy) (let ((kvxx (assocx kvyy))) (if kvxx (if (equal? kvxx kvx) (lp (cdr lx) (cdr ly)) (if (order? kvxx) #f (lp2 (cdr ly)))) #f))) (lp2 (cdr ly)))) (if (equal? kvx kvy) (lp (cdr lx) (cdr ly)) #f))) #f))) (lp (cdr lx) ly))) (let lp2 ((ly ly)) (if (pair? ly) (let ((ky (assocy (car ly)))) (if ky #f (lp2 (cdr ly)))) #t))))) (if (= (logxor hx1 hx2) (logxor hy1 hy2)) (if (= (+ nx1 nx2) (+ ny1 ny2)) (do-the-iteration) #f) #f))))) (define (next-mute lp ll l m n h) (lp (cdr ll) l m n h)) ... ... @@ -313,8 +430,9 @@ Output: set operations and iteratables (lp (cdr ll) (cons kv l) m n h)) (define (next-add-kv lp ll l m n h kv kv*) (lp (cdr ll) (cons kv* l) (acons kv* m) (+ n 1) (logxor h (hash kv* size)))) (lp (cdr ll) (cons kv* l) (acons kv* m) (+ n 1) (begin (hash kv* size) (logxor h (hash kv* size))))) (define (next-add-l lp ll l m n h kv*) (lp (cdr ll) (cons kv* l) m n h)) ... ... @@ -619,8 +737,10 @@ Output: set operations and iteratables r))) (values #:member member #:= ≡ #:u u #:n n #:- s- #:+ s+ #:< ⊂ #:<= ⊆ #:o= o≡ #:ou ou #:on on #:o- o- #:o+ o+ #:o< o⊂ #:o<= o⊆ #:= ≡ #:=4 ≡4 #:u u #:n n #:- s- #:+ s+ #:< ⊂ #:<= ⊆ #:o= o≡ #:o=4 o≡4 #:ou ou #:on on #:o- o- #:o+ o+ #:o< o⊂ #:o<= o⊆ #:n- tripple #:in in #:fold fold #:map map #:for-each for-each #:empty ∅ #:set->list set->list #:set->assoc set->assoc ... ...
 ... ... @@ -30,6 +30,8 @@ #:export (vhashx-null vhashx? vhashx-length vhashx-cons vhashx-assoc)) (define *size* 100000000000000000) ;;; Author: Ludovic Courtès ;;; ;;; Commentary: ... ...
 ... ... @@ -256,7 +256,8 @@ (if (eq? ch #\.) (lp #f ch (cons #\. r) #t) (lp #f ch (cons #\. r) #f)) (list->string (reverse (cons #\. r)))))))) (list->string ((@ (guile) reverse) (cons #\. r)))))))) (#\, (read-char) ... ...
 ... ... @@ -18,20 +18,30 @@ mk-prolog-biop -> s a))