セマンティクス(コンピュータサイエンス)

ウィキペディアから、無料の百科事典
ナビゲーションにジャンプ 検索にジャンプ

では言語理論をプログラミングセマンティクスはの意味の厳密な数学的研究に関わる分野であるプログラミング言語[1] これは、特定のプログラミング言語によって定義された構文的に有効な文字列の意味を評価し、関連する計算を示すことによって行われます。評価が構文的に無効な文字列であるような場合、結果は非計算になります。セマンティクスは、その特定の言語でプログラムを実行するときにコンピューターが従うプロセスを説明します。これは、プログラムの入力と出力の関係を説明するか、特定のプログラムがどのように実行されるかを説明することで示すことができます。プラットフォーム、したがって計算モデルを作成します。

概要

形式セマンティクスの分野には、次のすべてが含まれます。

  • セマンティックモデルの定義
  • 異なるセマンティックモデル間の関係
  • 意味への異なるアプローチ間の関係
  • 論理集合論モデル理論圏論などの分野からの計算と基礎となる数学的構造との関係

プログラミング言語の設計型理論コンパイラインタプリタプログラムの検証モデル検査などコンピュータサイエンスの他の分野と密接に関連しています

アプローチ

形式的セマンティクスには多くのアプローチがあります。これらは3つの主要なクラスに属しています。

  • 表示的意味論。これにより、言語の各句は外延として解釈されます。つまり、抽象的に考えることができる概念的な意味です。このような表示は、多くの場合、数学的空間に存在する数学的対象ですが、そうである必要はありません。実際の必要性として、外延は何らかの形の数学的表記を使用して記述され、それは次に外延メタ言語として形式化することができます。たとえば、関数型言語の表示的意味論は、多くの場合、言語を領域理論に変換します表示的意味論的記述は、プログラミング言語から表示的メタ言語への構成的翻訳としても機能し、コンパイラーを設計するための基礎として使用できます。
  • 言語の実行が(翻訳ではなく)直接記述される操作的意味論。操作的意味論は大まかに解釈に対応しますが、インタプリタの「実装言語」は一般に数学的な形式です。操作的セマンティクスは、抽象マシン SECDマシンなど)を定義し、マシンの状態でそれらが誘発する遷移を記述することによってフレーズに意味を与える場合があります。あるいは、純粋なラムダ計算と同様に、操作的意味論は、言語自体の句の構文変換を介して定義できます。
  • 公理的意味論。これにより、フレーズに適用される公理説明することにより、フレーズに意味を与えます。公理的意味論は、句の意味とそれを説明する論理式を区別しません。その意味、ある論理でそれについて証明できるものです。公理的意味論の標準的な例は、ホーア論理です。

外延的、運用的、または公理的アプローチの間の選択とは別に、形式的意味体系のほとんどのバリエーションは、数学的形式主義をサポートするという選択から生じます。

バリエーション

正式なセマンティクスのいくつかのバリエーションには、次のものがあります。

関係の説明

さまざまな理由から、さまざまな形式セマンティクス間の関係を説明したい場合があります。例えば:

  • 言語の特定の操作的意味論がその言語の公理的意味論の論理式を満たしていることを証明すること。そのような証明は、特定の(公理的)証明システムを使用して特定の(操作上の)解釈戦略について推論することが「健全」であることを示しています
  • 高レベルのマシンでの操作的セマンティクスが、低レベルのマシンでのセマンティクスとのシミュレーションによって関連付けられていることを証明します。これにより、低レベルの抽象マシンには、特定の言語の高レベルの抽象マシン定義よりも多くのプリミティブ操作が含まれます。このような証明は、低レベルのマシンが高レベルのマシンを「忠実に実装」していることを示しています。

抽象解釈の理論を介した抽象化を通じて、複数のセマンティクスを関連付けることも可能です。

歴史

Robert W. Floydは、Floyd(1967)でプログラミング言語セマンティクスの分野を創設したとされています[3]

も参照してください

参考文献

  1. ^ ジョセフ・ゴーゲン「計算と制御に適用される圏論に関するセマンティクス」会議、カリフォルニア州サンフランシスコ、1974 pp 151-163
  2. ^ アンジェイTarlecki、ロッド・バーストールジョセフ・ゴーグエン計算理論コンピュータ科学91(2)頁239から264までのセマンティクスのためにいくつかの基本的な代数ツール
  3. ^ Knuth、Donald E. 「記念の決議:Robert W. Floyd(1936–2001)」 (PDF)スタンフォード大学教員記念館スタンフォード歴史協会。

さらに読む

教科書
講義ノート

外部リンク

  • アービー、アンソニー(2004)。プログラミング言語入門2015年6月19日にオリジナルからアーカイブされました。CS1 maint:bot:元のURLステータスが不明です(リンク セマンティクス。