| 研究課題/領域番号 |
24500025
|
|---|
| 研究機関 | 法政大学 |
|---|
研究代表者 |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| 研究分担者 |
古森 雄一 千葉大学, 理学(系)研究科(研究院), 名誉教授 (10022302)
藤田 憲悦 群馬大学, 理工学研究科, 准教授 (30228994)
|
|---|
| キーワード | 具象領域 / 逐次アルゴリズム / 逆像層 / ゲーム意味論 / innocent戦略 |
|---|
| 研究概要 |
本研究の中心的な課題として，「アルゴリズムの内包構造に対する表示的意味論を実現する既知のモデルを層に基づく統一的な視点から新たに特徴付けること」がある．その考察対象となり得る枠組は非常に限定されていて，具象領域（とその上に定義される逐次アルゴリズム）の圏CDとgame（とその上に定義される戦略）の圏の２つしか存在しない．これまでは，特に前者の構造に焦点を当て考察を進め，ある種のコンパクト性を備えた層と具象領域との間に両方向の対応関係を自然な形で与えることができた．（最終的には，こうした層を対象とする圏SHと共に，CDからSHへの関手Sとその逆方向の関手Cを定義して，SHとCDの同等性を保証することを目標としている．これまでの研究は，対象の部分に限定してSとCに関する有望な対応を見いだした段階といえる．）
25年度の考察では，それまでの考察で得られた結果に対して，幾つかの細かな不備を発見・修正しながら対応関係を精査し，これまでの議論が厳密には「分配的具象領域とある種のコンパクト性を満たす散布層との間の対応」を与えていることを確認した．また，その上で，分配的具象領域DとC(S(D))の同型を保証する逐次アルゴリズムが存在することを証明した．これによって，次の考察ステップは「SHの射として逐次アルゴリズムに相当する概念を構築すること」となるが，この問題に対して，単純に層の間の自然変換を採用するだけでは不十分であることが判明し，層の逆像関手と自然変換を組合せた新たな射の概念を導入する結論に至った．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究の開始段階から，「逐次アルゴリズムに対応する射の概念を層の間に確立すること」は本研究課題において最も重要なステップと位置付けていて，同時に，これは最も困難が予想される問題でもあった．25年度の考察では，この課題に対して具体的な概念を得ることが出来てその後の証明にもある程度の見通しが立っている段階まで至った．こうした点を踏まえて，考察は着実に進展しているしていると捉えている．なお，今回の結果は，考察すべき価値のある新たな問題を多数派生させることにもなり，確認・発展すべき課題は数多く存在する状態にある．（特に，game意味論との対応を明らかにすることも手の届く段階に至っている．）こうした新たな問題についても，それらの重要度を考慮しながら優先順位を見極めて慎重に対応していく必要があると考えている．
また，その他のアプローチについても考察はおおむね順調に進んでいると考えている．例えば，藤田（研究分担者）は，2階型付ラムダ計算の型推論の仕組みを経由して2階直観主義命題論理の証明構造の分析に役立つ様々な性質を明らかにしている．古森（研究分担者）はそれまでの考察による組合せ論理とラムダ計算との翻訳関係を精査することにより，その副産物として計算評価の合流性に対するシンプルな証明を得ている．鹿島（連携研究者）は，時相論理ECTLに対して非常にシンプルな形式でヒルベルト流公理系を与えることに成功していて，これを更に強い論理（ETCL+やCTL*など）まで拡張することを進めている段階にある．
こうして得られた成果について，論文や研究集会（日本数学会やRIMS研究集会など）を通して発表する作業も着実に進められている．
|
| 今後の研究の推進方策 |
今後の研究を進めるにあたって直近の課題の１つは，（上記説明の中でも触れたとおり）逐次アルゴリズムの対応物として新たに導入した「逆像関手と自然変換の組合せによる射の定義」が全体の議論の中で正しく機能するか確認することである．これについては，特に「層の圏SHの中で，対象FとS(C(F))の間に同型な射が存在すること」の厳密な証明を与えながら検証する必要がある．また，今回導入した射の定義は数学的にも非常に自然な形式を持っているので，証明作業と並行して，このような概念が既に他分野でも有効に活用されている事例がないか調査する予定である．
圏CDと圏SHの間に正確な同等性を確立できたら，そこで得られた知見を利用して，gameの圏GAも層構造のインスタンスとして説明することを試みる予定でいる．game意味論の中で利用される射（innocent戦略など）の概念においては，逐次アルゴリズムよりも繊細な情報管理が行われ，計算履歴の参照範囲をコントロールする仕組が備わっている．（そのことが，PCFのfull abstractionを確立する際に不可欠な特徴でもあった．）これに対して，今回得られた新たな射の概念でも，逆像関手の与え方を調整することによって同様の情報コントロールが出来るのではないかと予想している．（基本的に圏CDと圏GAの構造には類似点が多いので，この部分が解消されれば，多くの議論が障害なく活用できる見込みである．）研究計画調書の段階では，game意味論との対応についてはやや長期的な研究課題と捉えていたが，内容の重要性を考慮して当初の計画よりも優先的に考察を進めたいと考えている．
|
