| 研究課題/領域番号 |
24500025
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 法政大学 |
|---|
研究代表者 |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| 研究分担者 |
古森 雄一 千葉大学, 総合メディア基盤センター, 教授 (10022302)
藤田 憲悦 群馬大学, 工学(系)研究科(研究院), 准教授 (30228994)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| キーワード | 具象領域 / 逐次アルゴリズム / 層論 / ゲーム意味論 |
|---|
| 研究概要 |
プログラム意味論に関する既知の枠組の多くは集合と関数の概念に基づいて構築されている．これに対して，本研究課題では，計算と論理に対して層構造とその上の自然変換に基づく一般的な数理モデルの枠組を確立して，従来の意味論では捉えることの困難な「アルゴリズムの内包構造」に対して，新しい視点から分析の手法を提供することを目的としている．
これに対して，様々な具体的課題を複合的に考察する計画を立てているが，特に，24年度の考察では「アルゴリズムの内包構造を捉えることのできるモデルとして知られる幾つかの既知の枠組を層構造として表現すること」に集中して考察を行った．
その結果として，「一種の強い有限性を満たすコンパクト開集合からなる可算基底を持つ位相空間」の上に展開される層構造のみに考察の対象を制限することによって，具象領域（concrete domain）と呼ばれる順序構造を特殊な層の形式で表現する手法を自然な形で与えることができた．具体的には，「具象領域は常にそのような層へ変換できること」また逆に「そのような層は常に具象領域へ変換できること」を示し，両概念に対して（これまでの考察で得られていた対応よりも理論的に優れた形で）双方向の翻訳関係を与えた．
具象領域（とその上に定義される逐次アルゴリズム）はラムダ計算の高階逐次性に対する数理モデルとして広く知られた重要な概念である．一方で，その定義には順序関係に関する技巧的な条件が幾つか要請されていて，それらの本質的な意図を説明することが困難であった．今回の結果によって，そうした技巧的な条件が全て層の断面の情報を（順序関係の言葉で）表現するために用意されたものであったことが観察できる．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
本研究で扱う主要な課題は以下の３点であり，特に，課題(B)の解決には困難が伴うことが予想されていて，研究期間全体を通して様々な視点から柔軟なアプローチを試みる予定でいる：
課題(A)．完備半順序集合の層にプログラムの有限近似性を特徴付ける仕組を付加して，領域の層に基づくプログラム意味論を構築する．課題(B)．具象領域・逐次アルゴリズムの圏やゲーム意味論などの構造が層の特殊化として説明できることを示す．課題(C)．従来のStone双対性を一般化して，より広範囲の位相空間と完備束に機能する対応を確立する．
24年度は，こうした課題の各々に対して，その足掛かりとなる具体的な問題から考察を開始することを計画していたが，実際には，課題(B)に対して集中的に考察を進める結果となった．これは，（上に述べたの見通しもあり）研究期間の初期段階で課題(B)を集中的に考察して問題の本質を明らかにする作業が不可避であるという判断によるものである．その代償として，課題(A)と課題(C)に対しては，相対的に達成度が低くなった．課題(A)と課題(C)は，考察時間に比例して成果をあげることが期待できるため，量的な部分でもう少し考察を進めることも可能であったと評価している．
この評価は絶対的なものでなく，一方では，最も困難と予想していた課題(B)について着実な進展があり，ゲーム意味論との対比を含め，ある程度先を見越した知見を得ることができた．その意味で，質的な部分では考察が順調に進んでいると考えることもできる．
|
| 今後の研究の推進方策 |
研究計画調書に挙げた具体的な課題に対する今後の方針として，課題(A)と課題(C)に関しては，当初から計画していた予定通りのアプローチを行い，結果を確認する作業を進める予定である．最も困難が予想される課題(B)に関しては，先ず，「既知の表現定理の結果と組合せて，24年度の考察で得られた具象領域と層の間の双方向変換を合成した結果が同型対応となるか否か」について確認する予定でいる．その上で，逐次アルゴリズムの概念の層論的解釈を確立することを試みる計画を立てている．（この段階で，数学的に自然な対応物を発見することが，本研究全体を通して最も重要なで課題であると位置付けている．）
なお，こうした大きな方向性と共に，藤田（研究分担者）は２階ラムダ計算に関する型推論の構造分析を詳細に進めていて，古森（研究分担者）は組合せ論理と呼ばれる計算体系と型無ラムダ計算との間の翻訳関係を精査している．また，鹿島（連携研究者）は時相論理CTLに対して知られるヒルベルト流公理系を自然な形で拡張して，新たに，ECTLと呼ばれる論理に対して完全なヒルベルト流公理系を与えている．藤田の考察は課題(C)と，古森の考察は課題(B)と密接に関連するものであり，鹿島の考察は，ECTLの更なる拡張であるCTL*やその周辺の論理に対しても同様の成果が期待されると共に，本研究の長期的な目標でもある「応用に関する方法論」を確立する上で重要な意義を持つ．そこで，これらの考察も並行して進めること，更に，一定の進展があった段階で頻繁に本課題との関係を検討することを計画している．
|
| 次年度の研究費の使用計画 |
次年度に繰越す研究費は古森（研究分担者）が研究の最終段階で生じた端数の465円であり，研究活動を行う上で必要となる軽微な文具の購入に充てる．
|
