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