利用者:I.hidekazu/表示的意味論

表示的意味論（ひょうじてきいみろん、denotational semantics）とは、...

概要

欠点：モジュール性の欠如

英国の計算機科学者であるピータ・モーゼス（Peter D. Mosses）は、表示的意味論の欠点として次のとおりモジュール性の欠如を指摘した。

表示的意味論の応用に関する別の問題として、意味記述の実用性（pragmatic aspects）の問題がある。”玩具の（toy）"言語に対して、”その領域をテーブルの上に並べ”、適当な（しかし、必ずしも十分に抽象的でない）意味を定義する意味方程式を与えるのはまったく簡単なことである。しかし、（不幸なことに）”現実”のプログラミング言語の表示的意味記述には多数の複雑な領域が必要であるから、このアプローチを実用的なレベルにまで高めるのは容易ではない。部分的には、意味方程式が表示的意味の領域に陽に（explicitly）依存するという理由によって、大規模な意味記述を理解することがきわめて困難になる可能性がある。関連する問題として、１つの言語（たとえば、Pascal）の意味記述の部分を、他の言語（たとえば、MODULA2）の意味記述に再利用することが現実的（feasible）でないという問題がある。ソフトウェア工学における同様な問題は、”モジュール（module）”の導入によって緩和された。しかし、表示的意味論には、モジュールを表す記法がない。実際、もし表示的意味の領域の定義をモジュールの中にカプセル化したとすれば、意味方程式の中でλ記法を使って意味を表すことは不可能になる。したがって、原始的（primitive）な意味を表現したり、意味を結合するために、モジュールの内部に限って定義される補助操作を使う必要がある。このようなわけで、高度のモジュール性（modularity）は（通常の）表示的意味論と両立しないように思われる。
— Peter D. Mosses 、表示的意味論(1989)^[1]

ここでモーゼスが主張した表示的意味論のモジュール性の欠如とは次のようなことである。

一般に、プログラミング言語の設計においては、言語の機能が直交設計（orthogonal design）されていたとしても、実装レベルでも分離がなされているわけではない。例えば、変数を保持する環境と例外処理はそれぞれ機能的に独立分離された概念のものであり、概念的には環境の振る舞いが例外処理に影響を与えることは考え難い。しかしながら、構文を意味領域に翻訳する意味関数を指定する意味方程式の観点からすると、環境の意味領域への翻訳と例外処理の意味領域への翻訳は複雑に入り組んでおり、意味領域として環境を持つプログラミング言語の意味関数の意味方程式と例外処理に関する意味方程式を単純に組み合わせるということができず、非常に面倒な変更を行わなくてはならない。モーゼスはこの意味領域を変更したときに意味関数を定める意味方程式に非常に面倒な変更を加えないとそれぞれの意味を両立する意味関数とならないことを指して表示的意味論にはモジュール性がないと主張した^[3]

これに対し、同英国のエジンバラ大学の大学院生だったエウジニオ・モッジは、1989年6月に発表した論文『An Abstract View of Programming Languages』^[4]において、このモーゼスの強調した表示的意味論の主要な欠点であるモジュール性の欠如（Mosses stresses as a major shortcoming of Denotational Semantics the lack of modularity）について解決策を提出した^[5]。これが計算モナドの理論（モジュール性を持たせた表示的意味論；modular denotational semantics）である^[6]。

まず、モッジはアントニー・ホーアの1988年の論文^[7]に基づいて次のような前提を取った^[8]。

プログラミング言語　＝　（有限積を持つ）２-圏

表示的意味論　　　　＝　（有限積を保存する）２-関手

詳細化（refinement）＝　lax-自然変換

そのうえで、モッジは通常の値（value）に対して（プログラムの表示的意味としての）計算した値（computation；計算結果）を区別し^[9]、その構造として強モナド（strong monad）を仮定した。そして、プログラムが値から計算した値への射であるという解釈から、強モナド（計算した値の構造）への射であるクライスリ圏の射がプログラムに対応する概念であると考えた。つまり、プログラムとはクライスリ圏の射である（program is arrow of Kleisli category）とした。そして、実際に例外（exceptions）、副作用（side-effects）、継続（continuations）といった計算効果（computational effect）をうまくクライスリ圏の枠組みで定式化できることを示した。

→詳細は「クライスリ圏 § 計算機科学における応用」を参照

実際にこの計算モナドを取り入れたプログラミング言語としてはHaskellがある。Haskellにおいては、リスト、例外処理、入出力、状態保持といった言語の機能は計算モナドと等価なクライスリ・トリプルとして実装されている。そのため、例えば例外処理 Maybe モナドの挙動を、あくまでこの計算モナドの枠組みの中で変更したとしても、その変更に対する影響は基本的にほかの計算モナドには波及することはない（言語の機能のモジュール化）という顕著な特徴を持つ。言語の機能としての実装変更はあくまで挙動変更を行う Maybe モナドの中で完結することになるのである^[10]。すなわち、Haskellは直交設計された言語の機能が実装レベルでも分離されているという珍しい構造を持つ言語となった。

脚注

^
P. Mosses (1989), “Denotational semantics”, Technical Report MS-CIS-89-16, to appear in North Holland Handbook of Theoretical Computer Science (Dept. of Comp. and Inf. Science, Univ. of Pennsylvania) p.106
- （抄訳：Peter D. Mosses（著）、山田眞市（編）「表示的意味論」『コンピュータ基礎理論ハンドブックⅡ 形式モデルと意味論』、丸善株式会社、1994年。 pp.611-612）
^ * Harold Abelson; Gerald Jay Sussman; Julie Sussman (1996). Structure and Interpretation of Computer Programs (Second ed.). Mit Press. ISBN 978-0262510875
^ これは非常に概念的でわかりづらい。具体的に理解したいのであれば、計算機プログラムの構造と解釈第二版^[2]の第４章におけるメタサーキュラーインタプリタの実装、特にeval 関数の実装（表示的身論における意味関数の意味方程式を定めることに相当する）に対する面倒な変更を念頭に考えればよい。
^ Eugenio Moggi (1989), An Abstract View of Programming Languages
^
ただし、アイディア自体は、1987年にエジンバラ大学におけるモッジの博士論文の口頭試験において参加者に対して披露された。
- 圏論の歩き方委員会編『圏論の歩き方』日本評論社、2015年。 p.75
年代的に前後する論文についてどのようにその内容を知ったのか、あるいは知らなかったかについては不明である。
^
モッジの計算モナドの使い方が間違っているという批判も存在する。
- G. Plotkin; J. Power (2003), “Algebraic Operations and Generic Effects”, Applied Categorical Structures 11 (1): 69-94
- 特集：圏論の世界, 現代思想, 7, 青土社, (2020) p.108
^ C.A.R. Hoare; H. Jifeng (1988), Natural transformation and data refinement
^ Eugenio Moggi 1989, p. 10.
^ 例えば、C言語であれば、データとしての0と、関数呼び出しをした戻り値 int zero() { return 0; } があったとする。この場合、同じ0というデータであるが、もともとあったデータと関数呼び出しという計算プロセスを経て得られたデータでその出自が異なる（違いがある）と考えたのである。
^ ただし、モナドを組み合わせたモナドの場合、元のモナドの挙動が変わると影響を受けることになる。

参考文献

[1] P. Mosses (1989), “Denotational semantics”, Technical Report MS-CIS-89-16, to appear in North Holland Handbook of Theoretical Computer Science (Dept. of Comp. and Inf. Science, Univ. of Pennsylvania) p.106
（抄訳：Peter D. Mosses（著）、山田眞市（編）「表示的意味論」『コンピュータ基礎理論ハンドブックⅡ 形式モデルと意味論』、丸善株式会社、1994年。 pp.611-612）

[2] （抄訳：Peter D. Mosses（著）、山田眞市（編）「表示的意味論」『コンピュータ基礎理論ハンドブックⅡ 形式モデルと意味論』、丸善株式会社、1994年。 pp.611-612）

[2] * Harold Abelson; Gerald Jay Sussman; Julie Sussman (1996). Structure and Interpretation of Computer Programs (Second ed.). Mit Press. ISBN 978-0262510875

[3] これは非常に概念的でわかりづらい。具体的に理解したいのであれば、計算機プログラムの構造と解釈第二版^[2]の第４章におけるメタサーキュラーインタプリタの実装、特にeval 関数の実装（表示的身論における意味関数の意味方程式を定めることに相当する）に対する面倒な変更を念頭に考えればよい。

[4] Eugenio Moggi (1989), An Abstract View of Programming Languages

[5] ただし、アイディア自体は、1987年にエジンバラ大学におけるモッジの博士論文の口頭試験において参加者に対して披露された。
圏論の歩き方委員会編『圏論の歩き方』日本評論社、2015年。 p.75
年代的に前後する論文についてどのようにその内容を知ったのか、あるいは知らなかったかについては不明である。

[7] 圏論の歩き方委員会編『圏論の歩き方』日本評論社、2015年。 p.75

[6] モッジの計算モナドの使い方が間違っているという批判も存在する。
G. Plotkin; J. Power (2003), “Algebraic Operations and Generic Effects”, Applied Categorical Structures 11 (1): 69-94

特集：圏論の世界, 現代思想, 7, 青土社, (2020) p.108

[9] G. Plotkin; J. Power (2003), “Algebraic Operations and Generic Effects”, Applied Categorical Structures 11 (1): 69-94

[10] 特集：圏論の世界, 現代思想, 7, 青土社, (2020) p.108

[7] C.A.R. Hoare; H. Jifeng (1988), Natural transformation and data refinement

[FOOTNOTEEugenio_Moggi198910-8] Eugenio Moggi 1989, p. 10.

[9] 例えば、C言語であれば、データとしての0と、関数呼び出しをした戻り値 int zero() { return 0; } があったとする。この場合、同じ0というデータであるが、もともとあったデータと関数呼び出しという計算プロセスを経て得られたデータでその出自が異なる（違いがある）と考えたのである。

[10] ただし、モナドを組み合わせたモナドの場合、元のモナドの挙動が変わると影響を受けることになる。

[1]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[2]