Denotational semanticsとは? わかりやすく解説

Weblio 辞書 > 辞書・百科事典 > 百科事典 > Denotational semanticsの意味・解説 

表示的意味論

(Denotational semantics から転送)

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/05/30 16:28 UTC 版)

ナビゲーションに移動 検索に移動

計算機科学における表示的意味論(ひょうじてきいみろん、: Denotational Semantics)とは、プログラミング言語の意味を形式的に記述する形式意味論プログラム意味論)の一つの枠組みである。初期には「数理的意味論」(mathematical semantics)、「スコット=ストレイチー意味論」(Scott–Strachey semantics)のようにも呼ばれた。表示的意味論では、記述された言語の各語句に、表示的意味(denotation)、すなわちプログラム全体の意味に対してその中に現れる各語句が担う役割を表す数学的対象(object)、を与える方法をとる[1]

表示的意味論の起源は、1960年代クリストファー・ストレイチーデイナ・スコットの研究である。ストレイチーやスコットが開発した本来の表示的意味論は、プログラムの表示(意味)を入力を出力にマッピングする関数に変換するものである。後にこれはプログラムの表示(意味)を定義するには非力であることが証明され、例えば再帰定義関数・データ構造を表現できないことが判明した。これを解決するため、スコットはより汎用的な領域理論に基づいた表示的意味論を提案した[2]。その後、研究者らはPower Domainsに基づいた手法を提案し、並行システムの意味論の困難さを克服する努力をしている[3]

概要

表示的意味論は、クリストファー・ストレイチーが1964年に形式言語記述言語(formal language description language)に関するIFIP作業部会のために書いた論文"Towards a formal semantics"に始まる。この論文は、抽象構文を関数(便宜的に関数は型無しラムダ計算で表現されていた)へ写像し、関数の合成で定義された意味関数を導入し、不動点組合せ演算子 Y を使ってループの意味を表示させるものであった。ここで理論的に問題であったのは、プログラムの要素の表示的意味(denotation)は、形式的には、型無しのラムダ計算(type-free lambda calculus)に写像される形になっていたが、その肝心の型無しのラムダ計算の数学的モデルがわかっていないということであった。これは、すなわち、不動点組合せ演算子 Y は操作的に規則として解釈することはできたが、表示的意味としてなにか関数を表すと考えることができなかった[4]

1969年に至って、ストレイチーの理論に興味を抱いたデイナ・スコットは、ストレイチーとの共同研究の末、当初期待していなかった型無しラムダ計算のモデルについて、結局、型無しラムダ計算が実は数学的モデルを持つことを発見することになった。その後すぐに、スコットは、意味の記述法の基礎となる領域理論を構築した。

不動点意味論

表示的意味は、システムが行うことを表現する数学的オブジェクトを探すことに関心がある。この理論は計算の数学的領域(ドメイン)を利用する。そのような領域の例として完備半順序集合などがある。

関係 x≤y は、xy に計算的に発展する可能性があることを意味する。表示が完備半順序集合の要素ならば、例えば f≤gf が定義されている全ての値について g と等しいことを意味する。

計算領域は次のような特徴を持つ:

  1. 下限の存在: 領域には必ず で表される要素が含まれ、領域内の任意の要素 x について ⊥≤x が成り立つ。
  2. 上限の存在: 計算を続けると表示は洗練されるが、限界を持つべきである。そのため、
    出典は列挙するだけでなく、脚注などを用いてどの記述の情報源であるかを明記してください。記事の信頼性向上にご協力をお願いいたします。2022年5月

    外部リンク




英和和英テキスト翻訳>> Weblio翻訳
英語⇒日本語日本語⇒英語
  

辞書ショートカット

すべての辞書の索引

「Denotational semantics」の関連用語

Denotational semanticsのお隣キーワード
検索ランキング

   

英語⇒日本語
日本語⇒英語
   



Denotational semanticsのページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
All text is available under the terms of the GNU Free Documentation License.
この記事は、ウィキペディアの表示的意味論 (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。 Weblio辞書に掲載されているウィキペディアの記事も、全てGNU Free Documentation Licenseの元に提供されております。

©2025 GRAS Group, Inc.RSS