| Project/Area Number |
08780236
|
|---|
| Research Category |
Grant-in-Aid for Encouragement of Young Scientists (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
龍田 真 京都大学, 大学院・理学研究科, 助教授 (80216994)
|
|---|
| Project Period (FY) |
1996
|
| Project Status |
Completed (Fiscal Year 1996)
|
| Budget Amount *help |
¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 1996: ¥1,100,000 (Direct Cost: ¥1,100,000)
|
|---|
| Keywords | プログラム合成 / プログラム理論 / 帰納的定義 / 実現可能性解釈 |
|---|
| Research Abstract |
本研究の目的は、プログラムの性質を形式化して論じる事のできる論理体系TIDを構成する事と、この論理体系の証明環境を計算機上に実現する事の2点である。
プログラムの性質を自然な形で表現するためには、帰納的定義および余帰納的定義(coinductive definition)が不可欠である。自然数、リスト、木などのデータおよびプログラムの繰り返しは、帰納的定義により自然に形式化でき、また、ストリームに関する性質は余帰納的定義により自然に形式化できるからである。
本研究では、帰納的定義をもつ論理体系EON+μ,TID0および余帰納的定義をもつ論理体系TID+νの性質に関する研究をいっそう進め、帰納的定義を用いたプログラム合成の基礎理論を進展させた。特に、対象となるプログラム言語を、catch/throw機構に拡張した場合のプログラムの公理的意味論および強正規化可能性について考察した。並行プログラムの合成を行なうため、π計算および線型論理含むような論理体系の拡張について考察した。構成的集合の内的形式化およびそれを用いた実現可能性解釈を得た。また、線形論理の独立論理式などを線形論理の基本的性質について考察した。合成されるプログラムの計算量を調べるため、有界算術についてその表現可能関数などの基本性質を考察した。
|
Report
(1 results)
Research Products
(1 results)
