|
プログラム意味論()とは、計算機科学(特に理論計算機科学と分類されることもある)の一分野で、プログラミング言語の意味と計算モデルに関する分野である。形式的なものは、プログラミング言語の形式意味論とも呼ばれる。標準規格等では形式的でなく意味論を与えているものも多い。 == 形式的意味論 == 形式化にはいくつかの手法があり、以下の 3 種類に大別される: * 表示的意味論: 対象とする言語の語句それぞれを「表示」に変換、すなわち別の言語の語句に翻訳する。表示的意味論はコンパイルと対応すると考えることもできるが、通常翻訳先の言語は他のコンピュータ言語ではなく数学的形式言語であることが多い。例えば、関数型言語の表示的意味論では、領域理論の言語に翻訳する。 * 操作的意味論: 何らかの変換を施すのではなく、その言語の実行によって直接的に意味を説明する。操作的意味論はインタプリタと対応すると考えることもできるが、この場合の「インタプリタの実装」は何らかのコンピュータ上での実装ではなく、数学的形式主義によるものである。操作的意味論を抽象機械(例えばSECDマシン)と定義することも可能で、プログラムの語句の並びが抽象マシンの上で引き起こす状態変化を説明することによって各語句の意味を説明する。あるいは、純粋なラムダ計算のように、操作的意味論を対象言語の語句の並びの統語的変形過程と定義することもできる。 * 公理的意味論: 語句の並びに「論理学的公理」を適用することによって意味を明らかにする。公理的意味論では語句の意味とそれを表す論理式を区別しない。この場合、プログラムの意味は論理学で証明可能なものと等価である。公理的意味論の典型的な例としてホーア論理がある。 この分類は必ずしも完全ではなく、また明確に分類できるものでもないが、既存の、意味論を形式化する手法は上記3種類のいずれかを使っているか、いくつかを組み合わせている。上記分類とは別に、利用している数学的形式手法によってプログラム意味論を分類することもある。 抄文引用元・出典: フリー百科事典『 ウィキペディア(Wikipedia)』 ■ウィキペディアで「プログラム意味論」の詳細全文を読む 英語版ウィキペディアに対照対訳語「 Semantics (computer science) 」があります。 スポンサード リンク
|