| 研究概要 |
本研究の目的は,層構造(厳密には,その間に定義される自然変換)を利用して「プログラムが答を算出するまでの計算構造」に対する数学的解釈を与えることである。今年度の考察では,そうした計算表現の中で重要な役割を果たす型の概念に焦点を当てて,多相型の機構に対応する論理体系として知られる2階直観主義命題論理の形式的体系NJ_2について,その解釈を与える層構造について考察を行った。(そのような層の間に定義される自然変換を調べることにより,これまでの考察で得られた知見を「多相型を伴う計算構造」に展開することが期待できる。)
NJ_2に関して完全性定理が確立されるモデル概念としては,Sobolevによるfull Kripkeモデルの層構造が知られている。その中では,可能世界の間に半順序構造が入れられていて,各可能世界における含意と全称束縛の解釈は,それよりも大きな全ての可能世界を考慮することによって与えられる。この可能世界の半順序構造をAlexandrov位相を伴った位相空間と捉え,より一般的な位相空間に関しても機能するように解釈の定義を与え直し,新たなKripkeモデルの定義を与えることができた。そして,この一般化された枠組の下でも,依然としてNJ_2の完全性が保証されていることを証明した。更に,soberな位相空間に限定したモデルのみに注目すれば,広く知られたStone双対性に基づいて,Kripkeモデルと同等な解釈を持つ束論的モデルの枠組みを得ることができることを示した。
|
