Toward ZDD library is SWI-Prolog (Useful Code) - Reply 1

This looks incredible …

Unfortunately, its way to terse for me to understand.

If you could find the time to write a short tutorial – starting from the very simple example … to illustrate use, that would be great.

Dan

A tutorial, for example BDDs - Binary Decision Diagrams, if I remember correctly,
is a main conceptual resource of my zdd library. I learned two things there

  1. A zdd represents a family of sets of ordered atoms (urelements).
  2. Minato’s zero suppress rule of ZDD guarantees Axiom of Extensionality of the set theory.

That’s all. I have no idea how to add to the tutorial about ZDD better than possibly many similar
tutorials on the net. Unfortunately I am a person who is good at explain simple things in difficult ways. But I will try to find time to write a simple codes which might be help to explain clearly internal behavior of my zdd library. Anyway, IMHO, above 1 and 2 are essential of ZDD.

This is a code which writes given a zdd (family of sets) as a set of
equations. It is almost a flat solved form of A. Colmerauer. Also it
is a special simple case of coalgebra, though it is mainly for non-well founded structure. (ZDD is for well-founded, correct ?)

% ?- open_state(S), zeval(pow([a, b, c, d, e, f]), I, S), show_family(I, X, S),
%	maplist(writeln, X).
%@ 7=t(a,6,6)
%@ 6=t(b,5,5)
%@ 5=t(c,4,4)
%@ 4=t(d,3,3)
%@ 3=t(e,2,2)
%@ 2=t(f,1,1)
%@ []
show_family(I, X, S):- show_family(I, X0, [], S),
	zdd_sort(X0, X1, S),
	reverse(X1, X).
%
show_family(0, X, X, _).
show_family(1, [[]|X], X, _).
show_family(I, X, Y, S):- memo(visited(I)-F, S),
	(	nonvar(F) 	->	Y = X
	;	F = true,
		cofact(I, t(A, L, R), S),
		X = [I=t(A, L, R)|X0],
		show_family(L, X0, X1, S),
		show_family(R, X1, Y, S)
	).