最内戦略に基づく項書換え計算の効率化の研究

Presentation on theme: "最内戦略に基づく項書換え計算の効率化の研究"— Presentation transcript:

1 最内戦略に基づく項書換え計算の効率化の研究
計算機数理科学専攻 酒井研究室 岡本 晃治

2 項書換え系（TRS） 関数型プログラミング言語の計算モデル 書換え規則で項を書き換えて計算 例：自然数の加算のTRS
Add(s(x), y) s(Add(x,y)) 規則が適用不能な 正規形に到達 R = Add(0, y) y s(x)：x+1 Add(s(0),s(s(0))) s(Add(0,s(s(0)))) s(s(s(0))) =

3 TRSの完全な書換え戦略 任意の項の全正規形に到達可能 書換え戦略：書き換えるリデックスの選び方 h(0) R= f(g(x)) x
R= f(g(x)) x f(x) h(x) s(x) f(g(h(0))) f(g(0)) ： 最内戦略の書換え s(g(h(0))) s(0) Rに対して最内戦略は完全

4 研究背景・目的 合流性を持たないTRSの計算戦略 完全な戦略を持つTRSの発見 関数の逆計算 複数解を持つ問題のTRS 書換えの枝刈りが可能
最内戦略に基づく戦略 合流性：計算結果が一意

5 研究成果 最内戦略が完全となる条件 弱最内戦略が完全となるTRS オーバーレイ 内側危険対右向き合流性 等価変換 T
[2003年度 電気関係学会東海支部連合大会] [2004年度 冬のLAシンポジウム]

6 与えられた項の全正規形に最内戦略で到達可能
最内戦略の完全性定理[岡本ら ‘03] 停止性 右線形 オーバーレイ であるTRSに対して最内戦略は完全 規則の右辺に2度以上 現れる変数が存在しない Rの規則による無限の 書換えがない 与えられた項の全正規形に最内戦略で到達可能 ｌ

7 オーバーレイTRS どの規則も左辺の先頭以外で重ならない R1はオーバーレイ R2はオーバーレイではない x f(g(x)) f(x)
先頭以外での重なり：規則 l1→r1 , l2→r2に対してl1の変数以外 の真部分項とl2が等しくなる代入が存在 x f(g(x)) f(x) R1= R1はオーバーレイ R2= f( g(x) ) x g(x) R2はオーバーレイではない

8 8ステップの最内書換えで全正規形に到達可能
例 H(0) R= H(s(x)) U(x) H：自然数を半分にする関数の逆関数 s(0) U(H(x)) s(s(x)) H(s2(0)) s2(H(s(0))) s2(U(H(0))) U(s2(H(0))) s2(U(0)) s4(H(0)) s2(U(s(0))) ：最内戦略の書換え U(s3(0)) s5(0) s4(0) U(H(s(0))) U2(H(0)) s2(H(s(0))) U2(0) s2(U(H(0))) U(s2(H(0))) U2(s(0)) s2(U(0)) U(s2(0)) s4(H(0)) s2(U(s(0))) 8ステップの最内書換えで全正規形に到達可能 深さ優先探索で37ステップの書換えが必要

9 最内戦略の完全クラスの拡張 全ての規則の重なりを 許せないか? 最内戦略が完全となる条件 先頭以外での重なりによって 分岐した書換えは合流
停止性 右線形 オーバーレイ 内側危険対右向き合流性 全ての規則の重なりを 許せないか? 先頭以外での重なりによって 分岐した書換えは合流 オーバーレイTRSはこの性質を持つ

10 内側危険対右向き合流性を持たないTRS 先頭以外での重なりを持ち，そのような重なりからの書換えの分岐が合流しない 最内戦略は不完全 f(a)
f(b) c 到達不可能 R= f( a ) c a b ： 最内戦略の書換え 最内戦略は不完全 先頭以外での重なりを扱える戦略が必要

11 弱最内戦略 最内リデックス 又は 最内リデックスと重なる リデックスを書き換える R= f( g(x) ) x g(x) f(g(0))
最内リデックス　又は　最内リデックスと重なる 　　リデックスを書き換える R= f( g(x) ) x g(x) f(0) f(g(0)) 書換え規則の重なり f(g(0))はg(0)と重なりを持つ g(0)はf(g(0))の最内リデックス

12 f(a)→h(a) : Rの弱最内ブリッジ規則
弱最内戦略が不完全な例[1/2] R’= f(a) h(a) R= f(x) h(x) g(h(a)) c a b g(f(a)) g(f(b)) g(h(a)) g(h(b)) c d 到達不可能 到達可能 ： 弱最内戦略の書換え 弱最内ブリッジ規則f(a)→h(a)をどのように得るのか Rに規則f(a)→h(a)を追加 f(a)→h(a) : Rの弱最内ブリッジ規則

13 弱最内戦略が不完全な例[2/2] Rの重なり発生リダクション 弱最内戦略を不完全にする書換え aと重なる弱最内リデックスを 書き換える
f(x) h(x) g(h(a)) c a b g(h(a)) g(h(a)) c 到達不可能 g(f(a)) ： 弱最内戦略の書換え g(f(b)) g(h(b)) d Rの重なり発生リダクション aと重なる弱最内リデックスを 書き換える 弱最内リデックスaが f(x)の変数xに代入 弱最内リデックスを 書き換えない h(x)の変数に代入された aに重なるリデックスが発生 ￢wi（R) p wi（R)

14 弱最内戦略を完全にする等価変換 T 重なり発生リダクションから規則を得る T(R)= f(a) h(a) R= f(x) h(x)
g(h(a)) c a b ￢wi（R) p wi（R) T(R) = R ∪ {l→r | l→rはRの弱最内ブリッジ規則} T i(R) = R T(T i-1(R)) (i > 0) (i = 0) Rの弱最内ブリッジ規則

15 定理 任意の項s,正規形t に対し s→Rt ならば s→wi(Ti(R))t Rを停止性を持つ右線形TRSとする
Ti(R)=Ti+1(R)である自然数 i が存在するとき 弱最内戦略はTi(R)に対して完全 任意の項s,正規形t に対し s→Rt　ならば　s→wi(Ti(R))t *

16 例(1/2) T2(R)には新しい規則を追加する 重なり発生リダクションは無く T2(R)=T3(R) T(R)の重なり発生リダクション
f(h(a , x)) s(h(a , x)) T(R)の重なり発生リダクション g(h(a , x)) s(h(b , x)) f(x) s(x) g(h(a , x)) h(x , b) a g(x) c d b R = s(h(a , x)) g(h(a , x)) c Rの重なり発生リダクション R = T(R) = f(h(a , x)) s(h(a , x)) T2(R) = s(h(a , x)) g(h(a , x)) R = T(R) = T(R)の弱最内ブリッジ規則 f(h(a , x)) s(h(a , x)) Rの弱最内ブリッジ規則 s(h(a , x)) g(h(a , x)) T2(R)には新しい規則を追加する 重なり発生リダクションは無く T2(R)=T3(R) ： 弱最内戦略の書換え

17 例(2/2) f(h(a,b)) f(x) s(x) g(h(a , x)) h(x , b) a g(x) c d b R =
T(R) = s(h(a , x)) f(h(a , x)) T2(R) = f(x) s(x) g(h(a , x)) h(x , b) a g(x) c d b R = ： T2(R)の規則による 弱最内戦略の書換え g(h(b,b)) s(h(b,b)) ： Rの規則による 弱最内戦略の書換え f(h(b,b)) f(d) s(h(a,b)) g(d) s(d) c g(h(a,b)) g(h(b,b)) s(h(b,b)) c,g(d)の両方に計７ ステップの T2(R)の弱最内書換えで到達可能 cに到達不可能なので 弱最内戦略はRに対して完全ではない 正規形の全解探索には深さ優先で ２２ステップが必要 変換Tによって TRS T2(R)を作成

18 まとめ 最内戦略 弱最内戦略 変換 最内戦略・弱最内戦略の完全クラスの関係 右線形 停止性 ：発表内容 非消去性 オーバーレイ
弱オーバーレイ 内側危険対 右向き合流性 最内戦略・弱最内戦略の完全クラスの関係 ：発表内容

19 今後の課題 変換Tが停止する条件 一般に変換Tは停止性を持たない 変換回数の上限が決定可能となる条件

20 変換が停止しない例 ・・・ f(h(・・・h(x)・・・)→ g(h(・・・h(x)・・・)
g(x) c f(x) f(h(x)) R = R = f(h(h(x))) g(h(x)) T2(R) = T3(R) = f(h(h(x))) g(h(x)) g(h(h(x))) R = g(h(x)) f(h(x)) T(R) = T2(R)の重なり発生リダクション g(h(h(x))) f(h(h(x))) g(h(x)) T(R)の重なり発生リダクション f(h(h(x))) g(h(x)) f(h(x)) Rの重なり発生リダクション g(h(x)) f(h(x)) g(x) T2(R)の弱最内ブリッジ規則 g(h(h(x))) f(h(h(x))) Rの弱最内ブリッジ規則 g(h(x)) f(h(x)) T(R)の弱最内ブリッジ規則 f(h(h(x))) g(h(x)) ・・・ f(h(・・・h(x)・・・)→ g(h(・・・h(x)・・・) g(h(・・・h(x)・・・)→ f(h(・・・h(x)・・・) の規則が無限に追加

21 定理 2 Rを停止性を持つ右線形TRSとする 項 s, 正規形 t, 自然数 nに対して s t ならば，n以下の自然数kが存在し s t
* t wi(Tk(R)) ステップ数が変換回数の上限になる