# A logical reading in a specification on division on family of sets similar to division by 0

**URL:** <https://swi-prolog.discourse.group/t/a-logical-reading-in-a-specification-on-division-on-family-of-sets-similar-to-division-by-0/5957>\
**Category:** Discussion\
**Tags:** zdd, divide-by-zero\
**Created:** [November 21, 2022, 3:37pm UTC](https://swi-prolog.discourse.group/t/a-logical-reading-in-a-specification-on-division-on-family-of-sets-similar-to-division-by-0/5957 "2022-11-21T15:37:59Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [November 21, 2022, 3:37pm UTC](https://swi-prolog.discourse.group/t/a-logical-reading-in-a-specification-on-division-on-family-of-sets-similar-to-division-by-0/5957/1 "2022-11-21T15:37:59Z")

</div>

Here is an exercise for ZDD programming. Let X, Y be a family of sets. For X, Y, compute a family Z of sets defined

```prolog
	Z = { A in X | forall B in Y B is a subset of A }.

```

Let the symbol X / Y be for Z for simplicity in the following. For example.

```prolog
			 {{a, b}} / {{a}} = {{a, b}}
 {{a, b}, {c, d}, {a, d}} / {{a}, {d}} = {{a, d}}

```

This should be an easy exercise, but I took time to point out bugs on my initial easy codes. The codes listed below is now correct, I hope. The first one of the following equations was most difficult to find, which was against my intuition.

```prolog
			X / {} = X
			X / {{}} = X

```

However, I noticed, if one stands on logical reading of forall/exists used in the given problem specification, both of them sounds quite natural.

> **Sample Query, and codes.**
>
> ```prolog
> % ?- #S, X<< +[*[a,b], *[c,d], *[a, d]], Y<< +[*[a], *[d]],
> %	zdd_divisible_by_all(X, Y, Z, S), psa(Z, S).
> %@ zid = 8
> %@ [a,d]
> %@ -------------------
> %@ S = ..,
> %@ X = 11,
> %@ Y = 12,
> %@ Z = 8.
> 
> zdd_divisible_by_all(X, Y, X, _):-Y<2, !. % was a bug.
> zdd_divisible_by_all(X, _, 0, _):-X<2, !. % was a bug.
> zdd_divisible_by_all(X, Y, Z, S):- memo(div_by_all(X, Y)-Z, S),
> (	nonvar(Z) -> true
> ; cofact(X, t(A, L, R), S),
> zdd_divisible_by_all(L, Y, L0, S),
> zdd_divisible_by_all(A, R, Y, R0, S),
> zdd_join(L0, R0, Z, S)
> ).
> %
> zdd_divisible_by_all(A, X, Y, Z, S):- Y<2, !,
> cofact(Z, t(A, 0, X), S).
> zdd_divisible_by_all(A, X, Y, Z, S):- cofact(Y, t(B, L, R), S),
> zdd_compare(C, A, B, S),
> (	C = (<) ->
> zdd_divisible_by_all(X, Y, Z0, S),
> zdd_insert(A, Z0, Z, S)
> ;	C = (=) ->
> zdd_divisible_by_all(X, R, R1, S),
> zdd_insert(A, R1, R0, S),
> zdd_divisible_by_all(R0, L, Z, S)
> ;	Z = 0 % Was a bug.
> ).
> 
> ```

> **\`zdd\_divisible\_by\_all/4\` seems efficient.**
>
> ```prolog
> % ?- N = 300, #S, numlist(1, N, Ns), X<<pow(Ns), Y << +[*Ns],
> %	time(zdd_divisible_by_all(X, Y, Z, S)), psa(Z, S).
> %@ % 1,772,696 inferences, 0.127 CPU in 0.133 seconds (95% CPU, 14007317 Lips)
> %@ zid = 900
> %@ [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300]
> %@ -------------------
> %@ N = 300,
> %@ S = ..,
> %@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
> %@ X = 301,
> %@ Y = Z, Z = 900.
> 
> ```

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [November 24, 2022, 3:38am UTC](https://swi-prolog.discourse.group/t/a-logical-reading-in-a-specification-on-division-on-family-of-sets-similar-to-division-by-0/5957/3 "2022-11-24T03:38:33Z")

</div>

> [@anon95304481](#):
>
> Maybe if you could establish a Galois connection between your  
> ZDD based “Sets” and the ordinary sets lets say from ZFC. So  
> that we could refute or verify your equation?

Thanks for the comment. I will check it later.

I use analogy of operations multiplication \* and addition + on polynomials when I write operations on ZDD. This is useful sometime and also misleading sometime, in particular, division by zero, which is not defined in the mathematics. My code `zdd_divisible_by_all` was the latter case.

> [@anon95304481](#):
>
> Counter example:
> 
> ```prolog
> X = { {}, {{}}, {{},{{}}} }.
> 
> ```

As ZDD treats only families of sets of atoms (urelements) in a totally ordered universe, this X is not allowed for ZDD, I think. Anyway I appreciate your “wild” idea, I like it personally.

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [November 24, 2022, 5:36pm UTC](https://swi-prolog.discourse.group/t/a-logical-reading-in-a-specification-on-division-on-family-of-sets-similar-to-division-by-0/5957/5 "2022-11-24T17:36:30Z")

</div>

You seem to have catch up easily with my naive analogy  
of polynomial to zdd. However, I don’t have any precise description  
of such analogy. This analoly is useful only partially for me,  
which helps writing codes on ZDD operations.

I hope following equations exlains my intuition to you. Please don’t  
ask me further on this informal analogy

```prolog
{} = 0,

{{}} = 1,

{{a,b}, {c,d}} = a*b + c*d

```

```prolog
divmod(a*b+c, a, b, c) ~ divmod(3*5+4, 3, 5, 4) ( divmod/4 )

```

```prolog
{{a,b}, {a,c}}/{a} = (a*b + a*c)/a = 
		= a*(b+c)/a 
		= b+c 
		= {{b}, {c}}

```

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [November 25, 2022, 5:42am UTC](https://swi-prolog.discourse.group/t/a-logical-reading-in-a-specification-on-division-on-family-of-sets-similar-to-division-by-0/5957/7 "2022-11-25T05:42:23Z")

</div>

> [@anon95304481](#):
>
> You can try yourself, use this, which implements your specification:
> 
> > [@anon95304481](#):
> >
> > ```prolog
> > mukai_op(X, Y, Z) :-
> > findall(A, (member(A,X),
> > forall(member(B,Y),subset(B,A))), Z).
> > 
> > ```

This seems to be a specification for `zdd_divisibles_by_all`.

```prolog
%! zdd_divisible_by_all(+X, +Y, -Z, +S) det.
%	Z = { A in X | forall B in Y B is a subset of A }.

% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, shift(zdd_divisible_by_all(X, Y, Z)), psa(Z))).
%@ zid = 3
%@ [a,b]
%@ -------------------
%@ X = 7,
%@ Y = 9,
%@ Z = 3.

```

I intended to show `zdd_div` in stead, by changing quantifier forall to exists.

````prolog
%!	zdd_div(+X, +Y, -Z, +S) is det.
%	Z is the quotient of X divided by Y;
%	Z = { A - B | A in X, B in Y, B is a subset of A }

% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, zdd_div(X, Y, Z), psa(Z))).
%@ zid = 10
%@ [c]
%@ [b]
%@ [a]
%@ -------------------
%@ X = 7,
%@ Y = 9,
%@ Z = 10.
% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))).
%@ zid = 8
%@ [a]
%@ -------------------
%@ X = 7,
%@ Y = 2,
%@ Z = 8.
% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))).
%@ zid = 6
%@ [c]
%@ [b]
%@ -------------------
%@ X = 7,
%@ Y = 8,
%@ Z = 6.
```
Anyway I have written a dozen of div like operations leaded by ZDD as polynomial analogy for various use of filters on ZDD. I must be careful not getting into confusion.
````

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [November 25, 2022, 8:02am UTC](https://swi-prolog.discourse.group/t/a-logical-reading-in-a-specification-on-division-on-family-of-sets-similar-to-division-by-0/5957/9 "2022-11-25T08:02:18Z")

</div>

> [@anon95304481](#):
>
> Use [cofactors](https://en.wikipedia.org/wiki/Boole%27s_expansion_theorem):

Yes. In fact, for my ZDD library, `cofact/3` is most fundamental and essential operation for all other operations including those div-like ones on ZDD. I think it is like ` [_|_]` construct in Prolog for list processing by recursion. It is so clear operation on ZDD, I often come to think there is really no need to say much about to others about ZDD. It is so simple and clear. Also always I strongly believe that some SWI-Prologers could implement much better ZDD library than mine.

```prolog
%!	cofact(?X, ?C, +State) is det.
% X is unified with the index of a triple C, or
% C is unified with the triple t/3 stored at index X of the array.

cofact(X, C, S):- nonvar(X), !, % X>1 assumed.
	vector_of_state(S, Vec),
    arg(X, Vec, C).
cofact(X, t(_, X, 0), _):-!. % the famous Minato's zero-suppress rule.
cofact(X, C, S):- array_hash_of_state(S, A, H),
	hash_update(C, H, X), % check C-X entry in H (hash)
	(	nonvar(X) -> true % exists.
	;	new_array_elem(C, A, X)	% new.
	).

```

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [November 25, 2022, 9:56pm UTC](https://swi-prolog.discourse.group/t/a-logical-reading-in-a-specification-on-division-on-family-of-sets-similar-to-division-by-0/5957/11 "2022-11-25T21:56:07Z")

</div>

> [@anon95304481](#):
>
> Can you use your division to compute the inverse of a binary matrice?

No. As far as I know, ZDD performs basically only standard union/intersection/subtraction/merge on families of sets of atoms, where merge (multiplication)

```prolog
 X*Y = { union of A and B | A in X, B in Y }. 

```

```prolog
% ?- #S, X<<{[a,b],[c,d]}, Y<<{[x], [y]}, Z<< (X*Y), psa(Z, S).
%@ zid = 14
%@ [c,d,y]
%@ [c,d,x]
%@ [a,b,y]
%@ [a,b,x]
%@ -------------------
%@ S = ..,
%@ X = 6,
%@ Y = 9,
%@ Z = 14.

```