2002 Fiscal Year Annual Research Report
| Project/Area Number |
14780235
|
|---|
| Research Institution | Tokyo Metropolitan University |
|---|
Principal Investigator |
倉田 俊彦 東京都立大学, 理学研究科, 助手 (40311899)
|
|---|
| Keywords | λ代数 / 領域方程式 |
|---|
| Research Abstract |
領域理論を用いた既知の表示的プログラム意味論は,Dとその上の連続関数全体[D→D]とが同型となるようになるように領域Dを構成して,その中でプログラムの持つ意味を解釈するものであった.その際,関数概念を経由して意味が割り当てられるため,プログラムの内部構造を反映した解釈を確立することはできない.これに対して,今年度はプログラムの内部構造を反映することが可能な枠組(具体的にはλ代数と呼ばれる構造)の領域理論的構成を試みた.
上の要請を満たすには,通常の議論における連続関数の代わりに「外延性を持たないある種の数学的対象」が必要となる.今年度の研究では,先ずそのような対象として「情報の近似を明示的に表現することが可能なpolynomial」の概念を導入し,それに伴って領域理論自体に若干のrefinementを施した.その上で,領域DからD上のpolynomialの全体からなる領域D[x]の構成法を与え,方程式D【similar or equal】D[x]の解となる領域の構成を目標とした.
領域方程式の解の構成法には様々なものが知られているが,その一つに(D.Scottによって考案された)逆極限法と呼ばれる手法がある.これは,領域が構成する圏の中で方程式の性質を反映した拡大列の双極限を解とするものである.上の方程式に対しても,逆極限法を適用することを考え,今回導入した領域の圏の中でも全ての拡大列が双極限を持つことを示した.現在は,以上のアプローチに沿って実際にλ代数の構成を行っているところである.
|
-
[Publications] Hajime Ishihara, Toshihiko Kurata: "Completeness of intersection and union type assignment systems for call-by-valueλ-models"Theoretical Computer Science. 272. 197-221 (2002)
-
[Publications] Toshihiko Kurata: "Intersection and singleton type assignment characterizing finite Bohm-Trees"Information and Computation. 178. 1-11 (2002)
