抽象解釈
ウィキペディアから無料の百科事典
抽象解釈（ちゅうしょうかいしゃく、英: Abstract interpretation）は、コンピュータプログラムの意味論の健全な近似の理論であり、順序集合（特に束）における単調関数に基づいている。全ての計算を実施することなく、プログラムの部分的な実行（ある種の部分評価）をするものと見ることができ、それによりプログラムの意味に関する情報（例えば、制御構造、情報の流れなど）を獲得する。
主な応用として、形式的な静的コード解析があり、プログラム実行に関する情報を自動抽出するものである。このような解析には次の2つの利用法がある。
抽象解釈は、Patrick Cousot と Radhia Cousot によって定式化された。
直観的解説[編集]
コンピュータ以外の実世界の例で、抽象解釈の意味を解説する。
会議室に人々が集まっているとする。ある人物がまだ来ていないことを証明したい場合、最も確実な方法は出席者の名前と何らかのID番号（例えばアメリカなら社会保障番号）をリストアップしていけばよい。2人の人間が同じID番号を持つことはないので、このリストを参照すれば特定の人物が出席しているか否かは簡単に判明する。
ここで、名前しかリストアップできないとする。ある人物の名前がリストにない場合、その人物が出席していないということは確実と思われる。しかし、もしあったとしても、出席していると確実に断言できるわけではない。なぜなら、同姓同名の別人かもしれないからである。実際には同姓同名はそうあることではないので、このような不正確な情報でも多くの場合は意味がある。しかし厳密に言えば、その人物が出席していると確実に言えるわけではなく、単に「おそらく」出席しているだろうとしか言えないのである。探している人物が犯罪者なら、「警報」を鳴らすことになるだろう。しかし、その警報が誤りである可能性ももちろんある。同様の現象はプログラムの解析においても発生する。
例えば「n歳の人物がその部屋にいるか」といった特定の情報だけを欲しい場合、名前と生年月日のリストを作る必要はない。単に出席者の年齢のリストだけを作れば、正確に質問に答えられる。そのようなリストを作るのも困難な場合、出席者の最小年齢 m と最大年齢 M だけを保持するものとする。もし質問の年齢 n が m より小さいか M より大きいなら、そのような人物はいないと確実に答えられる。しかし、それ以外の場合は「わからない」としか答えられないだろう。
コンピュータの場合、確実で正確な情報は、一般に有限の時間とメモリで計算できない（ライスの定理とチューリングマシンの停止問題を参照）。抽象化によって、問題を自動的に解けるレベルにまで単純化する。重要な問題は、「このプログラムはクラッシュするか?」といった質問に答えられるだけの精度を保ちつつ、問題（プログラム）を扱える程度にまで抽象化によって簡略化できるか、である。
コンピュータプログラムの抽象解釈[編集]
プログラミング言語や仕様記述言語について、抽象解釈は抽象関係でリンクされたいくつかの意味論を与える。意味論とは、プログラムの振る舞いについての数学的説明である。プログラムの実際の実行に非常に近い、最も正確な意味論を concrete semantics（具体的意味論）と呼ぶ。例えば命令型言語の concrete semantics は、各プログラムが生成する実行トレースのようなものである。実行トレースはプログラム実行時の一連の状態であり、状態はプログラムカウンタの値とメモリの内容（広域変数、スタック、ヒープなど）からなる。より抽象化された意味論はそこから抽出される。例えば、実行時に到達可能な状態の集合だけを考慮する意味論が考えられる。
静的解析の目標は、いくつかの点で計算可能な意味解釈を抽出することである。例えば、整数の変数を具体的な値ではなくその符号（正、負、ゼロ）だけで表すことでプログラムの状態を表す。乗算などの基本演算について、このような抽象化では精度は失われない。積の符号を知るには、引数の符号がわかれば十分である。他の演算については、この抽象化で精度を失う可能性がある。例えば、引数が正と負の2つであった場合、その和の符号を知ることはできない。
精度を失うことは、意味論を決定可能にするのに必須な場合もある（ライスの定理とチューリングマシンの停止問題参照）。一般に、解析の精度とその決定性（計算可能性理論）や tractability（計算複雑性理論）はトレードオフの関係にある。
実際に定義される抽象は、解析したいプログラムの属性と対象プログラム群に合わせて調整される。
形式的定義[編集]
L を concrete set（具体集合）という順序集合とし、L′ を別の順序集合 abstract set（抽象集合）とする。これら2つの集合は相互に元をマップする全域関数によって関連付けられる。
関数αは abstraction function（抽象化関数）と呼ばれ、x が L の元であるとき、α(x) が L′ の元となる。すなわち、L′ の元 α(x) は L の元 x の抽象化（abstraction）である。
関数γは concretization function（具体化関数）と呼ばれ、x′ が L′ の元であるとき、γ(x′) が L の元となる。すなわち、L の元 γ(x′) は L′ の元 x′ の具体化（concretization）である。
L1、L2、L′1、L′2 を順序集合とする。具体的意味論 f は、L1 から L2 への単調関数である。L′1 から L′2 への関数 f′ を f の「妥当な抽象化; valid abstraction」と呼び、L′1 に属する全ての x′ について (f ∘ γ)(x′) ≤ (γ ∘ f′)(x′) が成り立つ。
プログラム意味論は一般に、ループや再帰関数における不動点を使って表される。L が完備束で、f が L から L への単調関数とする。すると、f′(x′) ≤ x′ であるような x′ は f の最小不動点の抽象化である。
ここで問題となるのは、そのような x′ を求める方法である。L′ の高さが有限であるか、少なくとも昇鎖条件（全ての昇順は最終的に定常である）があるなら、そのような x′ は帰納によって次のように定義された昇順 x′n の定常の限界値として得られる。
- x′0=⊥ （L′ の極小な元）
- x′n+1=f′(x′n)
それ以外のケースでも、widening operator ∇ を通して、そのような x′ を得ることが可能である。これは、全ての x と y について x ∇ y が x と y のどちらよりも大きいか等しいという演算である。ここで全ての順序 y′n について、次のように定義される順序は最終的に定常的である。
- x′0=⊥
- x′n+1=x′n ∇ y′n
従って、y′n=f(x′n) となる。
場合によっては、ガロア接続（Galois connection）(α, γ) を使って抽象化を定義できる。ここで、αは L から L′ への関数、γは L′ から L への関数である。これは、必ずしも存在するとは限らない最良の抽象化の存在を前提としている。例えば、実数の組 (x,y) の集合を凸多面体で囲むことで抽象化する場合、x2+y2 ≤ 1 で定義される円板の最良の抽象化は存在しない。
抽象領域の例[編集]
プログラムのある時点で、変数 x に代入されている値の区間が [lx,hx] であるとする。値 v(x) を x に代入していることがその具体化であるとき、v(x) は [lx,hx] の区間にある。変数 x と y の区間が [lx,hx] と [ly,hy] であるとき、x+y ([lx+ly,hx+hy]) や x-y ([lx-hy,hx-ly]) の区間も容易に得られる。これは「厳密な; exact」抽象化であり、例えば x+y の取りうる値の集合はその区間([lx+ly,hx+hy])と正確に対応している。同様のより複雑な定式化が、乗算や除算などについても導出できる。これを interval arithmetics（区間演算）と呼ぶ。
ここで次のような単純なプログラムを見てみよう。
y = x; z = x - y;
一般的な算術型であれば、z の値はゼロになるはずである。しかし、ここで区間演算を行うために x の区間を [0,1] とすると、z の区間は [-1,1] となる。個々の演算は厳密に抽象化されているのに、それを合成した結果は厳密ではない。
問題は明らかである。ここでは x と y の値が等価であるという関係を無視していた。実際、区間の領域では変数間の関係は考慮されない。これを non-relational domain と呼ぶ。non-relational domain は高速で実装が容易であるが、正確とは言えない。
変数間の関係を扱う抽象領域の例として次のものがある。
- 凸多面体 - 計算コストが高い。
- "octagons"（八角形）
- difference-bound matrices
- linear equalities
そして、これらを組み合わせたものもある。
抽象領域を選んだとき、細かな関係性を保持しようとすれば、計算コストも高くつくのが一般的である。