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
   10%%% groupoid %%%%
   11% grupoid(_, B, X, Y, [], [],true):- eval([algebra(B)], X, Y).
   12% grupoid(_, B, X, Y, [], [],true):- algebra(B, X, Y).
   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
   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
   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
   76%%%% model calculus
   77% :- index(models(0,1)).
   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).
   85% models(M, Y=Z):- !, eval(M, Y, Y0), eval(M, Z, Y0).
   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
   94%
   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
  117%%%%%%%%
  118
  119algebra(M, A*B, C, [A,B], [A0,B0], memberchk(((A0,B0),C), M)).
  120algebra(_, A, A, [], [], true).
  121
  122%%%% an element of the domain.
  123in(X, M):- dom(M, D), member(X, D).
  124
  125%%%%% a binary operation M is associative over a domain D.
  126% models(G, every(X,every(Y,(every(Z, ((X* Y)*Z) = (X*(Y*Z))))))).
  127
  128% ?- module(pac).
  129% ?- hmodel:find_model(grupoid::[a,b], \+ $(associativity), X).
  130% ?- hmodel:find_model(grupoid::[a,b], \+ $(associativity), X).
  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
  141%%%%%%
  142assign([],_).
  143assign([X|R],D):- member(X, D), assign(R,D).
  144
  145%%%%% has a  subalgebra
  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
  154%%%%% generator of ordered grupoid %%%%
  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
  166% ?- hmodel:permutations([1,2,3], X).
  167%@ X = [[3, 2, 1], [2, 3, 1], [2, 1, 3], [3, 1, 2], [1, 3, 2], [1, 2, 3]] .
  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
  181% non deterministic permutation generator
  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
  222%%%% test connectivity of undirectied graph (X,E).
  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
  241%%%%  G is a grupoid over X.
  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
  254%%%% a set X is closed
  255%%%% with respect to an binary operation Alg.
  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
  279%%%%%% predicates over relations
  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
  303%%%%%% top level call
  304% ?- dags([a,b,c], Dags).
  305% ?- posets([a,b,c,d,e,f,g], X).
  306% ?- posets_in_fan([a,b,c,d,e,f,g], X).
  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).
  313% 'union' is better than 'append'  at least for Ns=[a,b,c,d,e,f,g].
  314
  315%%%%%%
  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
  338%%%%%% dags: universal predicate  %%%%%%
  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),  % append or union
  353	call(A, Dags1, Dags).
  354
  355new_peak(_, _, [], _, []).
  356new_peak(F, X, [L|Ls], Dag, [Dag0|Dags]):-
  357	F = (M, _),  % method to add a node
  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
  367%%%%%
  368% ?- find_model(grupoid::[a,b], $surj, X).
  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
  389%%%% for OG
  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))))))))