1:- module(count_algebra, [bin_symm_funs/3]). 2:- use_module(library(apply)). 3:- use_module(library(apply_macros)). 4:- use_module(library(clpfd)). 5:- use_module(library(statistics)). 6:- use_module(zdd('zdd-array')). 7:- use_module(util(meta2)). 8:- use_module(pac(basic)). 9:- use_module(pac(meta)). 10:- use_module(util(math)). 11:- use_module(pac('expand-pac')). 12:- use_module(zdd('zdd-misc')). 13:- use_module(zdd(zdd)). 14:- use_module(pac(op)). 15
16:- set_prolog_flag(stack_limit, 10_200_147_483_648). 17
18 :- op(1060, xfy, ~). 19 :- op(1060, xfy, #). 20 :- op(1060, xfy, <->). 21 :- op(1050, yfx, <-). 22 :- op(1060, xfy, <=> ). 23 :- op(1040, xfy, \/). 24 :- op(1030, xfy, /\). 25 :- op(1020, fy, \). 26 :- op(700, xfx, :=). 27 :- op(1000, xfy, &). 28
30 :- pac:op(1000, xfy, &). 31 :- pac:op(700, xfx, :=). 32
33term_expansion --> pac:expand_pac.
34
37
38join(X, Y, Z):- @(join(X, Y, Z)).
40join(X, Y, Z, S):- zdd_join(X, Y, Z, S).
41
43hyphen([],[],[]).
44hyphen([X|Xs],[Y|Ys],[X-Y|Zs]):- hyphen(Xs, Ys, Zs).
46mk_pair(X, Y, [X,Y]).
48prod_pair(A, B, C):- product(mk_pair, A, B, C).
49
50
53
59
60merge_xalg_der([], X, X).
61merge_xalg_der([P|Ps], X, Y):- merge_in_der(P, X, X0),
62 merge_xalg_der(Ps, X0, Y).
63
67merge_in_der(X, Y, Z):- merge_in_der_(Y, X, Z).
69merge_in_der_([], A-P, [A-[P]]).
70merge_in_der_([A-L|R], A-P, [A-L0|R]):-!,
71 add_ord_keyval(P, L, L0).
72merge_in_der_([A0-L|R], A-P, [A0-L|R0]):- A0 @< A,!,
73 merge_in_der_(R, A-P, R0).
74merge_in_der_(R, A-P, [A-[P]|R]).
75
81add_ord_keyval(K*V, [K*U|L], [K*V|L]):-!, U=V.
82add_ord_keyval(P, [Q|L], [Q|L0]):- P = K*_, Q = K0*_,
83 K0 @< K, !,
84 add_ord_keyval(P, L, L0).
85add_ord_keyval(P, L, [P|L]).
86
93check_ord_keyval(K*V, L, L):- var(V), !, check_ord_keyval(K*V, L).
94check_ord_keyval(P, L, L0):- add_ord_keyval(P, L, L0).
95
100check_ord_keyval(K*V, [K*U|_]):-!, U=V.
101check_ord_keyval(P, [K0*_|L]):- P=K*_, K0 @< K,
102 check_ord_keyval(P, L).
103
116
117find_model(N, B, S):-
118 open_state(S),
119 numlist(1, N, D),
120 filter_left_unit(D, A, S),
121 filter_non_commutative(2, 3, A, A0, S),
122 filter_inversible(D, A0, A1, S),
123 find_associative(A1, [], [], B, S).
125find_associative(A, _, _, A, _):- A<2, !.
126find_associative(A, Alg, Der, B, S):- cofact(A, t(Eqn, L, R), S),
127 find_associative(L, Alg, Der, L0, S),
128 ( L0 > 1 -> R0 = 0
129 ; ( merge_in_der(Eqn, Alg, Der, Der0)
130 -> find_associative(R, [Eqn|Alg], Der0, R0, S)
131 ; R0 = 0
132 )
133 ),
134 cofact(B, t(Eqn, L0, R0), S).
135
137filter_associative(A, B, S):- filter_associative(A, [], [], B, S).
139filter_associative(A, _, _, A, _):- A<2, !.
140filter_associative(A, Oprs, Der, B, S):- cofact(A, t(Opr, L, R), S),
141 filter_associative(L, Oprs, Der, L0, S),
142 ( merge_in_der(Opr, Oprs, Der, Der0)
143 -> filter_associative(R, [Opr|Oprs], Der0, R0, S)
144 ; R0 = 0
145 ),
146 cofact(B, t(Opr, L0, R0), S).
147
150eqn_der(L, Ls, P):- apply_eqn_one(L, [L|Ls], D, []),
151 sort(D, P).
153apply_eqn_one(_, [], P, P):-!.
154apply_eqn_one(L, [M|Ms], P, Q):- basic_der(L, M, P, P0),
155 apply_eqn_one(L, Ms, P0, Q).
156
161basic_der(P, Q, M, N):- der_rule(P, Q, L),
162 collect_der(L, M, N).
164collect_der([], V, V):-!.
165collect_der([X=X, A|U], [A|V], V0):-!, collect_der(U, V, V0).
166collect_der([_, _|U], V, V0):- collect_der(U, V, V0).
168der_rule([A, B]-C, [U, V]-W,
169 [ C = U, B-[A,V]*W,
170 C = V, A-[U,B]*W,
171 W = A, V-[U,B]*C,
172 W = B, U-[A,V]*C
173 ]).
174
176alg_der(Alg, Der):- merge_xalg_der(Alg, [], [], Der).
178merge_xalg_der([], _, Der, Der):-!.
179merge_xalg_der([Eqn|Alg], Alg0, Der, Der0):-
180 merge_in_der(Eqn, Alg0, Der, Der1),
181 merge_xalg_der(Alg, [Eqn|Alg0], Der1, Der0).
183merge_in_der(Eqn, Alg, Der, Der0):-
184 eqn_der(Eqn, Alg, P),
185 sort(P, Q),
186 merge_xalg_der(Q, Der, Der0).
187
189left_identy_rule(_, [], []):-!.
190left_identy_rule(E, [N|Ns], [[1, N]-N |Rest]):-
191 left_identy_rule(E, Ns, Rest).
192
198binary_algebra(D, A, S):- raise_list(D, 2, D2),
199 zdd_funs(D2, D, A, S).
200
204
205filter_left_unit(D, A, S):- D=[E|D0],
206 prod_pair(D0, D, D2),
207 zdd_funs(D2, D, A0, S),
208 left_identy_rule(E, D, U),
209 zdd_append(U, A0, A, S).
210
215filter_inversible([], A, A, _):-!.
216filter_inversible(_, A, 0, _):- A<2, !.
217filter_inversible(D, A, B, S):- memo(filter_inversible(D, A)-B, S),
218 ( nonvar(B) -> true 219 ;
220 cofact(A, t(P, L, R), S),
221 ( P = [_, X]-1
222 -> ( select(X, D, D0) -> true
223 ; D0 = D
224 )
225 ; D0 = D
226 ),
227 filter_inversible(D, L, L0, S),
228 filter_inversible(D0, R, R0, S),
229 cofact(B, t(P, L0, R0), S)
230 ).
232filter_non_commutative(_, _, X, 0, _):- X<2, !.
233filter_non_commutative(I, J, X, Y, S):- cofact(X, t(P, L, R), S),
234 filter_non_commutative(I, J, L, L0, S),
235 ( P = [I, J]-K
236 -> filter_non_commutative(J, I, K, R, R0, S)
237 ; filter_non_commutative(I, J, R, R0, S)
238 ),
239 cofact(Y, t(P, L0, R0), S).
240
242filter_non_commutative(_, _, _, X, 0, _):- X < 2, !.
243filter_non_commutative(I, J, K, X, Y, S):- cofact(X, t(Q, L, R), S),
244 filter_non_commutative(I, J, K, L, L0, S),
245 ( Q = [I,J]-N
246 -> ( N\==K -> R0 = R
247 ; R0 = 0
248 )
249 ; filter_non_commutative(I, J, K, R, R0, S)
250 ),
251 cofact(Y, t(Q, L0, R0), S).
252
253
254 257
264
265count_A_algebras_with_zdd(N, C):-
266 prepare_count_A_algebras(N, Track, Etree),
267 count_A_algebras([h(Etree, [], Track)], 0, C).
269prepare_count_A_algebras(N, Track, Etree):-
270 numlist(1, N, Dom),
271 raise_list(Dom, 2, Dom2),
272 distribute_cons(Dom, Dom2, Dom3),
273 maplist(pred([U, a(U, [], [])]), Dom3, Track),
274 set_pred(mk_pair, equational_mapsto),
275 zdd:zdd_funs(Dom2, Dom, Etree).
278count_A_algebras(X, Y, Z):- @(count_A_algebras(X, Y, Z)).
280count_A_algebras([], C, C, _).
281count_A_algebras([h(0, _, _)|Hs], C, C0, S):-!,
282 count_A_algebras(Hs, C, C0, S).
283count_A_algebras([h(_, _, 0)|Hs], C, C0, S):-!,
284 count_A_algebras(Hs, C, C0, S).
285count_A_algebras([h(1, _, [])|Hs], C, C0, S):-!, C1 is C+1,
286 count_A_algebras(Hs, C1, C0, S).
287count_A_algebras([h(1, _, _)|Hs], C, C0, S):-!,
288 count_A_algebras(Hs, C, C0, S).
289count_A_algebras([h(Etree, Es, Tr)|Hs], C, C0, S):-
290 cofact(Etree, t(E, L, R), S),
291 repeat_law([E|Es], Tr, Tr0), 292 ( Tr0 = 0
293 -> count_A_algebras([h(L, Es, Tr)|Hs], C, C0, S)
294 ; count_A_algebras([h(L, Es, Tr), h(R, [E|Es], Tr0)|Hs], C, C0, S)
295 ). 296
304
305count_AC_algebras_with_zdd(N, C):-
306 prepare_count_AC_algebras(N, Track, Etree),
307 count_AC_algebras([h(Etree, [], Track)], 0, C).
309prepare_count_AC_algebras(N, Track, Etree):-
310 numlist(1, N, Dom),
311 raise_list(Dom, 2, Dom2),
312 distribute_cons(Dom, Dom2, Dom3),
313 maplist(pred([U, a(U, [], [])]), Dom3, Track),
314 set_pred(mk_pair, equational_mapsto),
315 bin_symm_funs(Dom2, Dom, Etree).
316
317equational_mapsto([A,B], C, A+B = C).
318
321count_AC_algebras(X, Y, Z):- @(count_AC_algebras(X, Y, Z)).
322
324count_AC_algebras([], C, C, _).
325count_AC_algebras([h(0, _, _)|Hs], C, C0, S):-!,
326 count_AC_algebras(Hs, C, C0, S).
327count_AC_algebras([h(_, _, 0)|Hs], C, C0, S):-!,
328 count_AC_algebras(Hs, C, C0, S).
329count_AC_algebras([h(1, _, [])|Hs], C, C0, S):-!, C1 is C+1,
330 count_AC_algebras(Hs, C1, C0, S).
331count_AC_algebras([h(1, _, _)|Hs], C, C0, S):-!,
332 count_AC_algebras(Hs, C, C0, S).
333count_AC_algebras([h(Etree, Es, Tr)|Hs], C, C0, S):-
334 cofact(Etree, t(E, L, R), S),
335 symm_repeat_law([E|Es], Tr, Tr0), 336 ( Tr0 = 0
337 -> count_AC_algebras([h(L, Es, Tr)|Hs], C, C0, S)
338 ; count_AC_algebras([h(L, Es, Tr), h(R, [E|Es], Tr0)|Hs], C, C0, S)
339 ). 340
341
349
350test_equational_form([X, Y], [Z], X+Y=Z).
351
353bin_symm_funs(D, R, F):-
354 bin_symm_funs(D, R, F, equational_mapsto).
356:- meta_predicate bin_symm_funs(?,?,?,3). 357bin_symm_funs(D, R, F, Pred):- @(bin_symm_funs(D, R, F, Pred)).
359bin_symm_funs([], _, 1, _, _).
360bin_symm_funs([[U, V]|As], Bs, F, Pred, S):- U @> V, !,
361 bin_symm_funs(As, Bs, F, Pred, S).
362bin_symm_funs([A|As], Bs, F, Pred, S):-
363 bin_symm_funs(As, Bs, F0, Pred, S),
364 bin_symm_extend_funs_by_one(A, Bs, F0, 0, F, Pred, S).
366bin_symm_extend_funs_by_one(_, [], _, F, F, _, _):-!.
367bin_symm_extend_funs_by_one(A, [B|Bs], H, F0, F, Pred, S):-
368 call(Pred, A, B, Pair),
369 zdd_insert(Pair, H, H0, S),
370 zdd_join(H0, F0, F1, S),
371 bin_symm_extend_funs_by_one(A, Bs, H, F1, F, Pred, S).
372
380
381count_associative_algebra(N, NumOfAssocAlgebras):-
382 numlist(1, N, Dom),
383 raise_list(Dom, 2, Dom2),
384 distribute_cons(Dom, Dom2, Dom3),
385 maplist(pred([U, a(U, [], [])]), Dom3, Track0),
386 sort(Track0, Track1),
387 all_funs(Dom2, Dom, Maps, default_mapsto),
388 maplist(maplist( pred([[A,B]-C, A+B=C]) ), Maps, FamEs),
389 foldl( pred(Track1, ( [Es, C, C0] :-
390 repeat_law(Es, Track1, Track),
391 ( Track = [] -> C0 is C+1
392 ; C0 = C
393 ))
394 ),
395 FamEs, 0, NumOfAssocAlgebras).
396
398repeat_law(E, [a(_,[A],[A])|X], Y):-!, repeat_law(E, X, Y).
399repeat_law(_, [a(_,[_],[_])|_], 0):-!. 400repeat_law(Eqs, X, X0):- member(E, Eqs),
401 apply_law_once(E, X, X1),
402 !,
403 repeat_law(Eqs, X1, X0).
404repeat_law(_, X, X).
405
407apply_law_once(E, X, [A0|X0]):-
408 select(A, X, X0),
409 law(E, A, A0).
410
412law( A+B=C, a([X, A, B], U, []),
413 a([X, A, B], U, [X, C])).
414law( A+B=C, a(T, U, [A, B]),
415 a(T, U, [C])).
416law( A+B=C, a(T, [A, B], U),
417 a(T, [C], U)).
418law( A+B=C, a([A, B, X], [], U),
419 a([A, B, X], [C, X], U)).
420
427
428symm_count_associative_algebra(N, NumOfAssocAlgebras):-
429 numlist(1, N, Dom),
430 raise_list(Dom, 2, Dom2),
431 distribute_cons(Dom, Dom2, Dom3),
432 maplist(pred([U, a(U, [], [])]), Dom3, Track0),
433 sort(Track0, Track1),
434 all_funs(Dom2, Dom, Maps, ordered_mapsto),
435 sort(Maps, Maps0),
436 maplist(maplist( pred([[A,B]-C, A+B=C]) ), Maps0, FamEs),
437 foldl( pred(Track1, ( [Es, C, C0] :-
438 symm_repeat_law(Es, Track1, Track),
439 ( Track = [] -> C0 is C+1
440 ; C0 = C
441 ))
442 ),
443 FamEs, 0, NumOfAssocAlgebras).
444
446symm_repeat_law(E, [a(_,[A],[A])|X], Y):-!, symm_repeat_law(E, X, Y).
447symm_repeat_law(_, [a(_,[_],[_])|_], 0):-!. 448symm_repeat_law(Eqs, X, X0):- member(E, Eqs),
449 symm_apply_law_once(E, X, X1),
450 !,
451 symm_repeat_law(Eqs, X1, X0).
452symm_repeat_law(_, X, X).
453
455symm_apply_law_once(E, X, [A0|X0]):-
456 select(A, X, X0),
457 symm_law(E, A, A0).
458
459symm_law( A+B=C, a([X, A, B], U, []), a([X, A, B], U, [X, C])).
460symm_law( A+B=C, a([X, B, A], U, []), a([X, B, A], U, [X, C])).
461symm_law( A+B=C, a(T, U, [A, B]), a(T, U, [C])).
462symm_law( A+B=C, a(T, U, [B, A]), a(T, U, [C])).
463symm_law( A+B=C, a(T, [A, B], U), a(T, [C], U)).
464symm_law( A+B=C, a(T, [B, A], U), a(T, [C], U)).
465symm_law( A+B=C, a([A, B, X], [], U), a([A, B, X], [C, X], U)).
466symm_law( A+B=C, a([B, A, X], [], U), a([B, A, X], [C, X], U)).
467
469:- meta_predicate all_funs(?, ?, ?, 3). 470
471all_funs(Xs, Y, Z):-
472 all_funs(Xs, Y, Z, default_mapsto).
473
477
478all_funs([], _, [[]], _).
479all_funs([X|Xs], Y, Z, M):- all_funs(Xs, Y, Z0, M),
480 all_funs(Y, X, Z0, Z, [], M).
482all_funs([], _, _, Z, Z, _).
483all_funs([Y|Ys], X, Z, U, V, M):-
484 all_funs_extend(Z, Y, X, U, U0, M),
485 all_funs(Ys, X, Z, U0, V, M).
487all_funs_extend([], _, _, U, U, _).
488all_funs_extend([Z|Zs], Y, X, U, V, M):-
489 ( call(M, X, Y, P) -> U =[[P|Z]|U0]
490 ; U = [Z|U0]
491 ),
492 all_funs_extend(Zs, Y, X, U0, V, M).
494ordered_mapsto([A, B], Y, [A, B]-Y):- A@=<B, !.
495
497default_mapsto(X, Y, X-Y)