Document

合流性を持たないTRSの
計算戦略に関する研究
情報工学コース坂部研究室
岡本晃治
項書換え系(Term Rewriting System : TRS)


関数型言語の計算モデル
書換え規則に従い項を書き換えて計算を実行
Ex:自然数の加算のTRS
R=
Add(s(x), y) → s(Add(x, y))
Add(0, y) → y
s(x) は x+1 を表す
Add(s(0), s(s(0)))
１＋２
項書換え系(Term Rewriting System : TRS)


関数型言語の計算モデル
書換え規則に従い項を書き換えて計算を実行
Ex:自然数の加算のTRS
R=
Add(s(x), y) → s(Add(x, y))
Add(0, y) → y
s(x) は x+1 を表す
Add(s(0), s(s(0))) →R s(Add(0, s(s(0)))) →R s(s(s(0)))
１＋２
＝
３
これ以上書き換えられない項(正規形)に到達し計算が完了
背景・研究目的

複数解を持つ問題のTRSは一般的に合流性を持
たない
Ex:自然数の加算の逆関数 Add-1
Add-1(3)
背景・研究目的

複数解を持つ問題のTRSは一般的に合流性を持
たない
Ex:自然数の加算の逆関数 Add-1
Add-1(3)
1つの正規形に到達する複数の
経路が存在するので
全ての空間を探索しなければならない
(3,
0)
(2,
1)
(1,
2)
(0,
3)
計算機上での自動計算には
極めて効率が悪い
背景・研究目的

複数解を持つ問題のTRSは一般的に合流性を持
たない
Ex:自然数の加算の逆関数 Add-1
Add-1(3)
(3,
0)
(2,
1)
(1,
2)
特定の書換え戦略で全正規形に
到達可能であることを示し
計算の効率の改善を図る
(0,
3)
最左最内戦略に着目
最左最内戦略

項中の最左かつ最内の書換え可能な部分(リデッ
クス)を書き換える
Ex
R=
f(x) → x
h(f(0), g(0))
g(x) → s(x)
h(x, y) → y
h, f, gの３つのリデックスが存在
最左最内戦略

項中の最左かつ最内の書換え可能な部分(リデッ
クス)を書き換える
Ex
R=
f(x) → x
h(f(0), g(0))
g(x) → s(x)
h(x, y) → y
R
R
R
h(0, g(0))
h(f(0),
s(0))
g(0)
書き換えるリデックスの選び方で
3つの項に書換えが分岐
最左最内戦略

項中の最左かつ最内の書換え可能な部分(リデッ
クス)を書き換える
Ex
R=
f(x) → x
h(f(0), g(0))
g(x) → s(x)
h(x, y) → y
lin
R
R
h(0, g(0))
h(f(0),
s(0))
g(0)
h(f(0), g(0))→R h(0, g(0))は最左最内の書換えであり
h(f(0), g(0))→lin h(0, g(0))と記す
主定理
TRS Rが
停止性を持つ
 右線形
 左辺の先頭でしか規則の重なりを許さない

という条件を満たすとき
主定理
TRS Rが
停止性を持つ
 右線形
 左辺の先頭でしか規則の重なりを許さない

という条件を満たすとき
書換え関係→Rによる
t1→R t2→R t3→R …といった
無限の系列が存在しない
主定理
TRS Rが
停止性を持つ
 右線形
 左辺の先頭でしか規則の重なりを許さない

という条件を満たすとき
f(x) → g(x, x) など
規則の右辺に同じ変数が
２度以上出現しない
主定理
TRS Rが
停止性を持つ
 右線形
 左辺の先頭でしか規則の重なりを許さない

という条件を満たすとき
f (g(x)) → x , g(x) → s(x)
などの左辺の先頭以外での
規則の重なりを禁ずる
主定理
TRS Rが
停止性を持つ
 右線形
 左辺の先頭でしか規則の重なりを許さない

という条件を満たすとき
最左最内戦略によって
全ての正規形に到達可能である
*
*
t→
s
かつ
s
が正規形
⇒
t
→
R
lin s
補題
線形な項 t と代入 に対して
を
t 中の全ての変数を正規形にする代入
 に書き換えてから
t を最左最内戦略で書換える様に
順番を入れ替えることが可能
t
*
lin
s
補題
線形な項 t と代入 に対して
を
t 中の全ての変数を正規形にする代入
 に書き換えてから
t を最左最内戦略で書換える様に
順番を入れ替えることが可能
t
*
lin
s
lin
*
in
*
t 
t 中の全ての変数 x に対して
x は正規形
主定理の証明(1/2)
*
 l R s という正規形 s への書換え系列が存在する
* s
とき l 
lin という書換え系列も存在することを示す

停止性を持つ関係 (R 　) を用いたNoetherian帰
納法

 は部分項の関係： f (x)  x
l (R  ) t である全ての t に
帰納法の仮定が適用可能
主定理の証明(2/2)
l
*
R
s
主定理の証明(2/2)
l
*

R
l

r
R
*
R
s
*
l 
s
l R r の部分で初めて
R の系列は

の位置(先頭)を書き換えている
主定理の証明(2/2)
l
*

R
l

r
R
*
l R r
+
：帰納法の仮定
s
lin
*
r 
s
R
*
r 
s
lin
主定理の証明(2/2)
l
*

R
l

r
R
*
lin
*
in
：帰納法の仮定
：補題の適用
s
lin
*
r 
*
r 
s
lin
*
*

r 
r

s
in
lin
主定理の証明(2/2)
l
*

R
l

r
R
ε< *
*
lin
*
in
R
l 
：帰納法の仮定
：補題の適用
： の条件
ε
lin
s
lin
*
r 
 (xVar(r))
x



x  x (xVar(l) Var(r))

 
l 
l εlinr 
主定理の証明(2/2)
l
*

ε<
*
R
l

r
R
ε< *
in
l 
：帰納法の仮定
：補題の適用
： の条件
ε
lin
s
lin
lin
*
R
lin
*
*
r 
l 
l
主定理の証明(2/2)
l
s
ε<
lin
*
*
lin
l 
ε
lin
r 
*
l 
s
lin
定理の適用例
R=
f(x)
g(x)
s(x)
h(x, y)
h(x, s(y))
h(f(0), g(0))
→ x
→
→ y
→x
定理の適用例
R=
f(x)
g(x)
s(x)
h(x, y)
h(x, s(y))
→ x
→
→ y
→x
2つの正規形に対して
6通りの書換え経路が存在
h(f(0), s(0))
R
R
h(f(0), g(0))
R
f(0
)
0
R
R
h(0, g(0))
R
R
R
g(0
)
h(0,
s(0))
R
R
R
s(0
)
定理の適用例
R=
f(x)
g(x)
s(x)
h(x, y)
h(x, s(y))
→ x
→
→ y
→x
最左最内戦略以外の
書換え系路に対して枝刈りが
可能となる
h(f(0), s(0))
R
R
h(f(0), g(0))
lin
f(0
)
0
R
lin
h(0, g(0))
lin
R
R
g(0
)
h(0,
s(0))
R
lin
R
s(0
)
まとめ
TRS Rが
停止性を持つ
 右線形
 左辺の先頭でしか規則の重なりを許さない

という条件を満たすとき
最左最内戦略で全ての正規形に到達可能
という定理を証明した
今後の課題

特定の戦略で全ての正規形に到達可能となるよう
なTRSのクラスの拡張

一般的な合流性を持たないTRSの全ての正規形が
効率よく求まる戦略の提案
関係 (  ) が停止性を持つことの証明
R
( R  ) が停止性を持たないと仮定すると


なる無限系列が存在する.
t0 
t

t

R 1
2
R t3  t4 
このとき t1 C[t2 ] , t3  C [t4 ] となる文脈 C,C’に対して



t0  R C[t2 ]  R C[C [t4 ]]  R という無限系列が存在する.
これは R が停止性を持つことに矛盾
関係 ( R  ) は停止性を持つ
右線形ではない場合の反例
f(x) → g(x, x)
b
R= a →
a →
c
最左最内戦略では
正規形 g (b,c), g (c,b)に
到達できない
f (a)
*
R
lin
lin
g (a,a)
f (b)
f (c)
R
lin
lin
g(b,b), g(b,c)
g(c,b), g(c,c)
g (b,b)
g (c,c)
停止性を持たない場合の反例
f(x) → b
R= f(x) → c
a → a
f (a)
R
R
lin
最左最内戦略では
無限の系列から抜け
出すことができない
b
c
f (a)
lin
f (a)
lin
f (a)
lin

 以外での重なりが存在する場合の反例
f(g(x)) → a
R=
g(x)
f (g (0))
→ b
R
lin
a
f (b)
最左最内戦略では
正規形 a に到達できない

Download Report