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

Lets say we have some variable order fixed, and nf : Form → Norm is
the normal form. If such a computable total function exists, then it
might additiionally have this uniqueness property, where the first

(==)/2 is logical equality and where the second (=)/2 is just checking
the normal form verbatim for equivalence:

Uniqueness Property:

A == B    :<=>   nf(A) = nf(B)

Uniqueness Property is very handy. You can use it for satisfiablity check,
i.e. nf(A) != nf(0) means A is satisfiable. Thats basically the use of normal forms
in SAT solvers. But you can also use it for labeling and counting.

Edit 21.12.2023
The ZDD normal form is a little special, since its not a formula in itself.
For BDD and FDD the normal forms are in itself formulas, and one has
even nf(A) == A. For BDD one can use X*L+(-X)*R, were L is the left

cofactor and B is the right cofacture. And for FDD one can use L+X*R,
with the factors of the Reed-Muller expansion. But for ZDD this doesn’t work,
I didn’t find a connective where this would work, since propositional formulae

hardly express the jump involved in Minatos compression. But its interesting
to see how Minato compared ZDD and FDD, since ZDD and FDD have
something in common, both have a compression based on detecting a zero:

image
image

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

Without Prolog conjunction (',')/2 and with propositional
conjunction (*)/2, it should also give false? But it doesn’t
do that. I am using recent pac@1.8.6:

?- sat(a*(-a)), psa.
 zid = 4
        [a,-a]
-------------------
true.

Thats a strange DNF. Usually the conjunctive clauses C1, .., Cn,
that make up a Disjunctive Normal Form C1 v ... v Cn, are such
that each conjunctive clause Ci never has a literal and its

opposite in it, because such a clause is always false, and can be
removed. Here is a longer example where this happens:

?- sat((x=\=y)*x*y), psa.
 zid = 11
        [x,-x,y]
-------------------
true.

Should also show false.

Edit 23.12.2023
You can also compare with Markus Triskas CLP(B), that
is bundled with SWI-Prolog, it can do both examples correctly:

?- sat(A*(~A)).
false.

?- sat((X=\=Y)*X*Y).
false.
10

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