2007 Fiscal Year Annual Research Report
アルゴリズムの構造を反映する数理モデルの構成と応用
| Project/Area Number |
19700012
|
|---|
| Research Institution | Hosei University |
|---|
Principal Investigator |
倉田 俊彦 Hosei University, 経営学部, 准教授 (40311899)
|
|---|
| Keywords | プログラム意味論 / 型理論 / 層論 / 完備半順序集合 / 外延性 |
|---|
| Research Abstract |
様々なラムダ計算の枠組に対して(1)カルテシアン閉圏に基づいた数理モデルの外延性を保障するうえで「2分木の形をした項の違いを反映すること」の必然性を明らかにすること,(2)前層のトポスに基づいて「計算過程の構造を反映する数理モデルの一般的理論」を構築すること,を目標として考察を行った.その結果として,(2)の課題については,考察の初期段階で大きく進展があった.具体的には,(位相空間X上の前層に融和性の条件を付随して得られる)層の概念の中でSets(集合と関数の圏)の部分を全てCpos(完備半順序集合と連続関数の圏)に置き換えて,新たにCpos(X)(完備半順序集合の層とその上の自然変換の圏)の概念を導入すると,その圏の中で「対象の直積」や「射の集合」の各断面に対して自然に順序構造を導入することができ,それらも完備半順序集合の層となることが分かった.また,Cpos(X)の中で任意の拡大列の帰納極限を構成する方法も得られ,「Cpos(X)上の任意の連続関手に対して不動点を構成すること」が可能となった.こうした特徴を持つ構造は,「外延性を排除しながら様々なデータ構造や型無ラムダ計算のような強力な構文を矛盾なく解釈することが出来る数理モデルの一般的な枠組」を実現し,既知の研究にはない長所を数多く持つことになる.今後はこのアプローチの詳細を詰めながら,有限近似の概念を扱えるように拡張することや,具体的なモデルの中でラムダ式の解釈を精密に分析することが必要であると考えている.本年度の考察が(2)に集中したこともあり,(1)については十分に考察が進んでいないが,現時点で,「2分木の条件はテータ構造の追加などによって排除されることがない本質的な条件である」という印象を持っていて,単純型付ラムダ計算のηよりも強い理論の大域構造の分析と合わせて引き続き考察を続ける予定である.
|
Research Products
(1 results)
