a, c

表現系工学特論
項書換え系（３）
再帰的経路順序と停止性
homeomorphic embedding
１．同相的埋込み (1/4)
は項 f (s(a), g(b,c)) に同相的に埋め込まれる
項 f (a, c)
 emb
f
a
c
f
s
a
g
b
c
１．同相的埋込み (2/4)
同相的埋込み
つぎの３つのいずれかの条件を満たすときに，
項 s は項 t に同相的に埋め込まれるといい， s emb t と書く．
(1) s  t
(2) t  f (t1 ,
１つの引数への埋込み
, tn ) かつ s  emb ti (for some i )
各引数毎の埋込み
(3) s  f ( s1,
, sn ), t  f (t1,
, tn ) でかつ si  emb ti (for all i )
１．同相的埋込み (3/4)
 emb は，項の集合 T ( F ,V ) 上の半順序となる．
半順序
推移性 (s emb t  t emb u  s emb u)
反射性 (t emb t )
反対称性 (s emb t  t emb s  s  t )
【例１】 f (a, c)  emb f (a, g (b, c)) （∵ a  emb a ， c  emb g (b, c) より）
１．同相的埋込み (4/4)
定理１（Kruskal の木の定理）
F と V は有限集合であるとする．
 T ( F ,V ) に対して，
このとき，任意の項の無限列 t0 , t1 ,
ti emb t j
となる i, j (i  j ) が必ず存在する．
そういう i < j が存在しない
そういう無限列はない
simplification order
２．単純化順序 (1/4)
単純化順序
部分項性を満たす項の集合 T ( F ,V ) 上の書換え順序
部分項性
任意の f  F , x V について，
f ( , x, )
書換え順序
T ( F , V ) 上の厳格半順序
推移性： s t  t
非反射性：  (t
x
で，単調性と安定性を満たすもののこと．
us
u
単調性：
s
t)
t  f ( , s, )
安定性：
s
t   (s)  (t )
f ( , t, )
２．単純化順序 (2/4)
単純化順序の性質
性質１：任意の f , t について， f ( , t , )
t．
（∵安定性より）
性質２：任意の項 s と s の任意の真部分項 t について， s
t．
（∵推移性より）
【例２】 f (a, g (b, c))
性質３： s  emb t ならば s
g (b, c) b より， f (a, g (b, c)) b ．
t ．（ s
t はt
s または s  t のこと）
（∵ t のサイズに関する帰納法より）
【例３】例１より f (a, c)
（確認： c
f (a, g (b, c))
g (b, c) およびの単調性より）
２．単純化順序 (3/4)
定理２（単純化順序は簡約順序）
F が有限集合ならば，任意の単純化順序は簡約順序である．
簡約順序
整礎な（すなわち，無限下降列 t 0
t1
の存在しない）書換え順序．
項書換え系 R が停止性をもつ必要十分条件は，すべての書換え規則 l  r  R
について l
r となる簡約順序
が存在することである．
２．単純化順序 (4/4)
定理２（単純化順序は簡約順序）
F が有限集合ならば，任意の単純化順序は簡約順序である．
（証明）単純化順序は書換え順序なので，残っている条件「整礎であること」を
背理法で証明する．
もし
が整礎でなければ，項の無限下降列 t 0
ある i , j について ti
t1
が存在し，定理１より，
emb t j (i  j ) ．
このとき性質３より， t i
t j ．これは， ti
t j であることと矛盾する．
recursive path order
３．再帰的経路順序 RPO
優先順位
関数記号の有限集合 F の上で定義された厳格半順序
再帰的経路順序 (RPO)
これを項の集合 T ( F ,V ) の上で定義された半順序
rpo
に拡張
本講義では，その特殊ケースのみ扱う．
辞書式経路順序 (LPO)
lexicographic path order
４．辞書式経路順序 LPO(1/6)
優先順位
関数記号の有限集合 F の上で定義された厳格半順序
辞書式経路順序
lpo
項 s, t について以下のいずれかの条件が成り立つとき，
s
lpo
t
と書く．ただし，(2)～(4)では，
s  f ( s1 ,
, sm ),
t  g (t1 ,
, tn ) .
３．辞書式経路順序 LPO (2/6)
辞書式経路順序（続き）
s  f (s1 ,
, sm )
lpo
, tn )  t
g (t1 ,
(1) t は s の中に出現している変数である．
(2) si
(3) f
lpo
t (for some i )
g かつ s
lpo
t j (for all j )
(4) f  g かつ，ある k が存在して si  ti ( 1  i  k ),
sk
lpo
tk ， s
lpo
t j ( k  j  n )
３．辞書式経路順序 LPO (3/6)
定理３（RPO は単純化順序）
再帰的経路順序は単純化順序である．
系４（RPO による停止性証明）
ある優先順位から誘導された再帰的経路順序
rpo
のもとで，
項書換え系 R に含まれるすべての書換え規則 l  r について
l
rpo
r
ならば， R は停止性を持つ．
３．辞書式経路順序 LPO (4/6)
【例４】
 f ( x, e)  x
i (e)  e

R
i ( f ( x, y ))  f (i ( y ), i ( x))
 f ( f ( x, y ), z )  f ( x, f ( y, z ))
優先順位
i
f
e
３．辞書式経路順序 LPO (5/6)
優先順位
i
f
１． f ( x, e)
lpo
２． i (e)
e
lpo
３． i( f ( x, y))
e
x by (1).
by (2).
f (i( y), i( x)) by (3)
because i f and i( f ( x, y))
lpo
and i( f ( x, y))
lpo
lpo
i( y) by (4)
i( x) by (4).
LPOの定義
３．辞書式経路順序 LPO (6/6)
優先順位
i
f
e
４． f ( f ( x, y), z ) lpo f ( x, f ( y, z )) by (4)
because f ( x, y) lpo x by (1) and
f ( f ( x, y), z )
lpo
because f ( x, y )
f ( y, z ) by (4)
lpo
y by (1)
and f ( f ( x, y), z )
lpo
z by (1).
LPOの定義
演習問題
LPO を用いて，つぎの項書換え系の停止性を証明せよ．
not (or ( x, y ))  and (not ( x), not ( y ))

R  or ( x, and ( y, z ))  and (or ( x, y ), or ( x, z ))
and (and ( x, y ), z )  and ( x, and ( y, z ))


Download Report