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

Discussion
,
1

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

	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.

			 {{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.

			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. 
% ?- #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. 
% ?- 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.
2

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?

In ZFC we have {} =\= {{}}, and we also do not have in general:

X / {{}} = X.

Counter example:

X = { {}, {{}}, {{},{{}}} }.

Then we get X =\= X / {{}}:

X / {{}} = { {{}}, {{},{{}}} }.

Fun fact, in von Neumann Ordinals we have 0 = {} and 1 = { {} }.
And X = 3 = {0,1,2}. So basically X / 1 = {1,2}.

Most likely your symbol / doesn’t mean set difference?

3

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.

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.

4

Let me translate, this is the definition of X / Y right? So it is defined as:

X / Y = { A ∈ X | ∀B(B ∈ Y → B ⊆ A) }

Now since SWI-Prolog lists has subset/2, we could define it as follows:

mukai_op(X, Y, Z) :-
   findall(A, (member(A,X),
         forall(member(B,Y),subset(B,A))), Z).

I can verify the two examples:

?- mukai_op([[a, b]], [[a]], Z).
Z = [[a, b]].

?- mukai_op([[a, b], [c, d], [a, d]], [[a], [d]], Z).
Z = [[a, d]].

You can also use it with my X, the elements of the elements are also
orderable, at least Prolog (@<)/2 would do so. And I guess my mistake
was assuming that your symbol / means set difference? Since SWI-prolog

lists has subtract/3, we can compare the mistaken results:

?- mukai_op([[], [[]], [[], [[]]]], [[]], Z).
Z = [[], [[]], [[], [[]]]].

?- subtract([[], [[]], [[], [[]]]], [[]], Z).
Z = [[[]], [[], [[]]]].

You find subtract aka set difference indeed in the wild. It is part of
the lists library of SWI-Prolog. And usually the mathematical symbol
for difference is the back slash, you use the forward slash:

The relative complement of A in B is denoted B\A
according to the ISO 31-11 standard
https://en.wikipedia.org/wiki/Complement_(set_theory)#Relative_complement

One finds also the subtract sign used for this purpose, and an alternative name
for set difference is relative complement. But your operation isn’t all that and
since you use the forward slash, what does it have

in common with division? Could you enlighten us?

Edit 24.11.2022
You could define a division and a remainder:

X / Y = { A ∈ X | ∀B(B ∈ Y → B ⊆ A) }
X # Y = { A ∈ X | ∃B(B ∈ Y ∧ ¬B ⊆ A) }

You would then have:

X = (X / Y) ∪ (X # Y)

Is that the idea? But where is the multiplication for the division
remainder equation, which would be X = ((X / Y)*Y) ∪ (X # Y).
It also doesn’t fit the usual laws of division.

5

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

{}	 = 0,

{{}} = 1,

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

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

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

The only problem is that mukai_op/3 doesn’t deliver this result.
Maybe there is an error in the specification or in the implementation.
You can try yourself, use this, which implements your specification:

And now try the proposed division, its not reproducible. According
to what you posted the result should be [[b], [c]]. But I cannot
reproduce such a result:

?- mukai_op([[a,b], [a,c]], [a], X).
ERROR: No rule matches lists:subset(a,[a,b])

?- mukai_op([[a,b], [a,c]], [[a]], X).
X = [[a, b], [a, c]].

Your specification of X\Y is such that result is a subset of X. But you gave
an example where the result is also reduced in the multiplication dimension,
not only in the addition dimension.

7

This seems to be a specification for zdd_divisibles_by_all.

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

%!	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.
8

Fun fact. In the usual boolean ring, if you replace addition/disjunction (+)/2
with exclusive or/xor (++)/2, when forming polynomials, you get this

factoring. For every formula A and for every propositional variable
X, there are two formulas B and C, such that;

A = X*B ++ C.

So we could say there is this division B = A/X and this remainder
C = A#X. How determine B and C? Use cofactors:

C = A[X/0]
B = A[X/1] ++ A[X/0]

Would your division also give B and C somehow? This is the
special case where we divide by a singleton only.

If you repeat the process with different propositional
variables, you get the ring sum normalform.

9

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.

%!	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.
	).
11

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

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

% ?- #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.