The new aspects in constructive programming.
| Project/Area Number |
06680333
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kobe University (1995)
Ryukoku University (1994) |
|---|
Principal Investigator |
HAYASHI Susumu Kobe University, Department of Computer and Systems Engineering, Professor, 工学部, 教授 (40156443)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KOBAYASHI Satoshi Rykoku University, Department of Applied Mathematics and Informatics, Research A, 理工学部, 助手 (70234820)
NAKANO Hiroshi Rykoku University, Department of Applied Mathematics and Informatics, Lecturer, 理工学部, 講師 (30217799)
小林 聡 龍谷大学, 理工学部, 助手 (60195831)
|
|---|
| Project Period (FY) |
1994 – 1995
|
| Project Status |
Completed (Fiscal Year 1995)
|
| Budget Amount *help |
¥1,500,000 (Direct Cost: ¥1,500,000)
Fiscal Year 1995: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 1994: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | Constructive programming / Program verification / Program logic / 形式的方法 / 型理論 / 構成的数学 |
|---|
| Research Abstract |
(1) We extended PX system by catch/throw logic and investigated its relation to non-informative quantifiers. We added catch/throw logic by Nakano to constructive programming logic using the concept of "frame" of CIG induction scheme of PX.And we implemented a prototype of PX with Nakano logic and conducted experiments with it. As the logic of PX system is based on Lisp system, there is no way to know weather a throw occuerd in a computation. We showed this observation is naturally formalized by the non-informative quantifiers by Hayashi.
(2) We introduced the non-deterministic catch/throw mechanism. It naturally introduces non-deterministic computation. We gave a theory which shows such a non-deterministic mechanism does not lead to contradiction of the logic.
(3) We gave a constructive logic correspoinding to S4 modal logic. We showed that its realizability and Moggis's collapsing in his monad type theory are essentially the same. We showed that the evaluation modality can be counted as an extension of non-informative quantifier and it increases the expressivility of the modal logic.
(4) Besides the main results above, we got the following results : (i) two other versions of PX system were implemented, one is based on multiple value computation and the other has a much improved user interface. (ii) we improved the logical foundation of PX and related it to Frege structure.
|
Report
(3 results)
Research Products
(17 results)
