Software Engineering Lecture s11

Menu Menu


Prolog

SWI-Prolog
    Free soft です。規格(ISO Prolog)がちょっと古い
    http://www.swi-prolog.org/

SICStus Prolog
    Sweden 王立研究所で作られたもの。有料。若干性能が良いです。5倍ぐらい。
    http://www.sics.se/isl/sicstuswww/site/index.html
	琉大はライセンスを持っているんですけど...


論理型プログラミング

正しいと仮定した論理式があって、.... プログラム

これに、自分がやって欲しいことを論理式で書いて、その否定を追加する。

   この式って実行できないよね?

そうすると、Prolog の方が「いや、そんなことないよ」って反例を出して来る。

それがプログラムの実行になる。


SWI Prolog での例

finkに合わせてあるので、/opt/local/bin/swipl に installされる。

    ?- [user].
    |: a.
    |: b.                  
    |: % user://1 compiled 0.00 sec, 448 bytes <--- ^-D で抜ける。
    true.

ここで、a と b を公理として定義する。 listing で公理を見れる。

    ?- listing.
    a.
    b.

これで、問い合わせをしてみる。

    ?- a.
    true.
    ?- b.
    true.

定義されてないものには文句を言う。

    ?- c.
    ERROR: user://2:45:
	    toplevel: Undefined procedure: c/0 (DWIM could not correct goal)

明示的に false にした方が良い。

    ?- [user].
    |: c :- fail.
    |: % user://3 compiled 0.00 sec, 232 bytes
    true.
    ?- c.
    false.

not が否定。

    ?- not(c).
    true.

コンマが「かつ」、連言とか conjunction とか。

    ?- not(c),a.
    true.

セミコロンが「または」、disjunction とか。
    ?- c;b.
    true.

not が暗黙に定義されてない場合もあります。その時には自分で定義する。

    ?- [user].
    |: not(X) :- call(X),!,fail.
    |: not(_).
    |: % user://4 compiled 0.00 sec, 372 bytes
    true.


問題11.1

以下の論理式の真偽を Prolog で計算してみよ。

命題変数A,B の A=T, C=F として、次の論理式を Prolog の構文に直して、値を計算せよ。

1. A∧ ¬C
2. ¬A∨¬C
3. (¬A∨¬C)∧(A∧ ¬C )
4. (¬A∨C)∨¬(A∧ C )
5. (A∧¬C)∧(A∧C )

注: not(a,b) だと引数二つだと思われてしまうので、not((a,b)) と書く必要がある。not の後は空白をいれずにカッコを書く。


推論

    ?- [user].
    |: a.
    |: b.
    |: c :- fail.
    |: f :- c.
    |: f :- a,b.
    |: % user://1 compiled 0.00 sec, 848 bytes
    true.

f :- c. f :- a,b. は、 f ∨ ¬ c と f ∨ ¬ ( a ∧ c ) に対応します。

「c ならば f」は、「cでないか、または f」。

    if (c) f else true

有名な例ですが、

    If you move I will kill you.
    Don't move, or I will kill you.

実行は、trace みると良い。

    ?- trace,f.
       Call: (8) f ? creep
       Call: (9) c ? creep
       Call: (10) fail ? creep
       Fail: (10) fail ? creep
       Fail: (9) c ? creep
       Redo: (8) f ? creep
       Call: (9) a ? creep
       Exit: (9) a ? creep
       Call: (9) b ? creep
       Exit: (9) b ? creep
       Exit: (8) f ? creep
    true.

つまり、ルールが二つあって、

    (1) f :- c.
    (2) f :- a,b.

(1)をまず実行してみる。で、だめだったら、(2)を試す。これをバックトラックとか言います。

    if (c) return
    else a,b

にも見えますね。

    head :- condition1, !, body1.
    head :- condition2, !, body2.

というような感じで書きます。! は、ちょっと面倒。カットと呼ばれる。conditon1 が成立してたら、もう condition2 は試さない。
    
    


論理式の意味

論理式は、個々の構文要素に意味を対応する。ここでは、M(Q)という関数で論理式の意味を定義する。意味(Meaning)は、数学的な集合で、前もって定義されているとする。

Mの()の中に来るのは「記号列としての論理式」であって、

    P
    Q
    P ∨ Q
    P ∧ Q
    ¬P
    ( P ∧ Q ) ∧ Q 

とかが来る。この部分は、例えば、Java では、木構造を使って実現することができる。∧ とかの演算子であること、あるいは、PとかQ が変数を表すこと、() を使って、演算子のネスト(入れ子)を制御できることなどは、通常のプログラム言語に似ている。それに関して、細かく定義することは、自明なのでここではしない。

命題論理の場合は、M(Q) の値は、{T,F} の集合の要素、つまり、真か偽のどちらかである。例えば、PとかQ の変数の値は、前もって、T か F に決める。その決め方に従って、

    M(Q) = T
    M(P) = F

ということになる。「変数Q の意味(値)は、Tである」というように読む。

より複雑な論理式に対しては、M(Q) は、以下のように、記号列の構造(木構造)にそって決める。

M(P ∨ Q) = M (P) ∨ M (Q)
M(P ∧ Q) = M (P) ∧ M (Q)
M(¬P) = ¬ M(P)

右側の論理記号は既に知られている。(これで定義したことになるのか?)命題論理の場合は、これらは真理値表で定義することが出来る。

M(P) M(Q) M(P)∧ M(P) M(P)∨ M(Q) ¬ M(P)
T T TT F
T F FT F
F T FT T
F F FF T

この定義を使って命題論理式の値を計算することができる。

命題変数は、変数と真偽値を対応させる関数を定義する。
M(P) = T または F
これは変数の値の割当てである。変数は、変数に対応する集合の値、述語や関数は、それぞれに対応する写像に対応づけられる。

この対応を変更することにより論理式の真偽が変わる。変数の対応を論理式のインタープリテーション(Interpretation)という。

与えられた論理式を真にするようなインタープリテーションを論理式のモデル(Model)という。


論理式

命題変数の値に寄らず、必ず真だったり偽だったりする論理式がある。必ず真である論理式を恒真式(valid)と言う。

P ∨ ¬ P 必ず真
¬ (P ∨ ¬ P) 必ず偽

普通は論理式の真理値は、命題変数の値に依存する。


公理と論理

論理は、公理と呼ばれる、常に真と仮定する論理式の集合である。公理から推論により導かれる恒真式を定理と言う。公理が与えられた時に、ある論理式が恒真であることを示すことを証明と言う。

ここでは推論は、恒真式から新しい恒真式を作る方法ということにしておこう。

例えば、P, Q が恒真式なら、P∧Q や P∨Q も恒真式である。


完全性

公理から、推論を任意に当てはめて得られる定理の集合を考える。証明できるものは、すべてこの集合の中に入っている。


引数がある場合

    ?- [user].
    |: fact(0,1).
    |: fact(N,M) :- N1 is N-1,fact(N1,M1), M is N*M1.
    |: % user://2 compiled 0.01 sec, 436 bytes
    true.
    ?- fact(10,X).
    X = 3628800 .

実行してみるとこんな感じ。
    ?- trace,fact(3,N).
       Call: (8) fact(3, _G204) ? creep
    ^  Call: (9) _L167 is 3-1 ? creep
    ^  Exit: (9) 2 is 3-1 ? creep
       Call: (9) fact(2, _L168) ? creep
    ^  Call: (10) _L186 is 2-1 ? creep
    ^  Exit: (10) 1 is 2-1 ? creep
       Call: (10) fact(1, _L187) ? creep
    ^  Call: (11) _L205 is 1-1 ? creep
    ^  Exit: (11) 0 is 1-1 ? creep
       Call: (11) fact(0, _L206) ? creep
       Exit: (11) fact(0, 1) ? creep
    ^  Call: (11) _L187 is 1*1 ? creep
    ^  Exit: (11) 1 is 1*1 ? creep
       Exit: (10) fact(1, 1) ? creep
    ^  Call: (10) _L168 is 2*1 ? creep
    ^  Exit: (10) 2 is 2*1 ? creep
       Exit: (9) fact(2, 2) ? creep
    ^  Call: (9) _G204 is 3*2 ? creep
    ^  Exit: (9) 6 is 3*2 ? creep
       Exit: (8) fact(3, 6) ? creep
    N = 6 .

LISPの
  (defun fib1 (n a b)
       (if (< b n)
	   (cons b (fib1 n b (+ a b)))
	   nil))

これは、

    |: fib1(N,A,B,L) :- B<N,!,C is A+B,fib1(N,B,C,L1),L=(B,L1).
    |: fib1(_,_,_,true).
    ?- fib1(10,1,1,L).
    L = (1, 2, 3, 5, 8, true).

list の方が少しきれい。

    |: fib1(N,A,B,L) :- B<N,!,C is A+B,fib1(N,B,C,L1),L=[B|L1].
    |: fib1(_,_,_,[]).
    ?- [a,b,c] = [H|L].
    H = a,
    L = [b, c].
    ?- [a] = [H|L].
    H = a,
    L = [].

こうすると、ちょっと短くなる。

    |: fib1(N,A,B,[B|L1]) :- B<N,!,C is A+B,fib1(N,B,C,L1).
    |: fib1(_,_,_,[]).

記号ばっかりで、ローカル変数しかないので、短く書ける。特に、LISP の map/cons がcompactにかける。なので、LISPの半分ぐらい、Cの1/5ぐらいの大きさになります。

map/cons は、 Unification (単一化)とも呼ばれます。

    ?- [user].
    |: cons(A,B,[A|B]).
    |: % user://4 compiled 0.00 sec, 312 bytes
    true.
    ?- cons(A,B,[1,2]).
    A = 1,
    B = [2].
    ?- cons(1,2,X).
    X = [1|2].
    ?- cons(1,[2],X).
    X = [1, 2].

引数に構造体を書くと、mapにも consにも使える。


append

    ?- [user].
    |: ap([],X,X).
    |: ap([H|X],Y,[H|Z]) :- ap(X,Y,Z).
    |: % user://5 compiled 0.00 sec, 424 bytes
    true.
    ?- ap([a,b,c],[1,2,3],X).
    X = [a, b, c, 1, 2, 3].
    ?- ap(X,Y,[a, b, c, 1, 2, 3]).
    X = [],
    Y = [a, b, c, 1, 2, 3] ;
    X = [a],
    Y = [b, c, 1, 2, 3] ;
    X = [a, b],
    Y = [c, 1, 2, 3] ;
    X = [a, b, c],
    Y = [1, 2, 3] ;
    X = [a, b, c, 1],
    Y = [2, 3] ;
    X = [a, b, c, 1, 2],
    Y = [3] ;
    X = [a, b, c, 1, 2, 3],
    Y = [] ;
    false.
    ?- setof((X,Y),ap(X,Y,[a,b,c]),L).
    L = [ ([], [a, b, c]), ([a], [b, c]), ([a, b], [c]), ([a, b, c], [])].


Database として

    name1(Name,ID).
    class(ID,Claa).
    name1(shinji,2).
    name1(akiko,3).
    name1(taro,4).
    class(2,software).
    class(3,compiler).
    class(4,compiler).
    class(4,software).
    ?- name1(X,2).
    X = shinji .
    ?- name1(shinji,X).
    X = 2.

join 演算。

    ?- name1(X,_ID),class(_ID,Class).
    X = shinji,
    _ID = 2,
    Class = software ;
    X = akiko,
    _ID = 3,
    Class = compiler ;
    X = taro,
    _ID = 4,
    Class = compiler ;
    X = taro,
    _ID = 4,
    Class = software.

set of で取って来る。

    ?- setof((X,Class),_ID^(name1(X,_ID),class(_ID,Class)),L).
    L = [ (akiko, compiler), (shinji, software), (taro, compiler), (taro, software)].


Meta Programming

    | ?- [user].
    % compiling user...
    | solve((A,B)) :- solve(A), solve(B).
    | solve((A;B)) :- solve(A); solve(B).
    | solve(not(A)) :- not(solve(A)).
    | solve(A) :- c(A).
    | 
    | c(a).

この定義は、上の命題論理の M(P) とかに対応している。

    | ?- solve((a,not(c))).
    yes
    | ?- solve((not(a);not(c))).
    yes

実際に同じ答えを返す。

    % The debugger will first creep -- showing everything (trace)
	    1      1 Call: solve((not(a);not(c))) ? 
	    2      2 Call: solve(not(a)) ? 
	    3      3 Call: not(solve(a)) ? 
	    4      4 Call: solve(a) ? 
	    5      5 Call: c(a) ? 
	    5      5 Exit: c(a) ? 
	    4      4 Exit: solve(a) ? 
	    3      3 Fail: not(solve(a)) ? 
	    6      3 Call: c(not(a)) ? 
	    6      3 Fail: c(not(a)) ? 
	    2      2 Fail: solve(not(a)) ? 
	    7      2 Call: solve(not(c)) ? 
	    8      3 Call: not(solve(c)) ? 
	    9      4 Call: solve(c) ? 
	   10      5 Call: c(c) ? 
	   10      5 Fail: c(c) ? 
	    9      4 Fail: solve(c) ? 
	    8      3 Exit: not(solve(c)) ? 
    ?       7      2 Exit: solve(not(c)) ? 
    ?       1      1 Exit: solve((not(a);not(c))) ? 
    yes
    % trace
    | ?- 

Shinji KONO / Tue Jul 3 14:06:58 2012