2003 Fiscal Year Final Research Report Summary
Program synthesis using constructive sets and coinductive definitions
| 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)
|
|---|
| Project Period (FY) |
2000 – 2003
|
| 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.
|
Research Products
(5 results)
