多項式解釈と停止性

表現系工学特論
項書換え系（２）
多項式解釈と停止性
１．項書換え系の基本用語と記法 (1/4)
変数の集合 V   x, y, z,

関数記号の集合 F   f , g , h,
定数（ 0,1,
, a, b, c,

）も引数をもたない関数記号
項の集合 T ( F ,V )
項とは変数または定数または関数記号(項,…,項)の形をした式．
書換え規則：項の順序対 l  r ．
項書換え系：有限個の書換え規則の集合 R ．
１．項書換え系の基本用語と記法 (2/4)
代入  : V  T ( F ,V )
各変数 x  V に項  ( x)  T ( F ,V ) を割り当てる写像．
   x1
 ( x1 ), , xn
 ( xn ) の形で表現する．
代入の適用  (t )
項 t に出現している各変数 x をすべて項  ( x) で置き換えた
項を  (t ) と書く．
（例）    x
a, y
f (b) のとき，
 ( f ( g ( x, y)))  f ( g (a, f (b)))
１．項書換え系の基本用語と記法 (3/4)
インスタンス
 (t )  s となる代入  が存在するとき，
s は t のインスタンスであるという．
（例） f (g (a) ) は f (x) のインスタンス
１．項書換え系の基本用語と記法 (4/4)
簡約関係  R
ある書換え規則 l  r  R の左辺のインスタンス  (l ) が
項 s の部分項として含まれていて，
 (l ) を  (r ) に置き換えたときに，
s が t になるとき s  R t と書く．
（例）書換え規則 f(x) → g(x)
書換え関係 h(f(a)) →R h(g(a))
２．停止性の決定不能性 (1/2)
停止性
どんな初期項 t 0 からも，書換えの無限列 t0  R t1  R t2  R
が
存在しないこと．
（例１）
 f (0,1, x)  f ( x, x, x)

R   g ( x, y )  x
 g ( x, y )  y

は停止性をもたない．
f ( g (0,1), g (0,1), g (0,1))
 R   R f (0,1, g (0,1))
 R f ( g (0,1), g (0,1), g (0,1))
２．停止性の決定不能性 (2/2)
定理１（停止性は決定不能）
項書換え系の停止性は決定不能である．
すなわち，任意の項書換え系 R を入力として受け取り，それが
停止性をもつかどうかを有限時間内で判定するアルゴリズムは存
在しない．
３．簡約順序 (1/4)
整礎
無限下降列 a1
a2
a3
（ ai  A, i  1 ）が存在しないこと．
書換え順序
項の集合 T ( F ,V ) 上で定義されたつぎの条件を満たす
厳格半順序
のこと．
単調性：局所的な減少が大域的な減少となる．
すなわち，任意の項 s, t について：
s
t ならば f ( , s, )
f ( , t, )
安定性：代入により順序が変化しない．
すなわち，任意の項 s, t と代入  について：
s
t ならば  ( s)  (t )
３．簡約順序 (2/4)
簡約順序
整礎な書換え順序のこと．
定理２（停止性の必要十分条件）
項書換え系 R が停止性をもつ必要十分条件は，
すべての書換え規則 l  r  R について l
となる簡約順序
r
が項の集合 T ( F ,V ) の上に存在することである．
３．簡約順序 (3/4)
（例２）
項 t のサイズ（含まれる変数および関数記号の総数）を | t | と書く．
また，項 t に変数 x が現れている回数を | t |x と書く．
s
t
 | s |  | t | and | s |x  | t |x for all x  V
と定義すると，
は簡約順序である．
したがって，つぎの R は停止性をもつ．
nand ( x, x)  not ( x)

R
not (nand ( x, y ))  and ( x, y )
３＞２
４＞３
３．簡約順序 (4/4)
（例３）
変数に重み 1，関数記号 f に正の整数の重み w f を与え，
項 t の重みの総和を w(t ) と書く．
s
t
と定義すると，
 w(s)  w(t ) and | s |x  | t |x for all x  V
は簡約順序である．
したがって，つぎの R は停止性をもつ．
not (and ( x, y ))  or (not ( x), not ( y ))
R
not (not ( x))  x
w(not )  w(or )  1, w(and )  3
３＞１
６＞５
４．多項式解釈に基づく停止性証明 (1/6)
単調関数による解釈
A  {1,2,3, } を正の整数の集合とし，
各関数記号 f  F に A の上で定義された関数 f A : A   A  A を
対応させる． f A はつぎの式で定義される単調なものとする．
単調性： a  b 
f A ( , a, )  f A ( , b, )
項 t T ( F ,V ) に現れているすべての変数 x  V を A 上を動く変数
x  A と解釈し，各関数記号 f を A 上の単調な関数 f A と解釈して
できる数式を  (t ) とする．
f A と  (t ) をそれぞれ f と t の解釈という．
４．多項式解釈に基づく停止性証明 (2/6)
（例４）
f A ( x, y )  2 x  y  1, g A ( x, y)  xy のとき，
 ( g ( x, f ( y, z )))  g A ( x, f A ( y, z ))
 g A ( x, 2 y  z  1)
 x(2 y  z  1)
 2 xy  xz  x
４．多項式解釈に基づく停止性証明 (3/6)
解釈に基づく半順序
項の集合 T ( F ,V ) 上の半順序 A をつぎの式で定義する．
s A t   ( s )   (t )
ただし，不等式  (s)   (t ) は，含まれる変数が A のどの値をとっても
成り立つことを表す．
定理３すべての関数記号 f  F の解釈 f A が単調ならば，
A は項の集合 T ( F ,V ) 上の簡約順序である．
４．多項式解釈に基づく停止性証明 (4/6)
系４（解釈に基づく停止性証明）
すべての書換え規則 l  r  R について  (l )   (r ) となる単調な解
釈が存在すれば， R は停止性をもつ．
多項式解釈
f A が多項式のときの解釈を多項式解釈という．
多項式のすべての係数を正の整数とし，かつ，
式の値がすべての変数に依存するようにすれば，その多項式は単調．
４．多項式解釈に基づく停止性証明 (5/6)
（例５）
and ( x, or ( y, z ))  or (and ( x, y ), and ( x, z ))
R
or (or ( x, y ), z )  or ( x, or ( y, z ))
（停止性の証明）
A  {2,3,4, } ， orA ( x, y )  2 x  y  1, and A ( x, y )  xy とすると，
 (and ( x, or ( y, z )))  x(2 y  z  1)
 2 xy  xz  x
 2 xy  xz  1
  (or (and ( x, y ), and ( x, z )))
４．多項式解釈に基づく停止性証明 (6/6)
and ( x, or ( y, z ))  or (and ( x, y ), and ( x, z ))
R
or (or ( x, y ), z )  or ( x, or ( y, z ))
（停止性の証明）
A  {2,3,4, } ， orA ( x, y )  2 x  y  1, and A ( x, y )  xy とすると，
続き
 (or (or ( x, y ), z ))  2(2 x  y  1)  z  1
 4x  2 y  z  3
 2x  2 y  z  2
  (or ( x, or ( y, z )))
したがって，すべての書換え規則 l  r  R について  (l )   (r ) ．
演習問題
多項式解釈
A  {2,3, 4, }
plus A ( x, y )  x  2 y,
s A ( x)  x  1
double A ( x)  3x
0A  2
を用いて，つぎの項書換え系の停止性を証明せよ．
 plus ( x,0)  x
 plus ( x, s ( y ))  s ( plus ( x, y ))

R
 double(0)  0
 double( s ( x ))  s ( s (double( x ))

Download Report