Software Engineering Lecture s11
Menu Menu
仕様、実装、デバッグ
Prolog
SWI-PrologFree 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 に対応します。
「f ならば c」は、「fでないか、または c」。
if (f) c 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 | T | T | F |
T | F | F | T | F |
F | T | F | T | T |
F | F | F | F | 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 として
name(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). ?- name(X,2). X = shinji . ?- name(shinji,X). X = 2.join 演算。
?- name(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^(name(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 | ?-