指示的意味論

コンピュータ科学において、指示的意味論（当初は数学的意味論またはスコット・ストレイチー意味論として知られていた）は、プログラミング言語の式の意味を記述する数学的対象（指示と呼ばれる）を構築することによって、プログラミング言語の意味を形式化する手法である。プログラミング言語の形式的意味論を提供する他の手法には、公理的意味論や操作的意味論などがある。

大まかに言えば、指示的意味論は、プログラムが行うことを表すドメインと呼ばれる数学的対象を見つけることに関係しています。たとえば、プログラム（またはプログラム句）は、部分関数^{[ 1 ] [ 2 ]}や、環境とシステム間のゲーム^{[ 3 ]によって表現される可能性があります。}

指示的意味論の重要な原則は、意味論は構成的であるべきだということである。つまり、プログラム句の指示は、その部分句の指示から構築されるべきである。

表示的意味論は、1970年代初頭に発表されたクリストファー・ストラッチーとダナ・スコットの研究に端を発する。 ^{[ 1 ] [ 2 ]}ストラッチーとスコットによって最初に開発された表示的意味論は、コンピュータプログラムの意味を、入力を出力にマッピングする関数として提供するものであった。^{[ 2 ]}再帰的に定義されたプログラムに意味を与えるために、スコットは、ドメイン間の連続関数、具体的には完全半順序を扱うことを提案した。以下に説明するように、逐次性、並行性、非決定性、ローカル状態などのプログラミング言語の側面に適した表示的意味論を調査する研究が続けられている。

表示的意味論は、並行処理や例外処理などの機能を使用する現代のプログラミング言語、例えばConcurrent ML ^{[ 4 ]} 、CSP ^{[ 5 ]}、Haskell ^{[ 6 ]}向けに開発されました。これらの言語の意味論は構成的であり、句の意味はその部分句の意味に依存します。例えば、適用式の意味は、その部分句 f、E1、E2 の意味論によって定義されます。現代のプログラミング言語では、E1 と E2 は並行して評価でき、一方の実行は共有オブジェクトを介して相互作用することで他方に影響を与え、その結果、両者の意味が互いによって定義される可能性があります。また、E1 または E2 が例外をスローして、他方の実行を終了させる可能性もあります。以下のセクションでは、これらの現代のプログラミング言語の意味論の特殊なケースについて説明します。f(E1,E2)

int factorial ( int n ) { if ( n == 0 ) return 1 ; else return n * factorial ( n - 1 ); }

int factorial_nonrecursive ( Map < int , int > factorial_less_defined , int n ) { if ( n == 0 ) then return 1 ; else if ( fprev = lookup ( factorial_less_defined , n -1 )) then return n * fprev ; else return NOT_DEFINED ; }Map < int , int > F ( Map < int , int > factorial_less_defined ) { Map < int , int > new_factorial = Map.empty ( ) ; for ( int n in all <int> ( ) ) { if ( f = factorial_nonrecursive ( factorial_less_defined , n ) ! = NOT_DEFINED ) new_factorial.put ( n , f ) ; } return new_factorial ; }

データ型リスト= nat * listのCons |空

データ型D = D of ( D → D )

データ型αリスト= Cons of α * αリスト|空

指示的意味論と操作的意味論を結びつけることは、しばしば重要視される。これは、指示的意味論が数学的で抽象的である一方、操作的意味論がより具体的であったり、計算論的な直観に近い場合に特に重要となる。指示的意味論の以下の特性は、しばしば注目される。

1. 構文独立性：プログラムの説明表現は、ソース言語の構文に依存すべきではない。
2. 妥当性（または健全性）：観察可能なすべての異なるプログラムは、それぞれ異なる意味を持つ。
3. 完全な抽象化：観測的に同等なプログラムはすべて、同じ意味を持つ。

伝統的な意味論においては、妥当性と完全抽象化は、「操作的等価性が指示的等価性と一致する」という要件として大まかに理解できる。アクターモデルやプロセス計算などの、より内包的なモデルにおける指示的意味論においては、各モデル内で等価性の概念が異なるため、妥当性と完全抽象化の概念は議論の的となり、明確に定義するのが難しくなる。また、操作的意味論と指示的意味論の数学的構造は非常に類似する可能性がある。

操作的意味論と表示的意味論の間に保持したいその他の望ましい特性は次のとおりです。

1. 構成主義：構成主義は、ドメイン要素が構成的な方法によって存在することが証明できるかどうかに関心を寄せている。
2. 表示的意味論と操作的意味論の独立性：表示的意味論は、プログラミング言語の操作的意味論とは独立した数学的構造を用いて形式化されるべきである。ただし、根底にある概念は密接に関連している可能性がある。詳細は、下記の「構成性」の項を参照のこと。
3. 完全性または定義可能性：意味モデルのすべての射はプログラムの指示対象であるべきである。^{[ 19 ]}

プログラミング言語の指示的意味論における重要な側面の一つは構成性であり、これはプログラムの意味が、その構成要素の意味から構成されることを意味します。例えば、「7 + 4」という式を考えてみましょう。この場合の構成性とは、「7」、「4」、「+」の意味を用いて「7 + 4」の意味を与えることです。

ドメイン理論における基本的な表示的意味論は、以下のように与えられるため構成的です。まず、プログラム断片、つまり自由変数を持つプログラムについて考えます。型付けコンテキストは、各自由変数に型を割り当てます。たとえば、式 ( x + y ) は、型付けコンテキスト ( x : nat, y : nat) で考えることができます。次に、以下のスキームを使用して、プログラム断片に表示的意味論を与えます。

1. まず、言語の型の意味を説明します。各型の意味はドメインでなければなりません。型 τ を表すドメインを 〚τ〛 と表記します。例えば、型の意味はnat自然数のドメインです。〚nat〛=${\displaystyle \mathbb {N} }$_⊥ .
2. 型の意味から、型付けコンテキストの意味を導き出します。〚x ₁ :τ ₁ ,..., x _n :τ _n〛 = 〚 τ ₁〛× ... ×〚τ _n〛 と設定します。例えば、〚x : nat, y : nat〛=${\displaystyle \mathbb {N} }$_⊥ ×${\displaystyle \mathbb {N} }$_⊥。特殊なケースとして、変数のない空の型コンテキストの意味は、1 つの要素を持つドメインであり、1 で表されます。
3. 最後に、型コンテキスト内の各プログラム断片に意味を与える必要があります。型コンテキストΓにおける型σのプログラム断片Pを考えます。これはしばしばΓ⊢ P :σと表記されます。この型コンテキスト内のプログラムの意味は、連続関数〚Γ⊢ P :σ〛:〚Γ〛→〚σ〛でなければなりません。例えば、〚⊢7: nat〛:1→${\displaystyle \mathbb {N} }$_⊥は常に「7」関数であり、〚x : nat、y : nat⊢ x + y : nat〛:${\displaystyle \mathbb {N} }$_⊥ ×${\displaystyle \mathbb {N} }$_⊥ →${\displaystyle \mathbb {N} }$_⊥は2つの数を加算する関数です。

さて、複合式 (7+4) の意味は、3 つの関数 〚⊢7: nat〛:1→を合成することによって決定されます。${\displaystyle \mathbb {N} }$_⊥、〚⊢4: nat〛:1→${\displaystyle \mathbb {N} }$_⊥、および 〚x : nat、y : nat⊢ x + y : nat〛:${\displaystyle \mathbb {N} }$_⊥ ×${\displaystyle \mathbb {N} }$_⊥ →${\displaystyle \mathbb {N} }$_⊥ .

実際、これは構成的指示意味論の一般的な枠組みです。ここではドメインと連続関数について特別なことは何もありません。代わりに別のカテゴリで作業することもできます。たとえば、ゲーム意味論では、ゲームのカテゴリはゲームをオブジェクト、戦略を射として持ちます。型をゲーム、プログラムを戦略として解釈できます。一般的な再帰のない単純な言語の場合は、集合と関数のカテゴリで十分です。副作用のある言語の場合は、モナドのクライスリカテゴリで作業できます。状態のある言語の場合は、ファンクターカテゴリで作業できます。ミルナーは、インターフェースをオブジェクト、バイグラフを射として持つカテゴリで作業することにより、位置と相互作用をモデル化することを提唱しました。^{[ 20 ]}

ダナ・スコット（1980）によると：^{[ 21 ]}

意味論が実装を決定する必要はないが、実装が正しいことを示すための基準を提供するべきである。

クリンガー（1981）によると：^{[ 22 ]： 79}

しかしながら、通常、従来の逐次型プログラミング言語の形式意味論自体を解釈することで、その言語の（非効率的な）実装が得られる場合がある。ただし、形式意味論が必ずしもそのような実装を提供する必要はなく、意味論が必ず実装を提供すると考えることは、並行言語の形式意味論に関する混乱を招く。プログラミング言語の意味論に無制限の非決定性が存在することが、そのプログラミング言語の実装が不可能であることを意味すると主張される場合、このような混乱は痛々しいほど明らかになる。

表示的意味論における研究の中には、型をドメイン理論の意味でドメインとして解釈するものがあり、これはモデル理論の一分野と見なすことができ、型理論や圏論との関連性につながる。コンピュータ科学の分野では、抽象解釈、プログラム検証、モデル検査との関連性が見られる。

教科書

講義ノート

その他の参考文献

• 指示的意味論― ロイド・アリソン著の書籍概要
• シュライナー、ヴォルフガング（1995）。「プログラミング言語の構造 I：表示的意味論」。講義ノート。