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 に対応します。
「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
| ?-