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

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