2-1 / 32 4. 語問題 項書換え系 4.0. 準備 (3.1. 項 代入 等価性 ) 定義 3.1.1: - シグネチャ (signature): 関数記号の集合 (Σ と書く ) - それぞれの関数記号は アリティ (arity) と呼ばれる自然数が定められている - Σ (n) : アリティ n を持つ関数記号からなる Σ の部分集合 例 : 群 Σ G = {e, i, } (e Σ (0) G, i Σ(1) G, Σ(2) G )
2-2 / 32 X: 変数の集合 (Σ X = ) 定義 3.1.2: (Σ-) 項の集合 T (Σ, X) の再帰的定義 - X T (Σ, X) - f Σ (n) かつ t 1,..., t n T (Σ, X) ならば f (t 1,..., t n ) T (Σ, X) 基礎項 : 変数を持たない項 ( その集合を T (Σ, ) や T (Σ) で書く )
項の例 : - (e, (x, i(x))) は項 (e は e() の略記 ) - +(+(x, y), z) の代わりに (x + y) + z と書いたりする - g(g( g(t) )) を g n (t) と書く (n は g のネストの数 ) 2-3 / 32
2-4 / 32 例による項の木表現の説明 t = (e, (x, i(x))) を木で表現すると - 位置の集合 Pos(t) = {ε, 1, 2, 21, 22, 221} - ε: 根位置 (root position) - 根記号 (root symbol) は 位置 ε の関数記号
2-5 / 32 項 s の位置の集合 Pos(s): - Pos(x) = {ε} - Pos(f (s 1,..., s n )) = {ε} 接頭順序 (prefix order) - p q iff p pp = q p q iff (p q) (q p) 項の大きさ - s = Pos(s) n {ip p Pos(s i )} i=1 例 :2 221 21 221 (e, (x, i(x))) = 6 以降は位置を表すとき i, j N, p, q N と記号を用いる
項 s の位置 p の部分項 s p - s ε = s - f (s 1,..., s n ) iq = s i q ( ただし,1 i n) 項 s の位置 p を t で置き換えて得られる項 s[t] p - s[t] ε = t - f (s 1,..., s n )[t] iq = f (s 1,..., s i [t] q,..., s n ) 変数の集合 Var(s) 例 : (e, (x, i(x))) 22 = i(x) (e, (x, i(x)))[ (e, e)] 22 = (e, (x, (e, e))) Var( (e, (x, i(x)))) = {x} 2-6 / 32
2-7 / 32 問 : 次の性質を p の長さに関する帰納法で証明せよ - pq Pos(s) ならば s pq = (s p ) q このような性質として以下の性質がある ( 補題 3.1.4) - p Pos(s) q Pos(t) ならば (s[t] p ) pq = t q (s[t] p )[r] pq = s[t[r] q ] p - pq Pos(s) ならば (s[t] pq ) p = (s p )[t] q (s[t] pq )[r] p = s[r] p - p, q Pos(s) p q ならば (s[t] p ) q = s q (s[t] p )[r] q = (s[r] q )[t] p
例による代入の説明代入 σ = {x (e, y), y i(e)} とするとき (x, i(y))σ = ( (e, y), i(i(e))) 2-8 / 32
代入 σ : V T (Σ, V ) ただし Dom(σ) は有限集合 Dom(σ) = {x V σ(x) x} Dom(σ) = {x 1,..., x n } のとき σ を次のように書く {x 1 σ(x 1 ),..., x n σ(x n )} σ の項上への自然な拡張 ˆσ : T (Σ, V ) T (Σ, V ) - x ˆσ = σ(x) - f (s 1,..., s n )ˆσ = f (s 1ˆσ,..., s 1ˆσ) σ と ˆσ を同一視する 2-9 / 32
2-10 / 32 代入 σ と σ を合成して得られる代入 τ = σσ は任意の変数 x について以下を満たす代入 - xτ = (xσ)σ 例 :σ = {x (e, y), y i(e)} σ = {y e, z w} のとき σσ = {x (e, e), y i(e), z w}
2-11 / 32 Σ 等式 : T (Σ, V ) 項の対 - 等式 (s, t) を s t と書く - 例 : ( (x, y), z) (x, (y, z)) - 項の順序を意識するときは s t と書く 例による書換えの説明等式 ( (x, y), z) (x, (y, z)) E によって i( ( (i(e), e), e)) E i( (i(e), (e, e)))
定義 3.1.8 等式集合 E による書換え E T (Σ, V ) T (Σ, V ) - s E t iff (l, r) E, p Pos(s), σ s p = lσ t = s[rσ] p 2-12 / 32
2-13 / 32 補題 3.1.10: s E t とするとき 次が成り立つ (a) 任意の代入 σ について sσ E tσ (b) f ( s ) E f ( t ) 問 : 上の補題を証明せよ
2-14 / 32 定理 3.1.12: E は 以下を満たす最小の同値関係 1. s 1 t 1,..., s n t n ならば f (s 1,..., s n ) f (t 1,..., t n ) 2. s t ならば σ. sσ tσ 3. E 証明 : E が同値関係であること 1.2.3. をみたすことは容易に示せる最小性を示す を 1.2.3. を満たす同値関係とする これより E が示せる この両辺の対称閉包と反射的推移的閉包をとることにより E が得られる
4.1. E 上の語問題の決定性 E 上の語問題 :s, t T (Σ, X) が与えられて s E t を満たすかを答える問題 定理 4.1.1: E が SN( 停止性 ) と CR( 合流性 ) をもつとき E 上の語問題は決定可能 証明 : 定理 2.1.9 より s E t iff s E = t E 2-15 / 32
例 4.1.3: コンビネータ論理 Σ = {, S, K} E = { ((S x) y) z (x z) (y z) (K x) y x } - いかなるプログラムも ( コーディングにより ) 基礎項で表現可能 例えば I x x を満たす I は I = (S K) K で表せる - 語問題は決定不能 2-16 / 32
4.5. 単一化 s と t が E 単一化可能 : σ. sσ E tσ - このような σ を E 単一化子とよぶ - E 単一化は一般に決定不能 そうでなければ 語問題が決定可能になるため ( 構文的 ) 単一化 : 単一化 単一化可能な例 : f (x) =? f (a) x =? f (y) h(x, y) = h(a, x) 単一化不可能な例 :f (x) =? g(y) x =? f (x) 2-17 / 32
定義 4.5.1: 代入 σ が σ より一般的 (σ σ と書く ): δ. σδ = σ 例 :σ σ ここで σ = {x f (y)} σ = {x f (a), y a} 名前替えの例 :{x y, y z, z x} 補題 4.5.3:σ σ かつ σ σ(σ σ と書く ) iff σδ = σ を満たす名前替え δ が存在する 2-18 / 32
定義 4.5.4: - 単一化問題 S = {s 1 =? t 1,..., s n =? t n } - S の解は 次を満たす代入 σ s 1 σ = t 1 σ,..., s n σ = t n σ - S のすべての解の集合 U(S) = {σ (s =? t) S. sσ = tσ} 2-19 / 32
σ が S の最汎単一化子 (mgu): σ U(S) σ U(S). σ σ 例 4.5.5:S = {x =? y} とする - σ = {x y} は S の最汎単一化子 - σ = {x z, y z} は S の単一化子だが 最汎単一化子でない - σ = {x y, z 1 z 2, z 2 z 1 } は S の最汎単一化子 例えば σ {z 1 z 2, z 2 z 1 } = σ 2-20 / 32
2-21 / 32 代入 σ が巾等 :σσ = σ 定理 4.5.8: 単一化問題 S が解を持つならば 巾等な最汎単一化子が存在する 証明 : 次章に
2-22 / 32 4.6. 変換に基づく単一化の解法 ( 時間の関係で省略の可能性あり ) 定義 4.6.1: 次の条件を満たす単一化問題を解形式という - S = {x 1 =? t 1,..., x n =? t n } の形式 - x 1,..., x n は相異なる変数 - x 1,..., x n は t 1 から t n には出現しない 解形式の例 : S = {x =? f (z, z), y =? f (f (z, z), f (z, z))}
2-23 / 32 解形式 S = {x 1 =? t 1,..., x n =? t n } から代入 S = {x1 t 1,..., x n t n } が定められる 補題 4.6.2: 解形式 S について σ U(S). Sσ = σ 証明 :S = {x 1 =? t 1,..., x n =? t n } とする - x i Dom( S) について x i Sσ = ti σ = x i σ - x Dom( S) について x Sσ = xσ 補題 4.6.3: 解形式 S について S は巾等な最汎単一化子である 証明 : 巾等性については省略 S U(S) は明らか まら 補題 4.6.2 より σ U(S). S σ であり 最汎性が導かれる
最汎単一化子を得るための変換系 Unify(S): S に可能な限り変換 を繰り返し適用する その結果 S が解形式なら解 S を返す さもなければ 解なし ( 削除 ) {t =? t} S S ( 分解 ) {f (t 1,..., t n ) =? f (u 1,..., u n )} S {t 1 =? u 1,..., t n =? u n } S ( 方向 ) t が変数でないとき {t =? x} S {x =? t} S ( 消去 ) x Var(S) かつ x Var(t) のとき {x =? t} S {x =? t} S{x t} ここで Sσ = {tσ =? uσ t =? u S} 2-24 / 32
2-25 / 32 例 : {x =? f (a), g(x, x) =? g(x, y)} 消去 {x =? f (a), g(f (a), f (a)) =? g(f (a), y)} 分解 {x =? f (a), f (a) =? f (a), f (a) =? y} 削除 {x =? f (a), f (a) =? y} 方向 {x =? f (a), y =? f (a)} 問 : 上の例で 最初に = 分解を適用した変換を試みよ
2-26 / 32 x が既解 :x は x =? t の形式で S 中に一ヶ所だけ出現 補題 4.6.5: 手続き Unify(S) は 入力の単一化問題 S によらず停止する証明 : 変換 の停止性を S から (N N N, > 3 lex ) への測度関数 φ(s) = (n 1, n 2, n 3 ) を使って示す - n 1 :S の既解でない変数の数 - n 2 = ( s + t ) s=? t S - n 3 :S 中にある t =? x の形式の数
2-27 / 32 証明 ( 続き ) φ の単調性は以下のように示される n 1 n 2 n 3 削除 > 分解 > 方向 = > 消去 >
2-28 / 32 補題 4.6.6:S T ならば U(S) = U(T ) 証明 : 消去については以下の通り {x =? t} S {x =? t} S {x t} とする σ U({x =? t} S ) iff xσ = tσ σ U(S ) iff xσ = tσ ({x t}σ) U(S ) by 補 4.6.2 iff xσ = tσ σ U(S {x t}) iff σ U({x =? t} S {x t}) 他の変換規則については明らか
2-29 / 32 補題 4.6.7:Unify(S) は健全 ( 得られる代入 S は巾等な S の解 ) 証明 : 補題 4.6.6 から U(S) = U(S ) が導ける また 補題 4.6.3 より S は巾等である
2-30 / 32 補題 4.6.8:S が次の形式の要素を含むとき S は解を持たない f (s 1,..., s m ) =? g(t 1,..., t n ) ここで f g 補題 4.6.9:S が次の形式の要素を含むとき S は解を持たない x =? t ここで x Var(t) かつ x t
補題 4.6.10:S が解を持てば Unify(S) は解を返す証明 : 1. 解形式でない S が解を持てば 変換規則が適用できることが 補題 4.6.8 と補題 4.6.9 から示せる これは 変換の正規形は 解形式であるか あるいは 解を持たないことを意味する 2. 変換は停止性を持つ ( 補題 4.6.5) ので その正規形のひとつ S を必ず求めることが出来る S は解を持つという前提と 1. より S は解形式である 補題 4.6.6 より S は S の解である 2-31 / 32
解を持たないことを早く発見するために Unify に次の規則を追加してもよい ( 衝突 ) f g のとき {f (s 1,..., s m ) =? g(t 1,..., t n )} S ( 消去 ) x Var(t) かつ x t のとき {x =? t} S ここで は解を持たない特別な単一化問題とする 2-32 / 32