```    1:- module(hmodel,[]).    2
3:- use_module(util(math)).    4:- use_module(pac(op)).    5:- use_module(pac(basic)).    6
7truth(X, true):- once(X), !.
8truth(_, false).
9
10
11%%% groupoid %%%%
12% grupoid(_, B, X, Y, [], [],true):- eval([algebra(B)], X, Y).
13% grupoid(_, B, X, Y, [], [],true):- algebra(B, X, Y).
14
15grupoid(new, D, grupoid(D, M)):- product(D, D, D2), map(D2, D, M).
16grupoid(fun, grupoid(_, F), F).
17grupoid(dom, grupoid(D, _), D).
18
19%%% semigroup %%%%%%
20semigroup(new, D, B):- !,  grupoid(new, D, B),
21	models(grupoid::B, \$associativity).
22semigroup(F, X, Y):- grupoid(F, X, Y).
23
24%%%%%% the set of DAGS and Posets %%%%
25% ?- hmodel:dag(all, [a,b,c], Dags).
26dag(all, L, Ds):- dags(L, Ds).
27dag(new, L, dag(L,D)):- dag(all, L, Ds), member(D, Ds).
28dag(dom, dag(L,_), L).
29dag(rel, dag(_,R), R).
30dag(succ_pair, dag(L, R), dag(L, Ps)):- succlist_pairs(R, Ps).```
posets
?- `poset(all, [a,b,c], X)`. ?- hmodel:new(poset::[a,b,c,d,e], X).
```   35poset(all, L, Ds):- !, posets_in_fan(L, Ds).
36poset(new, L, dag(L,D)):- !,  poset(all, L, Ds), member(D, Ds).
37poset(F, X, Y):- dag(F, X, Y).
38
39%%%%  orderd grupoid class
40
41% ?- hmodel:og(new, [a,b], X), hmodel:rel(og::X, [_|_]).
42% ?- hmodel:(og(new, [a,b], X), rel(::(og,X), [_|_])).
43% ?- hmodel:(og(new, [a,b], X), og(rel, X, [_|_])).
44% ?- hmodel:(new(og::[a,b], X), rel(og::X, [_|_])).
45
46og(new, D, og(D,X,Y)):- poset(new, D, X0),
47	dag(succ_pair, X0, X1),
48	dag(rel, X1, X),
49	grupoid(new, D, Y0),
50	grupoid(fun, Y0, Y).
51og(dom, og(X,_,_), X).
52og(rel, og(_,X,_), X).
53og(fun, og(_,_,X), X).
54
55%%%%%%%%
56% ?- hmodel:entails(grupoid::[a,b,c], true, \$(associativity)).
57% ?- hmodel:entails(semigroup::[a,b,c], true, \$(associativity)).
58
59entails((P::X), B, C):- new(P::X, M),
60	models(P::M, B),
61	\+ models(P::M, C),
62        !,
63	fail.
64entails(_, _, _).
65
66%;; (setq module-query  "qcompile(util(hmodel)), module(hmodel).")
67% ?- qcompile(util(hmodel)), module(hmodel).
68% ?- hmodel:find_model(grupoid::[a,b,c], \+ \$(idempotence), X).
69
70find_model(Class::P, C, X):- call(Class, new, P, X),
71	models(Class::X, C).
72
73%%%% model calculus
74% :- index(models(0,1)).
75models(_, true):-!.
76models(M, (C1,C2)):- !, models(M, C1), models(M, C2).
77models(M, (C1;C2)):- !,( models(M, C1); models(M, C2)).
78models(M, (C1->C2)):- !, (\+ models(M, C1); models(M, C2)).
79models(M, (\+ C)):- !,  \+ models(M, C).
80models(M, every(Y,C)):- !, forall(in(Y,M), models(M,C)).
81models(M, some(Y,C)):- !,  in(Y, M), models(M, C).
82% models(M, Y=Z):- !, eval(M, Y, Y0), eval(M, Z, Y0).
83models(M, Y=Z):- !, call(M, Y, Y0), call(M, Z, Y0).
84models(M, \$(Property)):- !, call(Property, M).
85models(_, prolog(G)):- !, call(G).
86models(M, forall(P,G)):- !, forall(P, models(M, G)).
87models(M, exists(P,G)):- !, call(P), models(M, G).
88% models(C::M, X):- eh:mapterm(eval(M), X, X0), holds(C::M, X0).
89models(C::M, X):- eh:mapterm(M, X, X0), holds(C::M, X0).
90
91%
92holds(_,  A=<A).
93holds(M,  A=<B):- rel(M, Fs), memberchk((A,B), Fs).
94
95%%%%
96% ?-  new(semigroup::[a,b,c], S), models(semigroup::S, \$(has_subalgebra)).
97% ?-  new(dag::[a,b], X).
98% ?-  all(dag::[a,b], X).
99% ?-  new(dag::[a,b], X), send(dag::succ_pair, X, Y).
100% ?-  send(og::new, [a,b], X).
101
102send(Class::F, X, Y):- call(Class, F, X, Y).
103
104all(Class::X, Y):-  call(Class, all, X, Y).
105
106new(Class::X, Y):-  call(Class, new, X, Y).
107
108fun(Class::X, Y):-  call(Class, fun, X, Y).
109
110dom(Class::X, Y):-  call(Class, dom, X, Y).
111
112rel(Class::X, Y):-  call(Class, rel, X, Y).
113
114%%%%%%%%
115
116algebra(M, A*B, C, [A,B], [A0,B0], memberchk(((A0,B0),C), M)).
117algebra(_, A, A, [], [], true).
118
119%%%% an element of the domain.
120in(X, M):- dom(M, D), member(X, D).
121
122%%%%% a binary operation M is associative over a domain D.
123% models(G, every(X,every(Y,(every(Z, ((X* Y)*Z) = (X*(Y*Z))))))).
124
125% ?- module(pac).
126% ?- hmodel:find_model(grupoid::[a,b], \+ \$(associativity), X).
127% ?- hmodel:find_model(grupoid::[a,b], \+ \$(associativity), X).
128
129associativity(G):- dom(G, D), fun(G, M), associativity(D, M).
130
131associativity(D, M):-
132	forall(assign([X,Y,Z],D),
133	       (member(((Y,Z),YZ),M), member(((X,YZ),XYZ),M),
134	    	member(((X,Y),XY),M), member(((XY,Z),XYZ),M)
135	       )
136	      ).
137
138%%%%%%
139assign([],_).
140assign([X|R],D):- member(X, D), assign(R,D).
141
142%%%%% has a  subalgebra
143has_subalgebra(M):-  fun(M, Tbl),
144	dom(M, D),
145	powerset(D, P),
146	member(S, P),
147	S\==D,
148	S\==[],
149	subalgebra(S, Tbl).
150
151%%%%% generator of ordered grupoid %%%%
152
153succlist_pairs([],[]).
154succlist_pairs([(_,[])|R], Ps):- succlist_pairs(R, Ps).
155succlist_pairs([(A,L)|R], Ps):-
156	succlist_pairs(A, L, Qs),
157	succlist_pairs(R, P0s),
158	append(Qs, P0s, Ps).
159
160succlist_pairs(_,[],[]).
161succlist_pairs(A,[X|Xs],[(X,A)|Ys]):- succlist_pairs(A,Xs,Ys).
162
163% ?- permutations([1,2,3], X).
164
165% non deterministic permutation generator
166perm_nd(X, Y) :- perm_nd(X, [], Y).
167
168perm_nd([], X, X).
169perm_nd([X|Xs], Y0, Y):- insert_nd(X, Y0, Y1), perm_nd(Xs, Y1, Y).
170
171insert_nd(X, Y, [X|Y]).
172insert_nd(X,[Y|Ys], [Y|Zs]):- insert_nd(X, Ys, Zs).
173
174diagonal([]).
175diagonal([(X,X)|D]):-diagonal(D),!.
176
177make_id([],[]).
178make_id([X|Y],[(X,X)|D]):- make_id(Y,D).
179
180field([],[]).
181field([(X,Y)|R],[X,Y|F]):-field(R,F).
182
183compose(X,Y,Z):-compose(X,Y,Z,[]).
184
185compose([],_,X,X).
186compose([(X,Y)|Z],U,V,W):- compose(X,Y,U,V,R), compose(Z,U,R,W).
187
188compose(_,_,[],X,X).
189compose(X,Y,[(Y,Z)|U],[(X,Z)|V],W):-!, compose(X,Y, U,V,W).
190compose(X,Y,[_|U],V,W):- compose(X,Y, U,V,W).```
```  194trcl(R,X):- trcl(R,R,X).
195
196trcl(R,X,Y):- compose(R,X,RX), union(RX,X,Z), trcl(R,X,Z,Y).
197
198trcl(_,X,Y,X):- subset(Y,X),!.
199trcl(R,_,Y,Z):- trcl(R,Y,Z).
200
201trcl_sum(X,Y,Z):-compose(X,Y,Z1),compose(Y,X,Z2),
202	union(Z1,Z2,Z3),
203	trcl(Z3,Z4),
204	union([X,Y,Z4],Z).
205
206%%%% test connectivity of undirectied graph (X,E).
207
208connected(X,E):-makediscrete(X,Y),
209	union_find(E,Y,Class),Class=[_].
210
211makediscrete([],[]).
212makediscrete([X|R],[[X]|R1]):-makediscrete(R,R1).
213
214union_find([],X,X).
215union_find([(X,Y)|R],C,D):-union_find(X,Y,C,C1),union_find(R,C1,D).
216
217union_find(X,Y,Z,[Z5|Z4]):-find(X,Z,Z1,Z2),
218	find(Y,Z2,Z3,Z4),
219	union(Z1,Z3,Z5).
220
221find(X,[],[X],[]):-!.
222find(X,[Y|Z],Y,Z):- in(X, Y),!.
223find(X,[Y|Z],U,[Y|V]):- find(X,Z,U,V).
224
225%%%%  G is a grupoid over X.
226grupoid(X,G):-
227	product(X,X,XX),
228	eh:maps(XX,X,XXX),
229	in(G ,  XXX).
230
231grupoidx(X,G):-```
```  232	product(X,X,XX),
233	map(XX,X,G)```
```  233.
234
235map([],_,[]).
236map([X|R],Y,[(X,A)|S]):- member(A, Y), map(R,Y,S).
237
238%%%% a set X is closed
239%%%% with respect to an binary operation Alg.
240
241subalgebra(X,Alg):- in(Y, X), in(Z, X), in(((Y,Z),U), Alg),
242	\+ in(U,  X), !, fail.
243subalgebra(_,_).```
```  247binary_closed(G,X,Y):- bincl(G,X,Z), subset(Y,Z).
248
249bincl(G,X,Y):-binresult(G,X,X,Z), bincl1(G,X,Z,Y).
250
251bincl1(_,X,Y,X):- subset(Y,X),!.
252bincl1(G,X,Y,Z):- union(X,Y,U), bincl(G,U,Z).
253
254binresult(_,[],_,[]).
255binresult(G,[X|Y],Z,U):-
256	binresult1(G,X,Z,V),
257	binresult(G,Y,Z,W),
258	union(V,W,U).
259
260binresult1(_,_,[],[]).
261binresult1(G,X,[Y|Z],[U|V]):- in( ((X,Y),U),  G), !,  binresult1(G,X,Z,V).
262
263%%%%%% predicates over relations
264partial_order(R):-
265	anti_symmetric(R),
266	transitive(R),
267	refexive(R).
268
269reflexsive(R):-field(R,F),
270	reflexive(F,R).
271
272reflexive([],_).
273reflexive([X|Y],R):- in((X,X), R), reflexive(Y,R).
274
275anti_symmetric(R):- member((X,Y),R),
276	X\==Y,
277	member((Y,X),R),
278	!,
279	fail.
280anti_symmetric(_).
281
282symmetric(R):- in((X,Y), R),  \+ in((Y,X), R), !, fail.
283symmetric(_).
284
285transitive(R):- compose(R,R,RR), subset(RR,R).
286
287%%%%%% top level call
288% ?- dags([a,b,c], Dags).
289% ?- posets([a,b,c,d,e,f,g], X).
290% ?- posets_in_fan([a,b,c,d,e,f,g], X).
291
292dags(Ns, Dags):- dags((peak, append), Ns, Dags).
293
294posets(Ns, Ps):- sort(Ns, Ms), dags((anti_chain, append), Ms, Ps).
295
296posets_in_fan(Ns, Dags):- dags((fan, union), Ns, Dags).
297% 'union' is better than 'append'  at least for Ns=[a,b,c,d,e,f,g].
298
299%%%%%%
300peak(X, Dag, S, [(X,S)|Dag]).
301
302anti_chain(X, Poset, Chain, [(X, Chain)|Poset]):- anti_chain(Chain, Poset).
303
304anti_chain([],_).
305anti_chain([N|Ns], Poset):- anti_chain(Ns, Poset),
306	maplist(incomparable(N,Poset), Ns).
307
308incomparable(N, Poset, N0):- N @> N0, !, \+reach(N0,Poset,N).
309incomparable(N, Poset, N0):- \+reach(N, Poset, N0).
310
311reach(N,_,N):-!.
312reach(N0, Poset,N):- memberchk((N,L), Poset),
313	member(X, L),
314	reach(N0, Poset, X).
315
316fan(X, Poset, S, [(X,S0)|Poset]):-
317 	maplist(fan(Poset), S, Ls),
318 	union([S|Ls], S0).
319
320fan(P, X, L):- memberchk((X,L), P).
321
322%%%%%% dags: universal predicate  %%%%%%
323dags(F, Nodes, Dags):- once(dags(F, Nodes, [[]], [[]], _, Dags)).
324
325dags(_, [], X, Y, X, Y).
326dags(F, [N|Ns], Succs0, Dags0, Succs, Dags):-
327	new_node(F, N, Succs0, Dags0, Succs1, Dags1),
328        dags(F, Ns, Succs1, Dags1, Succs, Dags).
329
330new_node(F, N, Succs, Dags, Succs1, Dags1):-
331	new_node(F, N, Succs, Dags, Dags1),
332	extend_succs(N, Succs, Succs1).
333
334new_node(F, N, Succs, Dags0, Dags):-
335	maplist(new_peak(F, N, Succs), Dags0, Dags1),
336	F = (_, A),  % append or union
337	call(A, Dags1, Dags).
338
339new_peak(_, _, [], _, []).
340new_peak(F, X, [L|Ls], Dag, [Dag0|Dags]):-
341	F = (M, _),  % method to add a node
342	call(M, X, Dag, L, Dag0),
343	!,
344	new_peak(F, X, Ls, Dag, Dags).
345new_peak(F, X, [_|Ls], Dag, Dags):-
346	new_peak(F, X, Ls, Dag, Dags).
347
348extend_succs(_, [], []).
349extend_succs(X, [S|R0], [S, [X|S]|R]):- extend_succs(X, R0, R).
350
351%%%%%
352% ?- find_model(grupoid::[a,b], \$surj, X).
353
354isolated(X, G):- rel(G, E), forall(in((X,Y), E); in((Y,X), E), X==Y).
355
356maximal(X, M):-  in(X, M), rel(M, E), forall(in((X,Y), E), X=Y).
357
358minimal(X, M):- rel(M, E), forall(in((Y,X), E), X=Y).
359
360irreducible(L, M) :- fun(M,  G), forall(in(X, L), binary_closed(G,[X],L)).
361
362idempotence(M):- fun(M, F),  memberchk(((A,A),A), F).
363
364left_unit(U, G):- fun(G, M), dom(G, D),
365	forall(in(X,D), in(((U,X),X), M)).
366
367right_unit(U, G):- fun(G, M), dom(G, D),
368	forall(in(X, D), in(((X,U),X), M)).
369
370surj(M):- dom(M, D), fun(M, F), maplist(snd, F, M0),
371	sort(D, D0), sort(M0, D0).
372
373%%%% for OG
374aug(OG):- models(OG,every(X,every(Y, (Y=< (X*Y))))).
375
376slide1(M):- models(M, every(A,every(B, every(C,
377		(((A*B)*C) =< (A*(B*C))))))).
378mix(M):- models(M, every(A,every(B, every(C, every(D, ((A=<B, C=<D)
379		-> ((B*C) =< (A*D))))))))```