1:- module(hmodel,[]). 2
3:- use_module(misc(math)). 4:- use_module(pac(op)). 5:- use_module(pac(basic)). 6
7truth(X, true):- once(X), !.
8truth(_, false).
9
13
14
15grupoid(new, D, grupoid(D, M)):- cartesian(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
67
68%;; (setq module-query "qcompile(misc(hmodel)), module(hmodel).")
69% ?- qcompile(misc(hmodel)), module(hmodel).
70
71% ?- hmodel:find_model(grupoid::[a,b,c], \+ $(idempotence), X).
72
73find_model(Class::P, C, X):- call(Class, new, P, X),
74 models(Class::X, C).
75
78models(_, true):-!.
79models(M, (C1,C2)):- !, models(M, C1), models(M, C2).
80models(M, (C1;C2)):- !,( models(M, C1); models(M, C2)).
81models(M, (C1->C2)):- !, (\+ models(M, C1); models(M, C2)).
82models(M, (\+ C)):- !, \+ models(M, C).
83models(M, every(Y,C)):- !, forall(in(Y,M), models(M,C)).
84models(M, some(Y,C)):- !, in(Y, M), models(M, C).
86models(M, Y=Z):- !, call(M, Y, Y0), call(M, Z, Y0).
87models(M, $(Property)):- !, call(Property, M).
88models(_, prolog(G)):- !, call(G).
89models(M, forall(P,G)):- !, forall(P, models(M, G)).
90models(M, exists(P,G)):- !, call(P), models(M, G).
91% models(C::M, X):- eh:mapterm(eval(M), X, X0), holds(C::M, X0).
92models(C::M, X):- eh:mapterm(M, X, X0), holds(C::M, X0).
93
95holds(_, A=<A).
96holds(M, A=<B):- rel(M, Fs), memberchk((A,B), Fs).
97
98%%%%
99% ?- new(semigroup::[a,b,c], S), models(semigroup::S, $(has_subalgebra)).
100% ?- new(dag::[a,b], X).
101% ?- all(dag::[a,b], X).
102% ?- new(dag::[a,b], X), send(dag::succ_pair, X, Y).
103% ?- send(og::new, [a,b], X).
104
105send(Class::F, X, Y):- call(Class, F, X, Y).
106
107all(Class::X, Y):- call(Class, all, X, Y).
108
109new(Class::X, Y):- call(Class, new, X, Y).
110
111fun(Class::X, Y):- call(Class, fun, X, Y).
112
113dom(Class::X, Y):- call(Class, dom, X, Y).
114
115rel(Class::X, Y):- call(Class, rel, X, Y).
116
118
119algebra(M, A*B, C, [A,B], [A0,B0], memberchk(((A0,B0),C), M)).
120algebra(_, A, A, [], [], true).
121
123in(X, M):- dom(M, D), member(X, D).
124
127
131
132associativity(G):- dom(G, D), fun(G, M), associativity(D, M).
133
134associativity(D, M):-
135 forall(assign([X,Y,Z],D),
136 (member(((Y,Z),YZ),M), member(((X,YZ),XYZ),M),
137 member(((X,Y),XY),M), member(((XY,Z),XYZ),M)
138 )
139 ).
140
142assign([],_).
143assign([X|R],D):- member(X, D), assign(R,D).
144
146has_subalgebra(M):- fun(M, Tbl),
147 dom(M, D),
148 powerset(D, P),
149 member(S, P),
150 S\==D,
151 S\==[],
152 subalgebra(S, Tbl).
153
155
156succlist_pairs([],[]).
157succlist_pairs([(_,[])|R], Ps):- succlist_pairs(R, Ps).
158succlist_pairs([(A,L)|R], Ps):-
159 succlist_pairs(A, L, Qs),
160 succlist_pairs(R, P0s),
161 append(Qs, P0s, Ps).
162
163succlist_pairs(_,[],[]).
164succlist_pairs(A,[X|Xs],[(X,A)|Ys]):- succlist_pairs(A,Xs,Ys).
165
168
169permutations(X, Y):- permutations(X, [[]], Y).
170
171permutations([],X, X).
172permutations([X|Xs],Z0, Z):- maplist(perm_insert(X), Z0, Z1),
173 append(Z1, Z2),
174 permutations(Xs, Z2, Z).
175
176perm_insert(X, [], [[X]]).
177perm_insert(X, [Y|Ys], [[X, Y|Ys]|Z]):-
178 perm_insert(X, Ys, Z0),
179 maplist(cons(Y), Z0, Z).
180
182perm_nd(X, Y) :- perm_nd(X, [], Y).
183
184perm_nd([], X, X).
185perm_nd([X|Xs], Y0, Y):- insert_nd(X, Y0, Y1), perm_nd(Xs, Y1, Y).
186
187insert_nd(X, Y, [X|Y]).
188insert_nd(X,[Y|Ys], [Y|Zs]):- insert_nd(X, Ys, Zs).
189
190diagonal([]).
191diagonal([(X,X)|D]):-diagonal(D),!.
192
193make_id([],[]).
194make_id([X|Y],[(X,X)|D]):- make_id(Y,D).
195
196field([],[]).
197field([(X,Y)|R],[X,Y|F]):-field(R,F).
198
199compose(X,Y,Z):-compose(X,Y,Z,[]).
200
201compose([],_,X,X).
202compose([(X,Y)|Z],U,V,W):- compose(X,Y,U,V,R), compose(Z,U,R,W).
203
204compose(_,_,[],X,X).
205compose(X,Y,[(Y,Z)|U],[(X,Z)|V],W):-!, compose(X,Y, U,V,W).
206compose(X,Y,[_|U],V,W):- compose(X,Y, U,V,W).
210trcl(R,X):- trcl(R,R,X).
211
212trcl(R,X,Y):- compose(R,X,RX), union(RX,X,Z), trcl(R,X,Z,Y).
213
214trcl(_,X,Y,X):- subset(Y,X),!.
215trcl(R,_,Y,Z):- trcl(R,Y,Z).
216
217trcl_sum(X,Y,Z):-compose(X,Y,Z1),compose(Y,X,Z2),
218 union(Z1,Z2,Z3),
219 trcl(Z3,Z4),
220 union([X,Y,Z4],Z).
221
223
224connected(X,E):-makediscrete(X,Y),
225 union_find(E,Y,Class),Class=[_].
226
227makediscrete([],[]).
228makediscrete([X|R],[[X]|R1]):-makediscrete(R,R1).
229
230union_find([],X,X).
231union_find([(X,Y)|R],C,D):-union_find(X,Y,C,C1),union_find(R,C1,D).
232
233union_find(X,Y,Z,[Z5|Z4]):-find(X,Z,Z1,Z2),
234 find(Y,Z2,Z3,Z4),
235 union(Z1,Z3,Z5).
236
237find(X,[],[X],[]):-!.
238find(X,[Y|Z],Y,Z):- in(X, Y),!.
239find(X,[Y|Z],U,[Y|V]):- find(X,Z,U,V).
240
242grupoid(X,G):-
243 cartesian(X,X,XX),
244 eh:maps(XX,X,XXX),
245 in(G , XXX).
246
247grupoidx(X,G):-
248 cartesian(X,X,XX),
249 map(XX,X,G)
249.
250
251map([],_,[]).
252map([X|R],Y,[(X,A)|S]):- member(A, Y), map(R,Y,S).
253
256
257subalgebra(X,Alg):- in(Y, X), in(Z, X), in(((Y,Z),U), Alg),
258 \+ in(U, X), !, fail.
259subalgebra(_,_).
263binary_closed(G,X,Y):- bincl(G,X,Z), subset(Y,Z).
264
265bincl(G,X,Y):-binresult(G,X,X,Z), bincl1(G,X,Z,Y).
266
267bincl1(_,X,Y,X):- subset(Y,X),!.
268bincl1(G,X,Y,Z):- union(X,Y,U), bincl(G,U,Z).
269
270binresult(_,[],_,[]).
271binresult(G,[X|Y],Z,U):-
272 binresult1(G,X,Z,V),
273 binresult(G,Y,Z,W),
274 union(V,W,U).
275
276binresult1(_,_,[],[]).
277binresult1(G,X,[Y|Z],[U|V]):- in( ((X,Y),U), G), !, binresult1(G,X,Z,V).
278
280partial_order(R):-
281 anti_symmetric(R),
282 transitive(R),
283 refexive(R).
284
285reflexsive(R):-field(R,F),
286 reflexive(F,R).
287
288reflexive([],_).
289reflexive([X|Y],R):- in((X,X), R), reflexive(Y,R).
290
291anti_symmetric(R):- member((X,Y),R),
292 X\==Y,
293 member((Y,X),R),
294 !,
295 fail.
296anti_symmetric(_).
297
298symmetric(R):- in((X,Y), R), \+ in((Y,X), R), !, fail.
299symmetric(_).
300
301transitive(R):- compose(R,R,RR), subset(RR,R).
302
307
308dags(Ns, Dags):- dags((peak, append), Ns, Dags).
309
310posets(Ns, Ps):- sort(Ns, Ms), dags((anti_chain, append), Ms, Ps).
311
312posets_in_fan(Ns, Dags):- dags((fan, union), Ns, Dags).
314
316peak(X, Dag, S, [(X,S)|Dag]).
317
318anti_chain(X, Poset, Chain, [(X, Chain)|Poset]):- anti_chain(Chain, Poset).
319
320anti_chain([],_).
321anti_chain([N|Ns], Poset):- anti_chain(Ns, Poset),
322 maplist(incomparable(N,Poset), Ns).
323
324incomparable(N, Poset, N0):- N @> N0, !, \+reach(N0,Poset,N).
325incomparable(N, Poset, N0):- \+reach(N, Poset, N0).
326
327reach(N,_,N):-!.
328reach(N0, Poset,N):- memberchk((N,L), Poset),
329 member(X, L),
330 reach(N0, Poset, X).
331
332fan(X, Poset, S, [(X,S0)|Poset]):-
333 maplist(fan(Poset), S, Ls),
334 union([S|Ls], S0).
335
336fan(P, X, L):- memberchk((X,L), P).
337
339dags(F, Nodes, Dags):- once(dags(F, Nodes, [[]], [[]], _, Dags)).
340
341dags(_, [], X, Y, X, Y).
342dags(F, [N|Ns], Succs0, Dags0, Succs, Dags):-
343 new_node(F, N, Succs0, Dags0, Succs1, Dags1),
344 dags(F, Ns, Succs1, Dags1, Succs, Dags).
345
346new_node(F, N, Succs, Dags, Succs1, Dags1):-
347 new_node(F, N, Succs, Dags, Dags1),
348 extend_succs(N, Succs, Succs1).
349
350new_node(F, N, Succs, Dags0, Dags):-
351 maplist(new_peak(F, N, Succs), Dags0, Dags1),
352 F = (_, A), 353 call(A, Dags1, Dags).
354
355new_peak(_, _, [], _, []).
356new_peak(F, X, [L|Ls], Dag, [Dag0|Dags]):-
357 F = (M, _), 358 call(M, X, Dag, L, Dag0),
359 !,
360 new_peak(F, X, Ls, Dag, Dags).
361new_peak(F, X, [_|Ls], Dag, Dags):-
362 new_peak(F, X, Ls, Dag, Dags).
363
364extend_succs(_, [], []).
365extend_succs(X, [S|R0], [S, [X|S]|R]):- extend_succs(X, R0, R).
366
369
370isolated(X, G):- rel(G, E), forall(in((X,Y), E); in((Y,X), E), X==Y).
371
372maximal(X, M):- in(X, M), rel(M, E), forall(in((X,Y), E), X=Y).
373
374minimal(X, M):- rel(M, E), forall(in((Y,X), E), X=Y).
375
376irreducible(L, M) :- fun(M, G), forall(in(X, L), binary_closed(G,[X],L)).
377
378idempotence(M):- fun(M, F), memberchk(((A,A),A), F).
379
380left_unit(U, G):- fun(G, M), dom(G, D),
381 forall(in(X,D), in(((U,X),X), M)).
382
383right_unit(U, G):- fun(G, M), dom(G, D),
384 forall(in(X, D), in(((X,U),X), M)).
385
386surj(M):- dom(M, D), fun(M, F), maplist(snd, F, M0),
387 sort(D, D0), sort(M0, D0).
388
390aug(OG):- models(OG,every(X,every(Y, (Y=< (X*Y))))).
391
392slide1(M):- models(M, every(A,every(B, every(C,
393 (((A*B)*C) =< (A*(B*C))))))).
394mix(M):- models(M, every(A,every(B, every(C, every(D, ((A=<B, C=<D)
395 -> ((B*C) =< (A*D))))))))