抽象解釈と静的解析の理論

抽象解釈が答える問い

「このプログラムは決して配列の範囲外アクセスをしないか」「この変数は実行時に必ず正か」——こうした問いに、プログラムを動かさず・すべての入力に対して一括で答えたいのが静的解析です。だが厳密に答えようとすると停止性問題に行き当たり、非自明な意味的性質は一般に決定不能です。抽象解釈（abstract interpretation）は、Cousot 夫妻が定式化した「厳密解は諦め、安全な近似を体系的に作る」枠組みで、近似がどちら側に倒れるかを理論で固定することで健全性（soundness）——危険を見逃さないこと——を設計から保証します。

出発点は、プログラムの最も詳細な意味です。各プログラム点に、そこへ到達しうる具体的な状態（変数の値の組）の集合を割り当てたものを**収集意味論（collecting semantics）**と呼びます。これは「真に成り立つこと」の全体ですが、状態集合は無限になりうるうえ、そもそも計算できません。抽象解釈はこれを計算可能な対象へ写します。

抽象領域と格子

近似の舞台は**格子（lattice）です。集合 L に半順序 ⊑（「より精密／情報が多い」を表す）が入り、任意の二元に上限 ⊔（join）と下限 ⊓（meet）が定まる構造で、最大元 ⊤（何も分からない＝全状態）と最小元 ⊥（到達不能）を持つ完備格子を使います。具体側は状態集合の冪集合 P(States) がそのまま格子（包含で順序付け）になり、抽象側には目的に応じた抽象領域（abstract domain）**を設計します。

たとえば区間領域では、変数 x が取りうる具体値の集合 {2,5,9} を区間 [2,9] で近似します。[2,9] は元の集合を含む（過剰に見積もる）ので安全側であり、かつ有限のデータで表せて計算可能です。順序は区間の包含で、[2,9] ⊑ [0,100]、join は両区間を覆う最小区間です。

ガロア接続 — 具体と抽象を正しく結ぶ

具体格子 C と抽象格子 A を結ぶのがガロア接続（Galois connection）です。具体側を抽象側へ写す抽象化関数 α: C → A と、抽象値が表す具体集合へ戻す具体化関数 γ: A → C の対が、次の条件を満たすときガロア接続をなします。

α(c) ⊑ a   ⟺   c ⊑ γ(a)     （任意の c ∈ C, a ∈ A）

直観的には「c の抽象が a 以下であること」と「c が a の表す具体集合に含まれること」が同値、という対応です。ここから c ⊑ γ(α(c)) が導かれます。これは決定的に重要で、**具体値をいったん抽象化して戻すと、必ず元を含む（情報は失っても取りこぼさない）**ことを意味します。区間なら α({2,5,9}) = [2,9]、γ([2,9]) = {2,3,…,9} で、確かに元の集合を包含します。この「戻すと膨らむ」性質こそが、近似が安全側にしか倒れない理論的根拠です。

抽象転送関数と最良近似

各文の具体的な作用（状態集合をどう変えるか）を f: C → C とすると、抽象側でそれに対応する抽象転送関数 f#: A → A が要ります。健全性の条件は、抽象が具体を必ず覆うこと、すなわち次の不等式です。

α ∘ f  ⊑  f# ∘ α     （または等価に f ∘ γ ⊑ γ ∘ f#）

この条件を満たす f# のうち最も精密なものは f# = α ∘ f ∘ γ で与えられ、**最良抽象（best abstraction）**と呼ばれます。たとえば区間領域での加算は [a,b] +# [c,d] = [a+c, b+d] と定義でき、これは具体的な要素ごとの加算を区間で覆う最良近似です。設計者がこの不等式を各演算で守る限り、解析全体の健全性は局所的な健全性から合成的に従います。

固定点としての解 — クリーネ反復

ループや再帰があると、解析対象の方程式は自分自身を参照します。各プログラム点の抽象状態を未知数とする方程式系 X = F#(X) の解が求める解析結果で、その正体は**固定点（fixpoint）**です。タルスキの定理により、完備格子上の単調関数は必ず最小不動点を持ち、それが「すべての方程式を満たす最も精密な解」に対応します。

最小固定点は**クリーネ反復（Kleene iteration）**で構成的に求まります。⊥ から出発し、F# を繰り返し適用する上昇鎖を作ります。

X0 = ⊥
X1 = F#(X0)
X2 = F#(X1)
…
Xn が安定（F#(Xn) = Xn）したら、それが最小固定点

F# の単調性により列は単調増加し、格子が有限高（finite height）——任意の上昇鎖が有限長で止まる——なら必ず有限回で安定します。符号領域や有限の型領域はこの性質を持ちます。この骨格はデータフロー解析のワークリスト反復と同一で、データフロー解析は抽象解釈の特殊例（特に gen-kill 型の有限格子の場合）として理解できます。

幅演算と狭め演算 — 無限格子で停止させる

区間領域や多面体領域は無限高です。たとえば i = 0; while (…) i = i + 1; を区間で素朴に反復すると、[0,0] ⊑ [0,1] ⊑ [0,2] ⊑ … と上限が際限なく伸び、固定点に到達しません。これを有限時間で打ち切るのが**幅演算（widening, ▽）**です。幅演算は、上昇鎖が「まだ伸びそう」と見るや一気に ⊤ 側へ飛ばし収束を強制します。区間の典型的な幅演算は、上限が増え続けるなら上限を +∞ に飛ばす、という規則です。

[0,0] ▽ [0,1] = [0, +∞)     上限が増加 → 一気に無限へ

幅演算は安全側（過剰近似側）へ飛ばすので健全性は保たれますが、精度を犠牲にします。そこで反復後に**狭め演算（narrowing, △）**を施し、健全性を崩さない範囲で ⊤ へ飛ばし過ぎた境界を引き戻して精度を回復します。たとえば上のループに i が 100 未満 という条件があれば、狭めで [0, +∞) を [0,100] まで縮められます。

型推論・型システムへの応用

抽象解釈の見方は、静的解析を超えて型システムへも及びます。型を「値の集合の抽象」と捉えると、型付けは収集意味論の抽象解釈に対応します。Hindley-Milner 型推論が単一化で最汎な型を求めるのも、各式の取りうる値を型という抽象領域へ写し、制約の最小解（最も精密な健全解）を固定点的に求める営みと読み替えられます。

部分型を持つ型システムでは型の集合が格子をなし、join（最小上界）と meet が部分型関係から定まります。フロー感応な型解析（変数の型を制御点ごとに絞り込む）や、Null 安全性・テイント解析は、まさに抽象領域を取り替えた抽象解釈の実例です。健全性と精度のどちらを取るかという設計判断が、言語の型システムの厳しさとして表面化します。

まとめ

抽象解釈は、計算不能な収集意味論を、ガロア接続 (α, γ) で結ばれた抽象領域へ安全に写し、c ⊑ γ(α(c)) という過剰近似性によって健全性を保証する枠組みです。各演算には健全な抽象転送関数 f#（最良近似は α ∘ f ∘ γ）を与え、解析結果は単調関数の最小固定点として、⊥ からのクリーネ反復で求めます。有限高の領域は自然に停止し、区間や多面体のような無限高の領域では幅演算で収束を強制し、狭め演算で精度を取り戻します。データフロー解析・区間解析・型推論・テイント解析はいずれも抽象領域を取り替えただけの同一理論の応用であり、抽象解釈は「静的解析がなぜ健全か」を一枚の格子論で説明する基盤理論です。