Optimization in Constructive Programming

原计划将Beradi方法应用于PX系统变得困难。因此我们改变了计划。我们重新设计了PX系统，使其具有类型，因此提取的程序只是类型。我们甚至从基本的逻辑系统开始，对系统进行了彻底的重建。新的逻辑系统被称为S，新的实现被称为Proof Works。结果比原来的计划更好，因为系统使用了许多在设计和构建PX系统时没有的新知识。在研究过程中，Hayashi对构造性编程的应用有了一个新颖的见解，叫做“证明动画”。这种新的见解是目前研究的副产品，不仅比研究的最初目的更重要。预计这将成为该地区的核心问题之一。有一件事我们做不到，那就是对这个系统进行广泛的实验。这是由于整个系统的新设计和实现造成的延迟。即使项目正式结束，我们仍在继续。

The original plan to apply Beradi method to PX system turned to be difficult. Thus we changed the plan. We redesigned PX system so that it has types and so the extracted programs are simply typed. We rebuilt the system throughly even from the basic logical system. The new logical system was called S,and the new implementation is called Proof Works.The results turned out even better than the original plan, because the system was redone utilizing many new knowledges which were not available at the time PX system was designed and built.On the course of research, Hayashi got a novel insight on application of constructive programming called "Proof Animation." This new insight, which is a spin-off of the present research, is not only more important than the original aim of the research. It is expected to grow one of central issues of the area in the feature.One thing we could not achive is that extensive experiments with the system. This is due to the delay caused by the new design and implementation of the entire system. We are continueing it even after the project is officially finished.