| 研究概要 |
昨年度の考察から継続して,(アルゴリズムの記述を行う上で十分強力な)型なしλ計算と呼ばれる形式的体系に対して,弱外延性を持たない表示的意味論(与えられたプログラムに対して,入力と出力の関係のみでなくアルゴリズムの内包構造を反映した意味付けを可能にする数理構造)の一般的な構築方法の確立を試みた。
これに対して,昨年度までの考察を基に,「情報の近似を表す演算に基づいたある種のpolynomial」の概念を導入して,領域DとD上のpolynomial全体から構成される領域D[x]に対して,領域方程式D=D[x]の解を求めることによって目的の意味論を構成する試みを行っている。このアプローチに基づいて,実際にλ計算の構文解釈の定義を検討した結果,「polynomialの中に更にカルテシアン閉圏の射に関する演算が含まれていると,λ抽象の内部構造については従来の圏論的意味論と同様の手法で解釈を与えることができ,それを適用する段階では集合と写像の圏の中で通常の集合論的意味論と同様の形で解釈を与えることができる」ことが分かった。このように,既知の仕組みを二重に用い,それぞれで細かな視点と粗い視点を表現することによって,従来の意味論研究とのアナロジーからも自然で見通しがよい枠組みが得られると期待している。
上の考察に沿って,現在はλ計算の最も本質的な部分である単純型理論で扱われる構文に絞って解釈の定義を与え,これまでに知られている意味論の構造との比較を行っている。最終的には,この解釈の方法を領域方程式の解の構成に関する考察と併せて型なしλ計算の意味論まで拡張したいと考えている。
|
