表示的意味論

コンピュータサイエンスにおいて、表示的意味論（当初は数学的意味論またはスコット・ストラチー意味論と呼ばれていた）は、言語の式の意味を記述する数学的オブジェクト（表示と呼ばれる）を構築することによってプログラミング言語の意味を形式化するアプローチです。プログラミング言語の形式的意味論を提供する他のアプローチには、公理的意味論と操作的意味論があります。

大まかに言えば、表示的意味論は、プログラムが行うことを表現するドメインと呼ばれる数学的オブジェクトを見つけることに関係しています。たとえば、プログラム（またはプログラムフレーズ）は、部分関数^{[1] [2]}または環境とシステム間の ゲーム^{[3]によって表現される場合があります。}

表示的意味論の重要な信条は、意味論は構成的であるべきであるということです。つまり、プログラム句の表示は、そのサブ句の表示から構築されるべきです。

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

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

表示的意味論は、環境（自由変数の現在の値を保持）からその表示への関数としてプログラムフレーズに帰属します。たとえば、フレーズは、n*m2つの自由変数にバインドされている環境が提供されると、表示を生成しますn。m環境の のn値が3で のm値が5の場合、表示は15です。^[2]

関数は、引数とそれに対応する結果値の順序付けられたペアのセットとして表すことができます。たとえば、セット {(0,1), (4,3)} は、引数 0 に対して結果 1、引数 4 に対して結果 3、それ以外の場合は未定義となる関数を表します。

たとえば、階乗関数を考えてみましょう。これは次のように再帰的に定義されます。

int階乗( int n ) { n == 0の場合は1を返し、そうでない場合はn *階乗( n -1 )を返します。}                

この再帰的な定義に意味を持たせるために、近似の極限として表示が構築され、各近似は factorial の呼び出し回数を制限します。最初は呼び出しがない状態から開始します。したがって、何も定義されていません。次の近似では、順序付きペア (0,1) を追加できます。これは、factorial を再度呼び出す必要がないためです。同様に、(1,1)、(2,2) などを追加できます。これは、factorial(n)の計算にはn+1 回の呼び出しが必要なため、連続する近似ごとに 1 つのペアを追加していくことになります。この極限では、ドメイン内のどこでも定義されている からへの全関数が得られます。${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$

形式的には、各近似を部分関数 としてモデル化します。次に、近似では、空関数(空集合)から始めて、「より定義された部分階乗関数を作成する」、つまり を実装する関数を繰り返し適用します。F は、次のようにコードで定義できます (に を 使用)。 ${\displaystyle \mathbb {N} \rightharpoonup \mathbb {N} }$${\displaystyle F:(\mathbb {N} \rightharpoonup \mathbb {N} )\to (\mathbb {N} \rightharpoonup \mathbb {N} )}$Map<int,int>${\displaystyle \mathbb {N} \rightharpoonup \mathbb {N} }$

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 ; }  
 
     
       
          
       
  
   

次に、 Fがn回適用されたことを示すために、表記法F ^{n を}導入できます。

• F ⁰ ({}) は完全に定義されていない部分関数であり、集合 {} として表されます。
• F ¹ ({}) は集合 {(0,1)} として表される部分関数です。0 では 1 と定義され、それ以外の場所では未定義です。
• F ⁵ ({})は、集合{(0,1), (1,1), (2,2), (3,6), (4,24)}として表される部分関数です。これは、引数0、1、2、3、4に対して定義されます。

この反復プロセスは、からへの部分関数のシーケンスを構築します。部分関数は、順序付けとして ⊆ を使用して、連鎖完全な半順序を形成します。さらに、階乗関数のより良い近似のこの反復プロセスは、それぞれが順序付けとして ⊆ を使用するため、拡張的な（累進的とも呼ばれる）マッピングを形成します。したがって、不動点定理（具体的には、ブルバキ–ウィットの定理）により、この反復プロセスには不動点が存在します。 ${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$${\displaystyle F^{i}\leq F^{i+1}}$

この場合、不動点はこの連鎖の最小の上限であり、完全な関数であり、和集合factorialとして表現できる。

${\displaystyle \bigcup _{i\in \mathbb {N} }F^{i}(\{\}).}$

反復処理はドメイン内の最小の要素 (空集合) から開始されたため、発見した不動点はFの最小の不動点です。これを証明するには、クナスター・タルスキーの定理などのより複雑な不動点定理が必要です。

パワードメインの概念は、非決定性シーケンシャルプログラムに表示的意味を与えるために開発されました。パワードメインコンストラクタをP と記述すると、ドメインP ( D ) は、 Dで表される型の非決定性計算のドメインです。

非決定性の領域理論モデルでは公平性と無限性に関して困難がある。 ^[7]

多くの研究者は、上記のドメイン理論モデルは、より一般的な並行計算の場合には不十分であると主張してきました。このため、さまざまな新しいモデルが導入されました。1980年代初頭、並行言語の意味論を与えるために、表示的意味論のスタイルが使用され始めました。例としては、Will Clinger のアクターモデルに関する研究、Glynn Winskel のイベント構造とペトリネットに関する研究、^[8]、および Francez、Hoare、Lehmann、および de Roever (1979) による CSP のトレース意味論に関する研究などがあります。^[9]これらすべての研究分野は現在も調査中です (たとえば、CSP のさまざまな表示的モデル^[5]を参照)。

最近、ウィンスケルらは並行性のドメイン理論としてプロファンクタのカテゴリーを提案した。 ^{[10] [11]}

状態 (ヒープなど) と単純な命令型機能は、上記の表示的セマンティクスで簡単にモデル化できます。重要な考え方は、コマンドを何らかの状態ドメインの部分関数として考えることです。" x:=3" の意味は、状態を に3割り当てられた状態に移行する関数ですx。シーケンス演算子 " ;" は、関数の合成によって表されます。固定小数点構造は、" while" などのループ構造にセマンティクスを与えるために使用されます。

ローカル変数を持つプログラムをモデル化すると、状況はより困難になります。1つのアプローチは、ドメインを扱うのではなく、型を世界のカテゴリからドメインのカテゴリへの関数として解釈することです。プログラムは、これらの関数間の自然な連続関数によって表されます。^{[12] [13]}

多くのプログラミング言語では、再帰的なデータ型を定義することができます。たとえば、数値のリストの型は次のように指定できます。

データ型 リスト =  nat *リストの短所 |空     

このセクションでは、変更できない関数型データ構造についてのみ説明します。従来の命令型プログラミング言語では、通常、このような再帰リストの要素を変更することができます。

別の例として、型なしラムダ計算の表記の型は

データ 型D  =  D  （ D → D ）  

ドメイン方程式を解く問題は、これらの種類のデータ型をモデル化するドメインを見つけることに関係しています。大まかに言えば、1 つのアプローチは、すべてのドメインのコレクションをドメイン自体と見なし、そこで再帰定義を解くことです。

多態的データ型はパラメータで定義されるデータ型です。例えば、α lists の型は次のように定義されます。

データ型 α リスト =  αの短所 * αリスト|空      

したがって、自然数のリストは 型でありnat list、文字列のリストは 型ですstring list。

研究者の中には、多態性のドメイン理論モデルを開発している人もいます。また、構成的集合論内で パラメトリック多態性をモデル化した研究者もいます。

最近の研究分野には、オブジェクトおよびクラスベースのプログラミング言語の表示的意味論が含まれています。^[14]

線形論理に基づくプログラミング言語の発展に続いて、線形使用（証明ネット、コヒーレンス空間など）と多項式時間計算量のために言語に表示的意味論が与えられてきた。 ^[15]

シーケンシャルプログラミング言語PCFの完全抽象化の問題は、長い間、表示的意味論における大きな未解決問題でした。PCF の難しさは、非常にシーケンシャルな言語であることです。たとえば、 PCF では並列または関数を定義する方法がありません。このため、上で紹介したドメインを使用するアプローチでは、完全に抽象的ではない表示的意味論が生成されます。

この未解決の問題は、ゲームセマンティクスの発展と論理関係を伴う技術によって1990年代にほぼ解決されました。^[16]詳細については、PCFのページを参照してください。

あるプログラミング言語を別の言語に翻訳することは、多くの場合有用です。たとえば、並行プログラミング言語はプロセス計算に翻訳される可能性があり、高水準プログラミング言語はバイトコードに翻訳される可能性があります。(実際、従来の表示的意味論は、プログラミング言語をドメインのカテゴリの内部言語に解釈するものと見なすことができます。)

この文脈では、完全な抽象化などの表示的意味論の概念は、セキュリティ上の懸念を満たすのに役立ちます。^{[17] [18]}

表示的意味論と操作的意味論を結びつけることは、しばしば重要であると考えられています。これは、表示的意味論がむしろ数学的で抽象的であり、操作的意味論がより具体的であるか、計算上の直観に近い場合に特に重要です。表示的意味論の次の特性は、しばしば興味深いものです。

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〛= _⊥ × _⊥です。特別なケースとして、変数のない空の型付けコンテキストの意味は、1 で示される 1 つの要素を持つドメインです。${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$
3. 最後に、各プログラムフラグメントに意味を与える必要があります。Pがσ 型のプログラムフラグメントであり、Γ 型コンテキスト (Γ⊢ P :σ と表記されることが多い) であるとします。この場合、このプログラムフラグメントの意味は、連続関数 〚Γ⊢ P :σ〛:〚Γ〛→〚σ〛 でなければなりません。たとえば、〚⊢7: nat〛:1→ _{⊥ は}常に "7" 関数であり、〚x : , y : ⊢ x + y : 〛: _⊥ × _⊥ → _⊥は 2 つの数を加算する関数です。${\displaystyle \mathbb {N} }$natnatnat${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$

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

実際、これは合成的表示的意味論の一般的なスキームです。ここではドメインと連続関数について何も具体的に述べていません。代わりに別のカテゴリで作業することができます。たとえば、ゲーム意味論では、ゲームのカテゴリにはゲームがオブジェクトとして、戦略が射として存在します。つまり、型をゲームとして、プログラムを戦略として解釈することができます。一般的な再帰のない単純な言語の場合は、集合と関数のカテゴリで間に合わせることができます。副作用のある言語の場合は、モナドのクライスリカテゴリで作業できます。状態のある言語の場合は、関数カテゴリで作業できます。ミルナーは、インターフェイスをオブジェクト、バイグラフを射とするカテゴリで作業することで、場所と相互作用をモデル化することを提唱しました。^[20]

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

セマンティクスが実装を決定する必要はありませんが、実装が正しいことを示す基準を提供する必要があります。

クリンガー（1981）によれば：^{[22] : 79}

しかし、通常、従来の順次プログラミング言語の形式意味論は、それ自体が言語の (非効率的な) 実装を提供すると解釈されることがあります。ただし、形式意味論は常にそのような実装を提供する必要はなく、意味論が実装を提供しなければならないと信じることは、並行言語の形式意味論に関する混乱につながります。プログラミング言語の意味論における無制限の非決定性の存在が、プログラミング言語を実装できないことを意味すると言われるとき、そのような混乱は痛いほど明らかです。

表示的意味論の一部の研究では、ドメイン理論の意味で型をドメインとして解釈しており、これはモデル理論の一分野と見なすことができ、型理論やカテゴリー理論とのつながりにつながります。コンピューターサイエンスでは、抽象解釈、プログラム検証、モデル検査とのつながりがあります。

教科書

講義ノート

その他の参考文献

Wikibook Haskellには、表示的意味論に関するページがあります。

• 表示的意味論。ロイド・アリソン著の書籍の概要
• Schreiner, Wolfgang (1995)。「プログラミング言語の構造 I: 表示的意味論」。コースノート。