意味論（プログラミング言語）

プログラミング言語理論において、意味論とは、プログラミング言語の意味を厳密に数学的に論理的に研究することである。^{[ 1 ]}意味論は、プログラミング言語の構文における有効な文字列に計算上の意味を割り当てる。これは、数学的証明の意味論と密接に関連しており、しばしば重複する。

セマンティクスとは、コンピュータが特定の言語でプログラムを実行する際に従うプロセスを記述するものです。これは、プログラムの入力と出力の関係を記述したり、特定のプラットフォーム上でプログラムがどのように実行されるかを説明したりすることによって行われ、それによって計算モデルが作成されます。

1967年、ロバート・W・フロイドは論文「プログラムに意味を割り当てる」を発表しました。彼の主な目的は「正当性、等価性、終了性の証明を含む、コンピュータプログラムに関する証明の厳密な基準」でした。 ^{[ 2 ] [ 3 ]}フロイドはさらに次のように書いています。^{[ 2 ]}

私たちの手法では、プログラミング言語の意味論的定義は構文的定義に基づいています。構文的に正しいプログラムにおいて、どの句がコマンドを表すのか、そして各コマンドの近傍における解釈にどのような条件を課す必要があるのか​​を、意味論的定義は明確に規定しなければなりません。

1969年、トニー・ホーアは、フロイドのアイデアを基にしたホーア論理に関する論文を発表した。これは現在では公理的意味論と呼ばれることもある。^{[ 4 ] [ 5 ]}

1970年代には、操作的意味論と指示的意味論という用語が登場した。^{[ 5 ]}

形式意味論の分野は、以下のすべてを包含する。

• 意味モデルの定義
• 異なる意味モデル間の関係
• 意味に対する異なるアプローチ間の関係
• 計算と、論理学、集合論、モデル理論、圏論などの分野における基礎となる数学的構造との関係。

プログラミング言語設計、型理論、コンパイラとインタプリタ、プログラム検証、モデル検査など、コンピュータ科学の他の分野と密接な関連がある。

形式意味論には多くの手法があり、それらは大きく3つのカテゴリーに分類される。

• 指示的意味論^{[ 6 ]}では、言語の各句は指示、つまり抽象的に考えることができる概念的な意味として解釈されます。このような指示は、多くの場合、数学的空間に存在する数学的対象ですが、そうである必要はありません。実際的な必要性として、指示は何らかの形式の数学的記法を使用して記述され、それがさらに指示的メタ言語として形式化できます。たとえば、関数型言語の指示的意味論は、多くの場合、言語をドメイン理論に変換します。指示的意味論の記述は、プログラミング言語から指示的メタ言語への構成的変換としても機能し、コンパイラの設計の基礎として使用できます。
• 操作的意味論^{[ 7 ]}では、言語の実行が（翻訳ではなく）直接記述されます。操作的意味論は解釈に大まかに対応しますが、ここでもインタプリタの「実装言語」は一般的に数学形式です。操作的意味論は、抽象マシン（ SECDマシンなど）を定義し、マシンの状態に引き起こす遷移を記述することによってフレーズに意味を与えます。あるいは、純粋なラムダ計算と同様に、操作的意味論は言語自体のフレーズに対する構文変換によって定義できます。
• 公理的意味論^{[ 8 ]}とは、フレーズに適用される公理を記述することによってフレーズに意味を与える方法である。公理的意味論では、フレーズの意味とそれを記述する論理式を区別しない。その意味は、何らかの論理でそれについて証明できるものと全く同じである。公理的意味論の典型的な例は、ホーア論理である。

形式意味論におけるほとんどのバリエーションは、指示的アプローチ、操作的アプローチ、または公理的アプローチの選択を除けば、それを支える数学的形式主義の選択から生じる。

形式意味論のいくつかのバリエーションには、以下のようなものがある。

• アクション意味論^{[ 9 ]}は、指示的意味論をモジュール化しようとするアプローチであり、形式化プロセスを2つの層（マクロ意味論とミクロ意味論）に分割し、仕様を簡素化するために3つの意味的実体（アクション、データ、およびイールド）を事前に定義します。
• 代数的意味論^{[ 8 ]}は、プログラムの意味論を形式的に記述および推論するための代数法則に基づく公理的意味論の一形態です。また、表示的意味論と操作的意味論もサポートしています。
• 属性文法^{[ 10 ]}は、言語の構文のさまざまなケースに対して「メタデータ」（属性と呼ばれる）を体系的に計算するシステムを定義します。属性文法は、ターゲット言語が単に属性注釈で拡張された元の言語である指示的意味論として理解できます。形式意味論とは別に、属性文法はコンパイラでのコード生成や、正規文法または文脈自由文法に文脈依存条件を追加するためにも使用されています。
• 範疇的（または「関数的」）意味論^{[ 11 ]}は、中核となる数学的形式として圏論を使用します。範疇的意味論は通常、範疇構造の構文的表現を与える何らかの公理的意味論に対応することが証明されています。また、指示的意味論は、一般的な範疇的意味論のインスタンスであることがよくあります。 ^{[ 12 ]}
• 並行性意味論^{[ 13 ]}は、並行計算を記述するあらゆる形式的意味論を包括する用語です。歴史的に重要な並行形式には、アクターモデルやプロセス計算などがあります。
• ゲーム意味論^{[ 14 ]}はゲーム理論に触発されたメタファーを使用しています。
• Edsger W. Dijkstraによって開発された述語変換意味論^{[ 15 ]}は、プログラム断片の意味を、事後条件を確立するために必要な事前条件に

さまざまな理由から、異なる形式意味論間の関係を記述したい場合がある。例えば、次のような場合である。

• ある言語の特定の操作的意味論が、その言語の公理的意味論の論理式を満たすことを証明する。このような証明は、特定の（操作的）解釈戦略について、特定の（公理的）証明体系を用いて推論することが「妥当」であることを示す。
• 高水準機械上の操作的意味論が、シミュレーションによって低水準機械上の意味論と関連付けられることを証明する。この証明では、低水準抽象機械は、与えられた言語の高水準抽象機械の定義よりも多くの基本操作を含む。このような証明は、低水準機械が高水準機械を「忠実に実装している」ことを示す。

抽象解釈理論を通して、抽象化によって複数の意味論を関連付けることも可能である。

• 計算意味論
• 形式意味論（論理学）
• 形式意味論（言語学）
• オントロジー
• オントロジー（情報科学）
• 意味的等価性
• セマンティックテクノロジー

Textbooks

• Aaby, Anthony (2004).プログラミング言語入門。 2015年6月19日にオリジナルからアーカイブされました。意味論。