抽象解釈（ちゅうしょうかいしゃく、）は、コンピュータプログラムの意味論の健全な近似の理論であり、順序集合（特に束）における単調関数に基づいている。全ての計算を実施することなく、プログラムの部分的な実行（ある種の部分評価）をするものと見ることができ、それによりプログラムの意味に関する情報（例えば、制御構造、情報の流れなど）を獲得する。主な応用として、形式的な静的コード解析があり、プログラム実行に関する情報を自動抽出するものである。このような解析には次の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）である。"L"、"L"、"L"′、"L"′ を順序集合とする。具体的意味論 "f" は、"L" から "L" への単調関数である。"L"′ から "L"′ への関数 "f"′ を "f" の「妥当な抽象化; valid abstraction」と呼び、"L"′ に属する全ての "x"′ について ("f" ∘ γ)("x"′) ≤ (γ ∘ "f"′)("x"′) が成り立つ。プログラム意味論は一般に、ループや再帰関数における不動点を使って表される。"L" が完備束で、"f" が "L" から "L" への単調関数とする。すると、"f"′("x"′) ≤ "x"′ であるような "x"′ は "f" の最小不動点の抽象化である。ここで問題となるのは、そのような "x"′ を求める方法である。"L"′ の高さが有限であるか、少なくとも昇鎖条件（全ての昇順は最終的に定常である）があるなら、そのような "x"′ は帰納によって次のように定義された昇順 "x"′ の定常の限界値として得られる。それ以外のケースでも、widening operator ∇ を通して、そのような "x"′ を得ることが可能である。これは、全ての "x" と "y" について "x" ∇ "y" が "x" と "y" のどちらよりも大きいか等しいという演算である。ここで全ての順序 "y"′ について、次のように定義される順序は最終的に定常的である。従って、"y"′="f"("x"′) となる。場合によっては、ガロア接続（Galois connection）(α, γ) を使って抽象化を定義できる。ここで、αは "L" から "L"′ への関数、γは "L"′ から "L" への関数である。これは、必ずしも存在するとは限らない最良の抽象化の存在を前提としている。例えば、実数の組 ("x

出典:wikipedia