| Project/Area Number |
05680276
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYUSHU UNIVERSITY |
|---|
Principal Investigator |
HIROKAWA Sachio KYUSHU UNIVERSITY,DEPARTMENT OF PHYSICS,ASSOCIATE PROFESSOR, 理学部, 助教授 (40126785)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KOMORI Yuichi SHIZUOKA UNIVERSITY,DEPARTMENT OF MATHEMATICS,ASSOCIATE PROFESSOR, 理学部, 助教授 (10022302)
|
|---|
| Project Period (FY) |
1993 – 1994
|
| Project Status |
Completed (Fiscal Year 1994)
|
| Budget Amount *help |
¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 1994: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 1993: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | Constructive logic / Lambda calculus / Type theory / Intuitionistic logic / Relevant logic / Curry-Howard / Formulas-as-types / Classical logic / 線形論理 |
|---|
| Research Abstract |
A formal system was obtained for the correspondence between formulas and computation rules. This correspondence extends the Formulas-as-type notion which is a basis of functional programming languages and program extraction from the constructive proofs.
An essential discovery above the intuitionistic logic was the reduction rule for Peirce formula. This formula characterises the classical logic. The reduction rule we obtained has natural meaning not only from logical view point but also from program extraction using classical proofs. Several properties of the reduction were obtained. The similarity to the continuation computation was found as well. Further analysis is necessary.
The following are the selection of the result for substructural logics below intuitionistic logic. Komori gave a clear syntactic proof for the P-W problem in relevant logic by applying Gentzen system. Hirokawa characterised the lambda-terms that correspond to the proofs in P-W and clarified the structure of the proofs in P-W.In the joint work with M.Takahashi and Y.Akama, Hirokawa obtained a description of the set of proofs for a formula in intuitionistic logic as a context-free-like grammar.
|
