操作的・宣言的意味

by user

on 28 марта 2017

Category: Documents

>> Downloads: 0

views

Report

Comments

Description

Download 操作的・宣言的意味

Transcript

操作的・宣言的意味

ϓϩάϥϜཧ࿦ͱ‫ ޠݴ‬Part2-1-6
2
2.1
1
࿦ཧ‫ޠݴܕ‬
σʔλߏ଄ͱ୯ҰԽ
Ϧετ
Ϧετͷఆٛ
લճʹ͓͍ͯɺσʔλϕʔεͷ‫͔఺؍‬Β࿦ཧΛಋೖͨ͠ɻ
‫ݻ‬ମΛද͢ఆ਺ͱม਺ʹ‫ݶ‬ఆͨ͠࿩ͩͬͨ
ࠓճ͸ɺҰൠͷϓϩάϥϜ‫ͯ͠ͱޠݴ‬ɺσʔλߏ଄Λѻ͏ඞ
ཁੑ͔Βɺʮؔ਺‫߸ه‬ʯΛ‫ͨ͠ڐ‬৔߹ʹ͍ͭͯड़΂Δ
t = [X1 , ..., Xn ] = [X1 |[X2 |....[Xn |[ ]]...]]
ͳΔ୯ҰԽ͕੒ޭ͢Δ͜ͱɻ
[ ] ͸ۭϦετͰɼ௕̌͞ͷϦετΛ͢͞
ؔ਺‫߸ه‬ɿ σʔλߏ଄ߏ੒ࢠ
ಛʹɺؔ਺‫͋Ͱޠݴܕ‬Δ LISP ಉ༷ʹɺσʔλ͸શͯࣜͱ͠
ͯѻΘΕɺ·ͨɺಛʹɺϦετ͕ओཁͳߏ଄ද‫ͳͱݱ‬Δ
‫ج‬ຊ͸࠶‫ؼ‬తखଓ͖ʢ‫܁‬Γฦ͠΋࠶‫ؼ‬తʹॻ͘ʣ
ઢ‫ܗ‬Ϧετ [a,b,c]
[a|[b|[c|[]]]] ͷུ‫ه‬
໦ߏ଄ߏ੒ࢠ [_|_]
ෳ߹Ϧετ [a,[1,2,3],c]
[a|[[1|[2|[3|[]]]]|[c|[]]]]
ͷུ
Ϧετͷఆٛ
1
2
2.2
2.3
ࣜͱͯ͠ͷσʔλɺ୅ೖ
߲ (term): ม਺ɺఆ਺ɺ΋͘͠͸ f (t1 , ..., tn )ɺwhere f : ߲
Lisp ʹ͓͚Δ̨ࣜͷΑ͏ʹɺ࿦ཧ‫͕ޠݴܕ‬ѻ͏σʔλ͸શ
ͯɺ߲ (term) Ͱ‫ه‬ड़͢Δ
(T1) ఆ਺ a,b, ... ɺม਺ X, Y,... ͸߲
(T2) t1 , .., tn ͕߲Ͱɺf ͕ n Ҿ਺ͷؔ਺‫߸ه‬
˰ f (t1 , ...., tn ) ͸߲
Λ࡞Γग़͢ߏ੒ࢠͰʮؔ਺‫߸ه‬ʯͱ‫ݺ‬͹ΕɺҾ਺͸߲ tj
ΛͱΔɻϦετͰ͸ؔ਺‫ ]_|_[ ͯ͠ͱ߸ه‬ͷΈΛߟ͑Δ
୯ҰԽ θɿ ม਺ʹผͷ߲Λ୅ೖ͠ɺʮಉ͡‫ܗ‬ʯʹ͢Δ
ͦͷதͰ࠷΋Ұൠతͳ΋ͷ͕ ࠷൚୯ҰԽ (mgu) (*)
σʔλૢ࡞͸ʢ਺஋౳Λআ͖ʣࣜʹର͢Δ୅ೖૢ࡞ɿ
୅ೖ θ = {X1 = t1 , ..., Xn = tn }, dom(θ) = {X1 , ..., Xn }
t1 τ = t2 τ ͳΔ೚ҙͷ୅ೖ τ ʹର͠ some ζ s.t. θζ = τ
ม਺ X = t ɿ
߲ t ͕ X Λ‫͚ͳ·ؚ‬Ε͹੒ޭ͠ɺ
୅ೖ θ = {..., X = t, ...} ͷద༻ɿ ม਺ Xj Λ‫ؚ‬Ήࣜ s(Xj )
୅ೖ θ = {X = t} Λ࣮ߦ͢Δ
ʹ͓͚Δ Xj ͷग़‫ݱ‬ΛҰ੪ʹʢಉ࣌ʹʣରԠ͢Δ߲ tj ʹ
ஔ͖‫ ࣜͨ͑׵‬s(tj ) Λग़ྗɻ݁Ռͷ߲Λ sθ ͱද‫ه‬
g(s1 , ..., sm ) = f (t1 , ..., tn ) ͕੒ޭ
˱
୅ೖͷྫɿθ = { X=a, Y=[c] }
f(X,g(Y))θ = f(a,g([c]))
୯ҰԽɿ ߏจతͳύλʔϯϚονϯά
[a,X,Y,b]θ = [a,a,[c],b]
୅ೖͷ߹੒ɿ ୅ೖ͸ɺ߲Λೖྗͱͯ͠ɺ߲Λฦ͢ʮࣸ૾ʯ
Αͬͯɺࣸ૾ͱͯ͠ͷ߹੒͕Մೳ
θτ = {X = Xθτ | X ∈ dom(θ)}
∪{Z = Zτ | Z ∈ dom(τ ) \ dom(θ)}
ྫɿ { X=f(Y), Z=b } { Y=d } = { X=f(d), Y=d, Z=b }
f = g ʢಉ͡‫ Ͱ߸ه‬n = mʣɺ͔ͭ
s1 θ = t1 θ, ..., sn θ = tn θ ͳΔ θ ͕ଘࡏ
?- f(X,g(X,Y)) = f(k(a,W),Z)
ෆҰக X ,k(a,W): θ1 ={X=k(a,W)}
?- f(k(a,W),g(k(a,W),Y)) = f(k(a,W),Z)
ෆҰக g(k(a,W),Y), Z: θ2 ={Z=g(k(a,W),Y)}
?- f(k(a,W),g(k(a,W),Y))
= f(k(a,W),g(k(a,W),Y))
ෆҰகແ͠ɿ ୯ҰԽ͸੒ޭ͠ɼθ = θ1 θ2
(*) ࠶൚ੑͷ௚‫ײ‬తͳઆ໌ɿ
ෆҰக X = t ͷղফͷͨΊͷ୅ೖద༻͸ɼඞཁ࠷খ‫ݶ‬ͷૢ࡞ʢ༨‫ͱ͜ͳܭ‬͸͠ͳ͍ʣɽ
3
4
2.4
3
Ϧετͷ୯ҰԽ
Ϧετͷ୯ҰԽ΋Ұൠతͳ୯ҰԽΞ
ϧΰϦζϜʹै͏ɻϦετ͸্‫ه‬
ͷಛผͳུ‫ه‬๏Λ΋ͭͷͰɺ͜͜
ૢ࡞తҙຯ࿦ʢ࣮ߦ‫ܥ‬ʣ
͍ΘΏΔ ̝̾͆ ʢͲͷΑ͏ʹͯ͠‫͢ࢉܭ‬Δ͔ɺ‫ॲࢉܭ‬ཧ͕
ਐߦ͢Δͷ͔ʣΛ‫ه‬ड़
࿦ཧ‫ޠݴܕ‬ͷ৔߹ɺSLD(Selectvie Linear Resolution for Def-
Ͱ͸Լ‫ه‬ͷ‫ن‬ଇͰߦ͏
(U1) ۭϦετ [] ͱϚον͢ΔϦε
τ͸ۭϦετͷΈɻ
(U2) [X]: Ϧετཁૉ͕୯Ұͳ΋ͷ
ͷΈͱϚον͢Δɻ
(U3) [X1,X2]: ̎ͭͷϦετཁૉ͔
ΒͳΔ΋ͷͷΈͱϚον͢Δɻ
ྫɿ
inite Clauses) ಋग़͕ඪ४త
ΰʔϧઅɿ ? − A1 , ..., An
͜Ε·ͰɼΫΤϦʔͱ‫ݺ‬Μͩ
Aj ͸ ਖ਼Ϧςϥϧ p(t1 , ..., tn )
p ͸ड़‫ޠ‬ʢؔ܎Λද͢‫߸ه‬ʣɼtj ͸σʔλΛද߲͢
ෛϦςϥϧ \ + p(t1 , ..., tn ) \+ ͸൱ఆ
ਖ਼ϦςϥϧΛ୯ʹΞτϜʢ‫ࢠݪ‬࿦ཧࣜʣɽ
ม਺Λ‫͖ͱ͍ͳ·ؚ‬ɼ‫ج‬ఈΞτϜ (ground atom)
[X1,X2]=[a,[b,c]] ˰ X1=a, X2=[b,c]
[X1,X2]=[X] ͸୯ҰԽࣦഊɻಉ༷ʹɺ
[X] =[X1|X2] ͸ X=X1, X2=[] Ͱ੒ޭɻ
[X1,X2]=[Z1|Z2] ͸ X1=Z1, Z2=[X2] Ͱ੒ޭ
ҰൠʹɺϦετ [a1,....,an]=[X|Y] ʹର͠X=a1, Y=[a2,...,an]
ͱͳΔɻʢͨͩ͠ n ≥ 1 Ͱ n = 1 ͷͱ͖͸ Y=[]. ͭ·Γ
[a1,a2,...,an]=[a1|[a2,...,an]]
ϓϩάϥϜ P : ҎԼͷϧʔϧͷॱংू߹ʢॻ͔Εͨॱʣ
֬ఆઅ A : −B1 , ..., Bm ʢm ≥ 0ʣ
A: ਖ਼Ϧςϥϧɺϔου
Bj : ਖ਼ϦςϥϧͰɺB1 , ..., Bm ͸ຊମʢϘσΟɼ৚݅෦ʣ
A, B1 , ..., Bm ͕શͯม਺Λ‫͖ͱ͍ͳ·ؚ‬ɼ‫ج‬ఈϧʔϧ
ϧʔϧɿ ֬ఆઅɼ΋͘͠͸ຊମதʹෛϦςϥϧΛ‫͢ڐ‬΋ͷ
ΰʔϧઅΛɺΰʔϧϦμΫγϣϯʹΑΓɺม‫͢ܗ‬Δաఔ͕‫ܭ‬
ࢉաఔʢ൓ളʣ
5
6
3.1
ΰʔϧϦμΫγϣϯʢෛϦςϥϧ͕‫ݱ‬Εͳ͍৔߹ʣ
ΰʔϧઅதͷϦςϥϧΛબ୒͠ͳ͕Βɺϧʔϧͷ಄෦ͱ୯Ұ
3.2
୅ೖͷ߹੒ͱղ୅ೖ
?- A1 θ, ..., Ak−1 θ, B1 θ, ..., Bn θ, Ak+1 θ, ..., Am θ.
?- app([X],[b,c],Res)
app([X|Xs],Ys,[X|Zs]) :- app(Xs,Ys,Zs)
ม਺෼཭ɿ app([X1|X1s],Y1s,[X1|Z1s]) :- app(X1s,Y1s,Z1s)
θ1 = { X1=X, X1s=[], Y1s=[b,c], Res=[X|Z1s] }
?- app([],[b,c],Z1s)
app([],Xs,Xs).
ม਺෼཭ɿapp([],X2s,X2s)
θ2 = { X2s=[b,c], Z1s = [b,c] }
˘
͜ͷૢ࡞Λɺ̙̙̗Ͱઆ໌ͨ͠Α͏ʹɺ
୅ೖͷ߹੒ͱղ୅ೖ ্‫ه‬ͷΑ͏ʹɺΰʔϧϦμΫγϣϯʹΑ
Խ͠ɺϧʔϧͷຊମ෦ʹஔ͖‫͑׵‬Δૢ࡞
?- A1 , ..., Ak−1 , Ak , Ak+1 , ..., Am .
ͨͩ͠ɺϧʔϧ A : −B1 , ..., Bn ͱɺ
A : −B1 , ..., Bn ΰʔϧઅ : −A1 , ..., Am ͷม਺͕িಥ
θ s.t. Ak θ ≡ Aθ ͕ͳ͍Α͏ʹɺࣗಈͰม਺໊ͷ໊લସ
Λߦ͏ʢม਺෼཭ʣ
ۭઅ ˘ ͕ಋग़͞ΕΔ·Ͱଓ͚Δ
Γɺ୅ೖͷ‫ ྻܥ‬θ1 , ..., θk ͕ಘΒΕΔ
͜ΕΒͷ୅ೖΛશͯ߹੒ͨ͠΋ͷ
?- app([X],[b,c],Res)
app([X|Xs],Ys,[X|Zs])
ྫɿ Ϧετͷ࿈઀
:-app(Xs,Ys,Zs).
app([],Xs,Xs).
ม਺෼཭
app([X|Xs],Ys,[X|Zs])
app([X1|X1s],Y1s,[X1|Z1s])
:-app(Xs,Ys,Zs).
:- app(X1s,Y1s,Z1s).
В 1={ X1=X, X1s=[], Y1s=[b,c],
Res=[X|Z1s]}
?- app([],[b,c],Z1s)
app([],Xs,Xs).
ม਺෼཭ɿ app([],X2s,X2s).
В 2={ X2s=[b,c], Z1s = [b,c] }
˘
7
θ = θ1 . . . θk Λղ୅ೖͱ‫Ϳݺ‬
{X1=X, X1s=[], Y1s=[b,c], Res=[X|[b,c]],
X2s=[b,c], Z1s = [b,c]}
ಛʹɺτοϓΰʔϧதͷม਺ʢ͜ͷ৔߹ X, Resʣʹ੍‫͠ݶ‬
ͨ΋ͷ͕࠷ऴతͳ౴͑ͱͯ͠දࣔ͞ΕΔ
Res = [X|[b,c]] = [X,b,c], X=X
8
3.3
3.4
ࢉज़ࣜ̍ɿ ਺ྻ
ࢉज़ࣜ̎ɿ ‫܁‬ฦ͠Λ༻͍ͨ਺ྻ
खଓ͖‫Ͱޠݴܕ‬͸ while จͳͲΛ࢖͏
X is t ʢX ͸ม਺ɼt ͸ࢉज़ࣜʣ΋ਖ਼Ϧςϥϧ
ྫɿ X is Y2*Z+.
ॳ‫ظ‬஋ (1 = a0 , 1 = a1 , 1)
”is” Ϧςϥϧ͕બ୒͞ΕΔͱɼ
ӈลͷ஋ v Λ‫ٻ‬Ίɼ୯ҰԽɿ X = v
repeat
(v1 = an−1 , v = an , n)
⇓
(an = v, an+1 = v1 + v, n + 1)
until x = n
ϑΟϘφον਺ྻɿ a0 = a1 = 1, an = an−1 + an−2
Լ‫ه‬ϓϩάϥϜ͸ɼ਺ྻͷఆٛͦͷ΋ͷ
f(0,1).
f(1,1).
f(X,Y) :- N1 is X-1, f(N1,R1),
N2 is X-2, f(N2,R2), Y is R1+R2.
?- f(2,Y).
?- N1 is 2-1, f(N1,R1), N2 is 2-2, f(N2,R2), Y is R1+R2.
with N1=1
?- f(1,R1), N2 is 2-2, f(N2,R2), Y is R1+R2.
with R1=1
?- N2 is 2-2, f(N2,R2), Y is 1+R2.
with N2=0
?- f(0,R2), Y is 1+R2.
with R2=1
?- Y is 1+1.
with Y = 2
˘
୅ೖͷ߹੒ɿ N1=1, R1=1, N2=0, R2=1, Y=2
top level query ʹ੍‫ͨ͠ݶ‬ղ୅ೖɿ Y=2.
9
f(0,1).
f(1,1).
f(X,R)
:- X > 1, g(1,1,1,X,R).
g(R2,R1,N1,X,R)
:- N1 = X, R=R1.
g(R2,R1,N1,X,R)
:- N1 < X, NN1 is N1+1,
NR1 is R2+R1,
g(R1,NR1,NN1,X,R).
?-f(4,R).
?-g(1,1,1,4,R).
...
?-g(1,2,2,4,R).
...
?-g(2,3,3,4,R).
...
?-g(3,5,4,4,R).
˘
R=5
static int fib(int x) {
if (x==0 || x==1) return 1;
int vnminus1 = 1, vn = 2, n = 2;
while (n != x) {
int tmp=vnminus1;
vnminus1 = vn;
vn = tmp+vn;
n++;
};
return vn;
}
ஸ౓ɼwhile จͷதؒม਺͕ɼ
ड़‫ޠ‬ͷҾ਺ʹରԠ
ʢྫɿ v1 ͸ g ͷୈ̍Ҿ਺ʣ
தؒม਺ͷ஋Λɼड़‫ޠ‬ͷҾ਺ʹ‫ݱ‬
ΕΔ஋ͱͯ͠อ͍࣋ͯ͠Δɽ
10
3.5
બ୒ʹؔ͢Δ໿ଋࣄ ʵ Prolog ͷ৔߹
3.6
όοΫτϥοΫͱࣦഊʹΑΔ൱ఆʢෛϦςϥϧͷॲཧʣ
̍ɽϧʔϧͷબ୒͸ॻ͔Εͨॱʹɼ
̎ɽΰʔϧઅதͷϦςϥϧͷબ୒΋ࠨ͔Βӈ΁
ࣦഊΰʔϧઅ ˔
̏ɽ݁‫ہ‬ɼΰʔϧઅͷ࠷ࠨϦςϥϧͱ
Ͳͷϧʔϧ΋ద༻ෆೳ
୯ҰԽՄೳͳ࠷ॳͷϧʔϧ͕બ୒
ʢΰʔϧઅதͷʢ࠷ࠨʣϦςϥϧ͕
࠶ࢼߦͷࡍ͸ɼ୯ҐԽՄೳͳϧʔϧΛॱ࣍બ୒
Ͳͷϧʔϧͷϔουͱ΋୯ҰԽͰ͖ͳ͍ʣ
? − A ͔Βͷ‫͕ࢉܭ‬ແ‫ݶ‬ϧʔϓʹؕΔ৔߹΋
࠶ࢼߦͱόοΫτϥοΫͷҰൠ࿦
ࢼߦ͢΂͖ϧʔϧ͕࢒͍ͬͯΔ‫ݶ‬Γ࠶ࢼߦ
edge(a,b). edge(b,c)
path(X,Y) :- edge(X,Y).
path(X,Y) :- edge(X,Z),
path(Z,Y).
path(X,Y) :- path(Z,Y), edge(X,Z).
path(X,Y) :- edge(X,Y).
࢒Γͷϧʔϧ͕ͳ͍ͱ͖ɼ਌ΰʔϧઅʹ໭Δ
ෛϦςϥϧ \ + A ͷॲཧ
?-path(a,c).
?-path(Z,c),edge(a,Z).
?-path(Z1,c),edge(Z,Z1), edge(a,Z).
?-path(Z2,c),edge(Z1,Z2),
edge(Z,Z1), edge(a,Z).
...
?-path(a,c).
?-edge(a,Z),path(Z,Y).
?-path(b,c).
?-edge(b,c).
˘
...
ΰʔϧઅ ? − \ + A , A2 , ..., An
? − A Λτοϓΰʔϧʹηοτ
? − A ͕༗‫ࣦݶ‬ഊ ˱ def ˘ʹࢸΔύεΛ‫ͣ·ؚ‬ɼ
ແ‫ݶ‬ͷύε͕ଘࡏ͠ͳ͍
?−A ͕ ༗‫ࣦݶ‬ഊ ˰ \ + A ͸੒ޭ
࣍ͷΰʔϧઅ A2 , ..., An ɽ(୅ೖ͸ۭ୅ೖ)
? − A ͕੒ޭʢ˘Ͱऴྃʣ ˰ \ + A ͸ࣦഊ͠
Ұͭલͷΰʔϧ΁
11
12
3.7
4
ෛϦςϥϧͷॲཧɿ ྫ
like(a,b). like(b,a). like(a,c).
p(a). p(b).
like(X,X). // X likes X, p(X): X is a person
dislike(X,Y) :- p(Y), \+ X=Y, \+ like(X,Y)
// X ʹର͠ Y Λ‫ٻ‬ΊΔࡍ͸ɼ
// p(Y) Ͱ Y Λఆ਺Խͨ͠‫ʹޙ‬ෛϦςϥϧΛ࣮ߦ
?- dislike(b,Y).
?- p(Y), \+Y=b, \+ like(b,Y)
p(a), \+a=b
?- \+ like(b,a)
࠶ࢼߦ
p(b),
p(c).
?-dislike(a,Y)
?-\+ like(a,Y)
?-like(a,Y) ͸੒ޭ
ෛϦςϥϧͷ࠶ࢼߦ͸Ͱ͖ͳ͍
dislike(a,Y) ͸༗‫ࣦݶ‬ഊ
4.1
ྫ̍ɿ ൓సϓϩάϥϜ̍
rev([],[]).
rev([X|Xs],Zs) :- rev(Xs,Ws),
app(Ws,[X],Zs).
app([],X,X).
app([X|Xs],Ys,[X|Zs]) :- app(Xs,Ys,Zs).
࠶ࢼߦ
b=b
p(c), \+c=b
?- \+ like(b,c)
˘ Y=c ͕౴͑
൱ఆड़‫ޠ‬ͷ࣮ߦͷલʹ Πϯελϯε ?-dislike(c,Y)
Խ͠ͳ͍ͱͲ͏ͳΔ͔ɽ
ɽ
ɽ
ྫ୊
?-\+ like(c,Y)
?- like(c,Y) ͸༗‫ࣦݶ‬ഊ
Y ΁ͷ୅ೖ͸ͳ͠
˘ ʢ੒ޭʣ
?- rev([a,b],Res)
?- rev([b],W), app(W,[a],Res).
?- rev([],W1), app(W1,[b],W), app(W,[a],Res).
W1 = []
?- app([],[b],W), app(W,[a],Res).
W = [b]
?- app([b],[a],Res).
Res = [b|Res1]
?- app([],[a],Res1).
Res1 = [a]
˘
୅ೖͷ߹੒Λߦ͍ɺ
Res = [b|[a]]ɺͭ·ΓɺRes = [b,a] ͕౴͑
13
14
4.2
4.3
ྫ̎ɿ ൓సϓϩάϥϜ̎
append Λ࢖Θͳ͍όʔδϣϯ
ࠨ͔ΒॱʹཁૉΛநग़͠ͳ͕Β
‫ॱٯ‬ͷϦετΛ࡞Δ
ิॿม਺ Acc ͷ࢖༻
ߟ͑ํ͸ ਺ྻྫ̎ Ͱࣔͨ͠΋ͷ
ͱಉ͡
Acc
ೖྗ
-----------------------[a1,a2,a3,...,a9]
[]
[a2,a3,...,a9]
[a1]
[a3,...,a9]
[a2,a1]
...
[a9]
[a8,...,a2,a1]
[] [a9,a8,,...,a2,a1]
----------------------ೖྗ͕ [] ͷͱ͖ͷ Acc ͕౴͑
rev(Xs,Ys) :- auxrev(Xs,[],Ys).
auxrev([],Acc,Acc).
auxrev([X|Xs],Acc,Ys) :- auxrev(Xs,[X|Acc],Ys).
?- rev([a,b],Ys)
?-auxrev([a,b],[],Ys).
?-auxrev([b],[a],Ys).
?-auxrev([],[b,a],Ys).
Ys = [b,a]
˘
ྫ̏ɿ ϋϊΠͷౝ
ϙʔϧ̿̍ʹ̽ຕͷԁ൫͕େ͖ͳॱʹੵ·Ε͍ͯΔʢਤͰ͸ ̽ = ̏ʣɻ̿̍
ͷશͯͷԁ൫Λɺϙʔϧ̿̎Λ࢖ͬͯϙʔϧ̿̏ʹҠ͠ͳ͍͞ɻͦͷࡍɺ
େ͖ͳԁ൫Λখ͞ͳԁ൫ͷ্ʹஔ͍ͯ͸͍͚·ͤΜɻ
[pi,pj] : ʰϙʔϧ ̿ i ͷҰ൪্ʹ͋Δԁ൫Λ ϙʔ
ϧ ̿ j ʹҠಈͤ͞Δʱૢ࡞
Ұ࿈ͷҠಈૢ࡞ΛϦετͰද‫ه‬ɿ
p3 Λิॿͱͯ͠
p1 ͔Β̎ຕΛ p2 ΁
ͦͷ‫ޙ‬ɺ࠷େԁ൫Λ
p3 ΁Ҡಈ
p1 Λิॿͱͯ͠ɺ
̎ຕΛ p3 ΁Ҡಈ
[[p1,p3],[p1,p2],[p3,p2]]
্‫ه‬͸ solve(2,p1,p2,Sol) ͷղ Sol
solve(ຕ਺, ࠷ॳͷϙʔϧ, ໨ඪϙʔϧ, ղ)
solve(1,Pole1,Pole2,[[Pole1,Pole2]]).
// 1 ຕ໰୊ͷͱ͖͸ɺ୯ʹҠಈͤ͞ΔͷΈɻ
solve(N,Spole,Tpole,Solution) :N > 1, N1 is N-1, // N > 1 ͸ద༻৚݅
ano_pole(Spole,Tpole,Wpole),
// ࡞‫༻ۀ‬ϙʔϧ Wpole
solve(N1,Spole,Wpole,Sub1),
BottomDisk = [Sploe,Tpole];
solve(N1,Wpole,Tpole,Sub2),
app(Sub1,[BottomDisk|Sub2],
Solution).
ิॿड़‫ͯ͠ͱޠ‬ɺϦετͷ࿈઀ appɺ͓Αͼ
ิॿϙʔϧʹؔ͢Δ‫ه‬ड़ ano_pole Λ༻͍Δɿ
ano_pole(p1,p2,p3).
ano_pole(p1,p3,p2).
ano_pole(p2,p1,p3).
ano_pole(p2,p3,p1).
ano_pole(p3,p1,p2).
ano_pole(p3,p2,p1).
15
16
4.4
4.5
ྫ̐ɿ ‫ܦ‬࿏୳ࡧ̍
b
༗޲άϥϑ̜ɿ ϊʔυͷू߹ V ͱ
Τοδͷू߹ E ⊆ V × V ͷର
(a, b) ∈ E ˱ a ͔Β b ΁ͷ޲͖
෇͖ͷล (Τοδ)
࢝఺͔Βऴ఺ʢ໨త஍ʣ·Ͱͷ‫ܦ‬࿏
(path) Λ‫ٻ‬ΊΔ
d
a
ॳ‫ظ‬ϊʔυ ͔Β ϊʔυ Node1 ʹ͍ͨΔதؒ࿏ Acc Λอ࣋
f
c
ྫ̑ɿ‫ܦ‬࿏୳ࡧ̎
adj(Node1, Inode) ͳΔ Inode ͕ Acc ্͔ΛνΣοΫ
νΣοΫʹ੒ޭ͢Ε͹, Inode Λ Acc ʹ௥Ճ
e
ड़‫ ޠ‬csearch(+Node1, +Node2, +Acc, -Path)
adj(a,b). adj(a,c). adj(b,c).
adj(b,d). adj(c,e). adj(e,f).
‫ܦ‬࿏ n1,...,nk ΛϦετ [n1,...,nk] Ͱද‫ݱ‬
Acc ʹ͜Ε·Ͱ๚Εͨ nodes Λ஝ੵ͓ͯ͘͠ɻ
search(Node1,Node2,Path)
:- csearch(Node1,Node2,[Node1],Path).
search(+Snode, +Target, -Path)
࠶‫ؼ‬తϓϩάϥϛϯά͸͜͜Ͱ΋༗ޮ
search(Node,Node,[Node]).
search(Node1,Node2, [Node1|Path])
:- adj(Node1,Inode),
search(Inode,Node2,Path).
ด࿏Λ‫ؚ‬Ή৔߹ɺແ‫ݸݶ‬ͷղ
adj(a,b). adj(b,c). adj(c,a).
͜ͷͱ͖ɺ
search(a,a,[a]).
search(a,a,[a,b,c,a]).
search(a,a,[a,b,c,a,b,c,a]).
....
17
csearch(Node,Node,Acc,[Node]).
csearch(Node1,Node2,Acc,[Node1|Path])
:- adj(Node1,Inode),
not_on(Inode,Acc),
csearch(Inode,Node2, [Inode|Acc],Path).
not_on(Inode,Acc):- \+ mem(Inode,Acc).
mem(Inode,[Inode|Nodes]).
mem(Inode,[Node|Nodes])
:- \+ Inode=Node,
mem(Inode,Nodes).
18
·ͨ͸
not_on(Inode,[]).
not_on(Inode,[Node|Nodes])
:- \+ Inode=Node,
not_on(Inode, Nodes).
5
એ‫ݴ‬తҙຯɼૢ࡞తҙຯ
5.1
એ‫ݴ‬తҙຯ࿦: ࠷খෆಈ఺Ϟσϧ
ૢ࡞తҙຯɿ ͲͷΑ͏ͳτοϓΰʔϧઅ͕ϓϩάϥϜͷԼ
Ͱ੒ޭ͢Δ͔ʢ˘અ΁ͷϦμΫγϣϯΛ͔࣋ͭʣʁ
એ‫ݴ‬తҙຯɿ
ϓϩάϥϜ̥ʹଐ͢Δશͯͷϧʔϧ A : −B1 , ..., Bn ʹ
ର͠ɼB1 , ..., Bn ͕ਖ਼͚͠Ε͹ɼA ΋ਖ਼͍͠ɽ
ʮਖ਼͠͞ʯ͸਺ཧ࿦ཧֶͰ͍͏ɼ
ʮϞσϧʯɼ
ʮ࿦ཧత‫݁ؼ‬ʯ
ͱͯ͠ਖ਼֬ʹఆٛ͞ΕΔ͕ɼຊߨͰ͸ɼಛผͳϞσϧͰ
͋Δ࠷খෆಈ఺Ϟσϧʹ‫ݶ‬ఆͯ͠࿦͡Δ
݈શੑɿ੒ޭ͢Δΰʔϧ͸ਖ਼͍͠ʢ࠷খෆಈ఺Ϟσϧʹଐ
͢Δʣ
‫׬‬શੑ (*)ɿ ਖ਼͍͠΋ͷ͸ɺϓϩάϥϜͷԼͰ੒ޭ͢Δʢۭ
અΛಋग़Ͱ͖Δʣ
࡞༻ૉ TP : 2GA → 2GA , GA: ‫ج‬ఈΞτϜશମɻ
(*) ೖྗ͔Βग़ྗΛ‫ٻ‬ΊΔϓϩάϥϜͷ‫׬‬શੑ΋ɼ‫ޙ‬ड़͢Δʮlifting lemmaʯΛ༻͍Ε͹ɼ௚ͪʹಘΒ
ΕΔɽ
}
TP (A) = {α ∈ GA | ∃ θ s.t. (A : −B1 , ..., Bn ) ∈ P,
α ≡ Aθ, {B1 θ, ..., Bn θ} ⊆ A
TP ↑ (0) = φ, TP ↑ (n + 1) = TP (TP ↑ (n))
୯ௐੑ TP ↑ (n) ⊆ TP ↑ (n + 1) ΑΓ ू߹ྻͷ‫͕ݶۃ‬ଘࡏɿ
∞
TP ↑ (ω) = ∪ TP ↑ (n)
n=0
ਖ਼͍͠΋ͷɿ α ∈ TP ↑ (ω)
ਖ਼͘͠ͳ͍΋ͷɿ α ∈
/ TP ↑ (ω)
19
20
5.2
5.3
൓ള๏ͷ݈શੑ
ม਺Λ‫͍ͳ·ؚ‬ΞτϜ α = p(t1 , ..., tk ) ʹର͠ɼ
‫׬‬શੑ̍ɿ ม਺Λ‫͍ͳ·ؚ‬ΰʔϧ
∞
? − α ͔Β˘͕ಋग़͞ΕΔ ˰ α ∈ TP ↑ (ω).
?- r(a,b).
r(X1,X2) :p(X1,X3),
q(X3,X2).
X1=a, X2=b.
?-p(a,X3), q(X3,b). ൓ ള த
ͷม਺
p(a,Y1).
Λղ୅
X3=Y1
ೖʹΑ
?-q(Y1,b).
ΓҰ੪
ʹ۩ମ
q(Z1,b).
Խ
Y1=Z1.
˘
ղ୅ೖ X1=a, X2=b,
X3=Y1=Z1
˰
?- r(a,b).
r(a,b) :p(a,Z1),
q(Z1,b).
?-p(a,Z1), q(Z1,b).
p(a,Z1).
?-q(Z1,b).
࢒Γͷ
q(Z1,b).
ม਺Λ
˘
ద౰ʹ
˰
্‫ه‬ͷ SLD-ಋग़͸ɼ୯
ҰԽͷඞཁ͕ͳ͍ʢͭ
·Γɼղ୅ೖ͕ۭ୅ೖʣ
͜ͱʹ஫ҙɽ
·ͨҰൠʹɼඇ‫ج‬ఈ߲
͕ग़‫͢ݱ‬Δ͜ͱ΋͋Γ
ఆ਺Խ
͢Δ
Z1=c
൓ള๏ͷ‫׬‬શੑ
α = p(t1 , ..., tn ) ∈ TP ↑ (ω) = ∪ TP ↑ (n)
n=1
˰ ? − α ͔Βۭઅ ˘ ΁ͷ SLD ൓ള͕ଘࡏ͢Δ
‫׬‬શੑ̎ɿ Aθ = α ∈ TP ↑ (ω) ˰ ? − A ͔Βͷ ղ୅ೖ τ
?- r(a,b).
r(a,b) :p(a,c),
q(c,b).
?-p(a,c), q(c,b)
p(a,c).
?-q(c,b).
q(c,b).
˘
q(c,b) ∈ Tp ↑ (1).
p(a,c) ∈ Tp ↑ (1).
r(a, b) ∈ Tp ↑ (2).
Λ࣋ͭ SLD ൓ളͱ͋Δ୅ೖ ρ ͕ଘࡏ͠ɼτοϓΰʔϧ A
தͷ೚ҙͷม਺ X ʹର͠ɼXθ = Xτ ρ ͕੒ཱ
஫ҙɿ ൓ളͷʮࠨଆʯʹແ‫ݶ‬ύε͕ଘࡏ͢Δ৔߹΋͋Δɽ
p(X,Y):-q(Y,Z)
p(a,b):-q(b,c)
some n s.t. α ∈ TP ↑ (n) ͔ͩΒɼ໋୊Ϩ
ϕϧͷ൓ളΛߏ੒ɿ ‫ج‬ఈϧʔϧΛ༻͍ͨ
ΰʔϧϦμΫγϣϯ ̡
p(a,b)
໨ඪͱ͢ΔΰʔϧϦμΫγϣϯɿ ‫ج‬ఈԽ
͞Εͳ͍ϧʔϧΛ༻͍ͨϦμΫγϣϯ ̧ɽ
୯ҰԽͷ࠷൚ੑʹ஫ҙ͠ɼ
θ1 = θ ∪ {X = a, Y = b, Z = c}, V θ1 = b
θ1 = τ1 ρ1 . ಛʹɼ V θ1 = V τ1 ρ1
ρ1 = τ2 ρ2 .
‫ʹނ‬ɼ b = V θ1 = V τ1 ρ1 = V τ1 τ2 ρ2 = V τ ρ2
͑Δ
̡ͱಉ͡௕͞ͷ̧͕ߏ੒͞Εɼ̧ͷ࠷‫ޙ‬
ͷΰʔϧઅ͸ۭઅ ˘
Note: ‫ʹີݫ‬͸ϦμΫγϣϯͷ௕͞ʢஈ਺ʣʹؔ
͢Δ਺ֶత‫ؼ‬ೲ๏
‫ج‬ఈ୅ೖ θ1 , θ2 .
ม਺෼཭৚͔݅Β θ = θ1 ∪ θ2 ͱॻ͚Δ.
B1 θ = B1 θ1 = β1 = Aθ2 = Aθ
so mgu τ ʹରͯ͠ɼsome ρ s.t. τ ρ = θ
21
22
q(b,Z)
q(b,c)
6
ԋश໰୊
Q1: ࿦ཧϓϩάϥϜͷએ‫ݴ‬తҙຯͱૢ࡞తҙຯͱ͸ͲͷΑ͏ͳ΋ͷ͔Λ؆ܿʹड़΂Α
Q2: ༗޲άϥϑͷล͕ਖ਼ͷॏΈΛ࣋ͭͱ͖ʹɼ࢝఺͔Βऴ఺΁ͷ‫ܦ‬࿏ͱͦͷॏΈʢ֤ลͷॏ
Έ૯࿨ʣΛ‫ٻ‬ΊΔϓϩάϥϜΛॻ͖ɼͦͷ‫ࢉܭ‬աఔΛྫࣔ͠ͳ͍͞ɽ
Q3: Լ‫ه‬ͷ rev ͸ɼୈ 1 Ҿ਺ͷϦετʹରͯ͠ɼͲͷΑ͏ͳୈ 2 Ҿ਺ͷϦετΛฦ͔͢Λઆ
໌͠ͳ͍͞ɽ
list([]).
list([_|Xs]):- list(Xs).
app([],Y,Y). app([X|Xs],Ys,[X|Rs]):-app(Xs,Ys,Rs).
forElement(X,X):-atomic(X).
// atomic(X) ͸ఆ਺ͷͱ͖੒ޭɼͦΕҎ֎Ͱࣦഊ͢ΔγεςϜड़‫ޠ‬
forElement(X,R):-list(X), rev(X,R).
rev([],[]).
rev([X|Xs],Res):rev(Xs,RXs), forElement(X,RX), app(RXs,[RX],Res).
Q4. ޻৔ͷ੡඼ग़ՙঢ়‫ؔ͢ʹگ‬Δখ໰ (1),(2) ͷϧʔϧΛॻ͖ɼԼ‫ه‬ͷσʔλΛ༩͑ͨͱ͖ͷ
ಈ࡞Λઆ໌͠ͳ͍͞ɽͨͩ͠ɼship(X,Y) ͸ʰ޻৔ X ͸੡඼Y Λग़ՙʱΛද͢ɽ
factory(a). factory(b). factory(c).
product(x). product(y). product(z).
ship(a,y). ship(b,y). ship(b,z),
ship(c,x). ship(c,y). ship(c,z).
factory(d).
(1) Ͳͷ੡඼΋ग़ՙ͍ͯ͠ͳ͍޻৔Λ‫ٻ‬ΊΔϧʔϧ
(2) શͯͷ੡඼Λग़ՙ͍ͯ͠Δ޻৔Λ‫ٻ‬ΊΔϧʔϧ
23