| 研究概要 |
本研究課題はプログラムの表示的意味論に関するものであり,「従来のモデルとは本質的に異なる特徴を持つ数理構造の構築」と「そうした構造の一般的な特徴をプログラミング言語の実装の観点から考察すること」を目的としている。
プログラムの普遍的な意味を与える数理構造にはCCC(カルテシアン閉圏)の性質が必要不可欠であるが,既知の研究の多くは,(数理論理学における伝統的なモデルの構成と同様に)外延性を伴う概念を用いたCCC構造によるものが大多数となっている。このように必要以上に強い概念が取り入れられたモデルにおいては,プログラムの入出力の関係のみに依存してその意味が決められることになり,計算機科学に特有の概念であるアルゴリズムの内部構造を捉えることは不可能である。これに対して,本研究課題の目的は,(利便性のために取り入れられていた)外延性の概念を排除する形で,従来の理論と同様に様々なデータ構造の構文を矛盾なく解釈できるモデルの構成を与え,「出力を得るまでのアルゴリズムの構造の違いを反映できる数理モデル」の理論を確立することにある。
こうした視点の下では,様々な興味深い課題が考えられるが,その中でも最も大きな問題は「外延性を排除したCCCの形式を保ちながら,多様なデータ型を伴う強い表現力を持った構文体系の解釈を可能とするための仕組みを兼ね備えていて,更には,プログラム(特にラムダ計算)の有限近似性や高階遂次性等の特徴を反映している構造を実現すること」にある。
|
