Optimization in Constructive Programming

将Beradi方法应用于PX系统的原计划变得困难。因此我们改变了计划。我们重新设计了PX系统，使它有类型，所以提取的程序是简单的类型。我们甚至从基本的逻辑体系出发，对系统进行了彻底的重构。新的逻辑系统被命名为S，新的实现被命名为Proof Works。由于使用了当时PX系统设计和构建时所没有的许多新知识，系统被重新制作，结果比原计划更好。在研究过程中，Hayashi对构造性编程的应用有了新的见解，称为"Proof Animation"。“这一新的见解是目前研究的副产品，不仅比研究的最初目的更重要。它预计将增长的功能领域的中心问题之一。一件事，我们不能实现的是，广泛的实验与系统。这是由于整个系统的新设计和实施造成的延误。即使在项目正式完成后，我们仍在继续这项工作。

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.