４．語問題、項書換え系
4.0. 準備 (3.1. 項、代入、等価性) 定義3.1.1： - シグネチャ(signature)：関数記号の集合(Σと書く) - それぞれの関数記号は、アリティ(arity)と呼ばれる自 然数が定められている - Σ(n)：アリティnを持つ関数記号からなるΣの部分集合 例：群 ΣG = {e, i, ◦} (e ∈ Σ(0)G , i ∈ Σ(1)G , ◦ ∈ Σ(2)G )X：変数の集合 (Σ ∩ X = ∅) 定義3.1.2： (Σ-)項の集合T(Σ, X) の再帰的定義 - X ⊆ T(Σ, X) - f ∈ Σ(n) かつ t 1, . . . ,tn∈T(Σ, X)ならば、 f (t1, . . . ,tn) ∈T(Σ, X) 基礎項：変数を持たない項 (その集合を T(Σ, ∅) や T(Σ) で書く) 2- 2 / 32
項の例：
- ◦(e, ◦(x, i(x)))は項。 (eはe()の略記)
- +(+(x, y), z)の代わりに、(x + y) + zと書いたりする
例による項の木表現の説明 t = ◦(e, ◦(x, i(x))) を木で表現すると - 位置の集合Pos(t) = {ε, 1, 2, 21, 22, 221} - ε：根位置(root position) - 根記号(root symbol)は、位置εの関数記号◦ 2- 4 / 32
項s の位置の集合Pos(s)： - Pos(x) = {ε} - Pos(f (s1, . . . ,sn)) = {ε} ∪ n [ i=1 {ip | p ∈ Pos(si)} 接頭順序(prefix order) - p ≤q iff ∃p0 pp0 =q p ||q iff ¬(p ≤ q) ∧ ¬(q ≤ p) 項の大きさ - |s|= |Pos(s)| 例：2 ≤ 221 21 || 221 |◦(e, ◦(x, i(x)))| = 6 以降は位置を表すとき、i, j ∈ N, p, q ∈ N∗と記号を用
項s の位置 p の部分項 s|p - s|ε=s - f (s1, . . . ,sn)|iq=si|q （ただし，1 ≤i ≤ n） 項s の位置 p を t で置き換えて得られる項 s[t]p - s[t]ε=t - f (s1, . . . ,sn)[t]iq=f (s1, . . . ,si[t]q, . . . ,sn) 変数の集合 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}
問：次の性質を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 7→ ◦(e, y), y 7→ i(e)} とするとき、 ◦(x,i(y))σ = ◦(◦(e, y),i(i(e)))
代入 σ : V → T(Σ, V ) ただし、Dom(σ) は有限集合 Dom(σ) = {x ∈ V | σ(x) 6= x} Dom(σ) = {x1, . . . ,xn} のとき、σ を次のように書く {x1 7→ σ(x1), . . . ,xn 7→ σ(xn)} σ の項上への自然な拡張σˆ :T(Σ, V ) → T(Σ, V ) - x ˆσ = σ(x) - f (s1, . . . ,sn)ˆσ =f (s1σ, . . . ,ˆ s1σ)ˆ σ と ˆσ を同一視する
代入 σ と σ0を合成して得られる代入 τ = σσ0は任意の 変数x について以下を満たす代入
- xτ = (xσ)σ0
例：σ = {x 7→ ◦(e, y), y 7→ i(e)}、 σ0 = {y 7→ e, z 7→ w} のとき、
σσ0 = {x 7→ ◦(e, e), y 7→ i(e), z 7→ w}
Σ 等式： 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
補題3.1.10： s →E t とするとき、次が成り立つ (a) 任意の代入σについて、sσ →E tσ
(b) f (· · · s · · · ) →E f (· · · t · · · ) 問：上の補題を証明せよ
定理3.1.12：↔∗ Eは、以下を満たす最小の同値関係≡ 1. s1 ≡t1, . . . ,sn≡tnならば f (s1, . . . ,sn) ≡f (t1, . . . ,tn) 2. s ≡ tならば∀σ.sσ ≡ tσ 3. E ⊆ ≡ 証明：↔∗ E が同値関係であること、1.2.3. をみたすこと は容易に示せる 最小性を示す。≡ を1.2.3. を満たす同値関係とする。こ れより、→E ⊆ ≡ が示せる。この両辺の対称閉包と反射 的推移的閉包をとることにより、↔∗ E ⊆ ≡ が得られる。 2- 14 / 32
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
例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)
定義4.5.1：代入 σ が σ0より一般的(σ .σ0と書く)： ∃δ. σδ = σ0 例：σ . σ0 ここで、 σ = {x 7→ f (y)}、 σ0 = {x 7→ f (a), y 7→ a} 名前替えの例：{x 7→ y, y 7→ z, z 7→ x} 補題4.5.3：σ . σ0かつ σ0 . σ(σ ∼ σ0と書く) iff σδ = σ0を満たす名前替え δ が存在する 2- 18 / 32
定義4.5.4： - 単一化問題S = {s1 =?t1, . . . ,sn=?tn} - Sの解は、次を満たす代入σ s1σ =t1σ, . . . ,snσ =tnσ - Sのすべての解の集合 U(S) = {σ | ∀(s =?t) ∈ S. sσ = tσ}
σ がS の最汎単一化子(mgu)： σ ∈U(S) ∧ ∀σ0 ∈U(S). σ . σ0 例4.5.5：S = {x =? y} とする - σ = {x 7→ y}は、Sの最汎単一化子 - σ0= {x 7→ z, y 7→ z}は、Sの単一化子だが、最汎単一 化子でない - σ00= {x 7→ y, z1 7→z2,z27→z1}は、Sの最汎単一化子。 例えば、σ00{z17→z2,z27→z1} = σ 2- 20 / 32
代入 σ が巾等：σσ = σ
定理4.5.8：単一化問題 S が解を持つならば、巾等な最
汎単一化子が存在する 証明：次章に
4.6. 変換に基づく単一化の解法（時間の関係で省略の可能 性あり） 定義4.6.1：次の条件を満たす単一化問題を解形式と いう - S = {x1=?t1, . . . ,xn=?tn}の形式 - x1, . . . ,xnは相異なる変数 - x1, . . . ,xnはt1からtnには出現しない 解形式の例： S = {x =? f (z, z), y =? f (f (z, z), f (z, z))} 2- 22 / 32
解形式S = {x1 =? t 1, . . . ,xn=? tn} から代入 ~S = {x 1 7→t1, . . . ,xn 7→tn} が定められる 補題4.6.2：解形式 S について、∀σ ∈ U(S). ~Sσ = σ 証明：S = {x1 =? t 1, . . . ,xn =? tn} とする - xi ∈Dom(~S)について、xi~Sσ = tiσ =xiσ - x 6∈ 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 (t1, . . . ,tn) =?f (u1, . . . ,un)} ∪S ⇒ {t1 =?u1, . . . ,tn=?un} ∪S (方向) tが変数でないとき、 {t =?x} ∪ S ⇒ {x =?t} ∪ S (消去) x ∈ Var(S)かつx 6∈ Var(t)のとき、 {x =?t} ∪ S ⇒ {x =?t} ∪ S{x 7→ t} ここで、Sσ = {tσ =? uσ | t =? u ∈ S} 2- 24 / 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)}
x が既解：x は x =?t の形式で S 中に一ヶ所だけ出現 補題4.6.5：手続き Unify(S) は、入力の単一化問題 S に よらず停止する 証明：変換⇒ の停止性を、S から (N × N × N, >3 lex) へ の測度関数 φ(S) = (n1,n2,n3) を使って示す。 - n1：Sの既解でない変数の数 - n2 = X s=?t∈S (|s| + |t|) - n3：S中にあるt =?xの形式の数 2- 26 / 32
証明(続き) φ の単調性は以下のように示される n1 n2 n3 削除 ≥ > 分解 ≥ > 方向 ≥ = > 消去 >
補題4.6.6：S ⇒ T ならば U(S) = U(T) 証明：⇒消去については以下の通り {x =? t} ∪ S0 ⇒ {x =?t} ∪ S0{x 7→ t} とする σ ∈U({x =? t} ∪ S0) iff xσ = tσ ∧ σ ∈ U(S0) iff xσ = tσ ∧ ({x 7→ t}σ) ∈ U(S0) by 補 4.6.2 iff xσ = tσ ∧ σ ∈ U(S0{x 7→ t}) iff σ ∈ U({x =? t} ∪ S0{x 7→ t}) 他の変換規則については明らか 2- 28 / 32
補題4.6.7：Unify(S) は健全。(得られる代入 ~S0は巾等 なS の解)
証明：補題4.6.6 から U(S) = U(S0) が導ける。また、 補題4.6.3 より、~S0は巾等である。
補題4.6.8：S が次の形式の要素を含むとき、S は解を 持たない f (s1, . . . ,sm) =?g(t1, . . . ,tn) ここで、f 6= g 補題4.6.9：S が次の形式の要素を含むとき、S は解を 持たない x =?t ここで、x ∈ Var(t) かつ x 6= t 2- 30 / 32
補題4.6.10：S が解を持てば、Unify(S) は解を返す 証明： 1. 解形式でないSが解を持てば、変換規則が適用できる ことが、補題4.6.8と補題4.6.9から示せる。これは、 変換の正規形は、解形式であるか、あるいは、解を持た ないことを意味する 2. 変換は停止性を持つ(補題4.6.5)ので、その正規形のひ とつS0 を必ず求めることが出来る。Sは解を持つとい う前提と1.より、S0は解形式である。補題4.6.6より、 ~ S0はSの解である
解を持たないことを早く発見するために、Unify に次の 規則を追加してもよい (衝突) f 6= gのとき、 {f (s1, . . . ,sm) =?g(t1, . . . ,tn)} ∪S ⇒ ⊥ (消去) x ∈ Var(t)かつx 6= tのとき、 {x =? t} ∪ S ⇒ ⊥ ここで、⊥ は解を持たない特別な単一化問題とする 2- 32 / 32
