Loading article…
プログラミング言語理論において、意味論はプログラミング言語の意味に関する厳密な数学的研究である。[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]はゲーム理論に触発された比喩を用いている。
- エドガー・W・ダイクストラによって開発された変換器意味論[15]は、プログラムフラグメントの意味を、事後条件をそれを確立するために必要な事前条件に変換する関数として記述します。
関係性を説明する
さまざまな理由から、異なる形式意味論間の関係を記述したい場合があります。たとえば、次のようになります。
- ある言語の特定の操作的意味論が、その言語の公理的意味論の論理式を満たすことを証明すること。このような証明は、特定の（公理的）証明システムを使用して特定の（操作的）解釈戦略について推論することが「妥当」であることを示します。
- 高レベルマシン上の操作意味論が、シミュレーションによって低レベルマシン上の意味論と関連していることを証明します。低レベル抽象マシンには、特定の言語の高レベル抽象マシン定義よりも多くの基本操作が含まれます。このような証明は、低レベルマシンが高レベルマシンを「忠実に実装」していることを示します。
抽象解釈理論を介した抽象化を通じて複数の意味を関連付けることも可能である。[要出典]
参照
参考文献
- ^ Goguen, Joseph A. (1975). 「計算の意味論」.計算と制御へのカテゴリ理論の応用. コンピュータサイエンスの講義ノート. 第 25 巻. Springer . pp. 151–163. doi :10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6。
- ^ ab Floyd, Robert W. (1967). 「プログラムへの意味の割り当て」(PDF)。 Schwartz, JT (編)。 コンピュータサイエンスの数学的側面。 応用数学シンポジウム議事録。 第 19 巻。 アメリカ数学会。 pp. 19–32。ISBN 0821867288。
- ^ Knuth, Donald E.「追悼決議: Robert W. Floyd (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 出版。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) .ヨーロッパプログラミング言語およびシステムシンポジウムの議事録. 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.
さらに読む
- 教科書
- Floyd, Robert W. (1967)。「プログラムへの意味の割り当て」(PDF)。Schwartz, 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-06-27 にオリジナル(PDF)からアーカイブ。（作業草案）
- ニールソン、 HR; ニールソン、フレミング (2007)。セマンティクスとアプリケーション: 前菜。Springer。ISBN 978-1-84628-692-6。
- スタンプ、アーロン (2014)。プログラミング言語の基礎。Wiley。ISBN 978-1-118-00747-1。
- Krishnamurthi, Shriram (2012)。『プログラミング言語: アプリケーションと解釈』(第 2 版)。
- 講義ノート
- Winskel, Glynn. 「表示的意味論」(PDF)。ケンブリッジ大学。
外部リンク
- Aaby, Anthony (2004). プログラミング言語入門. 2015-06-19 にオリジナルからアーカイブされました。セマンティクス。