Operations on families of lists with extentionality

General
1

Library(pac/zdd) can handle families of lists with extentionality as well as the standard families of sets. In fact, for each given family F of lists, a unique id integer i is given, written i → F, in such a way that with i → F, and j → G, 1 and 2 are equivalent.

Extentionality

  1. i = j
  2. F = G as sets of lists .

Wihtout going to details, let me use a sample predicate coalgebra_for_signature/5, which I wrote yesterday in an half hour including comments, and its sample queries below.

I am not sure if there exists similar predicates to coalgebra_for_signature/5 in ordinal prolog programming, but I remember vaguely I saw an announcement somewhere on the net on such library without descriptions, and I have still no other relevant information.

Programming on families of lists with extentionaly is just an extention of the well-known cons-car-cdr prgraming on binary cells in Lisp to that on families of lists as seen in the codes below.

I would be glad to find readers on this forum who shares interest with such extentionality programming in Prolog. IMO, Minoto’s zero suppress rule of ZDD could be generalized on families of ZDD(X) like ZDD(sets), ZDD(lists), ZDD(assignments), etc, though I did not mention explicitly so far, and I haven’t formalized yet precisely.

%!	coalgebra_for_signature(+D, +Sgn, +As, -E, +S) is det.
%	E is unified with the set of all functions from D
%	to the set of signature terms over signature Sgn and
%	with arguments in As.

% ?- zdd coalgebra_for_signature([x], [f/1], [x], E), psa(E).
%@  zid = 5
%@ 	[(x->f(x))]
%@ -------------------
%@ E = 5.

% ?- zdd coalgebra_for_signature([x,y], [f/1,g/2], [x,y,1], E), psa(E).
%@  zid = 373
%@ 	[(x->g(y,y)),(y->g(y,y))]
%@ 	[(x->g(y,y)),(y->g(y,x))]
%@ 	[(x->g(y,y)),(y->g(y,1))]
%@ 	[(x->g(y,y)),(y->g(x,y))]
%@ 	[(x->g(y,y)),(y->g(x,x))]
%@ 	[(x->g(y,y)),(y->g(x,1))]
%@ 	[(x->g(y,y)),(y->g(1,y))]
%@ 	[(x->g(y,y)),(y->g(1,x))]
%@ 	[(x->g(y,y)),(y->g(1,1))]
%@ 	[(x->g(y,y)),(y->f(y))]
%@ 	[(x->g(y,y)),(y->f(x))]
%@ 	[(x->g(y,y)),(y->f(1))]
%@ 	[(x->g(y,x)),(y->g(y,y))]
%@ 	[(x->g(y,x)),(y->g(y,x))]
%@ 	[(x->g(y,x)),(y->g(y,1))]
%@ 	[(x->g(y,x)),(y->g(x,y))]
%@ 	[(x->g(y,x)),(y->g(x,x))]
%@ 	[(x->g(y,x)),(y->g(x,1))]
%@ 	[(x->g(y,x)),(y->g(1,y))]
%@ 	[(x->g(y,x)),(y->g(1,x))]
%@ 	[(x->g(y,x)),(y->g(1,1))]
%@ 	[(x->g(y,x)),(y->f(y))]

<snip many lines> 

%@ -------------------
%@ E = 373.

% ?- time((zdd coalgebra_for_signature([x,y,z,u,v], [f/2,g/2,h/2],
%	[x,y,z,u,v,0,1], E), card(E, C))).
%@ % 12,546,674 inferences, 1.040 CPU in 1.062 seconds (98% CPU, 12068183 Lips)
%@ E = 173825,
%@ C = 68641485507.

coalgebra_for_signature(D, Sgn, As, E, S):-
	signature(Sgn, As, T, S),
	signature_map(D, T, E, S).
%
signature_map([], _, 1, _):-!.
signature_map([X|Xs], T, E, S):-
	signature_map(Xs, T, E0, S),
	extend_signature_map(X, T, E0, E, S).
%
extend_signature_map(_, 0, _, 0, _):-!.
extend_signature_map(_, 1, E, E, _):-!.
extend_signature_map(X, T, E, F, S):- cofact(T, t(A, L, _), S),
	extend_signature_map(X, L, E, E0, S),
	l_cons(X->A, E, E1, S),
	zdd_join(E0, E1, F, S).

l_cons(_, 0, 0, _):-!.
l_cons(A, 1, U, S):-!, zdd_singleton(A, U, S).
l_cons(A, Y, U, S):- cofact(Y, t(B, L, R), S),
	l_cons(A, L, L0, S),
	l_append([A, B], R, R0, S),
	zdd_join(L0, R0, U,  S).
%
l_append([], X, X, _).
l_append([A|As], X, Y, S):-
	l_append(As, X, X0, S),
	cofact(Y, t(A, 0, X0), S).
2

EDIT [2023/12/20]

Viewing that ZDD system is a kind of a dynamic assoc list,
I have introduced bidirectional obj_id/3 which gives
an integer as unique identifier of the given ground prolog term as object,
and vice versa as below. From my experience on zdd,
I expect this tiny new helper predicate obj_id surely is handy without
loss of efficiency. I had replaced the get_root_atom/3 and zdd_singleton/3 with this bidirectional obj_id/3 in power_list/4, which got a little bit faster after replacing.

%!	obj_id(?X, ?Y, +S) is det.
%	Bidirectional. Y is the atom of the root X.
% ?- zdd obj_id([a,b,c], Id), obj_id(Obj, Id).
%@ Id = 2,
%@ Obj = [a, b, c].
obj_id(X, Id, S):-  cofact(Id, t(X, 0, 1), S).

END EDIT

I have rewritten codes power_list/4, which enumerates the set of lists of up to specified length whose elements are of a given set.

% ?- N = 100, numlist(1, N, _Ns),
%	time(((zdd power_list(N, _Ns, X), card(X, _Count)))),
%	_Count > 100^100, writeln(_Count).
%@ % 29,681,962 inferences, 2.735 CPU in 2.917 seconds (94% CPU, 10853693 Lips)
%@ 101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101
%@ N = 100,
%@ X = 515002.

The new version is about 10 times faster than old one. It uses a new simple technique on hashing in ZDD which I found recently. I expect it would be also useful for cases in which structure objects must be passed around as arguments but not suitable for hashing. See power_list_with_id/4and all_list_with_id/4 below which uses id number in stead of the structured objects, though I am not sure how this tricks are really effective on hashing.

For those who might be intereseted, I have attached a short memo
on family of lists, on which codes below really is based,
being afraid it is well known to the reader.

Codes on `power_list/4` and `all_list/4 
%!	get_root_atom(+X, -Y, +S) is det.
%	Y is unified with the atom of the root X.
get_root_atom(X, Y, S):- cofact(X, t(Y, _, _), S).

%!	power_list(+N, +As, -P, +S) is det.
%	P is unified with lists L such that length of L  is less than N, and
%	all members of L is in As.

power_list(N, As, P, S):- zdd_singleton(list(As), Id, S),
	power_list_with_id(N, Id, P, S).
%
power_list_with_id(0, Id, 1, S):-!, memo(power_list(0, Id)-1, S).
power_list_with_id(N, Id, Y, S):-
	N0 is N - 1,
	power_list_with_id(N0, Id, Y0, S),
	all_list_with_id(N, Id, Y1, S),
	zdd_join(Y0, Y1, Y, S).

%!	all_list(+N, +As, -X, +S) is det.
%	X is unified with the family of lists L of length N
%	such that all elements of L are in As.

% ?- N=100, numlist(1, N, Ns), time(((zdd all_list(100, Ns, X), card(X, C)))).
%@ % 29,015,728 inferences, 2.464 CPU in 2.553 seconds (97% CPU, 11774994 Lips)

all_list(N, As, Y, S):- zdd_singleton(list(As), Id, S),
	all_list_with_id(N, Id, Y, S).
%
all_list_with_id(0, Id, 1, S):-!, memo(all_list(0, Id)-1, S).
all_list_with_id(N, Id, Y, S):-  memo(all_list(N, Id)-Y, S),
	(	nonvar(Y) -> true
	;	N0 is N-1,
		all_list_with_id(N0, Id, Y0, S),
		get_root_atom(Id, list(As), S),
		distribute_cons(As, Y0, 0, Y, S)
	).

%!	singleton_family(+L, -F, +S) is det.
%	F is unified with the family of sigletones A
%	with A in L.
singleton_family([], 0, _):-!.
singleton_family([A|As], X, S):-
	singleton_family(As, X0, S),
	zdd_singleton(A, U, S),
	zdd_join(U, X0, X, S).

%!	distribute_cons(+F, +X, -Y, +S) is det.
%	Y is unified with the family of lists [A|M] with
%  	A in F and M in X.
distribute_cons(F, X, Y, S):- distribute_cons(F, X, 0, Y, S).
distribute_cons([], _, Y, Y, _).
distribute_cons([A|As], Y, U, V, S):-
	l_cons(A, Y, V0, S),
	zdd_join(U, V0, U0, S),
	distribute_cons(As, Y, U0, V, S).

%!	l_cons(+A, +X, -Y, +S) is det.
%	Y is unified with the family of lists [A|L] with
%	L in X.

% ?- zdd X<<pow([1,2]), l_cons(a, X, Y), psa(Y).
l_cons(A, Y, U, S):- cofact(U, t(A, 0, Y), S).

%!	l_append(+L, +X, -Y, S) is det.
%	Y is unified with the family of lists M such that
%	append(L, U, M) with U in X.
% ?- zdd X<<pow([1,2]), l_append([a,b], X, Y), psa(Y).

l_append([], X, X, _).
l_append([A|As], X, Y, S):-
	l_append(As, X, X0, S),
	l_cons(A, X0, Y, S).

Short note on families on lists.

Assume A=\{a, b, c\} with ordering a<b<c. Let X be a set of lists \{[x_1, \ldots, x_n]\mid x_i\in A\} over A. [b, c, a, c, a] is a list of length 5.

\mu(X) is the minimum element u in A such that u is the first element of some \ell \in X. Ex. \mu(\{[b, a], [a, b]\})= a.

Define \gamma(X) = \{ \ell \in X\mid \mbox{ the first element of } \ell \mbox{ is } \mu(X) \}. Ex. \gamma(\{[b, c, a], [c, c]\})=\{[b,c,a]\}.

Define \rho(X) = \{[x_1,\ldots,x_n]\mid [u,x_1,\ldots,x_n] \in \gamma(X)\}. Ex. \rho(\{ [b, c, a], [c, c]\})=\{[c,a]\}.

Define \lambda(X)= \{\ell \in X\mid \rho(X) \mbox{ is the first element of }\ell\}. Ex. \lambda(\{ [b, c, a], [c, c]\})=\{[c,c]\}.

If X is not empty then X is represented as a triple uniquely
(\mu(X), \lambda(X), \rho(X)). Ex. \{[b,c,a], [c,c]\} is represented as (b, \{[c,a]\}, \{[c,c]\})

Note that the first element of a list in \lambda(X) is not \mu(X),
and \lambda(X) is disjoint from \gamma(X).

It should be clear that for any family of lists over A is represented
as a binary DAG using such triples as a binary branching nodes,
and the binary DAG is uniquely determined upto isomorphism
between binary DAGs.

4

Yes, exactly. It is after the axiom of extension of the standard set theory.

So far, the counting library is the card/3 only for
both families of sets and families of lists. However, for polynomials over GF(2), a special counting method was needed (gf2_card/4). So it should depend on application, I think.

7

My sat is merely one of applications of my library on zdd
for DNF, which is a set of clauses as a set of literals
which has not a complementary pair. So as you pointed,
my sat doesn’t care/know about, for example, a + -a is tautology,
which is only detected by sat_count. My sat keeps satisfiability,
which is purpose of my sat.

% ?- sat(a + (-a)).
%@ true.

% ?- sat(a), sat(-a).  
%@ false.   <=== because of conjunction of sat queries.

% ?- sat(a + (-a)), sat_count(C).
%@ C = 2.
10

lt was a bug introduced in pac@1.8.6.
Fixed in pac@1.8.7 uploaded.
Thanks.