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.

5

This doesn’t help you to understand classical SAT solving. In SAT solving,
and when using normal forms, like BDD, FDD, ZDD, etc… the used
equality is logical equality, which is a different thing:

  • A, B: In logical equality A and B are not sets or sets of sets,
    but rather propositional formulae. This is a syntactic structure
    built from negation, conjunction, disjunction etc… and propositional variables.

  • =: In logical equality equality is not extensional equality of sets or
    of sets of sets, but rather semantical or syntactical equality, whereas
    one can show that they are the same.

Currently when I input a formula in your library, and display DNF for example,
it doesn’t compute a normal form. Two different formulae A and B that are
logically equivalent can lead to different DNF in your system, i.e. Example 2:

I suspect this is just the aftermath, that your library is built upon set equality
based on extensionality, and not upon logical equality. And that you use sets
with negative and positive literals as elements. Logical equality is not so

difficult to define. It looks almost the same as set equality:

           A == B   :<=> ∀Φ(AΦ <=> BΦ)

In the above Φ is a so called valuation. A valuation is a function that sends
each propositional variable to a boolean value, i.e. Φ : Vars → Bool, where
Bool = {False, True} or if you like sometimes also expressed as Bool = {0,1}.

6

(Nothing of importance)

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

Maybe the use of the acronym “DNF” is not optimal. Because
it translates to “Disjunctive Normal Form”. But in your system
“Normal Form” has a very weak meaning, in connection with the

Sum of Product (SoP) forms you are creating. They are not
in unique normal forms. Basically there are two interpretations
of the term “normal form”, one where the normal form is supposed

to be unique and one where normal form refers to some transformation
into a certain syntactic form, without the uniqueness requirement.

Edit 22.12.2023
The second interpretation is indeed common for DNF. So you are
even not wrong here. Also there are a dozen of variants of DNF, one
might impose further constraints than only being a Sum of

Products (SoP). On the other hand classical SAT Solving based on
BDD is based on the first interpretation of a normal form, similarly a
ZDD normal form belongs to the first interpretation.

9

(Nothing of importance)

10

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