权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

The new aspects in constructive programming.

建设性规划的新方面。

基本信息

批准号：
06680333
负责人：
HAYASHI Susumu
金额：
$ 0.96万
依托单位：
Kobe University (1995)Ryukoku University (1994)
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1994
资助国家：
日本
起止时间：
1994 至 1995
项目状态：
已结题

项目摘要

(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.

(1)我们通过catch/ throw逻辑扩展了PX系统，并研究了它与非信息量词的关系。我们利用PX的CIG归纳方案的“框架”概念，将Nakano的catch/ throw逻辑添加到构造性编程逻辑中，并用Nakano的逻辑实现了PX的原型并进行了实验。由于PX系统的逻辑基于Lisp系统，因此无法知道计算中是否发生了抛出。我们证明这一观察自然地由 Hayashi 的非信息量词形式化。(2)我们引入了非确定性的捕获/抛出机制。它自然地引入了非确定性计算。我们给出了一个理论，表明这种非确定性机制不会导致逻辑的矛盾。(3)我们给出了与S4模态逻辑相对应的构造逻辑。我们证明了它的可实现性和莫吉斯在他的单子类型理论中的崩溃本质上是相同的。我们表明，评估模态可以算作非信息量词的扩展，它增加了模态逻辑的表达能力。（4）除了上述主要结果外，我们得到了以下结果：（i）实现了PX系统的其他两个版本，一个基于多值计算，另一个具有大大改进的用户界面。 (ii)我们改进了PX的逻辑基础并将其与弗雷格结构联系起来。