弱最内戦略を完全にするためのTRSの等価変換について 名古屋大学大学院 情報科学研究科 岡本　晃治

書換え規則が適用不能な項（正規形）に到達 項書換え系(TRS) 関数型プログラミング言語の計算モデル 書換え規則で項を書換えて計算 例：自然数の加算のTRS R = Add(s(x) , y) → s(Add(x , y)) 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) 例: 例: f (g(x)) → x R= f (x) → s(x) f (g(h(0))) f (g(0)) h(x) → x s(g(0)) s(g(h(0))) ： 最内戦略の書換え Rにおいて最内戦略は完全な書換え戦略

研究概要・目的(1/2) 合流性を持たないTRSの計算戦略 最内戦略が完全となるTRSの条件の発見 弱最内戦略が完全となるTRSの条件 冗長な書換えの枝刈りが可能 弱最内戦略が完全となるTRSの条件 最内戦略が完全とならないTRS 合流性：規則の適用順序によらず 同一の正規形に到達

研究概要・目的(2/2) 深さ優先探索で37ステップの書換えが必要 H(0) → 0 H(0) → s(0) R= H(s(x)) → U(H(x)) U(x) → s(s(x)) H：自然数を1/2倍する関数の逆関数 H(s2(0)) H(s2(0)) U(H(s(0))) s2(H(s(0))) U2(H(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))) U(s3(0)) s4(0) s5(0) 深さ優先探索で37ステップの書換えが必要

8ステップの最内書換えで全正規形に到達可能 研究概要・目的(2/2) H(0) → 0 H(0) → s(0) R= H(s(x)) → U(H(x)) U(x) → s(s(x)) H：自然数を1/2倍する関数の逆関数 H(s2(0)) U(H(s(0))) s2(H(s(0))) U2(H(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))) U(s3(0)) ：最内書換え s4(0) s5(0) 8ステップの最内書換えで全正規形に到達可能

リデックスf(g(0))は最内リデックスg(0)と重なりを持つ 弱最内戦略 最内リデックスもしくは最内リデックスと重なりを持つリデックスを書き換える戦略 f (s(0)) wi(R) f (g(x)) → x R= g (x) → s(x) f (g(0)) wi(R) リデックスf(g(0))は最内リデックスg(0)と重なりを持つ g(0)はf(g(0))の 最内リデックス

例 項f(h(a,b))には,c,g(d)の 2つの正規形が存在 最内戦略が完全にならないTRS → → → → → f(h(a,b)) g(h(a,x)) → c s(h(a,b)) f(h(b,b)) f(d) h(x,b) → d R = f(x) → s(x) g(h(a,b)) s(h(b,b)) s(d) s(x) → g(x) a → b c g(h(b,b)) g(d) 項f(h(a,b))には,c,g(d)の 2つの正規形が存在 : R

例 Rによる弱最内書換えでは cに到達できない 最内戦略が完全にならないTRS → → → → → f(h(a,b)) g(h(a,x)) s(h(a,b)) f(h(b,b)) f(d) h(x,b) → d R = f(x) → s(x) g(h(a,b)) s(h(b,b)) s(d) s(x) → g(x) a → b c g(h(b,b)) g(d) Rによる弱最内書換えでは cに到達できない : R : wi(R)

例 最内戦略が完全にならないTRS → → → → → → → 弱最内書換えで cに到達できるように規則を追加 f(h(a,b)) g(h(a,x)) → c h(x,b) → d s(h(a,b)) f(h(b,b)) f(d) f(x) → s(x) s(x) → g(x) R2 = a → b g(h(a,b)) s(h(b,b)) s(d) s(h(a,x)) → g(h(a,x)) f(h(a,x)) → s(h(a,x)) c g(h(b,b)) g(d) 弱最内書換えで cに到達できるように規則を追加 : R2 : wi(R2)

弱最内戦略を完全にする等価変換(1/4) TRS Rの左辺の部分集合M(R) 規則の重なりに注目 → 他の規則と重なる 部分に注目 → → g(h(a,x)) → c 他の規則と重なる 部分に注目 h(x,b) → d R = f(x) → s(x) s(x) → g(x) a → b M(R)={g(h(a,x))}

弱最内戦略を完全にする等価変換(2/4) 集合M(R)から規則を追加 M(R)の要素とマッチング可能な右辺に注目 g(h(a,x)) → g(x’)とg(h(a,x))の最凡単一化子 　　　　　　　　　　　　　に対して, 規則　　　　　　　　　　を追加 c h(x,b) → d R = f(x) → s(x) s(x) → g(x) a → b M(R)={g(h(a,x))} R’={s(h(a,x)) → g(h(a,x))}

新しい規則が追加されなくなるまでTを実行 弱最内戦略を完全にする等価変換(3/4) T(R) = R ∪R’とする 新しい規則が追加されなくなるまでTを実行 T2(R) = f(x) s(x) g(h(a,x)) h(x,b) a g(x) c d b → s(h(a,x)) f(h(a,x)) M(T(R))={g(h(a,x)), s(h(a,x))} T3(R)=T2(R) g(h(a,x)) → c h(x,b) → d f(x) → s(x) T(R) = s(x) → g(x) a → b s(h(a,x)) → g(h(a,x))

新しい規則が追加されなくなるまでTを実行 弱最内戦略を完全にする等価変換(4/4) 集合M(R)の定義 l|pとl’が単一化可能 変換Tの定義 がr|pとl’の最凡単一化子} 新しい規則が追加されなくなるまでTを実行

予想 Rを停止性を持つ右線形TRSとする. Ti(R)=Ti+1(R)である自然数iが存在するとき R ⇒ T(R) ⇒T(T(R)) ⇒･･･⇒Ti(R) = T(i+1)(R) ∀t, s. t →R s ∈ NFR 　⇒ t →wi(Ti(R)) s