表現系工学特論 項書換え系（４） 完備化 １．語問題と等式証明 ２．合流性とチャーチ・ロッサ性 ３．完備化手続き.

Presentation on theme: "表現系工学特論 項書換え系（４） 完備化 １．語問題と等式証明 ２．合流性とチャーチ・ロッサ性 ３．完備化手続き."— Presentation transcript:

1 表現系工学特論 項書換え系（４） 完備化 １．語問題と等式証明 ２．合流性とチャーチ・ロッサ性 ３．完備化手続き

2 １．語問題と等式証明 語問題 (word problem) s = t ? 等式の集合 E ２つの項 s, t
(equational proof) 語問題 (word problem) 等式の集合 E ２つの項 s, t s = t ? 等　　　　式　f(g(x)) ＝ h(x) 書換え規則　f(g(x)) → h(x) (a set of equations) (two terms) (decision)

3 語問題の例： 群論(group theory)
◆右辺（単純な項）から左辺（複雑な項）への 書換えを含むので探索が困難 ◆左辺≠右辺であることの判定が困難

4 ２．合流性とチャーチ・ロッサ性(1/8) 会同性
a a b b ● ● ● c a=b の書換え証明

5 ２．合流性とチャーチ・ロッサ性(2/8) 合流性
完備性＝停止性＋合流性 (complete)

6 ２．合流性とチャーチ・ロッサ性(3/8) チャーチ・ロッサ性
書換え証明

7 ２．合流性とチャーチ・ロッサ性(4/8) 書換え証明
チャーチ・ロッサ性のないシステムの例

8 ２．合流性とチャーチ・ロッサ性(5/8) CR性 ⇒ 合流性

9 ２．合流性とチャーチ・ロッサ性(6/8) 合流性 ⇒ CR性

10 ２．合流性とチャーチ・ロッサ性(7/8) 合流性 ⇒ CR性

11 ２．合流性とチャーチ・ロッサ性(8/8) 完備な書換え系による語問題の解法
s t ● 正規形 s ＝ t s t ● 正規形 s’ t’ s ≠ t もし s=t ならば，s’=t’となるが，その書換え証明が存在しないので，CR性に矛盾する．

12 停止性を保証するように 等式を向き付けるための 簡約順序 ＞
３．完備化手続き(1/12) 等式の集合 E 完備化 手続き 成功： 完備な書換え系 R 失敗： 向き付けできない等式 発散： 成功も失敗もせず， 　　　　無限に計算し続ける 停止性を保証するように 等式を向き付けるための 簡約順序 ＞ たとえば，各記号の重さ (completion procedure) Knuth & Bendix (1970)

13 ３．完備化手続き(2/12) 初期状態 (initial state) f(a) = b a = c E R

14 s t s’ t’ ３．完備化手続き(3/12) 等式の向き付け ＞ (orient an equation) 正規形 正規形 ● ● ●

15 ３．完備化手続き(4/12) 等式の向き付け（続き）
f(a) ＝ b a ＝ c a ＝ c f(a) → b f(a) → b a → c 重さ a: 2 b,c,f: 1

16 ３．完備化手続き(5/12) 危険対の生成 f(a) → b f(c) ＝ b a → c f(a) → b a → c
(deduce critical pairs) f(a) → b f(c) ＝ b 左辺に重なりがある a → c f(a) → b a → c f(a) → b a → c f(a) f(c) ＝ b 危険対

17 ３．完備化手続き(6/12) 終了条件 f(c) ＝ b 空集合 f(a) → b a → c f(c) → b f(a) → b a → c 完備な書換え系 成功

18 ３．完備化手続き(7/12) 完備化手続きの正当性
● 危険対の生成 s t ＝ 危険対 ● ● 等式の向き付け ● ● s’ t’ ＞ 正規形 正規形

19 ３．完備化手続き(8/12) 例）群論の完備化(1/3)
e・x ＝ x x-1・x ＝ e (x・y)・z ＝ x・(y・z) 等式の向き付け e・x → x x-1・x → e (x・y)・z → x・(y・z) 簡約順序は，たとえば，つぎの多項式解釈を用いる φ(x・y) = 3 + 3x + 2y + xy φ(e) = 0 φ(x-1) = 1 + x + x2　

20 ３．完備化手続き(9/12) 例）群論の完備化(2/3)
x・z ＝ e・(x・z) e・z ＝x-1・(x・z) 危険対の生成 (x・(y・z))・w ＝(x・y)・(z・w) e・x → x x-1・x → e (x・y)・z → x・(y・z) e・x → x x-1・x → e (x・y)・z → x・(y・z) (x・y)・z → x・(y・z) (x・(y・z))・w ((x・y)・z)・w (x・y)・(z・w) x・z e・(x・z) (e・x)・z e・x → x (x・y)・z → x・(y・z) x-1・x → e (x・y)・z → x・(y・z) e・z (x-1・x)・z x-1・(x・z)

21 ３．完備化手続き(10/12) 例）群論の完備化(3/3)
x・z ＝ e・(x・z) e・z ＝x-1・(x・z) 等式の向き付け e-1・z ＝ z (x・(y・z))・w ＝(x・y)・(z・w) e・x → x x-1・x → e (x・y)・z → x・(y・z) e・x → x x-1・x → e (x・y)・z → x・(y・z) 危険対の生成 x-1・(x・z) →z x-1・(x・z) →z e-1・(e・z) e・x → x e-1・z z

22 ３．完備化手続き(11/12) 標準的な完備化手続きは，もう少し複雑な処理をする
[書換え規則の右辺を書き換える] f(a) → b b → c f(a) → c b → c [書換え規則の左辺を書き換えて等式とする] この書換え規則の停止性は保証できなくなったので等式とする f(c) ＝ b f(a) → b a → c a → c

23 ３．完備化手続き(12/12) 例）標準的な完備化手続きによる 群論の完備化の結果
３．完備化手続き(12/12) 例）標準的な完備化手続きによる 　　 群論の完備化の結果

24 演習問題