og.pl

    1:- module(model,[]).    2:- use_module(pac('expand-pac')).    3% :- expects_dialect(pac).
    4term_expansion --> pac:expand_pac.
    5:- use_module(pac(op)).    6
    7entails(X, B, C):- generate(X, M), models(M, B), \+ models(M, C), !, fail.
    8entails(_, _, _).
    9
   10% ?- hmodel:find_model( grupoid::[a,b], \+ $(idempotence), R).
   11
   12find_model(F, C, X):- call(F, generate, X), models(X, C).
   13
   14models(_, true):-!.
   15models(M, (C1,C2)):- !, models(M, C1), models(M, C2).
   16models(M, (C1;C2)):- !,( models(M, C1); models(M, C2)).
   17models(M, (C1->C2)):- !, (\+ models(M, C1) ; models(M, C2)).
   18models(M, (\+ C)):- !,  \+ models(M, C).
   19models(M, every(Y,C)):- !, forall(belong(Y,M), models(M,C)).
   20models(M, some(Y,C)):- !,  belong(Y, M), models(M, C).
   21models(M, Y=Z):- !, call(M, Y, V), call(M, Z, V).
   22models(M, $(Property)):- !, call(Property, M).
   23models(_, prolog(G)):- !, once(G).
   24models(M, forall(P, G)):- !, forall(P, models(M, G)).
   25models(M, exists(P, G)):- !, call(P), models(M, G).
   26models(M, X):- 	mapterm(M, X, X0), holds(M, X0).
   27
   28%%%%%
   29holds(_,  A=<A).
   30holds(M,  A=<B):- world(M, Fs), memberchk((A,B), Fs).
   31
   32% ?- listing(algebra).
   33% ?- listing('pac#52').
   34
   35algebra(M,A*B,A1):-!,(algebra(M,A,A2),algebra(M,B,A3)),'pac#431'(M,A2,A3,A1) .
   36algebra(A1,A,A):-! .
   37
   38'pac#431'(A,B,C,D):-memberchk(((B,C),D),A) .
   39
   40%%%% Plugin; an element of the domain.
   41belong(X,og(L,_,_)):-!, in(X, L).
   42belong(X,int(K,J)):- !,  between(K,J,X).
   43belong(X,[Y|Z]):-!, (X=Y; in(X, Z)).
   44belong(X,lin(N,_)):-!,  between(1,N,X).
   45belong(X,grupoid(L,_)):- in(X, L).
   46
   47%%%% Plugin: eval (interface) %%%%%%
   48
   49% :-bekind(og//3).
   50% X = with(_, _, H, model:algebra(H)::X).
   51% :-ekind.
   52
   53% :-bekind(grupoid//2).
   54% X = with(_, B, algebra(B)::X).
   55% :-ekind.
   56
   57%%%%% some tiny
   58promote_to_mode(M, [model:M]).
   59
   60world(og(_,X,_), X).
   61
   62%%%%  miscellaneous properties of models
   63
   64aug(OG):- models(OG,every(X,every(Y, (Y=< (X*Y))))).
   65
   66associative(G):-
   67	models(G, every(X,every(Y,(every(Z, ((X* Y)*Z) = (X*(Y*Z))))))).
   68
   69slide1(M):-
   70	models(M, every(A,every(B, every(C, (((A*B)*C) =< (A*(B*C))))))).
   71
   72mix(M):- models(M, every(A,every(B, every(C, every(D,
   73	((A=<B, C=<D) -> ((B*C) =< (A*D)))
   74	))))).
   75
   76isolated(X, graph(_,E)):- forall((in((X,Y),  E); in((Y,X),  E)), X==Y).
   77
   78maximal(X, graph(_,E)):- forall(in((X,Y), E), X=Y).
   79
   80minimal(X, graph(_,E)):- forall(in((Y,X),  E), X=Y).
   81
   82irreducible(L, grupoid(_,G)):- forall(in(X, L), binary_closed(G,[X],L)).
   83
   84idempotent(A, grupoid(_,H)):- in(((A,A),A),  H).
   85
   86idempotent(M):- grupoid_table(M, Table), memberchk(((A,A),A), Table).
   87
   88left_unit(U, grupoid(D,M)):- forall(in(X, D), in(((U,X),X),  M)).
   89
   90right_unit(U, grupoid(D,M)):- forall(in(X, D), in(((X,U),X), M)).
   91
   92rich(M):-!, M=lin(N,Asg),
   93	models(M, every(K, (setofint(K,1,N,S), subalgebra(S,Asg)))).
   94
   95surj(og(D,_,M)):- maplist(snd, M, M0), sort(M0, D).
   96
   97
   98in(X,[X|_]).
   99in(X,[_|Y]):- in(X,Y).
  100
  101belong_list(_, []).
  102belong_list(A, [X|R]):- belong(X,A), belong_list(A,R).
  103
  104grupoid_table(og(_,_,H), H).
  105
  106%%%% Plugin; generator for a class of structures (models)
  107
  108og(D, generate, og(D0,X,Y)):-!, sort(D, D0), ordered_grupoid(D0, X, Y).
  109
  110og0(D, _, _, domain, D).
  111og0(_, R, _, order, R).
  112og0(_, _, M, op, M).
  113
  114lin(N, generate, lin(N,X)):-!, linear_grupoid(N, X).
  115grupoid(D, generate, grupoid(D,X)):-!, grupoidx(D, X).
  116int(K, generate,  int(1, K)):-!.
  117int(K,J, generate,int(K, J)).
  118
  119generate(og(D),og(D0,X,Y)):-!, sort(D, D0), ordered_grupoid(D0, X, Y).
  120generate(lin(N),lin(N,X)):-!, linear_grupoid(N, X).
  121generate(grupoid(D),grupoid(D,X)):-!, grupoidx(D, X).
  122generate(int(K),  int(1, K)):-!.
  123generate(int(K,J),int(K, J)).
  124
  125perm_group(X, Y):- permutations(X, PermX), maplist(zip(X), PermX, Y).
  126
  127% bi-directional list comparison: less-than-or-equal:
  128% ?- leq_int_seq(3,X,Y).
  129% X = [1, 1, 1], Y = [1, 1, 1] ; ....
  130% ?- linear_grupoid(2,X).
  131% X = [ ((2, 1), 1), ((2, 2), 1), ((1, 1), 1), ((1, 2), 1)] ; ...
  132
  133linear_grupoid(N,X):-up_sequence(N,Y), list2grupoid(N,Y,X).
  134
  135leq_int_seq(N,X,Y):-leq_int_seq(N,N,X,Y).
  136
  137leq_int_seq(_,0,[],[]).
  138leq_int_seq(N,J,[X|Y],[Z|U]):- J>0,
  139	J1 is J-1,
  140	leq_int_seq(N,J1,Y,U),
  141	between(1,N,X),
  142	between(X,N,Z),
  143	lower_bound(N,Z,U),
  144	lower_bound(N,X,Y).
  145
  146% ?- up_sequence(3,X).
  147% X = [[1, 1, 1], [1, 1, 1], [1, 1, 1]] ; ....
  148
  149up_sequence(N,X):- up_sequence(N,N,X).
  150
  151up_sequence(_,0,[]).
  152up_sequence(N,J,[X|Y]):- J>0, J1 is J-1,
  153	up_sequence(N,J1,Y),
  154	up_sequence1(N,X,Y).
  155
  156up_sequence1(N,X,[]):-int_up_seq(N,N,X).
  157up_sequence1(N,X,[Y|_]):-leq_int_seq(N,X,Y).
  158
  159int_up_seq(_,0,[]).
  160int_up_seq(N,J,[X|Y]):- J>0, J1 is J-1,
  161	int_up_seq(N,J1,Y),
  162	lower_bound(N, X,Y).
  163
  164lower_bound(N,Z,[]):- between(1,N,Z).
  165lower_bound(_,Z,[H|_]):-between(1,H,Z).
  166
  167list2map(N,X,Y):- list2map(N,1,X,Y).
  168
  169list2map(_,_,[],[]).
  170list2map(J,K,[X|Y],[((J,K),X)|Z]):-
  171	K1 is K+1,
  172	list2map(J,K1,Y,Z).
  173
  174list2grupoid(_,[],[]).
  175list2grupoid(N,[X|Y],Z):-
  176	list2map(N,X,X1),
  177	N1 is N-1,
  178	list2grupoid(N1,Y,Y1),
  179	lists:append(X1,Y1,Z).
  180
  181
  182%%%%% eval_grupoid %%%%%
  183eval_grupoid(M,A*B,V):-!,
  184	eval_grupoid(M,A,A1),
  185	eval_grupoid(M,B,B1),
  186	in(((A1,B1),V), M).
  187eval_grupoid(_,A,A).
  188
  189%%%%%%%%%%%%% set of integers %%%%%%
  190setofint(0,_,_,[]).
  191setofint(J,K,L,[K|R]):- J>0, K=<L,
  192	J1 is J-1,
  193	K1 is K+1,
  194	setofint(J1,K1,L,R).
  195setofint(J,K,L,S):-J>0, K=<L,
  196	K1 is K+1,
  197	setofint(J,K1,L,S).
  198
  199%%%% rich alegbra %%%%%
  200rich_algebra(X,Alg):- powerset(X,P), length(X,N), N1 is N-1,
  201	rich_algebra(N1,P,Alg).
  202
  203rich_algebra(1,_,_):-!.
  204rich_algebra(K,P,Alg):- in(S, P), length(S,K), subalgebra(S,Alg),
  205	K1 is K-1, rich_algebra(K1,P,Alg).
  206
  207%%%%% generator of ordered grupoid %%%%
  208ordered_grupoid(X,E,G):-
  209	posets_in_fan(X,Ps),
  210	member(E0, Ps),
  211	succlist_pairs(E0, E),
  212	grupoid(X,G).
  213
  214succlist_pairs([],[]).
  215succlist_pairs([(_,[])|R], Ps):- succlist_pairs(R, Ps).
  216succlist_pairs([(A,L)|R], Ps):-
  217	succlist_pairs(A, L, Qs),
  218	succlist_pairs(R, P0s),
  219	append(Qs, P0s, Ps).
  220
  221succlist_pairs(_,[],[]).
  222succlist_pairs(A,[X|Xs],[(X,A)|Ys]):- succlist_pairs(A,Xs,Ys).
  223
  224%%%% misc
  225leq_poset(_,A,A).
  226leq_poset(E,A,B):- in((A,A1),  E), A\==A1, leq_poset(E,A1,B).
  227
  228% for debugging;  usage:
  229show(lin(N,G), Vs, L, R):- belong_list(lin(N,G), Vs),
  230       eval_grupoid(G,L,L1),
  231       eval_grupoid(G,R,R1),
  232       format("~w ~w :  ~w~n", [Vs, L1, R1]),
  233       fail; true.
  234
  235% permutations([1,2,3], X).
  236% X = [[3, 2, 1], [2, 3, 1], [2, 1, 3], [3, 1, 2], [1, 3, 2], [1, 2, 3]]
  237
  238permutations(X, Y):- permutations(X, [[]], Y).
  239
  240permutations([],X, X).
  241permutations([X|Xs],Z0, Z):- maplist(perm_insert(X), Z0, Z1),
  242	append(Z1, Z2),
  243	permutations(Xs, Z2, Z).
  244
  245perm_insert(X, [], [[X]]).
  246perm_insert(X, [Y|Ys], [[X, Y|Ys]|Z]):-
  247	perm_insert(X, Ys, Z0),
  248	maplist(cons(Y), Z0, Z).
  249
  250% non deterministic permutation generator
  251perm_nd(X, Y) :- perm_nd(X, [], Y).
  252
  253perm_nd([], X, X).
  254perm_nd([X|Xs], Y0, Y):- insert_nd(X, Y0, Y1), perm_nd(Xs, Y1, Y).
  255
  256insert_nd(X, Y, [X|Y]).
  257insert_nd(X,[Y|Ys], [Y|Zs]):- insert_nd(X, Ys, Zs).
  258
  259diagonal([]).
  260diagonal([(X,X)|D]):-diagonal(D),!.
  261
  262make_id([],[]).
  263make_id([X|Y],[(X,X)|D]):- make_id(Y,D).
  264
  265field([],[]).
  266field([(X,Y)|R],[X,Y|F]):-field(R,F).
  267
  268compose(X,Y,Z):-compose(X,Y,Z,[]).
  269
  270compose([],_,X,X).
  271compose([(X,Y)|Z],U,V,W):- compose(X,Y,U,V,R), compose(Z,U,R,W).
  272
  273compose(_,_,[],X,X).
  274compose(X,Y,[(Y,Z)|U],[(X,Z)|V],W):-!, compose(X,Y, U,V,W).
  275compose(X,Y,[_|U],V,W):- compose(X,Y, U,V,W).

  279trcl(R,X):- trcl(R,R,X).
  280
  281trcl(R,X,Y):- compose(R,X,RX), union(RX,X,Z), trcl(R,X,Z,Y).
  282
  283trcl(_,X,Y,X):- subset(Y,X),!.
  284trcl(R,_,Y,Z):- trcl(R,Y,Z).
  285
  286trcl_sum(X,Y,Z):-compose(X,Y,Z1),compose(Y,X,Z2),
  287	union(Z1,Z2,Z3),
  288	trcl(Z3,Z4),
  289	union([X,Y,Z4],Z).
  290
  291%%%% test connectivity of undirectied graph (X,E).
  292
  293connected(X,E):-makediscrete(X,Y),
  294	union_find(E,Y,Class),Class=[_].
  295
  296makediscrete([],[]).
  297makediscrete([X|R],[[X]|R1]):-makediscrete(R,R1).
  298
  299%%%%  G is a grupoid over X.
  300grupoid(X,G):-
  301	cartesian(X,X,XX),
  302	maps(XX,X,XXX),
  303	in(G, XXX).
  304
  305grupoidx(X,G):-

  306	cartesian(X,X,XX),
  307	map(XX,X,G)

  307.
  308
  309map([],_,[]).
  310map([X|R],Y,[(X,A)|S]):- in( A,  Y), map(R,Y,S).
  311
  312%%
  313maps(Xs, Ys, Fs):-  foldl(maps(Ys), Xs, [[]], Fs).
  314
  315maps(Ys, X,  F0s, Fs):- foldl(maps(F0s, X), Ys, Fs, []).
  316
  317maps([], _, _, Gs, Gs).
  318maps([F|Fs], X,Y, [[(X,Y)|F]|G0s], Gs):- maps(Fs, X, Y, G0s, Gs).
  319
  320
  321%%%% a set X is closed
  322%%%% with respect to an binary operation Alg.
  323
  324subalgebra(X,Alg):- in(Y, X), in(Z, X), in(((Y,Z),U), Alg), \+ in(U, X), !, fail.
  325subalgebra(_,_).
  326
  327%%%%% a binary operation M is associative over a domain D.
  328associative(D,M):-assign([X,Y,Z],D),
  329	member(((Y,Z),YZ),M),
  330	member(((X,YZ),XYZ),M),
  331	member(((X,Y),XY),M),
  332	member(((XY,Z),XYZ),M),
  333	!,
  334	fail.
  335associative(_,_).
  336
  337assign([],_).
  338assign([X|R],D):- in(X , D), assign(R,D).

  342binary_closed(G,X,Y):- bincl(G,X,Z), subset(Y,Z).
  343
  344bincl(G,X,Y):-binresult(G,X,X,Z), bincl1(G,X,Z,Y).
  345
  346bincl1(_,X,Y,X):- subset(Y,X),!.
  347bincl1(G,X,Y,Z):- union(X,Y,U), bincl(G,U,Z).
  348
  349binresult(_,[],_,[]).
  350binresult(G,[X|Y],Z,U):-
  351	binresult1(G,X,Z,V),
  352	binresult(G,Y,Z,W),
  353	union(V,W,U).
  354
  355binresult1(_,_,[],[]).
  356binresult1(G,X,[Y|Z],[U|V]):- in(((X,Y),U),  G), !,  binresult1(G,X,Z,V).
  357
  358%%%%%% predicates over relations
  359partial_order(R):-
  360	anti_symmetric(R),
  361	transitive(R),
  362	refexive(R).
  363
  364reflexsive(R):-field(R,F),
  365	reflexive(F,R).
  366
  367reflexive([],_).
  368reflexive([X|Y],R):- in((X,X), R), reflexive(Y,R).
  369
  370anti_symmetric(R):- member((X,Y),R),
  371	X\==Y,
  372	member((Y,X),R),
  373	!,
  374	fail.
  375anti_symmetric(_).
  376
  377symmetric(R):- in((X,Y), R),  \+ in((Y,X), R), !, fail.
  378symmetric(_).
  379
  380transitive(R):- compose(R,R,RR), subset(RR,R).
  381
  382%%%%%% the set of DAGS and Posets %%%%
  383% ?- dags([a,b,c], Dags).
  384% ?- posets([a,b,c,d,e,f,g], X).
  385% ?- posets_in_fan([a,b,c,d,e,f,g], X).
  386
  387%%%%%% top level call
  388
  389dags(Ns, Dags):- dags((peak, append), Ns, Dags).
  390
  391posets(Ns, Ps):- sort(Ns, Ms), dags((anti_chain, append), Ms, Ps).
  392
  393posets_in_fan(Ns, Dags):- dags((fan, union), Ns, Dags).
  394
  395%%%%%%
  396peak(X, Dag, S, [(X,S)|Dag]).
  397
  398anti_chain(X, Poset, Chain, [(X, Chain)|Poset]):- anti_chain(Chain, Poset).
  399
  400anti_chain([],_).
  401anti_chain([N|Ns], Poset):- anti_chain(Ns, Poset),
  402	maplist(incomparable(N,Poset), Ns).
  403
  404incomparable(N, Poset, N0):- N @> N0, !, \+reach(N0,Poset,N).
  405incomparable(N, Poset, N0):- \+reach(N, Poset, N0).
  406
  407reach(N,_,N):-!.
  408reach(N0, Poset,N):- memberchk((N,L), Poset),
  409	member(X, L),
  410	reach(N0, Poset, X).
  411
  412fan(X, Poset, S, [(X,S0)|Poset]):-
  413 	maplist(fan(Poset), S, Ls),
  414 	union([S|Ls], S0).
  415
  416fan(P, X, L):- memberchk((X,L), P).
  417
  418%%%%%% dags: universal predicate  %%%%%%
  419
  420dags(F, Nodes, Dags):- once(dags(F, Nodes, [[]], [[]], _, Dags)).
  421
  422dags(_, [], X, Y, X, Y).
  423dags(F, [N|Ns], Succs0, Dags0, Succs, Dags):-
  424	new_node(F, N, Succs0, Dags0, Succs1, Dags1),
  425        dags(F, Ns, Succs1, Dags1, Succs, Dags).
  426
  427new_node(F, N, Succs, Dags, Succs1, Dags1):-
  428	new_node(F, N, Succs, Dags, Dags1),
  429	extend_succs(N, Succs, Succs1).
  430
  431new_node(F, N, Succs, Dags0, Dags):-
  432	maplist(new_peak(F, N, Succs), Dags0, Dags1),
  433	F = (_, A),  % append or union
  434	call(A, Dags1, Dags).
  435
  436new_peak(_, _, [], _, []).
  437new_peak(F, X, [L|Ls], Dag, [Dag0|Dags]):-
  438	F = (M, _),  % method to add a node
  439	call(M, X, Dag, L, Dag0),
  440	!,
  441	new_peak(F, X, Ls, Dag, Dags).
  442new_peak(F, X, [_|Ls], Dag, Dags):-
  443	new_peak(F, X, Ls, Dag, Dags).
  444
  445extend_succs(_, [], []).
  446extend_succs(X, [S|R0], [S, [X|S]|R]):- extend_succs(X, R0, R)