プログラム理論特論

表現系工学特論
項書換え系（４）
完備化
１．語問題と等式証明
２．合流性とチャーチ・ロッサ性
３．完備化手続き
(word problem) (equational proof)
１．語問題と等式証明
等式の集合
E
(a set of equations)
２つの項
s, t
語問題
(word problem)
(two terms)
s=t?
(decision)
等
式 f(g(x)) ＝ h(x)
書換え規則 f(g(x)) → h(x)
 等式の集合 E 及び２つの項 s , t が与えられたとき，
E のもとで s  t かどうかを判定する問題．

E を項書換え系 R とみなし，両方向の書換え（左辺→右辺，左辺←右辺）
によって， s から t を導ければ s  t である．その書換え列が「証明」
．
 両方向の書換えを  で表すと，s  t は 0 回以上の書換えで s から t を導
くことなので， s * t と書くこともある．
語問題の例：群論(group theory)
1
群(group)はつぎの等式の集合 E で定義される．群における語問題の例： a  a  e
( e1) 左単位元の存在
e  x  x


E   x 1  x  e
( e2) 左逆元の存在
( x  y )  z  x  ( y  z ) ( e3) 結合則


( r 1)
e  x  x

R   x 1  x  e
( r 2)
( x  y )  z  x  ( y  z ) ( r 3)

a  a 1  e  (a  a 1 )


 (a 1 )1  (a 1 )  (a  a 1 )


 (a 1 )1   (a 1  a)  a 1 
 (a 1 )1   e  a 1 
 (a 1 )1  (a 1 )  ( a  a 1 )
 (a 1 )1  a 1
e
◆右辺（単純な項）から左辺（複雑な項）への
書換えを含むので探索が困難
◆左辺≠右辺であることの判定が困難
２．合流性とチャーチ・ロッサ性(1/8)
会同性
会同性(joinability)
ab
a * c かつ b * c を満たす c  A が存在する
a b
a
b
●
●
●
c
a=b の書換え証明
２．合流性とチャーチ・ロッサ性(2/8)
合流性
合流性(confluent)
任意の a, b, c  A に対して， a * b かつ a * c ならば b  c ．
a
*
完備性＝停止性＋合流性
(complete)
*
b
c
*
*
d
合流性
２．合流性とチャーチ・ロッサ性(3/8)
チャーチ・ロッサ性
チャーチ・ロッサ性(Church-Rosser property：CR 性)
任意の a , b  A に対して， a * b ならば a  b
（ a  b ならば a  b ）
*
a
b
a
b
*
*
c
チャーチ・ロッサ性
書換え証明
２．合流性とチャーチ・ロッサ性(4/8)
書換え証明
a  b の書換え証明(rewrite proof)
a  b から得られる書換え列 a  
チャーチ・ロッサ性のないシステムの例
a
e
b
c
d
図１
a  e の書換え証明 a  b  d  e
c  e の書換え証明はない．
c 
b．
２．合流性とチャーチ・ロッサ性(5/8)
CR性 ⇒ 合流性
■定理 (合流性  ＣＲ性)
合流性がある  チャーチ・ロッサ性をもつ．
（CR 性  合流性
の証明）
a * b かつ a * c ならば b * c なので，CR 性より b  c ．
*
a
a
b
*
a
b
*
*
*
b
c
*
*
c
d
チャーチ・ロッサ性
合流性
２．合流性とチャーチ・ロッサ性(6/8)
合流性 ⇒ CR性
（合流性  CR 性の証明: Case 1）
a * b の長さによる数学的帰納法．
a  a1 * b （Case 1） a  a1 * b （Case 2）
a
a1
*
induction
* *
c
(Case 1)
b
a
*
a
*
b
*
b
c
*
*
a
b
*
*
d
c
合流性
チャーチ・ロッサ性
２．合流性とチャーチ・ロッサ性(7/8)
合流性 ⇒ CR性
（合流性  CR 性の証明: Case 2）
a * b の長さによる数学的帰納法．
a  a1 * b （Case 2）
a
*
a
*
b
*
b
c
*
*
a
b
*
*
d
c
合流性
チャーチ・ロッサ性
a
a1
*
induction
* 合流性 * *
c
*
d (Case 2)
b
２．合流性とチャーチ・ロッサ性(8/8)
完備な書換え系による語問題の解法
■定理 (完備な書換え系による語問題の解法)
書換え系が完備であるとき， s * t である必要十分条件は，
s の正規形と t の正規形が一致することである．
s
t
●
●
●
s＝t
●
●
正規形
s
t
●
●
●
●
s’ t’
正規形正規形
s≠t
もし s=t ならば，s’=t’となるが，その書換え証明
が存在しないので，CR性に矛盾する．
３．完備化手続き(1/12)
等式の集合
E
成功：完備な書換え系 R
停止性を保証するように
等式を向き付けるための
簡約順序
＞
たとえば，各記号の重さ
完備化
手続き
失敗：向き付けできない等式
発散：成功も失敗もせず，
無限に計算し続ける
(completion procedure)
Knuth & Bendix (1970)
３．完備化手続き(2/12)
初期状態
基本的な完備化手続き：等式の集合 E と書換え規則の集合 R の対 ( E, R)
を手続きの「状態」として，以下の考え方で状態を遷移させる．
(initial state)
［初期状態］手続きを開始するときに，
E ＝入力で与えられた等式の集合，
R ＝空集合とする．
E
R
f(a) = b
a=c
３．完備化手続き(3/12)
等式の向き付け (orient an equation)
［等式の向き付け］ E に含まれる任意の等式 s  t を E から削除し，
現在の R を用いて s  t の両辺を書き換えて正規形 s '  t ' を計算する．

s ' と t ' が異なる項ならば，これを停止性が保証される方向に向き付
けて，書換え規則（ s '  t ' または t '  s ' ）として R に追加する．

s ' と t ' が同一の項ならば s '  t ' は自明な等式なので削除する．
s
t
●
●
●
●
s’＞ t’
正規形正規形
３．完備化手続き(4/12)
等式の向き付け（続き）
f(a) ＝ b
a＝c
a＝c
f(a) → b
重さ
a: 2
b,c,f: 1
f(a) → b
a→c
３．完備化手続き(5/12)
危険対の生成 (deduce critical pairs)
［危険対の生成］ R に含まれる２つの書換え規則の重なり s u t から
危険対 s, t を生成し，それを等式 s  t として E に追加する．
f(a) → b
f(c) ＝ b
左辺に重なりがある
a→c
f(a) → b
a→c
f(a) → b
a→c
f(a)
f(c)
＝
危険対
b
３．完備化手続き(6/12)
終了条件
［終了条件］
 現在の R から危険対をすべて生成済みで，かつ，
E が空集合になったら成功．この時点の R を出力する．
 停止性が保証される方向に向き付けられない等式が存在したら失敗．
 成功も失敗もせず，無限に実行を続けることもある（発散）
．
f(c) ＝ b
f(a) → b
a→c
空集合
f(a) → b
a→c
f(c) → b
成功
完備な書換え系
３．完備化手続き(7/12)
完備化手続きの正当性
完備化手続きの正当性
成功した時点で，
R は停止性が保証され，かつ，
すべての危険対 s, t は会同（ s  t ）している
ので，ニューマンの補題と危険対定理（前回参照）により，
R は合流性をもつ．ゆえに， R は完備である．
●
s
危険対
●
●
正規形
t
＝
●
●
s’ ＞ t’正規形
危険対の生成
等式の向き付け
３．完備化手続き(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
３．完備化手続き(9/12)
例）群論の完備化(2/3)
危険対の生成
e・x → x
x-1・x → e
(x・y)・z → x・(y・z)
(x・y)・z → x・(y・z)
e・x → x
(e・x)・z
x・z
e・(x・z)
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)
(x・y)・z → x・(y・z)
x-1・x → e
(x-1・x)・z
e・z
(x・y)・z → x・(y・z)
(x・y)・z → x・(y・z)
((x・y)・z)・w
x-1・(x・z)
(x・(y・z))・w
(x・y)・(z・w)
３．完備化手続き(10/12)
例）群論の完備化(3/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)
等式の向き付け
危険対の生成
x-1・(x・z) →z
e・x → x
e-1・z ＝ z
e・x → x
x-1・x → e
(x・y)・z → x・(y・z)
x-1・(x・z) →z
e-1・(e・z)
e-1・z
z
３．完備化手続き(11/12)
標準的な完備化手続きは，もう少し複雑な処理をする
[書換え規則の右辺を書き換える]
f(a) → b
b→c
f(a) → c
b→c
[書換え規則の左辺を書き換えて等式とする]
f(c) ＝ b
f(a) → b
a→c
a→c
この書換え規則の停止性は保証
できなくなったので等式とする
３．完備化手続き(12/12)
例）標準的な完備化手続きによる
群論の完備化の結果
e  x  x

1

x  x  e
R
( x  y )  z  x  ( y  z )
 1

x  ( x  z)  z
( r 1)
x  x 1  e
( r 9)
( x 1 ) 1  e
( r 2)
x e  x
( r 10)
( x  y ) 1  y 1  x 1 ( r 20)
( r 3)
y  ( y 1  x)  x ( r 11)
( r 4)
e 1  e
( r 12)
群論の語問題 a  a1  e に対して，(r9)により，ただちに書換え証明 a  a1  e を
示すことができる．
a  (b  a1)  b は両辺の正規形が異なる（両辺ともすでに正規形）なので，
a  (b  a1)  b である．
( r 13)
演習問題
任意の文字 a は， a( x) という項を表すと考えよう．
同様に，文字列 ab は項 a (b( x )) ， abc は a(b(c( x))) を表す．
ab  c のような「文字列書換え規則」は，項書換え規則 a(b( x))  c( x) を表す．
たとえば，この書換え規則を用いた dabd  dcd という書き換えは，
d (a(b(d ( x))))  d (c(d ( x))) という項書換えに対応する．
文字列間の等式の集合 E  ab  a, bc  a を考える．
(1) E を完備化して，完備な書換え系 R を求めよ．
（停止性を保証するために，
a  b  1, c  2 という重みを定義し，左辺と右辺のうち，重みの和が大きい方
から小さい方に等式を向き付けよ．
）
(2) R を用いて， bcc  bca の書換え証明を示せ．
(3) R を用いず， E を直接用いて， bcc  bca の証明を示せ．
(4) R を用いて， cbc  bcb であることを示せ．

Download Report