セマンティクス（コンピュータサイエンス）

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

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

歴史

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

私たちのアプローチでは、プログラミング言語の意味的定義は構文的定義に基づいています。構文的に正しいプログラム内のどのフレーズがコマンドを表すのか、そして各コマンドの近傍における解釈にどのような条件を課すべきかを明確にする必要があります。

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

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

概要

形式意味論の分野には、以下のすべてが含まれます。

セマンティックモデルの定義
異なる意味モデル間の関係
意味に対する異なるアプローチの関係
論理学、集合論、モデル理論、カテゴリー理論などの分野における計算と基礎となる数学的構造との関係。

プログラミング言語設計、型理論、コンパイラとインタープリタ、プログラム検証、モデル検査など、コンピュータサイエンスの他の分野と密接な関係があります。

アプローチ

形式意味論にはさまざまなアプローチがあり、それらは 3 つの主要なクラスに属します。

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

表示的、操作的、または公理的なアプローチの選択とは別に、形式意味システムにおけるほとんどのバリエーションは、サポートする数学的形式主義の選択から生じます。^{[引用が必要]}

バリエーション

形式意味論のバリエーションには次のようなものがあります。

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

関係性を説明する

様々な理由から、異なる形式意味論間の関係を記述したい場合があります。例えば、

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

抽象解釈理論を介した抽象化を通じて、複数の意味を関連付けることも可能である。^[^要出典^]

参照

参考文献

^ ゴーゲン、ジョセフ・A. (1975). 「計算の意味論」.圏論の計算と制御への応用. コンピュータサイエンス講義ノート. 第25巻.シュプリンガー. pp. 151– 163. doi :10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6。
^ ab フロイド, ロバート W. (1967). 「プログラムへの意味の付与」(PDF) . シュワルツ, JT (編). コンピュータサイエンスの数学的側面. 応用数学シンポジウム議事録. 第19巻. アメリカ数学会. pp. 19– 32. ISBN 0821867288。
^ ドナルド・E・クヌース「追悼決議：ロバート・W・フロイド（1936–2001）」（PDF）。スタンフォード大学教職員追悼式典。スタンフォード歴史協会。
^ Hoare, CAR (1969年10月). 「コンピュータプログラミングの公理的基礎」. Communications of the ACM . 12 (10): 576– 580. doi : 10.1145/363235.363259 . S2CID 207726175.
^ ab Winskel, Glynn (1993). 『プログラミング言語の形式意味論入門』マサチューセッツ州ケンブリッジ: MIT Press. p. xv. ISBN 978-0-262-23169-5。
^ シュミット、デイビッド・A. (1986). 『表示的意味論：言語発達のための方法論』ウィリアム・C・ブラウン出版社. ISBN 9780205104505。
^ Plotkin, Gordon D. (1981). 操作的意味論への構造的アプローチ（報告書）. 技術報告書 DAIMI FN-19.オーフス大学コンピュータサイエンス学部.
^ ab Goguen, Joseph A. ; Thatcher, James W. ; Wagner, Eric G. ; Wright, Jesse B. (1977). 「初期代数意味論と連続代数」. Journal of the ACM . 24 (1): 68– 95. doi : 10.1145/321992.321997 . S2CID 11060837.
^ Mosses, Peter D. (1996). 動作意味論の理論と実践（報告書）. BRICS報告書 RS9653.オーフス大学.
^ デランサール, ピエール; ジュールダン, マーティン; ロルホ, ベルナール (1988). 「属性文法：定義、システム、参考文献」. コンピュータサイエンス講義ノート 323.シュプリンガー・フェアラーク. ISBN 9780387500560。
^ Lawvere, F. William (1963). 「代数理論の関数的意味論」.米国科学アカデミー紀要. 50 (5): 869– 872. Bibcode :1963PNAS...50..869L. doi : 10.1073/pnas.50.5.869 . PMC 221940. PMID 16591125 .
^ Andrzej Tarlecki; Rod M. Burstall ; Joseph A. Goguen (1991). 「計算の意味論のための基本的な代数的ツール：第3部インデックス付きカテゴリ」.理論計算機科学. 91 (2): 239– 264. doi : 10.1016/0304-3975(91)90085-G .
^ Batty, Mark; Memarian, Kayvan; Nienhuis, Kyndylan; Pichon-Pharabod, Jean; Sewell, Peter (2015). 「プログラミング言語の並行性セマンティクスの問題」(PDF) . Proceedings of the European Symposium on Programming Languages and Systems . Springer . pp. 283– 307. doi : 10.1007/978-3-662-46669-8_12 .
^ Abramsky, Samson (2009). 「インタラクションの意味論：ゲーム意味論入門」Andrew M. Pitts、P. Dybjer編著『計算の意味論と論理』ケンブリッジ大学出版局. pp. 1– 32. doi :10.1017/CBO9780511526619.002. ISBN 9780521580571。
^ Dijkstra, Edsger W. (1975). 「ガード付き命令、非決定性、そしてプログラムの形式的導出」Communications of the ACM . 18 (8): 453– 457. doi : 10.1145/360933.360975 . S2CID 1679242.

さらに読む

教科書

フロイド, ロバート W. (1967). 「プログラムへの意味の付与」(PDF) . シュワルツ, JT (編). コンピュータサイエンスの数学的側面. 応用数学シンポジウム議事録. 第19巻. アメリカ数学会. pp. 19– 32. ISBN 0821867288。
ヘネシー, M. (1990). 『プログラミング言語の意味論：構造的操作的意味論を用いた初歩的入門』 Wiley. ISBN 978-0-471-92772-3。
テネント、ロバート・D. (1991). 『プログラミング言語の意味論』プレンティス・ホール. ISBN 978-0-13-805599-8。
グンター、カール（1992年）『プログラミング言語の意味論』MIT出版、ISBN 0-262-07143-6。
ニールソン, HR; ニールソン, フレミング (1992). 意味論とその応用：形式的入門(PDF) . Wiley. ISBN 978-0-471-92980-2. 2012年4月17日時点のオリジナル（PDF）からアーカイブ。2011年5月27日閲覧。
ウィンスケル、グリン（1993年）『プログラミング言語の形式意味論入門』 MIT出版、ISBN 0-262-73103-7。
ミッチェル、ジョン・C. (1995). プログラミング言語の基礎(Postscript) .
スロンネガー、ケネス; カーツ、バリー・L. (1995). 『プログラミング言語の形式構文と意味論』アディソン・ウェスレー. ISBN 0-201-65697-3。
レイノルズ、ジョン・C. (1998). 『プログラミング言語の理論』ケンブリッジ大学出版局. ISBN 0-521-59414-6。
Harper, Robert (2006). 『プログラミング言語の実践的基礎』（PDF） . 2007年6月27日時点のオリジナル（PDF）よりアーカイブ。（作業草案）
ニールソン, HR; ニールソン, フレミング (2007). 『セマンティクスと応用：前菜』シュプリンガー. ISBN 978-1-84628-692-6。
スタンプ、アーロン（2014年）『プログラミング言語の基礎』 Wiley社、ISBN 978-1-118-00747-1。
クリシュナムルティ、シュリラム（2012年）『プログラミング言語：応用と解釈』（第2版）。

講義ノート

ウィンスケル、グリン. 「表示的意味論」（PDF） . ケンブリッジ大学.

外部リンク

Aaby, Anthony (2004). プログラミング言語入門. 2015年6月19日時点のオリジナルよりアーカイブ。セマンティクス。