1:-module(models,[]).    2:- use_module(util(math)).    3:- use_module(util(misc)).    4:- use_module(pac(basic)).    5:- use_module(pac(meta)).    6
    7%  models.pl   一階述語論理式のインタプリタ
    8%
    9%                        by  向井 国昭   1994年4月28日
   10%                                        2006年10月　　 　CGI化
   11%
   12% 制限： モデルの個体領域は, 有限個のアトムからなる： 関数記号は
   13% 扱わない。
   14%
   15% 使い方： まず個体領域と基本事実の集まりを次の例のように与える。
   16%   individual(taro).
   17%   individual(taro).
   18%   individual(hanako).
   19%   fact(love(taro,hanako)).
   20%   fact(love(hanako,hanako)).
   21%   fact(love(jiro,hanako)).
   22%
   23% このモデルで 論理式 たとえばall(x,some(y,love(x,y)))の真偽は判定するには
   24% 次のように実行する：
   25%
   26% | ?- models([], all(x,some(y,love(x,y))).
   27%
   28%
   29%  例：すぐ下に与えるモデルが次の論理式を充足するかいなかを
   30%       計算しよう。
   31%
   32% 用意された例題を動かすには次を実行すればよい:
   33%
   34% | ?- start.
   35%
   36% all(x,some(y, love(x,y))).
   37% some(x,all(y, love(x,y))).
   38% all(x,all(y, love(x,y))).
   39% some(y,some(x, love(x,y))).
   40% all(x,some(y, love(x,y))).
   41% some(x,all(y, love(x,y))).
   42% all(x,all(y, love(x,y))).
   43% some(y,some(x, love(x,y))).
   44
   45% 被テスト論理式：
   46% formula(all(x,some(y, love(x,y)))).
   47% formula(some(x,all(y, love(x,y)))).
   48% formula(all(x,all(y, love(x,y)))).
   49% formula(some(y,some(x, love(x,y)))).
   50% formula(all(x,some(y, love(x,y)))).
   51% formula(some(x,all(y, love(x,y)))).
   52% formula(all(x,all(y, love(x,y)))).
   53% formula(some(y,some(x, love(x,y)))).

individual(taro). individual(jiro). individual(hanako).

   60% fact(love(taro,hanako)).
   61% fact(love(hanako,hanako)).
   62% fact(love(jiro,hanako)).
   63%% end of example model
   64
   65start(F,Q,R):- split(F,F1), remove([],F1,F2),
   66	maplist(herbrand,F2,Facts),
   67	herbrand(Q,Query),
   68	individuals(Facts,Inds),
   69	(models(Inds,Facts,[],Query)-> R1=true; R1=false),
   70	term_smash0(["<font color=\"red\">", R1, "</font>\n"], R).
   71
   72set_of_individuals(F,R):- split(F,F1), remove([],F1,F2),
   73	maplist(herbrand,F2,Facts),
   74	individuals(Facts,Inds),
   75	insert(",", Inds, Inds0),
   76	term_smash0(Inds0,R).
   77
   78individuals(F,S):- maplist(atoms,F,F1),
   79	append(F1,F2),
   80	sort(F2,S).
   81
   82atoms(X,[X]):-atomic(X),!.
   83atoms(X,Y):- is_list(X),!,
   84	maplist(atoms, X, Z),
   85	append(Z, Y).
   86atoms(X,Y):- X=..[_|A],
   87	maplist(atoms, A, B),
   88	append(B, Y).
   89
   90% テストのメイン。
   91% start:-	printfact,
   92% 	(formula(S), write(S), test(S),nl,fail;true).
   93
   94% printfact:-a
   95% 	fact(X),write(X),nl,fail;
   96% 	write('**** end of facts ****'),nl,nl,nl.
   97
   98% test(S):- models([],S),!,write('  は真.').
   99% test(_):- write('  は偽.').
  100:- op(1100,xfx, <=>).  101
  102def_macro(false, not(true)).
  103% def_macro((X -> Y), or(not(X), Y)).
  104% def_macro((X <=> Y), and((X->Y), (Y->Y))).
  105def_macro(imply(X,Y), or(not(X), Y)).
  106def_macro(iff(X,Y), and(imply(X,Y), imply(Y,X))).
  107def_macro(all(X,P), not(some(X, not(P)))).

 models(Individuals, Facts, Assignments, Formula)

  110models(_,_,_,true) :-!.
  111models(X,Y,M,and(P,Q)) :-!, models(X,Y,M,P), models(X,Y,M,Q).
  112models(X,Y,M,or(P,Q))  :-!, (models(X,Y,M,P); models(X,Y,M,Q)).
  113models(X,Y,M,not(P))   :-!, \+ models(X,Y,M,P).  % negation of models(M,P)
  114models(I,F,M,some(X,P)):-!, member(A,I), models(I,F,[X=A|M],P).
  115models(I,F,M,P):- def_macro(P,P1), !, models(I,F,M,P1).
  116models(_,F,M,P):- substitute(P,M,Q), member(Q,F).
  117
  118% % membership
  119% member(X,[X|_]).
  120% member(X,[_|Y]):-member(X,Y).
  121
  122% substitute(X,M,Z)   apply the substitution M to X to get Y.
  123substitute(X,M,Y):-atomic(X), member(X=Y,M), !.
  124substitute(X,_,X):-atomic(X),!.
  125substitute(X,M,Y):-
  126        functor(X,F,N),
  127	functor(Y,F,N),
  128        substitute(N,X,M,Y).
  129
  130substitute(0,_,_,_):-!.
  131substitute(J,X,M,Y):-
  132        arg(J,X,A),
  133        substitute(A,M,B),
  134        arg(J,Y,B),
  135        K is J-1,
  136        substitute(K,X,M,Y).
  137
  138%%%%%%%% Yet Another DCG for `Tiny' PTQ.
  139
  140run :- prompt(A,''),
  141	(sample(S), get0(_), format("~w.",[S]),
  142       call(models:S, X), get0(_), nl,
  143       format("~w~n~n",[X]), fail; prompt(_, A)).
  144
  145sample(semantics(pn, [john], [male(j),male(b),female(m),unicorn(u), find(m,u),walk(j),walk(b),walk(m)])).
  146sample(semantics(np, [a, unicorn], [male(j),male(b),female(m),unicorn(u), find(m,u),walk(j),walk(b),walk(m)])).
  147sample(semantics(s, [a, unicorn, walk], [male(j),male(b),female(m),unicorn(u), find(m,u),walk(j),walk(b),walk(m)])).
  148sample(semantics(vp, [find, a, unicorn], [male(j),male(b),female(m),unicorn(u), find(m,u),walk(j),walk(b),walk(m)])).
  149sample(semantics(s, [john,find, a, unicorn], [male(j),male(b),female(m),unicorn(u), find(m,u),walk(j),walk(b),walk(m)])).
  150sample(semantics(pn, [john], [man(a),find(j,a),walk(j)])).
  151sample(semantics(pn, [john], [man(a),find(j,a),walk(j)])).
  152sample(semantics(tv, [find], [man(a),find(j,a),walk(j)])).
  153sample(semantics(itv, [walk], [man(a),find(j,a),walk(j)])).
  154sample(semantics(vp, [find, a, unicorn], [unicorn(a),find(j,a),walk(j)])).
  155sample(semantics(s, [john, walk], [man(a),find(j,a),walk(j)])).
  156sample(semantics(s, [every, man,  walk], [man(a),find(j,a),walk(j)])).
  157sample(semantics(s, [every, man,  walk], [man(j),find(j,a),walk(j)])).
  158
  159s(member(VP,NP)) --> np(NP), vp(VP).
  160
  161np(apply(currify(A), CN)) --> determiner(A), cn(CN).
  162np(PN) --> pn(PN).
  163
  164vp(ITV)  --> itv(ITV).
  165vp(inverse(currify(TV), NP)) --> tv(TV), np(NP).
  166
  167itv(ext(walk))-->[walk].
  168
  169tv(ext(find)) --> [find].
  170tv(ext(kick)) --> [kick].
  171
  172pn(filter(j)) --> [john].
  173pn(filter(b)) --> [bill].
  174pn(filter(m)) --> [mary].
  175
  176cn(ext(unicorn)) --> [unicorn].
  177cn(ext(man)) -->   [man].
  178cn(ext(woman)) --> [woman].
  179
  180determiner(q_sem(a)) --> [a].
  181determiner(q_sem(every)) --> [every].
  182
  183%%%%% Interpreter
  184
  185% ?- models:semantics(pn, [john], [man(a),find(j,a),walk(j)],X).
  186% ?- models:semantics(s, [john, walk], [man(a),find(j,a),walk(j)],X).
  187% ?- models:semantics(s, [every, man,  walk], [man(a),find(j,a),walk(j)],X).
  188% ?- models:semantics(s, [every, man,  walk], [man(j),find(j,a),walk(j)],X).
  189% ?- models:semantics(pn, [john], [man(x),find(j,x),walk(j)],X).
  190% ?- models:semantics(np, [a, man], [man(j), man(k)],  X).
  191% ?- models:semantics(np, [a, man], [man(j), man(k)],  X).
  192
  193semantics(S, Facts, V)  :- semantics(s, S, Facts, V).
  194%
  195semantics(C, S, F, V):- call(C, E, S, []),
  196	individuals(F, Inds),
  197	sem(Inds, F, E, V).
  198semantics(_,_,_,'** Category  mismatch ?').
  199%
  200sem(_, Fac, ext(R), V) :- !, extension(Fac,R,V1), sort(V1,V).
  201sem(D, _, filter(S), V) :- !, math:principal_filter(D, S, V).
  202sem(D, _, q_sem(Q), V) :- !, q_sem(Q, D, V).
  203sem(D, F, E, V)   :- meta:mapterm_rec(models:sem(D,F), E, E1),
  204	call(E1,V).
  205
  206%
  207extension([],_, []).
  208extension([A|B],R, [A1|B1]):- A=..[R|L], !,
  209	convert(L,A1),
  210	extension(B,R,B1).
  211extension([_|B],R, B1):- extension(B,R,B1).
  212
  213convert([],    void):-!.
  214convert([X],   X):- !.
  215convert([X|Y], (X,Y1)):- convert(Y,Y1).
  216
  217%
  218% apply(F,A,V):- member((B,V),F), subset(A, B), subset(B, A).
  219apply(F,A,V):- member(B-V,F), subset(A, B), subset(B, A).
  220
  221%
  222member(X,Y,true) :- member(X,Y),!.
  223member(_,_,false).
  224
  225%
  226currify --> math:rel_to_fun.
  227
  228% ?- models:q_sem(a, [1,2,3], R).
  229
  230q_sem(a, D, R):- !,
  231	(   powerset(D,PowD),
  232	    setof((X,Y), (member(X,PowD), member(Y,PowD), meet(X,Y)), R)
  233	->  true
  234	;   R=[]
  235	).
  236q_sem(every, D, R):- !,
  237	(   powerset(D,PowD),
  238	    setof((X,Y), (member(X,PowD), member(Y,PowD), subset(X,Y)), R)
  239	->  true
  240	;   R=[]
  241	).
  242
  243meet(X,Y):- member(A,X), member(A,Y).
  244
  245inverse(F, R, S):- inverse_image(F,R,S)