widening解説
2013年12月 舟越 和己
この資料は、初めにwideningの要点を説明し、その後に参考としてFlemming Nielson他著：Principles of Program Analysisの第4章 Abstract Interpretationのwideningの内容を紹介する。
１．wideningの要点
抽象解釈では、プログラムの安全性（例えば変数がオーバーフローしないなど）はプログラムのセマンティクスを考え、変数の単調増大する存在範囲の最小不動点を求めることで得られる。このとき最小不動点が存在することはタルスキの不動点定理から保証されるが、これは存在定理であり、実際にはこの不動点の近似値を有限回の操作で求める方法が必要となる。wideningはこれを求める手法である。
１．１ widening演算子の定義
下記を満たすとき、∇：L×L→Lがwidening演算子であるという；
① ∇は上界演算子である。すなわち、任意のx, y∈Lに対して、x∪y⊆x∇y
② 有限鎖(Chain)の条件： 任意の単調増大する鎖 x0⊆x1⊆・・・⊆xn・・・に対して、
∇演算子による鎖 y0=x0, y1=y0∇x1, y2=y1∇x2,・・・, yn+1=yn∇xn+1,・・・
は、有限で安定する（増大が有限回で止まる）
（例）widening演算子の具体例としては下記がある；
１．２ widening演算子の性質
いまwidening演算子∇が定義できたとし、完備束L上に与えられた任意の単調関数（注）f：L→Lが与えられたとする。
（注）半順序集合L上のf：L→Lが単調関数(monotone function)であるとは、任意のl, l'∈Lに
対して、l⊆l'ならばf(l)⊆f(l')が成立すること。すなわち、順序保存である。isotoneとも言う。
このとき、fとwidening演算子∇から下記の式
により生成される上昇鎖(fn∇)n：f0∇=⊥, f1∇=⊥∇f(⊥), f2∇= f1∇∇f(f1∇),・・・は有限回で増加を止めて安定し、かつfの最小不動点の近似となることが示される（この証明は次頁以降を参照）。つまり、widening演算子はfの不動点の近似値を有限回の操作で求める方法を提供している。
以上を纏めると、
「widening演算子∇が定義されたとすると、完備束上の単調関数fの最小不動点の近似は、fにその∇を有限回作用させることで得られる。」
①wideningの具体例；
区間の集合に対してwidening演算子を以下のように定義する
このとき、∇はwidening演算子の条件を満たす；
(xn)：⊥⊆[0, 0]⊆[0, 1]⊆[0, 2]⊆・・・・
に対して、y0=⊥, y1=y0∇x1=⊥∇[0, 0]=[0, 0], y2=y1∇x2=[0, 0]∇[0, 1]=[0,∞],
y3=y2∇x3=[0,∞]∇[0, 2]=[0,∞]
となり、(yn)：⊥⊆[0, 0]⊆[0,∞]=[0,∞]・・・
すなわち、有限回（3回）で[0,∞]に収束する。
②下記の再帰処理の式をwideningで解く；
上記の式は左側の変数X2が右側の変数X2の関数で表現されている（すなわち、右側の変数X2に対して右側の式の値が変数X2の次の値を決める）。これを関数Fで表現すると、
X2(i+1)=F(X2(i))=[0, 0]∪((X2(i)∩[-∞, 99])[x:=x+1])
この式の変数X2の最初の4個の値（X2(0),X2(1),X2(2),X2(3))を求めると、
したがって、Fは下記を対応させる単調関数である；
F(⊥)=[0, 0], F([0, 0])=[0, 1], F([0, 1])=[0, 2], ...F([0,∞])=[0,∞]
上記はF0(⊥)=⊥として次のように表現できる；
F1(⊥)=[0, 0],
F2(⊥)=F(F1(⊥))=F([0, 0])=[0, 1],
F3(⊥)=F(F2(⊥))=F([0, 1])=[0, 2],
...
すなわち、F0⊆F1⊆F2⊆F3⊆・・・
この単調関数Fに対し、区間の集合で定義したwidening∇から１．２項のfn∇のように上昇鎖を作るとFn∇は有限回で安定する；実際、
F0∇=⊥,
F1∇= F0∇∇F(F0∇)=⊥∇F(⊥)=⊥∇[0, 0]=[0, 0]
F2∇= F1∇∇F(F1∇)=[0, 0]∇F([0, 0])=[0, 0]∇[0, 1]=[0,∞]
F3∇= F2∇∇F(F2∇)=[0,∞]∇F([0,∞])=[0,∞]∇[0,∞]=[0,∞]
すなわち、widening演算子により
F0⊆F1⊆F2⊆F3⊆・・・という有限でない単調増加列に対し、
F0∇⊆F1∇⊆F2∇= F3∇=・・・という有限で安定する単調増加列が作られる。
ここで、F0∇⊆F1∇⊆F2∇= F3∇=・・・の安定した値F3∇をX=F(X)に代入することを考える；
これは縮小写像F(Fm∇)⊆ Fm∇となり、F(Fm∇)はFの最小不動点の近似値となることが知られている（この証明は第２節参照）。
上記の例でF(F2∇)を求めると、
F(F2∇) =[0, 0]∪((F2∇∩[-∞, 99])[x:=x+1])
=[0, 0]∪(([0,∞]∩[-∞, 99])[x:=x+1])
=[0, 0]∪(([0, 99])[x:=x+1])
=[0, 0]∪[0, 100]
=[0, 100]
これを図で示すと次のようになる；
【上図の説明】 Fの最小不動点の近似を有限回の操作で求めるために、F0⊆F1⊆F2⊆F3⊆・・・という有限でない単調増加列の代わりに、F0∇⊆F1∇⊆F2∇= F3∇=・・・という有限で安定する単調増加列を作り、これをF(X)に代入（F(F2∇))している。
■CousotのMIT講義資料のwidening図示について
CousotのMIT講義のスライド1ではwideningを下記の手順（①～③）で表現している；
①まず、区間の完備束上の単調関数Fを下記で定義する；
F(区間のトレース）=トレースの各区間の和
このとき、Fは単調増加関数になる；
②区間のwidening∇の定義は下記を使用する；
③区間のwidening∇が安定する図が下に、∇を関数Fに作用させたFn∇が安定する図が上である；
２．（参考）Principles of Program Analysisの第4章のwidening紹介
この本には、「widening演算子∇が定義されたとすると、完備束上の単調関数fの最小不動点の近似は、fにその∇を有限回作用させることで得られる。」ことの数学的証明が書かれているので、下記にこれを紹介する。証明は少し長いが数学的帰納法と背理法を使用している。
２．１ 用語の説明
①プログラムのセマンティクス
プログラムpのセマンティクスは、状態、区間、倍精度の実数のような値の集合Vに対し、プログラムpがVの１つの値v 1を他の値v2にどのように変換するかを規定する。
（例）トレースセマンティクス：プログラムポイントppと変数の値xの組(pp, x)の集合。
→これは(pp, x)がどのように推移するかを示している。
②プログラム解析
プログラム解析とは、抽象区間、実数の上下限のようなプロパティの集合Lに対し、プログラム pがLの１つのプロパティl1を他のプロパティl2にどのように変換するかを規定する。
すなわち、プログラムpのプログラム解析をfpとすると、fp(l1)= l2である。ここで、fが単調であるという要求はプログラク解析で非常に自然なことである。
２．２ 有限な列で不動点近似を求めること
完備束L=(L,⊆,∪,∩,⊥,Τ）を与えたとき、１つのプロパティl1を他のプロパティl2に変換するプログ ラムpの結果はプログラムpに依存する単調関数fp： L→ Lに対して式fp(l1)=l2により与えられる。fpが単調であるという要求はプログラク解析で非常に自然なことである； それは単に、l1'がl1より小さい値を記述するならば、fp(l1')もfp(l1)より小さい値を記述することを言っているだけである。
再帰的または繰り返しのプログラムの構成に対しては、有限の繰り返しプロセスの結果として、最小不
動点(least fixed point) lfp(f)を獲得したい。しかし有限の範囲では、単調増加する繰り返しのシーケンス (f n(⊥)) n =( f (⊥),f2(⊥)=f (f (⊥)), f3(⊥)=f (f (f (⊥))),・・・, fn(⊥)=f (・・・f (f (⊥))) )は最終的に安定する必要はなく、その上限は必ずしもlfp(f)と等しくなる必要はない。
有限の繰り返しのシーケンス(f n(⊥)) nは最終的に安定することもその上限が必ずlfp(f)と等しくなるということも保証できないので、lfp(f)を近似する他の方法を考えなければならない。
→ここに、wideningという概念が登場する。その概念は、最終的に安定し最小不動点の安全な（上位）近似の値を持つことで知られる新しいシーケンス(f∇n ) nにより(f n(⊥)) nを置換えることである。
２．３ 上界演算子(upper bound operators)
完備束L=(L,⊆ )上の演算子∪～：L×L→ Lは下記が成り立つとき、上界演算子と呼ばれる；
任意のl1, l2∈Lに対して、l1⊆ ( l1∪～l2)⊇ l2
すなわち、演算子∪～ は常にその引数のどちらよりも大きな要素を返す。
(ln)n={l1, l2,・・・, ln}をLの要素のシーケンスとし、φ：L×L→LをL上の全域関数(total function)とする。φを使用して以下で定義される新しいシーケンス(lφn)n={lφ1, lφ2,・・・, lφn}を構成する（訳注）；
n=0のとき、lφn= ln n＞０のとき、lφn= lφn-1φln （式１）
（訳注） 順次式を展開すると、lφnはφによるl0からlnまでの合成関数で表される；
lφ0=l0
lφ1=lφ0φl1=l0φｌ１
lφ2=lφ1φl2=(l0φｌ１)φl2
lφ3=lφ2φl3=((l0φｌ１)φl2)φl3
・・・
lφn=lφn-1φln=((l0φｌ１)φl2)φl3)φ・・・)φln
このとき、任意のシーケンスは次のFact 4.11のように上界演算子により上昇鎖に転換することができる：
Fact４．１１ (ln)nをシーケンスとし、∪～を上界演算子とするとき、(l∪～n)nは上昇鎖である； さらに、
全てのnに対して、l∪～n ⊇ ∪{l0, l1, ..., ln}
証明 (l∪～n)nが上昇鎖であることを示すには、任意のnに対してl∪～n⊆ l∪～n+1を示せばよい。
n=0とすると、上記の（式１）でφ=∪～と置き、∪～が上界演算子であることからl∪～0= l0⊆l0∪～l1= l∪～1
したがって、n=0のとき (l∪～n)nは上昇鎖である。n＞0のとき∪～が上界演算子であることからl∪～n ⊆
l∪～n∪～ln+1となる。一方、上記の（式１）からn＞0のときl∪～n ∪～ln+1 = l∪～n+1である。したがって、n＞0のとき、l∪～n⊆l∪～n+1が成立し、上昇鎖となる。 また、l∪～n-1 ∪～ln = l∪～nかつ∪～が上界演算子であることからln⊆(l∪～n-1 ∪～ln )= l∪～nとなり、ln⊆l∪～nが成立する。したがって、l0⊆l∪～0, l1⊆l∪～1, l2⊆l∪～2,・・・, ln⊆l∪～nかつ(l∪～n)nが上昇鎖であることからl0, l1, ..., ln⊆l∪～n が得られる。 ■
２．４ widening演算子(widening operators)
最小不動点の近似に使用できる特別なクラスの上界演算子∇を導入する。
演算子∇：L×L→Lは下記の条件を満たすときwidenig演算子という；
● ∇は上界演算子である。
● 任意の上昇鎖(ln)nに対して、上昇鎖(ln∇)nは最終的に安定する。
(ln∇)nが実際に上昇鎖であることはFact4.11から導かれる。
∇が最小不動点の近似をサポートするという考えは以下の通りである；
単調関数f：L→Lが完備束上に与えられ、widening演算子∇が与えられたとき、下記の式により定義さ れたシーケンス(fn∇)nを計算する。
Fact４．１１により、これは上昇鎖であることが分かり（この証明はFact4.14の(i)を参照）、下の命題4.13によりこのシーケンスが最終的に安定することを保証する。Fact４．１４から、これはあるmに対してf(fm∇)⊆fm∇であることを意味する。これはfがfm∇で縮小的(reductive)であることを意味し、タルスキの不動点定理からf m∇⊇lfp(f)でなければならないことが分かる（この証明はFact4.14の(iv)を参照）；したがって、lfp(f)の望ましい安全な近似として、 lfp∇(f) = fm∇ が得られる。図４．４にこれが図示されている。
しかし、f(fm∇)⊆fm∇であり、f(fm∇)⊇lfp(f)なので、この近似lfp∇(f)はf(fm∇)により改善される。fを繰り返すと
f(fm∇)⊇f2(fm∇)⊇・・・⊇fn(fm∇)⊇lfp(f)という下降鎖(descending chain)が得られ、近似lfp∇(f)はfn(fm∇)によりさらに改善される。
---------------------------------------------------------------------
命題 ４．１３ ∇がwidening演算子ならば、上昇鎖(fn∇)nは最終的に安定する。
---------------------------------------------------------------------
命題４．１３の証明の準備として、以下のFactを最初に示す；
Fact４．１４ ∇がwidening演算子ならば、下記が成立する；
(i)シーケンス(fn∇)nは上昇鎖である。
(ii)あるmに対してf(fm∇)⊆fm∇ならば、任意のn＞mに対して(fn∇)nは最終的に安定する：
すなわち、fn∇= fm∇ かつ∪nfn∇= fm∇
(iii) (fn∇)nが最終的に安定するならば、f(fm∇)⊆fm∇となるようなmが存在する。
(iv) (fn∇)nが最終的に安定するならば、∪nfn∇⊇lfp(f)
証明
(i) fn∇の定義よりn＞0のとき、
f(fn-1∇)⊆fn-1∇ならば、fn∇=fn-1∇ ・・・①
f(fn-1∇)⊆fn-1∇でないならば、fn∇=fn-1∇∇f(fn-1∇)・・・②
∇は上界演算子なのでfn-1∇⊆fn-1∇∇f(fn-1∇)・・・③
②③より、fn-1∇⊆fn-1∇∇f(fn-1∇)= fn∇・・・④
①④から何れの場合もn＞0のとき、fn-1∇⊆fn∇ となり、上昇鎖である。
(ii)あるmに対してf(fm∇)⊆fm∇と仮定する。帰納法により、n＞mに対してfn∇=fm∇であることを示す：
f(fm∇)⊆fm∇とfn∇の定義から①よりfm+1∇=fm∇ が成立する。したがって、n=m+1のとき、fn∇=fm∇ が成立する。n=k＞m+1に対してfk∇=fm∇と仮定すると、n=k+1のとき、fの単調性からf(fk∇)⊆f(fm∇)、f(fm∇)⊆fm∇なのでf(fk∇)⊆fm∇=fk∇となる。したがって、fn∇の定義からfk+1∇=fk∇となる。即ち、数学的帰納法（注）によりn＞mに対してfn∇=fm∇が成立することが証明された。また、(fn∇)nは上昇鎖なので∪nfn∇= fn∇= fm∇
（注）：n=m+1のとき成立することが示され、n=k＞m+1に対して成り立つと仮定すると、n=k+1のとき
成り立つことが示された。
(iii) (fn∇)nが最終的に安定すると仮定すると、これは、或るmが存在して、任意のn＞mに対して
fn∇= fm∇が成立することである。ここで、背理法によりf(fm∇)⊆fm∇が成立しないとすると、
fn∇の定義の3番目の式が成立するので、fm+1∇=fm∇∇f(fm∇)・・・①
仮定よりfm+1∇=fm∇・・・・②
∇は上界演算子なのでfm∇∇f(fm∇)⊇f(fm∇)・・・・③
①②③から、fm+1∇⊇f(fm∇)これは背理法の仮定に矛盾する。
したがって、f(fm∇)⊆fm∇が成立する。
(iv) (fn∇)nが最終的に安定するならば、(iii)からf(fm∇)⊆fm∇となるようなmが存在する。(ii)より
f(fm∇)⊆fm∇となるようなmとn＞mに対して、∪nfn∇= fm∇が成立する。
f(fm∇)⊆fm∇より、fm∇∈Red(f)であり、タルスキの不動点定理よりlfp(f)=∩Red(f)⊆fm∇
したがって、fm∇=∪nfn∇⊇lfp(f)となる。 ■
以上の準備（Fact4.14)をもとに命題４，１３の証明を下記に示す；
証明 背理法により証明するため、上昇鎖(fn∇)nは決して安定しないと仮定する。すなわち、
任意のn0に対して或るn≧n0が存在して、fn∇≠fn0∇・・・① とする。
上昇鎖(fn∇)nは決して安定しないならば、Fact4.14(ii)より任意のn＞0に対してf(fn-1∇)⊆fn-1∇は成立しない。これはfn∇の定義から下記が成立することを意味する；
fn∇=⊥ (n=0のとき） fn∇= fn-1∇∇f(fn-1∇) （n＞0のとき）
今、シーケンス(ln)nを下記により定義する；
ln=⊥ (n=0のとき） ln= f(fn-1∇) （n＞0のとき）
(ln)nは上昇鎖となる(⇒Fact4.14(i)より(fn∇)nは上昇鎖であり、fは単調なので）。
次に、任意のnに対して、ln∇=fn∇が成立することを数学的帰納法により示す；
n=0のとき、この式は成立する（⇒l0∇=l0=⊥、f0∇=⊥）。
n-1に対して成立すると仮定し、n＞0の場合を考える。定義より、ln∇=ln-1∇∇ln
n-1に対してln-1∇=fn-1∇なので、ln∇=ln-1∇∇ln = fn-1∇∇ln= fn-1∇∇f(fn-1∇)= fn∇
したがって、任意のnに対して、ln∇=fn∇が成立する。
一方、(ln)nは上昇鎖で∇はwidening演算子なので、(ln∇)nは最終的に安定する。
すなわち、(fn∇)も最終的に安定する。これは最初の仮定に矛盾する。
したがって、 上昇鎖(f n∇)nは最終的に安定する。 ■
－ 以上 －