メタ項書き換え計算における単純メタ項の停止性に関する研究

メタ項書き換え計算における
左辺正規性を持つ
メタ項の停止性について
名古屋大学大学院情報科学研究科
蛸島洋明酒井正彦坂部俊樹
1
項書き換え系（ＴＲＳ）


関数型言語の計算モデル
左辺項と右辺項からなる書き換え規則の有限集合
(例)
f(x) → x
a → f(b)
出力項
入力項
a
f(b)
b
2
メタ項とその書き換え
[a  [b  c]d ]
[b  c]
a
項
規則
メタ項の書き換えの特徴
•規則は上の規則で書き換えることができる
3
メタ項とその書き換え
[a  [b  c]d ]
[b  c]
a
規則中に規則を
含むことが可能
メタ項の書き換えの特徴
•規則は上の規則で書き換えることができる
4
メタ項とその書き換え
[a  [b  c]d ]
[b  c]
a
[a  [b  c]d ]
[b  c]
[b  c]
d
メタ項の書き換えの特徴
•規則は上の規則で書き換えることができる
5
メタ項とその書き換え
[a  [b  c]d ]
[b  c]
a
[a  [b  c]d ]
[b  c]
[b  c]
d
[a  [b  c]d ]
[b  c]
[c  c ]
d
メタ項の書き換えの特徴
•規則は上の規則で書き換えることができる
6
メタ項書き換え計算（ＭＲＣ）
ＴＲＳの記述・実行・検証を目的として提案さ
れた計算モデル
 ＴＲＳの等価性証明の自動化などに応用可能

 MRCの停止性が判定できると
・メタ項の書き換えの結果が確実に得られる
・他の性質を調べるときに容易になる
7
目的

メタ項の停止性判定法を明らかにする
8
研究内容

左辺正規性の定義

単純メタ項からTRSへの変換 

単純メタ項の停止性の判定定理

左辺正規性に関する考察
9
単純メタ項[洪 ‘９９]
規則の両辺に規則を含まないメタ項
単純ではないメタ項
[ x. f ( x)  [ x.g ( x)  h( x)] f (a )]
g (b)
右辺に規則が含まれている
単純メタ項
h( a )
[ x.h( x)  f ( x)]
[ x. f ( x)  g ( x)]
10
左辺正規性
規則の左辺が書き換え不可能

左辺正規性を持たないメタ項
[ x. f ( x)  g ( x)][ x. f ( g ( x))  h( x)] g (a)
f ( g ( x)) が [ x. f ( x)  g ( x)]によって書き換えられる

左辺正規性を持つメタ項
[ x. f ( x)  g ( x)][ x.h( x)  g ( x)]g (a)
11
単純メタ項の停止性判定法
１．単純メタ項
TRS
M
 (M )
変換
２．  (M ) の停止性を判定する
・TRSの停止性判定法を利用
 (M ) に停止性がある
M に停止性がある
12
単純メタ項からＴＲＳへの変換 
 M   0
・ M  a  Namesのとき
・ M   f1 / ･･･f m / x1....xn .L  RM' のとき
 M   x1...xn .L  R   M' 
・ M  M 0 M1,･･･,M k  のとき
 M    M 0    M1  ･･･  M k 
メタ項中の規則を取り出してTRSを生成
(例
) M  [ x. f ( x)  g ( x)]
[ x.g ( x )  h( x )]
f (a)
 ( M )  {x. f ( x)  g ( x),
x.g ( x)  h( x)}
13
定理
定理
単純メタ項Mが左辺正規であるとする。
このとき、TRS M  が停止性を持つならば、
Mは停止する。
14
定理を証明するための補題

補題1 左辺正規性を持つ単純メタ項を
書き換えても左辺正規性は保たれる

補題2 M：左辺正規性を持つ単純メタ項
M → Nのとき L  R    N    M 
L * R
について
 M 
15
定理の証明
定理
単純メタ項Mが左辺正規であるとする。このとき、TRS
が停止性を持つならば、Mは停止する。
M 
証明方法 Mの書き換えが停止しないならば、TRS
 M 
も停止しないことを示す。
t0  t1  ･･･ ti  ti 1  ･･･
   
 t0 　 t1 　 ti 　 ti 1 
任意の項a,bと任意のiについて
 b
a   b ならば a 
 ti 1 
 ti 
16
単純メタ項の停止性判定例

M:左辺正規性を持つ単純メタ項
M  [ x.g ( x)  h( x)][ x. f ( x)  g ( x)] f (a)について
 M   x.g  x   h x , x. f  x   g  x 
再帰経路順序[Dershowitz ‘82]を用いると M は停止す
る定理よりMは停止性を持つ
[ x.g ( x)  h( x)][ x. f ( x)  g ( x)] f (a)
↓
[ x.g ( x)  h( x)][ x. f ( x)  h( x)] f (a)
↓
[ x.g ( x)  h( x)][ x. f ( x)  h( x)]h(a)
17
予想
左辺正規性を保つ単純メタ項の停止性が判定可能

左辺正規性を保つメタ項についても
停止性を判定できると予想
考察
•メタ項が左辺正規性を保ち続ける条件とは？
18
左辺正規性を保つメタ項の調査
(1/2)
規則中に規則を持つメタ項
[a  [b  c]d ]
[b  c]
a
[a  [b  c]d ]
[b  c]
[b  c]
d [b  c] によって
書き換えられる
左辺正規性を保つことができない
19
左辺正規性を保つメタ項の調査
(1/2)
規則中に規則を持つメタ項
[a  [b  c]d ]
[b  c]
a
このbが書き換え
られないようにす
ればよい
[a  [b  c]d ]
[b  c]
[b  c]
d
左辺正規性を保つことができない
20
左辺正規性を保つメタ項の調査
(2/2)
規則の中の規則の左辺を隠蔽したメタ項
[ x. f ( x)  [b / b  c]x]
f ([b  c]b)
規則中のbは他の規則に
よって書き換えられない
全ての規則の左辺を隠蔽したメタ項
[ a / a  b]
[a / a  [b / b  c]c]
b
21
左辺正規性を保つメタ項の調査
(2/2)
規則の中の規則の左辺を隠蔽したメタ項
[ x. f ( x)  [b / b  c]x]
[ x. f ( x)  [b / b  c]x]
f ([b  c]b)
[b / b  c] [b / b  c] によって
書き換えられる
[b  c]b
左辺正規性を保つことができない
全ての規則の左辺を隠蔽したメタ項
[ a / a  b]
左辺正規性が
[a / a  [b / b  c]c]
保たれることは自明
b
22
まとめと今後の課題
まとめ
 左辺正規性を持つ単純メタ項の停止性の判
定法を与えた
 メタ項の左辺正規性について考察した
今後の課題
 メタ項が左辺正規性を保つことができる非自
明な条件の発見
23

Download Report