2001 Fiscal Year Annual Research Report
| Project/Area Number |
13480082
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
佐藤 雅彦 京都大学, 情報学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
亀山 幸義 筑波大学, 電気・情報工学系, 助教授 (10195000)
竹内 泉 京都大学, 情報学研究科, 助手 (20264583)
|
|---|
| Keywords | 型理論 / 文脈 / 環境 / 計算体系 |
|---|
| Research Abstract |
本研究の目的は、(1)環境と文脈の概念を第一義的な要素として持つ計算系を構築すること、(2)論理の立場からこの計算系の理論的分析を行なうこと、(3)これらを通じて環境と文脈を持つ計算系の特性を明らかにすること、であった。
本研究では,明示的環境や明示的文脈を持った計算系を提案した.この体系では,通常メタレベルで扱われる環境や文脈を体系内で形式化している.しかし,文脈の扱いについては,以前として,メタレベルで可能なすべての操作ができるような体系にはなっていないので柔軟性を欠く点があり,さらに研究を進めている必要がある.
この体系の計算では,文脈の穴が超変数の役割を持っていて,穴へプログラムを挿入するときに変数への束縛が起こるとみなることが出来る.この点に注目すれば,文脈に関するメタレベルでの操作をすべて形式化することが出来るであろう.更に,超変数の概念を形式化するにはメタレベルでのどのような概念を形式化すればよいのかがはっきりしてくるはずである.
この計算系は型理論に基くものである.本研究ではこの計算系に対する理論的考察を行った.ここでいう理論的考察とは,型の保存性,合流性,強正規化可能性,従来の体系に対する保守的拡大性などのことである.この計算系はこれらの性質を充すことが確かめられた。
この体系は計算機上に部分的にではあるが実装された.
|
Research Products
(1 results)
