1999 Fiscal Year Annual Research Report
| Project/Area Number |
10480061
|
|---|
| Research Institution | KYOTO UNIVERSITY |
|---|
Principal Investigator |
佐藤 雅彦 京都大学, 大学院・情報学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
竹内 泉 京都大学, 大学院・情報学研究科, 助手 (20264583)
亀山 幸義 京都大学, 大学院・情報学研究科, 助教授 (10195000)
|
|---|
| Keywords | 古典論理 / 構成的プログラミング / 型理論 |
|---|
| Research Abstract |
本研究では、古典論理に基く構成的プログラミングの構築のため、例外処理機構を追加した関数型プログラミング言語PActを発展させ、以下の成果を得た。
研究代表者佐藤は、述語論理、及び関数型プログラミング言語にとって重要な概念である束縛変数について研究した。その結果、変数の名前替えを行なわない束縛変数の計算体系を提案した。従来の述語論理やラムダ計算では、変数の束縛がある環境の中の変数へ項を代入する際には、煩雑な変数の名前替えの処理が必要であった。この計算体系は、その煩雑さの陰にあった名前替えの本質を明らかにした。この点に於て、この研究は画期的なものである。この研究は国際学会「型付ラムダ計算とその応用・99年」論文集に収録された。
研究分担者亀山は、古典論理に基く型付き関数型プログラミング言語に於る例外処理機構及び部分継続について研究した。そして、例外処理機構や部分継続を持つ幾つかの型付き計算に対してそれらを分類、整理した。その計算体系の停止性問題、合流性問題を解き、停止性、合流性が成り立つことの条件を明らかにした。この研究は英文学術雑誌「理論的計算機科学」に収録される。
研究分担者竹内は、帰納法とパラメトリシティーの関係を研究した。帰納法は構成的プログラミングに於て重要な証明手段であり、パラメトリシティーの理論から、各種の帰納法が自然に導出されることを示した。この研究は英文学術雑誌「フンダメンタ・インフォルマチカ」に収録された。
|
-
[Publications] 佐藤 雅彦 他: "Explicit Environments"Lecture Notes in Computer Science. 1581. 340-354 (1999)
-
[Publications] 亀山 幸義 他: "Strong Normalizability of the Non-deterministic Cateh/Thow caluculi"Theoretical Computer Science. (掲載予定). (2000)
-
[Publications] 亀山 幸義: "A Type System for Delimited Continuations"JSSST Workshop on Programming & Programming Languages. (掲載予定). (2000)
-
[Publications] 竹内 泉: "An Axiomatic System of Parametricity"Fundamenta Informatical. 33. 397-432 (1998)
