| Project/Area Number |
12680346
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | National Institute of Informatics (2001-2003)
Kyoto University (2000) |
|---|
Principal Investigator |
TATSUTA Makoto National Institute of Informatics, Professor, 情報学基礎研究系, 教授 (80216994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
照井 一成 国立情報学研究所, 情報学基礎研究系, 助手 (70353422)
|
|---|
| Project Period (FY) |
2000 – 2003
|
| Project Status |
Completed (Fiscal Year 2003)
|
| Budget Amount *help |
¥3,000,000 (Direct Cost: ¥3,000,000)
Fiscal Year 2003: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2002: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2001: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2000: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | Constructive logic / Type theory / Theory of programs / Strong normalization / Permutative reductions / 構成的集合 / 余帰納的定義 / 実現可能性解釈 / プログラム合成 |
|---|
| Research Abstract |
The aim of this research project was to construct a constructivelogical system which has constructive sets and coinductive definitions, to investigate programs with coinductive types using this locig, and tomake a prototype of program sysnthesis system based on this logic. We have obtained the following three main results.
(1) We have prove that if a formula A has a long D-normal form proof, then a long normal form of A is unique. (2) We have pointed out an error of Parigot's proof of strong normalization of second order classical natural deduction by the CPS-translation, discussed erasing-continuation of the CPS-translation, and corrected that proof by. using the notion of augmentations. (3) A simple and complete proof of strong normalization for first and second order intuitionist natural deduction including disjunction, existence and permutative conversions has been given. We followed Tait-Girard approach via computability predicates (reducibility) and saturated sets. Strong normalization was first established for a set of conversions of a new kind, then deduced for the standard conversions. Difficulties arising for disjunction were resolved using a new logic where disjunction is restricted to atomic formulas.
|
