2015年度情報論理学講義資料

2015 年度情報論理学講義資料 (4)
青戸等人
1
単一化と単一化手続き
照合問題では，左辺に代入して右辺を得らえるかという問題を考えた．左辺だけ
ではなく，右辺にも代入をして，同じ項を得ることができるかという問題を単一化
問題という．単一化手続きは，述語論理の自動定理証明や合流性検証手続きの基本
的な構成要素となっている．
定義 1 (単一化) 項 s と項 t が単一化可能 (unifiable) であるとは， sσ = tσ となるよ
うな代入 σ が存在するときをいう．このような代入 σ を， s と t の単一化子 (unifier)
とよぶ．
例 2 単一化のさまざまな例を示す．
• s = f(x, b) と t = f(g(a), y) とおくと， s と t は単一化可能．代入 σ = {x :=
g(a), y := b} は s と t の単一化子．実際， sσ = tσ = f(g(a), b)．
• f(x, a) と f(g(y), y) は単一化可能． {x := g(a), y := a} は単一化子．同じ変数が
複数出現する場合に注意．
• f(x, a) と f(y, x) は単一化可能． {x := a, y := a} は単一化子．同じ変数が両方
の項に出現する場合に注意．
• g(x) と g(y) は単一化可能．以下の代入はすべて単一化子． σ1 = {x := y}，
σ2 = {y := x}， σ3 = {x := z, y := z}， σ4 = {x := a, y := a}， σ5 = {x :=
g(a), y := g(a)}， . . .．つまり，単一化子は一般的には複数ある．
• f(x, x) と f(a, b) は単一化不能．第 1 引数を同じにするには，代入に x := a が
必要だが，そうすると，第 2 引数が同じにならない．
• f(x, y) と g(z) は単一化不能．代入によって， f や g は不変なので，どんな代入
σ をとっても， f(x, y)σ 6= g(x, y)σ ．
• g(y) と g(g(y)) は単一化不能．代入 σ = {y := g(y)} は単一化子にならないこ
とに注意．
単一化子は一般に複数あるが，そのうち，最も一般的なもの (最汎単一化子) が存
在する．最汎単一化子を与える準備として，まず，代入順序について説明する．
1
def
定義 3 (代入順序) 代入集合上の関係 - を次のように定める： σ - τ ⇐⇒ ∃ρ. ρ ◦ σ =
τ．
def
代入の合成の定義： (ρ ◦ σ)(x) ⇐⇒ ρ(σ(x)) に注意しておく 1 ．
補題 4 関係 - は擬順序 (反射的かつ推移的な関係)．
直観的には， σ - τ は， τ より σ の方が一般的な代入であることを表わしている．
例 5 以下が成立する．
• {x := f(y)} - {x := f(a), y := a}．なぜなら， {x := f(a), y := a} = {y :=
a} ◦ {x := f(y)}．
• {x := y} - {y := x}， {y := x} - {x := y}．なぜなら， {y := x} = {y :=
x} ◦ {x := y}， {x := y} = {x := y} ◦ {y := x}．
• {x := y} - {x := z, y := z}， {y := x} - {x := z, y := z}．なぜなら，
{x := z, y := z} = {y := z}◦{x := y}， {x := z, y := z} = {x := z}◦{y := x}．
定義 6 (最汎単一化子) 代入 σ が項 s と t の最汎単一化子 (most general unifier) で
あるとは， (1) σ は s と t の単一化子，かつ， (2) s と t の任意の単一化子 ρ について
σ<
∼ ρ が成立する，ときをいう．項 s と t の最汎単一化子 (の 1 つ ) を， mgu(s, t) を
記す 2 ．
例 7 g(x) と g(y) の単一化子は， {x := y}， {y := x}， {x := t, y := t} (t ∈
/ {x, y})
となる．このとき， {x := y} と {y := x} は， g(x) と g(y) の最汎単一化子． {x :=
t, y := t} (t ∈
/ {x, y}) は，最汎ではない単一化子となる．
2 つの項 s, t が与えられたときに， s と t が単一化可能であるか否かを判定する問
題を単一化問題とよび， s ? ≈? t により表す．以下では， s ? ≈? t と t ? ≈? s を同一視
する．
単一化問題を E = {s1 ? ≈? t1 , . . . , sn ? ≈? tn } のように有限集合へ一般化する．こ
のとき， E の単一化子とは， i = 1, . . . , n について si σ = ti σ となる代入 σ のことで
あり， E の単一化子 σ で， E の任意の単一化子 ρ について σ <
∼ ρ となるものを単一
化問題 E の解とよぶ．
以下では，単一化問題を解く手続き (単一化手続き ) を，導出規則で与える (図 1)．
この手続きは，単一化問題 E と代入 σ の対 hE, σi に関する導出を行いながら問題
def
これは数学の世界では標準的な代入の合成の定義．一方，計算機科学の世界では， (ρ ◦ σ)(x) ⇐⇒
σ(ρ(x)) とする場合もときどき見かける．このような左を先に適用する関数合成には，記号 “◦” でな
1
def
く，記号 “;” を用いることを推奨する： (ρ; σ)(x) ⇐⇒ σ(ρ(x))．これは， “;” はプログラムの statement
の合成の標準的な記法であるので，この順番は直観に合う．
2
すぐ次の例で示すように，最汎単一化子は 1 つとは限らないが，どの最汎単一化子であっても，
最汎であるという性質からそのうち 1 つを考えれば十分である．このため，唯一に定まるかのように
mgu(s, t) を記しても問題ない．
2
Delete
h{x ? ≈? x} ⊎ E, σi
hE, σi
Decompose
h{f (s1 , . . . , sn ) ? ≈? f (t1 , . . . , tn )} ⊎ E, σi
h{s1 ? ≈? t1 , . . . , sn ? ≈? tn } ∪ E, σi
Eliminate
Crash
Occur-Check
h{x ? ≈? t} ⊎ E, σi
h{x := t}(E), {x := t} ◦ σi
x∈
/ V(t)
h{f (s1 , . . . , sn ) ? ≈? g(t1 , . . . , tm )} ⊎ E, σi
⊥
h{x ? ≈? t} ⊎ E, σi
⊥
f 6= g
x ∈ V(t), x 6= t
図 1: 単一化手続き
を解く．導出規則は，上の式を下の式へ変形する，と読むように記述されている．
X ⊎ Y は直和集合 (disjoint union，積集合が空 (X ∩ Y = ∅) となる和集合 X ∪ Y ) を
表わす．なお， s ? ≈? t と t ? ≈? x は同一視されるので，例えば， Eliminate 規則は対
hE ⊎ {t ? ≈? x}, σi についても適用されることに注意する． hE, σi から hF, ρi (もし
くは hE, σi から ⊥) がこれらの規則で導出されることを hE, σi ❀ hF, ρi (もしくは
hE, σi ❀ ⊥) と記す．直観的には， E はまだ残っている単一化問題， σ はこれまで
解いた部分解を表わす．単一化できないことが判明した場合には ⊥ が導出される．
単一化問題 s ? ≈? t を解くには， h{s ? ≈? t}, ∅i から導出を始めて，導出が ⊥ で終
わった場合には解は単一化不能であり， h∅, σi で終わった場合は単一化可能となる．
このとき， σ は，単一化問題の解 (実際には最汎単一化子) となる．
定義 8 (単一化手続き )
入力：単一化問題 s ? ≈? t
出力：項 s と項 t が単一化可能か否か，単一化可能な場合にはその最汎単一化子
h{s ? ≈? t}, ∅i から図 1 の導出規則による導出を可能な限り繰り返す． ⊥ が得られた
場合は，単一化不能を返す．また， h∅, σi が得られた場合は， σ を最汎単一化子とし
て返す．
例9
• h{f(x, b) ? ≈? f(g(a), y)}, ∅i ❀ h{x ? ≈? g(a), b ? ≈? y)}, ∅i ❀ h{b ? ≈? y}, {x :=
g(a)}i ❀ h{y ? ≈? b}, {x := g(a)}i ❀ h∅, {x := g(a), y := b)}i．
• h{h(a, y, x) ? ≈? h(a, y, c)}, ∅i ❀ h{a ? ≈? a, y ? ≈? y, x ? ≈? c}, ∅i ❀ h{y ? ≈?
y, x ? ≈? c}, ∅i ❀ h{x ? ≈? c}, ∅i ❀ h∅, {x := c}i．
3
• h{f(x, x) ? ≈? f(a, b)}, ∅i ❀ h{x ? ≈? a, x ? ≈? b}, ∅i ❀ h{a ? ≈? b}, {x := a}i ❀
⊥．
定理 10 (単一化手続きの正しさ ) 項 s と t が単一化可能なとき，その時にかぎり，
単一化手続きは s と t の最汎単一化子を返す．
演習 11 単一化手続きの正しさについて，付録の証明を確認せよ．
代入に関するデータ型や関数をおく Subst ストラクチャに，関数の合成をする
compose 関数および単一化手続きを実現する unify 関数を追加しよう． compose σ ρ
は， ρ ◦ σ を表わす代入を返す． unify (s,t) は s と t が単一化可能なとき SOME σ (σ
は s と t の最汎単一化子) を返し，単一化不能な場合には NONE を返す． unify 関数本
体の let 文のなかの main 関数が，導出規則を適用して導出を繰り返す部分であり，
第 1 引数が E に部分，第 2 引数が σ に部分に対応する．導出規則で ⊥ が得られると
ころでは， NONE を返し，単一化に成功するときは最終的に E が空リストとなり， 19
行目で SOME σ が返される．
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(* subst.sml *)
signature SUBST =
sig
type subst
...
val compose: subst -> subst -> subst
val unify: Term.term * Term.term -> subst option
end
structure Subst: SUBST =
struct
local
structure AL = AssocList
structure L = List
structure LP = ListPair
structure T = Term
in
type subst = (Var.key * Term.term) list
...
19
20
21
(* composition of substitutions: rho o sigma *)
fun compose sigma rho = ...
22
23
24
25
26
27
28
29
30
fun unify (term1,term2) =
let fun main [] sigma = SOME sigma
| main ((T.Var x, t)::rest) sigma =
...
...
...
| main ((T.Fun (f,ts), T.Fun (g,us))::rest) sigma =
...
4
31
32
33
34
35
36
37
...
...
| main ((t, T.Var x)::rest) sigma =
rest) sigma
in main [(term1,term2)] []
end
end (* of local *)
end
main ((T.Var x, t)::
演習 12 関数 compose および unify を完成させよ．
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
(* 実行例 *)
# Subst.unify (T.fromString "f(?x,b)", T.fromString "f(g(a),?y)");
val it = _ : ((string * int) * Term.term) list option
# Subst.toString (valOf it);
val it = "{?x := g(a), ?y := b}" : string
# Subst.unify (T.fromString "f(?x,a)", T.fromString "f(g(?y),?y)");
val it = _ : ((string * int) * Term.term) list option
# Subst.toString (valOf it);
val it = "{?x := g(a), ?y := a}" : string
# Subst.unify (T.fromString "f(?x,a)", T.fromString "f(?y,?x)");
val it = _ : ((string * int) * Term.term) list option
# Subst.toString (valOf it);
val it = "{?x := a, ?y := a}" : string
# Subst.unify (T.fromString "f(?x)", T.fromString "f(?y)");
val it = _ : ((string * int) * Term.term) list option
# Subst.toString (valOf it);
val it = "{?x := ?y}" : string
# Subst.unify (T.fromString "f(?x,?x)", T.fromString "f(a,b)");
val it = _ : ((string * int) * Term.term) list option
# isSome it;
val it = false : bool
# Subst.unify (T.fromString "f(?x)", T.fromString "g(?y)");
val it = _ : ((string * int) * Term.term) list option
# isSome it;
val it = false : bool
# Subst.unify (T.fromString "g(?y)", T.fromString "g(g(?y))");
val it = _ : ((string * int) * Term.term) list option
# isSome it;
val it = false : bool
ここでは，代入を文字列に変換する Subst.toString 関数を用意して使っている．
5
2
危険対と危険対補題
加算の書き換え規則
R=
(
+(0, y)
→ y
+(s(x), y) → s(+(x, y))
)
による項 +(s(x), +(0, y)) の書き換えを考えてみよう．この項には，書き換え可能な
位置が 2 箇所存在する．このため，次のように， 2 通りの書き換えが可能：
s(+(x, +(0, y))) R ← +(s(x), +(0, y)) →R +(s(x), y)
この場合，片方の書き換えによって，もう一方の書き換えが出来なくなることはな
いため，
s(+(x, +(0, y))) →R s(+(x, y)) R ← +(s(x), y)
のように， 2 通りの書き換えのどちらを先にやっても最終的に同じ計算結果が得ら
れる．しかし，このような場合ばかりではない．
例 13 次のように，加算の書き換え規則に結合律の規則を追加してみよう：




+(0, y)
→ y
 (1)

′
R =
(2)
+(s(x), y)
→ s(+(x, y))


 (3)
+(x, +(y, z)) → +(+(x, y), z) 
今度は，
+(+(x, 0), y) R′ ← +(x, +(0, y)) →R′ +(x, y)
となり，片方の書き換えを行うと，対応する他方の書き換えが出来なくなってしまっ
ている．実際，得られた 2 つの項はさらに書き換えることが出来ない (つまり，正規
形になっている )．従って，どちらの書き換えを行うかによって，計算結果が異なっ
てしまう．このような状況は， 2 つの書き換え規則 (2) と (3) が “重なっている ” こと
に起因している．
このように，非決定的な計算においては，異なる計算順序を使っても同じ計算結果
が得られるかは自明ではない．どのような計算順序を使っても同じ計算結果が得られ
るという性質は，合流性 (confluence) もしくはチャーチ・ロッサー性 (Church-Rosser
property, CR と略す ) とよばれ，項書き換えシステムに基づく定理自動証明に重要な
役割を果たす．合流性の解析に重要となるのが，書き換え規則の重なりであり，こ
れは単一化によって計算することができる．
定義 14 (重なり ) l1 → r1 と l2 → r2 を書き換え規則とし，一般性を失うことなく，
l1 → r1 と l2 → r2 に用いられている変数は名前替えを行って別々になっているもの
とする (つまり， V(l1 ) ∩ V(l2 ) = ∅)．また， l1 → r1 と l2 → r2 は同じ書き換え規則
をとってきてもよいが，その場合も用いられている変数は別々となるように変える
ものとする．このとき，項 l2 のある非変数部分項 l2 |p と l1 が単一化可能であるとき，
位置 p で l1 → r1 は l2 → r2 へ重なるといい，この重なりを l1 → r1 >p l2 → r2 と記
す．ただし， l1 → r1 と l2 → r2 が (変数名だけが異なる ) 同じ書き換え規則で， p = ε
のときは (自明に ) 単一化可能となるので，その場合は除外するものとする．
6
例 15 例 13 の項書き換えシステム R′ の書き換え規則 (1)∼ (3) を考える．このとき，
以下の 7 つの重なりがある．
• l1 → r1 = (1)， l2 → r2 = (3)， p = ǫ ととると， mgu(+(x′ , +(y ′ , z ′ )), +(0, y)) =
{x′ := 0, y := +(y ′ , z ′ )} となるので，位置 ǫ で書き換え規則 (1) は書き換え規
則 (3) へ重なる．同様に，位置 ǫ で書き換え規則 (3) は書き換え規則 (1) へ重
なる．
• l1 → r1 = (1)， l2 → r2 = (3)， p = 2 ととると， mgu(+(y ′ , z ′ ), +(0, y)) =
{y ′ := 0, z ′ := y} となるので，位置 2 で書き換え規則 (1) は書き換え規則 (3) へ
重なる．
• l1 → r1 = (2)， l2 → r2 = (3)， p = ǫ ととると， mgu(+(x′ , +(y ′ , z ′ )), +(s(x), y)) =
{x′ := s(x), y := +(y ′ , z ′ )} となるので，位置 ǫ で書き換え規則 (1) は書き換え
規則 (3) へ重なる．同様に，位置 ǫ で書き換え規則 (1) は書き換え規則 (3) へ重
なる．
• l1 → r1 = (2)， l2 → r2 = (3)， p = 2 ととると， mgu(+(y ′ , z ′ ), +(s(x), y)) =
{y ′ := s(x), z ′ := y} となるので，位置 2 で書き換え規則 (1) は書き換え規則 (3)
へ重なる．
• l1 → r1 = (3)， l2 → r2 = (3)， p = 2 ととると， mgu(+(y ′ , z ′ ), +(x, +(y, z))) =
{y ′ := x, z ′ := +(y, z)} となるので，位置 2 で書き換え規則 (3) は書き換え規
則 (3) へ重なる．
定義 16 (危険頂，危険対) R を項書き換えシステム， l1 → r1 , l2 → r2 ∈ R，位置
p で l1 → r1 が l2 → r2 へ重なるとする 3 ． σ = mgu(l2 |p , l1 ) とおくとき， l2 [r1 ]p σ ←
l2 σ → r2 σ を危険頂 (critical peak) とよぶ．項の対 hl2 [r1 ]p σ, r2 σi を危険対 (critical
pair) とよぶ． l1 → r1 の l2 → r2 へ重なり l1 → r1 >p l2 → r2 から得られる危険頂の
集合を CPK(l1 → r1 , l2 → r2 )，危険対の集合を CP(l1 → r1 , l2 → r2 ) と記す． R を
任意の 2 つの書き換え規則の重なりから得られる危険頂の集合を CPK(R)，危険対
の集合を CP(R) と記す．
例























17 例 13 の項書き換えシステム R′ を考える．このとき， CPK(R) =
(1) >ǫ (3) :
+(y ′ , z ′ )
(3) >ǫ (1) :
+(+(0, y ′ ), z ′ )
(1) >2 (3) :
+(x′ , y)
(2) >ǫ (3) :
s(+(x, +(y ′ , z ′ ))
(3) >ǫ (2) :
+(+(s(x), y ′ ), z ′ )
(2) >2 (3) :
+(+(x′ , s(x)), y)
(3) >2 (3) : +(x′ , +(+(y ′ , y), z))
←
+(0, +(y ′ , z ′ ))
←
+(0, +(y ′ , z ′ ))
←
+(x′ , +(0, y))
←
+(s(x), +(y ′ , z ′ ))
←
+(s(x), +(y ′ , z ′ ))
←
+(x′ , +(s(x), y))
← +(x′ , +(y ′ , +(y, z)))
→
→
→
→
→
→
→
+(+(0, y ′ ), z ′ )
+(y ′ , z ′ )
+(+(x′ , 0), y)
+(+(s(x), y ′ ), z ′ )
s(+(x, +(y ′ , z ′ ))
+(x′ , s(+(x, y)))
+(+(x′ , y ′ ), +(y, z))
(重なりのときに述べたように，変数は重なりがないように名前替えされていることに注意．ま
た， l1 → r1 と l2 → r2 は (変数名を変えた ) 同じ書き換え規則でもよいが，そのときは p = ǫ の場合
は除外されていることに注意．
3
7

























(1) >ǫ (3) :
h+(y ′ , z ′ ),




(3) >ǫ (1) :
h+(+(0, y ′ ), z ′ ),





h+(x′ , y),
 (1) >2 (3) :
CP(R) =
(2) >ǫ (3) :
hs(+(x, +(y ′ , z ′ )),



(3) >ǫ (2) :
h+(+(s(x), y ′ ), z ′ ),





(2) >2 (3) :
h+(+(x′ , s(x)), y),


 (3) > (3) : h+(x′ , +(+(y ′ , y), z)),
2
+(+(0, y ′ ), z ′ )i
+(y ′ , z ′ )i
+(+(x′ , 0), y)i
+(+(s(x), y ′ ), z ′ )i
s(+(x, +(y ′ , z ′ ))i
+(x′ , s(+(x, y)))i
+(+(x′ , y ′ ), +(y, z))i























以下では，項 t の位置 p1 , . . . , pn の部分項を s1 , . . . , sn で置き換えて得られる項を
t[s1 , . . . , sn ]p1 ,...,pn と記す．
以下の補題は，書き換えが分岐するとき，その分岐が合流するケースと合流しな
いケースにおける危険頂との関係を示している．
補題 18 (危険対補題) R を項書き換えシステム， l1 → r1 , l2 → r2 ∈ R， t1 l1 →r1 ←
∗
→l1 →r1 ◦ →l2 →r2
s →l2 →r2 t2 とする．このとき，以下のいづれかが成立する． (1) t1 −
∗
∗
∗
◦ l1 →r1 ←
− t2 ， (2) t1 −
→l2 →r2 ◦ l1 →r1 ← ◦ l2 →r2 ←
− t2 ， (3) ある文脈 C ，代入 θ，および，
危険頂 v1 ← u → v2 ∈ CPK(l1 → r1 , l2 → r2 ) もしくは v2 ← u → v1 ∈ CPK(l2 →
r2 , l1 → r1 ) が存在して， t1 = C[v1 θ]， s = C[uθ]， t2 = C[v2 θ] が成立する．
合流性に関係する関数を置く Cr ストラクチャを cr.sml を用意し， cr.sml に危険頂
を計算する関数を作る．関数 cpkRule isIdentical (l1,r1) (l2,r2) は CPK(l1 →
r1 , l2 → r2 ) を計算する．ここで， isIdentical は l1 → r1 と l2 → r2 が同一の書き
換え規則かどうかを表わすブール値 (true または false) である．
関数 cpkRule は，まず， l2 の構造に関する再帰により， l2 |p (∈
/ V) と l1 が単一化可能
な箇所をすべて数え上げる．これを行っているのが，補助関数 cpkTerm である．具体
的には， l2 |p と l1 が単一化可能となるような p すべてについての，文脈 C = l2 []p と
σ = mgu(l2 |p , l1 ) の対をリストにして返す． cpkTerm t は， t の真部分項について出来
る [hC1 , σ1 i, . . . , hCn , σn i] に， t = l2 |p と l1 が単一化可能には h, σi を追加して返す．
前者についての再帰的な計算は， t = f (t1 , . . . , tn ) のとき， cpkTermList [ ] [t1 , . . . , tn ]
の形でよびだす． cpkTermList [t1 , . . . , ti−1 ] [ti , . . . , tn ] は， ti の部分項について出来
′
′
る [hC1′ , σ1′ i, . . . , hCm
, σm
i] を計算し，文脈 Cj′ を Cj′′ = [t1 , . . . , ti−1 , Cj′ , ti+1 , . . . , tn ] と
′′
′
いうリスト文脈に修正し， [hC1′′ , σ1′ i, . . . , hCm
, σm
i] を返す．
最後に，このようにして得られた文脈 C と σ から， C[r1 ]σ ← l1 σ ← r1 σ をそれぞ
れ計算すれば，すべての危険頂が得られる．
また， l1 → r1 と l2 → r2 が同一の書き換え規則の場合には，根位置での重なりを
再帰の一回目はスキップする必要がある．このため， cpkTermProper 関数を用意し
ている．また，書き換え規則 l1 → r1 と l2 → r2 に同じ変数がないように，変数の名
前替えをする関数 rename やリストに関する補助関数 mapAppend を用いている．関
数 rename l1 → r1 l2 → r2 は， l1 → r1 に表われる変数のインデックスの最大値 n を
計算して， l2 → r2 の変数のインデックスにそれぞれ n + 1 増やしてやればよい．
1
2
(* cr.sml *)
signature CR =
8
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
sig
val cpk: (Term.term * Term.term) list
-> (Term.term * Term.term * Term.term) list
end
structure Cr: CR =
struct
local
structure L = List
structure LU = ListUtil
structure T = Term
in
fun cpkRule isIdentical (l1,r1) (l2,r2) =
let fun cpkTerm (T.Var _) = []
| cpkTerm (t as T.Fun (f,ts)) =
let val atRoot = case Subst.unify (t,l1) of
SOME sigma => [(fn x=>x, sigma)]
| NONE => []
val atArgs =
L.map
(fn (C,sigma) => (fn x => T.Fun (f,C x), sigma))
(cpkTermList [] ts)
in atRoot @ atArgs
end
and cpkTermProper (T.Var _) = ...
| cpkTermProper (t as T.Fun (f,ts)) = ...
and cpkTermList _ [] = []
| cpkTermList us (t::ts) =
let val atHead = ...
val atTail = cpkTermList (us@[t]) ts
in atHead @ atTail
end
in L.map (fn (C,sigma) => (Subst.apply sigma (C r1),
Subst.apply sigma l2,
Subst.apply sigma r2))
(if isIdentical
then (cpkTermProper l2)
else (cpkTerm l2))
end
41
42
43
44
45
46
47
48
49
50
51
52
fun cpk rs =
LU.mapAppend
(fn lr1 => (LU.mapAppend
(fn lr2 => let val (lr1’, lr2’) =
Trs.rename (lr1, lr2)
in cpkRule (lr1 = lr2) lr1’ lr2’
end)
rs))
rs
end (* of local *)
end (* of struct *)
9
53
54
55
56
57
58
59
60
61
62
63
64
(* list_util.sml *)
...
val mapAppend: (’a -> ’b list) -> ’a list -> ’b list
...
fun mapAppend f [] = []
| mapAppend f (x::xs) = (f x) @ (mapAppend f xs)
...
(* trs.sml *)
...
val rename: (Term.term * Term.term) * (Term.term * Term.term)
-> (Term.term * Term.term) * (Term.term * Term.term)
...
演習 19 危険頂を計算する関数 cpk を完成させよ．
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
A
(* 実行例 *)
# val R = List.map Trs.rdRule ["+(0,?y) -> ?y", "+(s(?x),?y) -> s
(+(?x,?y))", "+(?x,+(?y,?z)) -> +(?x,+(?y,?z))"];
...
# val CPK = Cr.cpk R;
...
# List.map (fn (v1,u,v2) => print ("<" ^ (Term.toString v1) ^ " <- "
^ (Term.toString u) ^ " -> " ^ (Term.toString v2) ^ ">\n")) CPK
;
<+(?y_1,?z_1) <- +(0,+(?y_1,?z_1)) -> +(0,+(?y_1,?z_1))>
<+(?x_1,?y) <- +(?x_1,+(0,?y)) -> +(?x_1,+(0,?y))>
<s(+(?x,+(?y_1,?z_1))) <- +(s(?x),+(?y_1,?z_1)) -> +(s(?x),+(?y_1,?
z_1))>
<+(?x_1,s(+(?x,?y))) <- +(?x_1,+(s(?x),?y)) -> +(?x_1,+(s(?x),?y))>
<+(0,+(?y,?z)) <- +(0,+(?y,?z)) -> +(?y,?z)>
<+(s(?x_1),+(?y,?z)) <- +(s(?x_1),+(?y,?z)) -> s(+(?x_1,+(?y,?z)))>
<+(?x_1,+(?x,+(?y,?z))) <- +(?x_1,+(?x,+(?y,?z))) -> +(?x_1,+(?x,+(?
y,?z)))>
val it = [(), (), (), (), (), (), ()] : unit list
#
代入の性質に関する証明
(補題 4 の証明) (反射性) 任意の代入 σ について， ∅ ◦ σ = σ ．よって， - は反射的．
(推移性) σ - τ - ξ とする．このとき，定義より，ある ρ1 , ρ2 について ρ1 ◦ σ = τ
かつ ρ2 ◦ τ = ξ となる．すると， ξ = ρ2 ◦ τ = ρ2 ◦ (ρ1 ◦ σ) = (ρ2 ◦ ρ1 ) ◦ σ ．よって，
σ - ξ が成立．よって， - は推移的．
以下の代入に関する性質は，次節で用いる．
10
補題 20 (代入の性質)
1. xτ = tτ とする．このとき，任意の項 u について (u{x := t})τ = uτ ．
2. {x := t} - τ かつ x ∈
/ V(t) ならば， xτ = tτ ．
3. ρ ◦ σ - τ ならば， σ - τ ．
4. x ∈
/ V(t)， x ∈
/ dom(σ)， V(t) ∩ dom(σ) = ∅ とする．このとき， {x := t} ◦ σ - τ
ならば， {x := t} - τ ．
(証明)
1. xτ = tτ と仮定する．このとき， (u{x := t})τ = uτ となることを u に関する
帰納法で示す．
(a) u = x ∈ V の場合．このとき， (x{x := t})τ = tτ = xτ より成立．
(b) u = y ∈ V, x 6= y の場合．このとき， (y{x := t})τ = yτ = yτ より成立．
(c) u = f (u1 , . . . , un ) の場合．このとき，帰納法の仮定を用いて， (f (u1 , . . . , un ){x :=
t})τ = f ((u1 {x := t})τ, . . . , (un {x := t})τ ) = f (u1 τ, . . . , un τ ) = f (u1 , . . . , un )τ
となり，成立．
2. {x := t} - τ ， x ∈
/ V(t) とする．このとき，ある代入 ρ が存在して， τ =
ρ ◦ {x := t}．よって， xτ = ρ({x := t}(x)) = ρ(t)．一方， x ∈
/ V(t) より，
tτ = ρ({x := t}(t)) = ρ(t)．よって， xτ = tτ が成立．
3. ρ ◦ σ - τ とする．このとき，ある代入 ξ が存在して， τ = ξ ◦ (ρ ◦ σ)．よって，
τ = (ξ ◦ ρ) ◦ σ より， σ - τ ．
4. x ∈
/ V(t)， x ∈
/ dom(σ)， V(t) ∩ dom(σ) = ∅ と仮定する．このとき， ({x := t} ◦
σ)(x) = {x := t}(σ(x)) = {x := t}(x) = t ({x := t} ◦ σ ◦ {x := t})(x) = {x :=
t}(σ({x := t}(x))) = {x := t}(σ(t)) == {x := t}(t) = t y 6= x については，
({x := t}◦σ)(y) = {x := t}(σ(y)) ({x := t}◦σ◦{x := t})(y) = ({x := t}◦σ)(y)
よって， {x := t} ◦ σ = {x := t} ◦ σ ◦ {x := t}. 従って， {x := t} ◦ σ - τ なら
ば， {x := t} ◦ σ ◦ {x := t} - τ となり，ゆえに， {x := t} - τ ．
B
単一化手続きの正しさの証明
補題 21 ❀ は整礎，つまり， hE0 , σ0 i ❀ hE1 , σ1 i ❀ · · · なる無限導出列は存在し
ない．
S
(証明) E を単一化問題とするとき， V(E) = {V(s) ∪ V(t) | s ? ≈? t ∈ E}， |E| =
Σ{|s| + |t| | s ? ≈? t ∈ E} と定義する．また， w(hEi , Φi i) = h|V(Ei )|, |Ei |i とおく．
このとき， > を自然数上の自然な順序とするとき， w(hEi , Φi i)(>)lex w(hEi+1 , Φi+1 i．
無限導出列があったとすると， w(hE0 , Φ0 i)(>)lex w(hE1 , Φ1 i) > · · · なる無限列があ
ることになるが，これは矛盾．
11
補題 22 ❀ による導出は ⊥ もしくは h∅, σi で終了する．
(証明) 補題 21 より導出はいつも終了する．題意が成立しないとして， hE, σi (E 6= ∅)
で終了したとする．このとき， E 6= ∅ より， s ? ≈? t ∈ E が存在． root(s), root(t) ∈ F
のときは， Decompose もしくは Clash が適用可能． s = x ∈ V(もしくは t ∈ F) のと
きは， x ∈
/ V(t) なら Eliminate が， x ∈ V(t) かつ x 6= t なら Occur-Check が， x ∈ V(t)
かつ x = t なら Delete が適用可能．よって，終了という仮定に矛盾．
補題 23 hE, σi ❀ hE ′ , σ ′ i とする．このとき， V(E) ∩ dom(σ) = ∅ ならば， V(E ′ ) ∩
dom(σ ′ ) = ∅．
(証明) hE, σi ❀ hE ′ , σ ′ i で使われた導出規則により場合分けする．
1. (Delete) このとき， E = {x ? ≈? x} ∪ E ′ かつ σ = σ ′ ．よって， V(E ′ ) ⊆ V(E)
より明らか．
2. (Decompose) このとき， E = {f (s1 , . . . , sn ) ? ≈? f (t1 , . . . , tn )} ⊎ F ， E ′ =
{s1 ? ≈? t1 , . . . , sn ? ≈? tn } ∪ F ，かつ， σ = σ ′ ．このとき， V(E ′ ) = V(E) より
明らか．
3. (Eliminate) このとき， E = {x ? ≈? t} ⊎ F ， E ′ = {x := t}(F ) = {u{x :=
t} ? ≈? v{x := t} | u ? ≈? v ∈ F }， x ∈
/ V(t)，かつ， σ ′ = {x := t} ◦ σ ．このと
き， V(E ′ ) = V(E) \ {x}, dom(σ ′ ) = dom(σ) ∪ {x} より明らか．
定義 24 E を単一化問題， σ を代入とする．代入 τ が hE, σi の解であるとは， τ が
E の解であり，かつ， σ - τ となるときをいう．
補題 25 hE, σi ❀ hE ′ , σ ′ i， V(E) ∩ dom(σ) = ∅ とする．このとき， τ が hE, σi の解
であるとき，その時に限り， τ は hE ′ , σ ′ i の解．
(証明) hE, σi ❀ hE ′ , σ ′ i で使われた導出規則により場合分けする．
1. (Delete) このとき， E = {x ? ≈? x} ∪ E ′ かつ σ = σ ′ ．任意の代入 τ について，
xτ = xτ であることから明らか．
2. (Decompose) このとき， E = {f (s1 , . . . , sn ) ? ≈? f (t1 , . . . , tn )} ⊎ F ， E ′ =
{s1 ? ≈? t1 , . . . , sn ? ≈? tn }∪F ，かつ， σ = σ ′ ．よって， ∀i (1 ≤ i ≤ n). si τ = ti τ
⇔ f (s1 , . . . , sn )τ = f (t1 , . . . , tn )τ より明らか．
3. (Eliminate) このとき， E = {x ? ≈? t} ⊎ F ， E ′ = {x := t}(F ) = {u{x :=
t} ? ≈? v{x := t} | u ? ≈? v ∈ F }， x ∈
/ V(t)，かつ， σ ′ = {x := t} ◦ σ ．
• (⇐) τ が hE, σi の解であると仮定する．すると， xτ = tτ ，任意の u ? ≈?
v ∈ F について uτ = vτ ，かつ， σ - τ ．まず， {x := t} ◦ σ - τ か
ら，補題 20(3) より， σ - τ ．また， xτ = tτ であるから，補題 20(1) よ
り， (u{x := t})τ = uτ = vτ = (v{x := t})τ となる．よって，任意の
u′ ? ≈? v ′ ∈ {x := t}(F ) について u′ τ = v ′ τ ．よって， τ は {x := t}(F ) の
解．以上より， τ は hE ′ , σ ′ i の解．
12
• (⇒) τ が hE ′ , σ ′ i の解であると仮定する．すると，任意の u ? ≈? v ∈ F
について (u{x := t})τ = (v{x := t})τ ，かつ， {x := t} ◦ σ - τ ．まず，
{x := t} ◦ σ - τ から，補題 20(3) より， σ - τ が成立する．いま，仮定
から V(E) ∩ dom(σ) = ∅ なので， x ∈
/ dom(σ) かつ V(t) ∩ dom(σ) = ∅ が
成立する．よって， x ∈
/ V(t)， {x := t} ◦ σ - τ から，補題 20(4) より，
{x := t} - τ ．よって， x ∈
/ V(t) なので，補題 20(2) より， xτ = tτ が成立．
xτ = tτ と補題 20(1) より，任意の u ? ≈? v ∈ F について uτ = (u{x :=
t})τ = (v{x := t})τ = vτ となる．従って， τ は E = {x ? ≈? t} ⊎ F の解．
以上より， τ は hE, σi の解．
∗
補題 26 hE, σi ❀ hF, ρi， V(E) ∩ dom(σ) = ∅ とする． τ が hE, σi の解であるとき，
その時に限り， τ は hF, ρi の解．
∗
(証明) hE, σi ❀ hF, ρi，導出の長さに関する帰納法で示す．導出の長さが 0 のとき
∗
は明らか．導出の長さが > 0 のとき，導出は， hE, σi ❀ hE ′ , σ ′ i ❀ h∅, τ i とおける．
このとき， V(E) ∩ dom(σ) = ∅ の仮定と補題 23 より，仮定 V(E ′ ) ∩ dom(σ ′ ) = ∅．
よって，帰納法の仮定が適用できて， τ が hE ′ , σ ′ i の解 ⇔ τ が hF, ρi の解．よって，
補題 25 より，題意が成立．
∗
補題 27 h{s ? ≈? t}, ∅i ❀ h∅, τ i ならば， τ は s と t の単一化子．
(証明) τ は h∅, τ i の解．よって， V({s ? ≈? t}) ∩ dom(∅) = ∅ なので，補題 26 より，
τ は h{s ? ≈? t}, ∅i の解．従って， τ は s と t の単一化子．
∗
補題 28 h{s ? ≈? t}, ∅i ❀ h∅, τ i とする． σ が s と t の単一化子ならば， τ - σ ．
(証明) σ を s と t の単一化子とする．このとき， σ は h{s ? ≈? t}, ∅i の解．よって，
V({s ? ≈? t}) ∩ dom(∅) = ∅ なので，補題 26 より， σ は h∅, τ i の解．従って， τ - σ ．
∗
補題 29 h{s ? ≈? t}, ∅i ❀ h∅, τ i とする．このとき， τ は s と t の最汎単一化子．
(証明) 補題 27 より， τ は s と t の単一化子．また， σ を s と t の単一化子とすると，
補題 28 より， τ - σ ．よって， τ は s と t の最汎単一化子．
∗
補題 30 hE, σi ❀ ⊥， V(E) ∩ dom(σ) = ∅ とする．このとき， hE, σi は解を持たな
∗
い．特に， h{s ? ≈? t}, ∅i ❀ ⊥ ならば， s と t は単一化不能．
∗
(証明) hE, σi ❀ ⊥ の導出の長さに関する帰納法で示す．
1. 導出の長さが 1 の場合． hE, σi ❀ ⊥ に用いられた導出規則で場合分けする．
(a) (Crash) このとき， E = {f (s1 , . . . , sn ) ? ≈? g(t1 , . . . , tm )} ⊎ F (f 6= g)．任
意の代入 σ について f (s1 , . . . , sn )σ 6= g(t1 , . . . , tm )σ となるから， hE, σi
は解を持たない．
13
(b) (Occur-Check) このとき， E = {x ? ≈? t} ⊎ F (x ∈ V(t), x 6= t)．よって，
任意の代入 σ について xσ 6= tσ となるから， hE, σi は解を持たない．
∗
2. 導出の長さが > 1 の場合． hE, σi ❀ hE ′ , σ ′ i ❀ ⊥ とおくと，帰納法の仮定よ
り， hE ′ , σ ′ i は解を持たない．よって， hE, σi が解をもつとすると，補題 25 に
矛盾．
定理 31 s ? ≈? t を単一化問題とするとき， h{s ≤? t}, ∅i から始まる導出は (a) h∅, σi
で終了するか，もしくは (b) ⊥ で終了し，
(a) ⇔ s と t は単一化可能かつ σ は s と t の最汎単一化子
(b) ⇔ s と t は単一化不能
が成立する．
(証明) 補題 22 より， h{s ? ≈? t}, ∅i から始まる導出は h∅, σi もしくは ⊥ で終了する．
1. (⇒) h∅, σi で終了したとする．このとき，補題 29 より σ は s と t の最汎単一化
子．また，最汎単一化子が存在するから， s と t は単一化可能．
(⇐) s と t が単一化可能とする．もし (b) が成立すると，補題 30 より， s と t
は単一化不能となるので矛盾．
2. (⇒) 補題 30 より成立．
(⇐) s と t が単一化不能とする．もし (a) が成立すると， 1 と同様に補題 29 より
σ は s と t の最汎単一化子となり， s と t は単一化可能となるから，矛盾．よっ
て， (b) が成立．
C
危険対補題の証明
(補題 18 の証明) t1 l1 →r1 ,p1 ,σ ← s →l2 →r2 ,p2 ,σ t2 とする．ここで， V(l1 ) ∩ V(l2 ) = ∅ よ
り，同じ代入 σ を用いていると仮定してよいことに注意する．位置 p1 , p2 の関係に
よって場合分けする
1. p1 k p2 の場合．このとき， s = s[l2 σ, l1 σ]p1 ,p2 ， t1 = s[l2 σ, r1 σ]p1 ,p2 ， t2 =
s[r2 σ, l1 σ]p1 ,p2 とおける．よって， t2 = s[r2 σ, l1 σ]p1 ,p2 →l1 →r1 s[r2 σ, r1 σ]p1 ,p2 l2 →r2 ←
s[l2 σ, r1 σ]p1 ,p2 = t1 となるので， (1)(および (2)) が成立する．
2. p1 > p2 の場合．このとき， p1 = p2 .w とおける． 2 通りに場合分けする．
(a) l2 の変数位置 wx が存在して wx 6 w が成立する場合．このとき，ある q
が存在して w = wx .q とおける． l2 |wx = x， {p ∈ Pos(l2 ) | x = l2 |p } =
{w1 , . . . , wn }， wx = w1 とおく．このとき，任意の i について， s|p2 .wi =
14
(l2 σ)|wi = σ(x)．また， p1 = p2 .w = p2 .wx .q = p2 .w1 .q ．よって， l1 σ =
s|p1 = s|p2 .w1 .q = (s|p2 )|w1 .q = (l2 σ)|w1 .q = σ(x)|q ．以上より，
t1 =
=
=
=
=
=
=
=
s[r1 σ]p1
s[r1 σ]p2 .w1 .q
s[s[r1 σ]w1 .q ]p2
s[l2 σ[r1 σ]w1 .q ]p2
s[l2 σ[r1 σ]w1 .q ]p2
s[l2 σ[r1 σ, (l2 σ)|w2 .q , . . . , (l2 σ)|wn .q ]w1 .q,w2 .q,...,wn .q ]p2
s[l2 σ[r1 σ, σ(x)|q , . . . , σ(x)|q ]w1 .q,w2 .q,...,wn .q ]p2
s[l2 σ[r1 σ, l1 σ, . . . , l1 σ]w1 .q,w2 .q,...,wn .q ]p2
が成立する．次に，代入 σ̂ を，任意の z ∈ V(l2 )\{x} について σ̂(z) = σ(z)，
σ̂(x) = σ(x)[r1 σ]q とおくと，
l2 σ̂ =
=
=
=
(l2 [x, . . . , x]w1 ,...,wn )σ̂
l2 σ̂[σ̂(x), . . . , σ̂(x)]w1 ,...,wn
l2 σ[σ(x)[r1 σ]q , . . . , σ(x)[r1 σ]q ]w1 ,...,wn
l2 σ[r1 σ, . . . , r1 σ]w1 .q,...,wn .q
よって，
t1 =
→l1 →r1 ,p2 .w2 .q
→l1 →r1 ,p2 .w3 .q
→l1 →r1 ,p2 .wn .q
=
→l2 →r2 ,p2
s[l2 σ[r1 σ, l1 σ, . . . , l1 σ]w1 .q,w2 .q,...,wn .q ]p2
s[l2 σ[r1 σ, r1 σ, . . . , r1 σ]w1 .q,w2 .q,...,wn .q ]p2
···
s[l2 σ[r1 σ, r1 σ, . . . , r1 σ]w1 .q,w2 .q,...,wn .q ]p2
s[l2 σ̂]p2
s[r2 σ̂]p2
が成立する．一方， σ(x) = σ(x)[l1 σ]q →l1 →r1 σ(x)[r1 σ]q = σ̂(x) であった
から，
∗
t2 = s[r2 σ]p2 −
→l1 →r1 s[r2 σ̂]p2
∗
よって， t1 →
− l1 →r1 →l2 →r2 s[r2 σ̂]p2
l1 →r1 ∗
←
− t2 となり， (1) が成立する．
(b) 任意の l2 の変数位置 wx について wx 66 w となる場合．このとき， p1 = p2 .q
とおくと， l2 |q は l2 の非変数部分項．よって，
l1 σ = s|p1 = s|p2 .q = (s|p2 )|q = (l2 σ)|q = (l2 |q )σ
が成立する．これは l1 と l2 |q が単一化可能なことを意味するから， τ =
mgu(l1 , l2 |q ) - σ が存在する．従って， σ = θ ◦ τ となる代入 θ および危険
頂 l2 [r1 ]q τ ← l2 τ → r2 τ ∈ CPK(l1 → r1 , l2 → r2 ) が存在する． C = s[]p2
ととると，
t1 = s[r1 σ]p1 = s[l2 σ[r1 σ]q ]p2 = C[l2 [r1 ]q σ] = C[l2 [r1 ]q τ θ]
s = s[l2 σ]p2 = C[l2 σ] = C[l2 τ θ]
t2 = s[r2 σ]p2 = C[r2 σ] = C[r2 τ θ]
となり， (3) が成立する．
15
3. p1 < p2 の場合．これとき p1 > p2 と対称的となるだけであるから，場合 2. と
同様にして， (2) または (3) が成立することが示せる．
16

Download Report