The new aspects in constructive programming.

点击翻译按钮获取中文摘要

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