Conditional Dependency Pair Method for Proving Termination of

Institute
工nstitute
of
of
Eleotronios
Electronics,，Information,
工 nformation
and Co
Communication
unioation
Engineers
Engineers
，and
一般社団法人
電子情報通信学会
信学技報
IEICE　Technical Report
THE INSTITUTE　OF　ELECTRONICS，
INFORMATION AND COMMaJNICATION　ENGINEERS
例外処理を含む関数型プ
SS2013 − 23，
肥 SE2013 − 23　（
2013−07）
グラム停止性証明のための条件付き依存対法
ロ
毅 †　酒井正彦 †
濱口
†名古屋大学大学院情報科学研究科
〒 464−8601 愛知県名古屋市千種区不老町
−u ・
nagoya
ac ・
E −mail †｛
hamaguti sakai ｝◎is．
jp
：
，
CS −TRS ）
（
あらまし　先に提案した文脈依存項書換え系
グラム
ル
を利用すると非常に短いプ
の
停止性
・非停止性証
ロ
CS −TRS
から変換された
ロ
変換による例外処理を持つ先行評価に基づく関数型プ
の
へ
明法では，変換で得られる
CS−TRS
グラムしか証明に成功しな
い
，そ
停止性・非停止性証
の
，本論文では例外処理を持っ関数型プ
TRS ）の停止性証
る．まず，項書換え系（
こで
の停止性証明のための新しい手法を提案す
ー
明に汎用の停止性証明ツ
グラム
ロ
明に用
文脈を条件として記述する条件付き依存対を定義する．次に
，条件付き依存対から構成さ
一
れる条件付き依存対鎖の存在と CS −TRS の最内停止性が致することを証明する．さらに，依存グラフを用いた既存
の停止性判定手法を提案する．本手法によりこれまで証明が
の手法を拡張し，条件付き依存対グラフによる CS −TRS
・
できなか
た多くのプログラムの停止性非停止性が証明可能となる．
い
られる依存対を拡張し，
っ
キーワード　関数型プ
ロ
グラム
，例
，項
外処理
書換え系，停止性
Dependency　Pair
Method for
Proving
Termination
of
Conditional
Programs　wi 七h　Exception　Handlil
！g
Functional
Masahiko　SAKAI †
Takeshi　HAMAGUCHI
† and of lnformation
Science　Nagoya University
†Graduate　School
−
−
−
Furo cho Chikusaku Nagoya 464 8601　Japan
ac ．
sakai ｝
◎is．
nagoya −u ，
jp
E −mai1
†｛hamaguti ，
，
，
，
，
：
一
eva 更
Abstract We have recently proposed a method forproving termination ／non −termination properties　of eager ．
Sensitive
The method
transforms them into
Context．
uation −based　functional
programs with exception handling ．
Term Rewri七三ng Systems （
CS −TRSs ）in　preserving　the properties．
However　we encounter a problem that　the existing
CS −TRSs fail
even if　a very short program　is　given ，
In　this　paper we present　a dependency
termination provers for
，
−
，
programs with exception handling
for　CS −TRSs transformed from　functional
We introduce con
condi 七ional　dependency　chains ，
that　represent
context
information into　the　dependency　pairs and define　We
ditiQns
dependency
prove that　the target　CS −TRS is　inner一 ost termina 七ing　if　and only if　there　exists no in且nite conditional
method
specialized
，
皿
．
Moreover ，
we augment
graph notion
into
the hamework
of the　dependency pair　problems ，
and propose some
，
processors．
The new method
works effectively for
CS −TRSs produced bY the transformation
chain
new
Key
1．
すで
グラ
functional　program
words
ム
handling，
term rewriting
exception
の停止性
CS −TRS
（
っ
先行評価に基づく関数型プ
・非停止性証明法
を提案した
ML ／ex
／ex
ML
とし，
1］
．対象プ
［
っ
・非停止
，CS −TRS
ことで．プ
完全であるため
性を証明する
の
ロ
の
変換は停止性
This　article isa　technical　report
witheut
グラム
peer review
ロ
，and
い
ては停止性証明
停止性
ていたが
の
こ
フ
つ
5｝が広く知られて
［
い
，文脈依存と最内の
，証明できたプ
た．
関数型プ
ロ
version
may
グラムから変
明法を提案する
．項書換
4］
，依存グラ
［
る．項の到達性を条件として記述可能
一 61 −
／or extended
は既存
能力が弱く
は非常に短い限られたものであっ
で
・非停止性に
TRS ）の停止性証明の手法として依存対法
え系（
its　polished　and
ム
の
，本論文では例外処理を持
換された CS −TRS に有効な停止性証
・
停止性
の
，
グラ
そ
最内書換えによ
termination
止性証明ツール［
2 ］［
3］を用い
組み合わせにお
ロ
グ
ロ
を文脈依存項書換え系
）に変換して停止性の判定を行う．こ
に対して健全か
る停止性
の停
我々は例外処理を持
ラミング言語は
and
，
非停止性が証明できる．CS −TRS
まえがき
に
system
，
be　published　elsewhere
．
Copyright◎ 2013 by IEICE
工工一
Eleotronio
Library Service
NNII-Electronic
Library
Institute
工nstitute
of
of
Eleotronios
Electronics,，Information,
工 nformation
and Co
Communication
unioation
Engineers
Engineers
，and
な条件付き依存対（
σDP
Conditional
Dependcy Pair）
の定義
，
，次に［
1］で得られる CS −TRS の σDP 集合の変換
法を与え，CDP から構成される無限の条件付き依存対鎖の非
存在と CS −TRS の最内停止性が一致することを示す．この効
を与える
へ
果的な証明のため，依存対を用いた項書換え系の停止性
手法として提案された DP
プ
セ
ロ
ッ
の
判定
4 ］の適用
［
サを用いた手法
を図る，σ DP 列が鎖となるためにはそれらのすべて
条件を
の
成立させる代入の存在が必要となるため，制約付き項書換え系
の
停止性判定のための
に
，DP
プ
セ
ロ
ッ
サ
の
GDP
た
っ
成
CDP
された
．そ
こ
CDP
情報を追加した
の
ラムから生
ロ
セ
6 ］の
［
サ
ッ
よう
入力に依存グラフの情報を加えることが
効果的であることが分か
存グラフ
問題とそのプ
，GDP
で
問題
ように依
の
問題を定義し、関数型プ
問題例に効果的なプ
セ
ロ
ロ
とする
．7
：
は
を説明する．概念の詳細は文
関数記号からなる有限集合を ∫
集合
の
arity
、そ
の
引数
μ
arity （
f
f）⊆｛1，＿，
（
f）｝を満たす．
と可算無限個
集合
と文脈を表す関数
して
があるとする
μ
ソから生成されるす
べ
D
σ と被定義記号の集合
割されるものとする．関数記号に対
表す関数
s
→
in
か
Rt
う，t
∫ 項
ての
ある
（
い
に分
の
．こ
は項
の
数を
こ
で
変数
の
）の集合
t
っ
ッ
系列が存在しな
い
R
ク
関係
A
とき，t は
項もR
一＊で
R
→
，t は
→
規形
→
と
ut
in
う．ま
とい
た
，
最内正規形とい
s の
→
（
π ）による書換え
in
π
もとで停止性（
最内停止性）
の
という．
，一＋
射推移閉包を，それぞれ
表す．文脈 μ がどの関数記号 ∫ ∈
＝
R は（
文脈に
1μ （f）亅 arity （f）を満たすとき，
書換え系である．
と
t ，s
π
もとで（
最内）停止性を持っとき，
の
，反
推移閉包
の
を持たない項を正
最内）停止性を持っ
（
は
ら始まる無限の
，どの
といい
ス
が正規形であるとき
，
を持っ
『
∫ V ）か
7（
∈
アにつ
い
しない
依存
ても
）項
3 ．条件付き依存対と条件付き依存対問題
る関数型プ
ロ
し
した依
6 ］ GDP
，［
プ
の
は依存対に条件を
法と同様な依存グラフを導入
セッサ手
ロ
存対問題を定義する．
書換え系に対する依存対法と同様に，関数記号
通常
の項
f∈
に対して組記号と呼ばれる新しい記号
D
CS −TRS
グラムから変換で得られた
停止性を効果的に判定するために，本節で
導入
つ
書く．また，リデ
の
を持
構成子
次節で述べ
本節では本論文で用いる記法
献［
7 ］などを参照されたい．
ィ
サを提案
ッ
備
固定したアリテ
最内書換えされることを，それぞれ，s
グ
し，その停止性証明例を示す．
2．準
は
を導入する．
；｛fU　1f ∈ D ｝とし，戸；eUDWDt 「とす
る，ここで，arity （
f：）＝ ari ty （f），μ （∫：）＝μ（f）とする．項
t ；f（
tl ，
＿）∈ T （
ア，
V ）に対して根記号 f を ftS
で置き換
えて得られる項を te で表す．文脈依存性を扱うために依存対に
関係論理の式を導入する．
定義 3．
1］　項上の関係論理の論理式は，項の対 s
［
t を原始
式とし．原始式と論理積で構成される．その論理式 F の値は，
S と代入から
項上の関係一
以下のように定められる，
f
：
すなわち，が
1tn
O）を T （∫ ）と，項 t17．
．
．，
tn のリスト
を［
tli＿，
tn ］と書く．項 t に現れるす
ての変数の集合を
V r （t）で表す．項を木と捉えることにより，出現する記号の
位置を通常どおり自然数列で表す．例えば t ＝ f（
a）
b ）に
，
g（
一，
一 ta
t ⇔
s
〈
のト5
い
お
て，a は位置 11 に出現するという．項 t に対する μ 置
’
一，＞e＝F 〈 F ぐ⇒ （
一，〉ト Fand 〈一，〉旨 F
＜
t ）は（
1 ）x ∈ ソに
いて，
換位置 Pos 〈
Pos （
x ）＝
｛｝，（2）
一，〉ト F が真となる代入が存
与えられた一のもとで，（
POS （
t1，
…　，
tn ）
f（
i ∈ μ （
）＝｛｝∪ ｛ip　l
f） ∈ POS （ti）｝とし
S 充足可
て再帰的に定義される．根の位置
在するとき，F は一
に出現する記号ノを root （
t）
能であるという．そうでないとき，
‘
で表す．項 6 の μ 置換位置 p における部分項を μ 部分項と呼び
充足不能であるという．
定
2］（
s
tls で表す．それ自身以外の部分項を真部分項という．
t の
匚義 3．
条件付き依存対）
tttと F 項上の関係論
戸 E．
p に
おける部分項を項 s で置き換えて得られる項を t［
理式 c の対（
s
c
を
CDP ）と呼ぶ，ここ
s ］で表す．
条
件
付
き依
存
対
くめ）
（
労
で c を条件部と呼ぶ．
代入 θ の項オに適用して得られる項を tθ で表す．θ ソ
ア
V
の
s
t 〉
c ）は代入
T （，）を θ 定義域と呼び，定義域が空の代入をのと書く．直感的には CDP （〈
に対して c が成立する
，
『
特に，どの x ∈ Dorn （
θ）に対しても θ（
とき項 s が 1 回以上の書換えで項 t に書き換えることがで
x ）∈ 7 （
ア）であるとき，
θ を基底代入という、代入 θ は項のリストから項のリストへの
きることを表す．
定義 3．
3］（
写像に自然に拡張される．
［
条件付き依存対鎖） R を f 上の CS −TRS とする．
si ，
tl＞
Cl ）
s5 tl＞
c2 ）… は，以下の条件をす
上の書き換え規則（
t，
r ）は root （
1） ∈ D ， σDP の列（
，
て
〈
（
〈
，
ア＝ CuD
1，
r
た
，
，
．
が
∈ T （
fi　V ）
，
Var （
1）⊇Var （
r ）を満たす項の対 1，
満す代入 1 ，21
存在するとき条件付き依存対鎖（
CDP
r であり，
1 r で表す．
鎖）という，
をア（
ア，
V ）と，
T （
」
，
→
べ
α
・
→
σ
’
σ
μ
μ
っ
μ
σ
μ
ε
σ
ε
σ
iP
σ
ε
：
，
：
，
：
，
→
：
：
σ
，
σ
σ
σ
べ
，
σ
σ
→
F 上の書換え規則の集合 R
（CS −TRS ）という．ある 1 → r
すとき，te を t
を
∈
とき，tθ は
に
つ
tの最内
ッ
の
最内）リデ
（
に
隰内丿書換えされるという．s
クスとして持つ
ク
R
上の文脈依存項書換え系
いて
リデックスという．さらに
の
デ
ッ
f
ス
が
tθ で
t
1θ が te の
みをリ
リデックスという．項 s
あるとき，s
が
t ［＝le を満た
，
＃
に
；s ［
tθ］
＃は
t
＝s ［
rθ
慘
書換えられる，あるい
（1 ）
1
オσ
2）
→
（
＜
3）
（
51
・
冠
→
1
の
、＋、
灸，i＞← q
σ乞
は
R
また，（
1），
（2）中の
ε
σ
．、
σ
→
．
もとで停止性を持っ
の
旋をオ旋で置き換えた条件を満た
が正規形であるような代入
れを最内条件付き依存対鎖
1
σ
フ
）
を
f
，こ
．
鎖）と呼ぶ
R
’
，〔3 ）
るとき
σ
σ DP
（
最内
4］（
［定義 3 ．
条件付き依存対グラ
．
．が存在す
，2 ，，
し
上の
CS −TRS ，
一 62 一
一
NNII-Electronic
工工 Eleotronio
Library Service
Library
Institute
工nstitute
of
of
Eleotronios
Electronics,，Information,
工 nformation
and Co
Communication
unioation
Engineers
Engineers
，and
γ を
CDP
ラフ
σ DP
（
．9
V，
E ）を条件付き依存対グ
（
と呼ぶ．また，グラフの経路上の頂点列
の集合とする
〉
グラフ
＝
9
が（
最内） σ DP 鎖であるとき，これを
ア
＝｛9 （x ，
y）
Fundef
（
最内） σDP 鎖
上の
if，
raise
handJe ，
恥 nde4
A ，
B ｝
，
，
f ｝，
｛
＞
handJe （
if（
Je（
x ，
raise
A ）
x ）
A，
O）
，
y ），
（
9（
y，
），
｝
False ，
O ，
succ
＜
｛TYue ，
＝
→
と呼ぶ．
図 1 例外処理を含む ML ／ex
5 ］（（
最内）条件付き依
匚定義 3 ．
最内）条件付き依存対問題）
（
Fig ．
1 Terminating
（
CDP
存対問題
問題）とは（］
DP
9
グラフ
CS −TRS R
と
の
対
（
最内） CDP
無限の
の
鎖が存在
判定する問題である．（
9 R ＞を（最内） CDP
，9
しないかを
は σDP
以下で
問題
R ）を単に
9，
（
入力
3．
6］ R
問題に変換で
α ワP
CS −TRS ，V
を
を
問題
鎖となる
，
CDP
．こ
とする
，
，（最
とき，か
は
もの
存在
しない
，
B，
z ）
石re （
A ），
，，
5elec
fire（
B）
A，
z ）
五re （
β ）
，，
，
（
x
x
x
ard （
isData （）
x ，
，
，
，
，
y
9
，
92 （
y）
，
9 （ y ） 91 （ y ） 91 （）
）
m
isDa
亡
a
92 （，
y ） guard （
（
y）
，
93 ゆ，
y）
）
，
m ，
1e（
x ，
rafse
A ）
M ）
A ，
O ）・
，
，
93 （
y ） handle σf（
y ），
（
9（
Y，
）
亡
，
セッサを定
問題を入力と
セ
．
3．
8］（（最内〉条件付き依存対プ
9i，
Ri ）が有限で
（
あるとき
→
→
どめ
っ
則の
セッサの
ロ
健全性）
Proc（9 ．
R ）に
R の∈
g‘，
（
R
9
（，）が無限の
，
つ
い
CDP
（
最内）
2ML
図
＋
，
一部を省略
＋3
g g3
，
文脈 μ
，g1
の
．こ
isData，
，関数記号 rais fire，
f4
handle
値は空集合，
succ ，
guardl
，
1
と
の
は
2
で
，
十
2
値
g2
μ
｛｝ある．
｛｝
値は
ても
鎖を
2 条件付き依存対
4 ．
ML ／ex
で
こ
9 ］（（
最内）条件付き依存対プ
［定義 3 ，
内停止性の証明に焦点を合わせ
Proc（9 ，
R ）＝ ⊥
ロ
セ
R ，）∈
またはある（
9z，
ッ
サの完全性）
Proc （
R ）が無限の
9，
（最内） σ DP 鎖をもつとき，（
R ）が無限の
9，
（
最内） σ DP 鎖
を持つならば，Proc は完全であるという．
紙面の都合上省略するが
を除いた近似グラフ
，σDP
存グラフに変換するプ
ロ
い
る
こ
セッサを容易に設
とで
こ
とがない辺
，
より単純な依
計するこ
4．関数型プログラム停止性証明の
とがで
きる．
ための依存
対法
は本論文において対象とする先行評
／ex
の
定義および，
ML
変換を与えた．本節ではこ
4．
1 節），CS −TRS
（
与える
1
4 ．
の
から σDP
／ex
プ
ロ
価に基づく関数型
グラムから
変換で得られた
と
CDP
CS −TRS
CS −TRS
を示
鎖を構成する方法を
．
4，
2節）
（
，関数記号の集合，関数を定義する書換
グラム
え規則の集合 Fundef ，例外の集合の 3 項組である，プ
の
ユ］
例を図 1 に示す．ただし，組込み関数の定義は省略した．［
グラム P を入力とし，
CS −TRS
P）
変換 φ は肌／ex のプ
φ（
−
を出力とする．このとき，プ
グラム P の停止性は，CS TRS
1］
．図 1 のプグラムか
P ）の最内停止性として保存される［
φ（
ら φ で変換得られる CS −TRS を図 2 に示す．ただし関数の規
ML ／ex
プログラムは
ロ
ロ
ロ
ロ
CS −TRS
，最内 CDP
問題
P ＞の最
φ（
へ変換を考
．
ML ／ex
得られる CS −TRS
から変換して
は一意に定
．しか
1 以下で
P ）では，すべて
φ（
あるため，最内リデック
，条件付き依存対や条件付き
，無限書換え系列を導く項が現在の
文脈 μ では書換え不能な場所に出現することがあるため，文脈
による依存対の条件部が必要となる．
まず，σDP の候補を求めるための関数 Cand を定義する．
t ）は項と
σand
は φ（
P ）の項を引数とする関数であり，
Cand （
．
の第 1 要
理
式
の
対
を
要
素
と
す
る
集
合
で
あ
る
直
感
的
に
は
，
対
論
素は t 中の停止しない部分項の候補であり，第 2 要素は第 1 要
ス
まる
しながら
依存対鎖を設計する際には
素の項が将来
μ
置換位置に出現して書換え対象になるための条
件を表す関係論理式である
4．
1］
［定義
関数型プログラムから変換された文脈依存項書換え系
θ1
から変換して得られる
の関数に対する μ の要素数は
鎖に含まれる
4 ］を用
概念［
の
える
は
from ML ／ex prDgram
の
select1
μ
CS −TRS
グラムを変換した
ロ
以下で
し
コ，
・
transformed
している
の
，
十1
プ
／ex
Fig．
2　CS −TRS
持たないならば，Proc は健全であるという，
の
Z
→
・
→
＝
サ）　（
最内）条件
ッ
σDP プロセッサ＞Proc は（
最内）CDP
（
し，（
最内） CDP 問題の集合または ⊥ を返す関数
か
へ
，）
→
ッサ
Proc （
R ）キ ⊥
g，
言語
B ），
＝
侮 e（
IB
亡
→
付き依存対プロセ
肌
z ）
x ），
x，
B ，
，
（
Z selec
→
7 ］（（
［定義 3 ．
最内）条件付き依存対プロ
1］で
［
，
＝
＝
亡（
isData
→
fire（
A ）X
8elec 亡（
義する．
［定義
→
，
isData （）
x ，
A，
x ）
，
，
（
select
．
内）条件付き依存対プロ
，
β ）→ fire
（
（θ ）
raise
，
handle＠，
B，
の → 5elec
selec 亡（
五re （
A ）：
＝，
A，
Z）
のとき
，
この問題の変換を行う　（
最
である
A ）　（
五re
z
fire
x ），5e 亅ec 右（
亡ちコ，，
（
y，
の
handle （r ，
A ，
x ）
→
V ｛（
e et）［el　et ∈ V ｝
（
）R ）が有限の
R に対する
ときに限り，V の要素の無限列で，
（
最内）
その
→
コ
内） CDP
つ
A ）→
（
raise
きる．
［補題
handling（1）
τ
if（
fire
x ），
z ）→
（
y，
、
問題と呼ぶ
（
最内） σDP 鎖の存在性は（
最内） CDP
無限の
→
ff（
Trule，
y ，
z ）→ y ，
if
Faise ，
y ，
z ）→
（
CDP
Q）
グラム
ロ
exception
ロ
そのときに限り（
9 ， R ）は有限であるという，
の
プ
with
isDa 亡a （
T ｝ue ）→ 亡亡，ゴsDa 右a （
Faise）→ tt，
fsDa 亡a （
五re ゆ）
→
fire
x
s
x）
， cc （fire＠））→ 五re （
，
）
（）
（
最内） σDP 鎖が存在するとき，かつ
上の無限の
記
問題の入力とす
，
るとき
program
tt，
fire（
x ）
x ）
9 ard （
y ）払 9Hard （
，
y ） fire（
，
f5Da 亡a （
succ
（）
）→ fsDa 亡a （）
，ゴsDa 亡a （0）→ tt，
・
9上
を入力とし，
ML ／ex
義する
（
関数 σan
．
f）　Cand （
t ）を以下の
（
ように再
帰的に定
．
1） t ＝succ （
tl）の
（
2）
（
t ＝g
．
とき，
Cand（
tl）
to ，
ft
tll ＿ tn ）
u ，
c 〈 to
（
＋1（
）
）のとき，｛
（
ロard
，
→
・
・，
tl1．
tn）
fi＋ 1 （
）｝・
（
3 ） t ＝if（
tl t2 t3 ）のとき，
Cand （
t1）∪ ｛（
u2 c2 〈 tl
（
→ False） 1
t2
∪
u31c3
〈
t1
［
1｝ue ） 1 （
u2 ，
c2 ） ∈ Cand（）
｝｛
（
tの
1（u ，c ）∈
σ and
，
，
t3 ）
C3 ）∈ Cand （
，
｝，
4 ） t ＝ handle（
ti，
E，
t3）の
（
→
，
U3
（
］and
とき，（
t1 ）U ｛（
u3
（
c3
，
〈
一 63 一
一
NNII-Electronic
工工 Eleotronio
Library Service
Library
Institute
工nstitute
of
of
Eleotronios
Electronics,，Information,
工 nformation
and Co
Communication
unioation
Engineers
Engineers
，and
成り立っような規則ど →
、
‘rue ）
，
Yl ）
〉
．
x ，
（
（
gi ｛ 2 ，
y ）
9茎
y ）
（
＞」 D 亡回一 t亡）
’
x 、
，
x ．
i D 亡 ω 一亡）
（
〈
9弖
（
Y3 ）
9§
（
y ）
〉，
x
x
．
J （
，
（
（
95 （
Y4 ）
y ）
， ue ）
〉
x5
・
x5
、
，
，
（
（
95 （ Y5 ）9 （
シ5
）
〉1e＠5 ，
YS ）→False ）
x6
，
hand1
iKJe
x6
（（
95 （，
Y6 ）
．
（
（，
り6 ）
4）
，
A ，
0）
亡 e）
9（
Y6 ．6 ）
ra15e （・
），
〉，
＝ 1，
Xl
（
（
9 二（
ワ1 ）
，
gi （
＝
、
、
・
、
，
・
、
亡・
，
・
CDPo
＝
（P ｝
・
・
：
、
・
・
め
亡
図
3 図 2 の CS −TRS
Fig ．
3 COP
set
of
の
CS −TRS
σ
Fig．
2
−“fire（E ））1（u3 ・
C3 ）∈ Cand（
t3）｝U ｛
ち true）
（
｝．
5） t
．
．
．
tn ）（
f （ti．．
（
∫ ∈ fB U7 D ）のとき，
Ui
・
Ci
Aj
isData
UirCi ）∈ Calld（
UiSiSn｛（ t　ち）
（
ち）→ 亡亡）1（
｝∪
−
…
tl
・
tn
〈
ti
t
．
∫
，
，
1
i
nisData
（（
） ≦≦
（）
の
6 ） t ＝fi（
tl ，
＿，
tn＞（
fi∈ 7セ）のとき，
（
tl
＝
：
’
く
tl、
＿，
tn ）
true ）
fi（
，
｛（
｝．
CDPo （p ）は以下の
1→
r
d（
・）
｝
：
・
it
CS −TRS の CDP は図 3 のようになる．
−
3 ］ CS TRS φ（
［定理 4 ．
P ）が最内停止するならば，かそのと
きに限り．φ（
P ）のもとで条件付き最内 CDP 鎖となる CDP φ（p ）
の要素からなる無限列が存在しない．
ここでは紙面の都合上，証明の概略を示す．SN を停止性を
持項の集合とし，項の集合 7 猛。を｛
SlS
S ＞ t
≠SN 〈 ∀t（
＝
t ∈ SN ）
．
とす
る
ま
た
，
Tffn
tt
t
丁
と
．
∈
す
る
｝
｛ l
詔｝
−
補題 4，
4 ］ CS TRS が停止しないなら瑠、の要素が存在
［
する．
5 ］ tt ∈ 篇ならばある規則 1 → r が存在し，
［
補題 4．
・
壕論 1 ∈ 嘸である・
6 ］ ta ≠ SN である項 t と代入に対して，すて
［
補題 4．
の x
∈ Var （
t）および x ？ u であるすての ut に対して，
’c ∈ Cand t か c か
ut ∈ SN ならば項 t が存在し，（
t ．
）
（）
t
∈ 瑠 n である．
の
つ
っ
⇒
。
：
σ
べ
σ
σ　’
べ
’
っ
σ
っ
’
σ
この
補題は項
匚
補題 4 ．
7］
tの
サイズに関する帰納法で証明できる，
Range（）
⊆SN
σ
に対してどσ ∈
瑠
n
とする．補題
ならば r ≧
r
’
か
っ
4，
6よ
〆σ ∈
t→
り規則
瑠。か
’ c が存在する，
CDP （
lt，
T ：〉
，）
〈
8 ］　（
t c ）∈ Cand （
r ）
［
補題 4 ．
〈c
ならばある文脈 C
r
t］である・
盛教P ） σ ［
っ
r
Cσ が成
立する
σ
，
σ
補題は
Cand
の
CS −TRS φ（
P ）に
対して無限の最内書換えが
存在することを示す．
｛
・
が
擁
t： ∈
する’
嘸
α［
司μ σ
vl ）とお
g（
ttσ i
たとき
い
Siai
，
鎖の定義
を満たす代入
は
成立
，Siai
し
（］
tt］
at
i［
in φ（p ）
であ
→
．
8 より
う書換え系列が存在する．ここで，
Ci 圏）で
（
とい
Σ
て
っ
とき（
ti，
Ci ）∈ σand
の
Si ÷ lai
帚教恥
あるため，補題 4
1 かつ Si
＋
＋ 1 σ i＋ 1
が
，g （
房） 8（）g 催）∈ NF で
肱
なければならない，このとき，s ＋ 1 ＝g ＠分である．それゆえ，
以下のような書換えが存在し，これは無限である．
：
クスであるためには
ソ
鎖が構成できる
項に対して部分
につ V 丶て・
喩
t］
ゴ φ（）C ［
・σ ・
ゴ
・
醇
→
評（・）0 ｛國
・・・
・
．
oi ［
C ・［
t・11 ・
・・
（・
σ
・
・
5．依存グラ
・
本節
存対問題
・
翻
‘甘・
・・】σ ・
｛［
・
σ ・
を用いた停止性証明
フ
CS −TRS
では
）C
盛ち（P
レ】
…
・ σ・
暇
霊ら（）・ci ［
…
CE
）α ［［］］
言φ（P ＞
・）
・（
ln8
P ）の最内停止性証明のために有効な依
φ（
の
プ
ロ
セッサを与える
まず本節
で
用
い
るグラ
9 ＝σろE ），頂点 v
V
∈
に
．
基本操作の記法を述べる．グラフ
フの
いて
つ
delnode （
9
v
，
）は
a
から頂点 v
とそれを含む辺を除いて得られるグラフを表す．delnode は v を
頂点の集合に自然に拡張できる，また，coaJesnode
は
，二
っ
頂点 Vi ， v ゴ
の
ラフを表す．こ
させるが，辺
，Vi
で
を縮約させて
p
以下で
CDP
SCCO
皿
分割
，
は強連
，
は
．
しない
導入
結グラ
プロセ
．こ
かの性質を示す
フ
．すな
こで，91 ．
．
．9 ．は 9 の
，
っ
くっ
して
の
9
とき，Proc （
R）
9，
，
ない条件付き依存対グラフ）
上に
R
無限の最内
の
とする
＝
，
．
Proc
CDP
は健全か
完全である．
次
の
定理は
，頂点の
stt te＞c ）の条件
条件付き依存対（＜
，
灸充足不能であればそ
in
の
，c
が
が
寸夷充足不能
，
c が
頂点を取り除けることを表す．
2］（
［定理 5 ．
頂点の削除）
最内 CDP
て
い
こでは最内書換えの場合のみ議論するが
，
存在しな
と
サに用いられる依存対問題の
ッ
問題（
9 R ）に対
い
，
9i 9ゴは非連
，かつ，相異なる
1］（
［
定理 5，
無限条件付き依存対鎖
鎖が
Va ，
v ゴ，
Vk ）
9，
（
にして得られるグ
Vk
もしくは Vj に接続する辺は Vil に接続
Ule ）は
．
．
9 ）＝｛91 ，
，
，
9n ｝，こ
（
．
，各 9
結である．
わち
こ
Vk
（
V
∈
はグラフを強連結成分に分割する関数である
sccomp
→
く＝
（
）無限の書換えに対して無限の最内 CDP
ことを示す．補題 4 ．
4 より，停止性を持たない
9・t ∈ 瑠
C ［
司帚3 う
＝
そのときに限り
．この
る
最内 CDP
定義に関する帰納法で証明できる．
［
証明］（定 mp 4 ．
3 ）無限の最内 CDP 鎖が存在するならば，か
つ
乙
σ
通常の書換えにも容易に拡張可能である
が存在し，
μσ
この
＿
，
．
．
．が存在する．
，2 ，
は最内リデックスである．従
s
P ）
∈φ （
〔例 1 ］　図 2
内 σ DP
sl σ 3
（p ＞
jn あ
このときすべての Ciai
→
書換え
｛
tn）〉
c ）1（
，
，
ち）∈ 伽
lt
1
σ
tl
に対応する
．また，最
る
，
→
sl σ 2 ， σ 2
p
jn 〔　）最内リデ
集合
の
ように定義される．
f‘（t・
｛（
〈
∪
CDP
，
仮定する．各 CDP
と
C ［
tt］が存在す
→
tl σ 1
より
ti
ら定まる
’
iC2
CDP 鎖が存在する
規則 Si
7 ） t が上記以外のとき，の，
（
2］（
σ DP 集合〉 φ（
匚定義 4 ．
P ）か
σ
：
，
集合
in
り
っ
⇒
川
CDP
4．
5よ
の
，
：
＝
べ
’：
二
・
が存在する．補題
σ
であり，
la
す
て
真部分項は停止性を持
た
r
Range（）⊆SN である．また，
は停止性を持たない．補
ti
7 より r a ∈ Tk n となる（
題 4，
〈1 r ＞c ）∈ σDP が得られる．
これを繰り返して無限の最内 σ DP 鎖が構成できる．
（）いかなる無限の最内 σDP 鎖に対しても，
対応する無限の書換えが存在することを示す．
S5 ，
tE ＞
C1
t茎
sl ，，
（（
，
，
）
（
（茎
＞）
（
〈
慮〉C3 ）… ようなとなる最内
ICa ∈ Tkln
・
・
r と代入
の
な頂点を v
E ，
問題（
V，
（
）R ）にお
三（く紙の
c
，
い
）∈ V とする，
一 64 一
一
NNII-Electronic
工工 Eleotronio
Library Service
Library
Institute
工nstitute
of
of
Eleotronios
Electronics,，Information,
工 nformation
and Co
Communication
unioation
Engineers
Engineers
，and
×
×
Pi
一
⇒
Pゴ
曾
一
Pk
図 4 頂点の縮約
Fig．
4 coalesing
P
’
i
⇒
Pl
⊥
．
t
Pk
P
P1
±
of vertices
iji
Proc （
V E ）R ）＝（
deinode （
V，
E）
v｝
R ）とす
，
，
（
（
｛
）
，
，
次の定理は，辺
，
ると Proc
Fig、
5 expansion
σDP
の始点と終点の
53 ］（辺
の削除）最内 σDP
11
V E ）R ）にお
（
（
問題
・
1
→
→
，
，
（’
て
→
の
σ
π
σ
，
，
σ
縮約し，もとの頂点を取り除
に
．
くことができることを表す
5．
5ユ
（
頂点の縮約）　CDP
P ・一（（
鋼
1
，
V ，　E ）， R ）において
問題（
（
1 1＞
一（
〈
〉・t ）P 」　，
ように、分岐のない頂点と合流のない頂
の
点が隣接する場合は頂点を一つ
［定理
し
，
最内 σDP 鎖となる．
Xn ）
（（
ft「＠1 ，．．，
，
f9（X ，，．，，コrn ）〉，伽
f
e）
x1 ．．
Xl ，
．，
コrn ）
isData（
Xl ）→ tt）
，
，
（
〈
ノ（
7 ＝ n ）fS（
〉
，
，
．
，
，
・・。
，
（
褫ゆ・，
繍
最内 CDP
この
・
，
1−
，
オ
，
（
〈撫
閉路上
） ∈ v ，（
P ・，
Pj） ∈ E
。）〉f D
，・
t ・飼
・
・
，
以下
で
1 個
の
セ
ロ
x
、（・
．
・。
・
・
・
・・）
（
・古
・
−
る条件は成立しても 2 回まわると成立しなく
して図
5
の
頂点以外の
．この
頂点では分岐，合流がないものとする
の
サを繰り
ッ
条件付き依存対
の
→
1 回まわ
5．
5 を適用
理
）
むむ
→
なる場合がある．Pi を始点とする閉路があり，こ
・」
，
・，
＿，）θ … θn ＞，〈 i D
，
鴻
Xn
θi … θ．
（
） tt）
）となる．
isData
tt〈 … A （
閉路を
と
こ
．
．
．
，
嚇
・，
＿
x
（
．、
鎖は条件付き依存対プ
返し適用する
っ
，
4
条件付き依存対が存在
して以下の
，
皿
次の定理は，図
if，
handle ，
raise
，
σ
，
・
，
て
1
っ
11
f に対
以外の被定義記号
＝
・
circuit
P ）におい
［例 2］　条件付き項書換え系 φ（
い
＝（
オ，
51
，（
（
く，
〉Ci ）
〈
拷＞」））∈ E とする．罐 in 荒 ss −　a ゴ，
cri＞ト q かつ（
（ifilz ，
，j ＞ト Cj を満たす代入 i ゴが存
ill
在しないならば，Proc （
R）（
V，
E ＼｛
R ）とする．
玩 E）
，
p｝
，
（
（
）
このとき Proc は健全かつ完全である．
定理 5，
3 の Proc によて roo 塵1）キ root （．
）であるような辺
．
オ
こ
が
で
・
は
取
り
除
く
と
きる．
（（
〈
＞lc ）1 （（拷＞iCj ））
へ
4］（
強連結成分の分割）
R ）を最内 σDP 問題と
［定理 5 ，
9，
（
＝
．
＿
で
する scco
9 ）｛9 ，，
9 諺あるとき，Pr c （9 R ）＝
p（
Proc は健全か
完全である．
91 R ）1 ＿ 1 （9．R ）｝とすると，
｛（
p
展開
of adjacent
が σDP 鎖となるよう
な代入が存在しなければその辺を取り除けることを表す．
［定理
5　隣接閉路の
図
．
は健全かっ完全である
とき
，定
の左側のグラフのように閉路上の途中の
i・
aj が存
ことができる，次の定理は Pi
頂点を一の頂点 Pj にまとめる．
’
在するとする．ps 十 p ゴならば（
Pi pl） ¢ E か
pl キ
と Pj のような隣接閉路を図 5 の右側のグラフのように展開で
ノ
V，
7こ）
E ）
，
p ならば（
Pi，
Pj） ≠ E であるとき，Proc （
（
（
）＝
きることを表す．
d （（
V E ）（〈
sl − tl＞
ci ）（
，
，t 〈
（ alesn
〈甥〉ゴ）
（
〈1 講ゴ〉
定理 5，
6］（隣接閉路の展開）　（
V，
E ）が φ（
P ）の CDP グラフ
匚
．
c ゴゴ）
R ）とすると，
Proc は健全か
完全である
，
）
である CDP 問題
V
E
π
に
お
て
・
（
（，
），）
。）． al
d （
V　E）
、1
，哇
［証明］（V ，
，
，、〉
，
（
（
（1，
＞）
編 j，
j 〉
オ
，
，
，
，
｛（（
（
瀬〉，の（〈＞ゴ））（
（
〈ゆゴ）
（
く1蹴 c1 ）
）
｝
⊆E か
51
（
〈
湾の〉Ciat 〈 cゴの））とする．
が劇
立
ような代入
・オ1 詐
講・詐
V，
E ）上に無限の σDP 鎖が存在し，
（
sSitS ＞
Cj ）において分岐，合流がないとき，
，
ゴが存在し，（
〈
sS．t；
cゴ）
，
（
（〈1湾〉cO （
〈
〉
）が含まれる場合．
＝
Proc （（
（V E ）R ）
）
以下のような鎖が存在したとする．
’
／
Ci 〈・）i j ）
vx
sl
t
，（〈，
，）〉
（
（
（｛（
（，］
〉
｝u ｛（〈
射〉，
考〉，（i 〈
オ
c
sl
ti
Ct
（（＜，＞，）（＜
砥 1＞，の〉，
c ゴ））
，
｝
），
（（（1，
臨 t），
（
＜野＞，ゴ）
E ＼｛（（
〈1 ε1＞Ci ）1 （
〈看＞
1c
））（
（
〈考＞
1c ）（
〈繍，の）
｝∪
sx
古
（
（
〈
sk ，
tk＞
Ck ）（
嬲〉，ゴ）（〈監〉））
，
｛（
（
〈
〈1，＞（〈’ ））），
Ci 〈ゴ）、ゴ〉（
ss ，
tl＞ ∂）
，
（（
〈1 1
＞
1（
〈
Proc によて以下のような鎖が代わりに現れる．
・
sZ
t
，
，；
，（露ゴ）の），
（
（
〈娠〉
ω （
〈／
〉
オゴ〉
（1 ，
，
，（・ ai 〈ゴゴ）），
〈
（
（
〈諦，）（
i
i
，
，
（
）
）
1
（（瀚
の）｝
（
（
〈1 咢〉
ゴ
sl
〈
sL
tL
Cm
噛
（（（講 j ）（
＜
＞）
）
Cle）
め1
π）
，
，（
，
，の），
，），
亅｛
（
（
〈慧〉
〈ξ
＞
（
（
（鵠〉
（
〈溜＞））
｝⊆E ，
とすると，Proc は健全かっ完全である．
、
か
詐
亡・ i
つ
・
が成り立
・・
つ
ような代入
・
・
っ
つ
，
｛
・・
・
・
，
，
，
，
，
・
・
，
・ σ
σ
・ σ・
つ
σ
1
’
’
’
、。
，，、、σ
，
，
，
iCi
、
・
σ乞
つ
11
・
・
・
・
，
，
，
1
，
・・
・
●
1
1
・
・
・
っ
・・
σ 乞t σ
β
，
，
，
，
，
・
・，
r
・
σ
・
1
・
・
，
・
・・
・
1
・
σ
，
この
2つ
E ）上
（V ，
の
σ
・・
・
・
，
・
限
の
，
CDP
鎖
Proc
が
存在
しす
11
によって無限
CDP
鎖は変化
しない
・
・
）
sl 擁〉Ct ）
ε ≠ ＞
c ゴ）
，
（
（（
1（
（
）が含まれない場合
，
・
，
るが
σ
σ
・
，
・
σ
・・
1
・ゴ
1
・
，
・
ロ
・
・
・
，
・
プ
・
，
・
・
・
・
，
σ ・σ ゴ
，
・
1
・
，
・
なお，既存の DP
・
セッサ
セソサにも導入可能である
，
V，
E ）上に無限 CDP 鎖が存在しない場合，
（
Proc によって無限 σDP 鎖が出現することはない．
・
，
・
，
・
系列が鎖となる条件は同じである
に無
・
・
，
1
・
，
11
1
・
，
1
・
・
，
・m
，
，
・
、
・
っ
・
・
・・
4 】の
［
技法
の
・
iCl
多くは CDP
プロ
．
6 ． CDP を用いた停止性証明例
●
よって
Pr σ c
本節では
CDP
を用いたプ
ロ
グラム
の
停止性証明の例を示す．
は健全かっ完全である．
一 65 一
一
NNII-Electronic
工工 Eleotronio
Library Service
Library
Institute
工nstitute
of
of
Eleotronios
Electronics,，Information,
工 nformation
and Co
Communication
unioation
Engineers
Engineers
，and
も削除できる，また，頂点（
c ）を始点とする辺と頂点
点とする辺が存在しなくなるため，定理 5 ．
4 のプ
d ）を終
（
セッサを用
ロ
いて
4 ）のグラフになる．この（
削除でき，（
部分）グラ
限長
の
経路は存在しな
7．
関連研究
61 で
［
規則
フには無
．
い
は組み込み意味論で評価される制約
付いた書換え
の
を用いる制約付き項書換え系の停止性を証明するために
graph −handling　DP fぬ
を提案している．依存対に条
mework
．また，
ている．
件部が付加されているが本論文とは条件の形式が異なる
本論文と同様に依存グラフを導入した
その中では制約を利用したグラフ
与えて
い
るが
8．おわ
本論文
CS −TRS
辺を削除するプ
の
っ
ロ
セッサを
．
りに
では例外処理を持つ関数型プ
新
の
問題を扱
，本論文で導入したような新たな頂点を加えるプ
セッサは定義されていない
ロ
GDP
しい
ロ
グラムから変換された
．条件付き依存対
停止性証明法を提案した
条件付き依存対鎖の定義を与え，例外処理を持つ関数型プ
GS −TRS
ラムから変換された
図 6
付き依存対鎖
グラフの変換
Fig ．
6　transf
プ
graph
｛）rmatioll
of ロ
セ
ッ
6．
1　例
3よ
定理 4．
り図
2 の CS −TRS
性に置き換えることができる．また
り図
3 の条件付
き依存対
CDP
CDP
停止性は最内
の
，この
φ（ア）を頂
鎖の存在
存在性は補題
3．
6よ
点とする完全グラフを
9。とするとき，（
R ）を入力とする最内 CDP 問題の有限性を
9。
，
調
ればよい，（
9。
R ）に定理 5 ．
3 のプセッサを適用すると図
，
6の（
1 ）のグラフが得られる．（
1 ）に定理 5 ，
5 のプセソサを適
2 ）のグラフが得られる．（
用すると（
2 ）に定理 5．
6のプセサ
を適用すると（
3 ）のグラフが得られる．頂点（
a ）（
b）
c）
e）
，
，
（
（d ）（
は以下のとおりである．
x
f D ta （
（）（
gt （
，
〈
）
gl （
y ）
〉i D ta （〉描
y ）→
tt）
，
b）（
x ，
1（，
（
gl （
，
．
〈
y ）
gtt（
y
）
〉，
y ） F 1e ）
：
C）（
19 （
iD t （
x ）→ tt 〈 i・D
（
（
9 （rg ，
Y9 ）
y ，）
，
ta（
〉
y ）
ttAJe （
Xg ，
False
，
Y9 ）
）
d ）　（〈
xlo ，
xlo ）
isData（
xlo ） →　亡亡く
（
9 （
Ylo），
9 ：（
Ylo ，
，
〉
fsDa 亡a （
1e
→
描
x
伽）
，
（
Y1 ） FaJse）．
e ）　（
Xl1
〔
9
，
xll ）
isData（
x11 ）
む亡く
（（ Yll）
，
95 （
Yl1，
〉，
→
isData（
se ）
，
Y11） tt 〈 1e＠ 11 ，
Y11 ） Fa 亅
で
経
路
c
d
が
CDP
＝
，
鎖となる条件は
（）（）
＝ Y12 YIO l＝ 12 ｝とすると，
Yg ＝ Y12 XIO
｛g ＝ X12 ，
→
isData（
Xg ）
tt〈 isData（
Xg ，
（
False 〈
Yg）→ tt 〈 Ie（
Yg ）
i D ta （）一 tt 〈 i D 亡（
→
x
y ） tt〈 1 （
，
y ） F 1 e）
である，fsData（
x12
→
tt
〈
isData
tt
〈
le（
x12
）
（
Y12）
，
Y12 ）→・
False〈 1e（
→
x12 ）
False は充足不能であるため，定理 5 ．
Y12 ，
3の
プ
セッサを用いて，辺 c
d
は
削
除
で
．
（）（）
きる同様に辺（
d）（
d）
べ
ロ
ロ
ロ
ッ
1
・
・
・・
iY
・
・
：
：
・
・，
・
・
， 7x
コ
・
，
・
、
・・・
・
・
・
・
，
・
→
、
・
→
，
1
・
・
，
・・
・
・
，
→
→
＃
：
→
・。
・
：
：
→
→
σ
＝
：
：
：
，
＝
，
→
・
・
＝・・
”　・
→
ロ
・
・
・・
→
・
・・
・。
・
・・
σ
し
ッ
非存在
ロ
プロセ
ッ
と
グ
最内停止性と無限の最内条件
の
が一致する
41 と GDP
［
サ
む関数型プ
プロセ
の
ロ
サ
．また，DP
61
を
拡
張
し
例
，外処理を含
［
ことを証明した
グラム停止性証明に有効な条件付き依存対問題の
サの定義を与えた．本手法による停止性証明器を実現
，有用性を示すこ
とが今後の課題である
文
．
献
‘
」
1 ］濱口毅，馬場正貴，酒井正彦，阿草清滋，例外処理を持っ関
［
”情報処理学会論文
非停止性証明法，
数型プログラムの停止性・
−
誌
プ
グ
ミ
ン
vQL4
ラ
グ
，
no
．
2
，
．
13
30
，2011 ．
pp
2］ J ．Giesl，
R ．
Thiemann
P．
Schneider −Kamp
and S ．
Falke
［
，
，
“
Proceedings
Automated termimation proofs with aprove ／
of the 15th　International　Conference　on Rewriting Tech −
niques and Applications（RTA −04 ）（Lecture Notes　in　CQm −
210 −220 ，
Aachen ，
Germany
puter Science　3091 ）　pp ．
，2004 ．
ロ
，
tt
1
3］
Alarc6n，
R ．
Guti6rrez ，
J ．
Iborra ，
and
［
B 、
termination
−sensitive
of context
Proceedings of
’
Lucas ，
S．
LProving
rewriting
with
mu
）
−term ，
−
t
the Sixth Spanish Conference
on Program
ming and Computer Languages PROLE 2006 （Electronic
pp ．
105 ．
／15 ，
，188 ），
Notes in　Theoretical Computer Science
，
2007 ．
4j　J ．
Giesl
R
［
，
P ，
Schneider −Kamp
， The
pair　fra皿 ework ： Combining techniquies　f r
”
automated
termination proefs 〜
Proceedings of llth
LNAI 3452 ）
pp ．
301 −331 ，
2005 ，
LPAR
（
，
5］ J ．Giesl，
S．
Swiderski
P ，
Schneider −Kamp ，
and R ．
Thie −
［
，
“
mann
Automated
termination
analysis for　haskell
FrQm
，
term
rewriting
to
languages
Proceedings
programming
；
of Term Rewriting and Applications 17th International
Conference RTA 2006 （Lec 七ure Notes　in　Computer Science
297 −312 Seattle USA ，
2006，
4098 ）．
“
．
6｝ T Sakata，
N ．
Nishida ，
and
T ．
Sakabe ，On proving termi −
［
nation
of constrained
term
rewrite
systems
by eliminating
，
Proceedings
of the 20th In−
edges 丘om dependency graphs ，
ternational　Workshop　on Functional and （Constraint
）Logic
WFLP 2011）in Vel ．
6816 of Lecture Notes
（
Programming
pp ．
138−155 ，
2011 ．
in　Gomputer　Science ，
7
F
．
Baader
and T ．
Nipkow ，
Term Rewriting and All　Thatl
［］
1998 ．
Cambridge University Pres ＄，
dependency
．Thiemann ，and
”
｛）
，
：
’
1pp
，
，
i
一 66 一
一
NNII-Electronic
工工 Eleotronio
Library Service
Library

Download Report