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
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
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).
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
40
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
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).
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
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
115
116algebra(M, A*B, C, [A,B], [A0,B0], memberchk(((A0,B0),C), M)).
117algebra(_, A, A, [], [], true).
118
120in(X, M):- dom(M, D), member(X, D).
121
124
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
139assign([],_).
140assign([X|R],D):- member(X, D), assign(R,D).
141
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
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
164
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
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
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
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
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
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).
298
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
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), 337 call(A, Dags1, Dags).
338
339new_peak(_, _, [], _, []).
340new_peak(F, X, [L|Ls], Dag, [Dag0|Dags]):-
341 F = (M, _), 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
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
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))))))))