Design and Implementation of Constructive Programming Systems

在这个为期两年的研究项目中，我们设计并实现了一个辅助构造性编程的原型软件系统。并通过编程实例对该系统进行了评估。1996年，(1)我们实现了函数式程序设计语言Lambda的解释器，它是本领域所有软件系统的基础；(2)我们实现了一个直观一阶谓词演算的交互式定理证明系统。在此基础上，1997年，(3)我们实现了一个用于多种逻辑系统的交互式定理证明系统，如多种形式的模态逻辑；(4)我们实现了一个用于经典逻辑的构造性程序设计系统。(2)：我们基于X窗口系统实现了一个具有复杂图形用户界面的交互式定理证明系统。我们的部分实现是用Java编程语言编写的，我们的设计旨在通过模块进行分布式编程(分布式证明)。(3)：WE…对系统(2)进行了更多的扩展，使得目标逻辑系统不需要是直观的一阶逻辑。我们的实现包括多种形式的模态逻辑，如T、S4、S5、B等。该系统可以看作是一个独立于特定逻辑的证明策略的系统。(4)：从经典证明中提取算法内容是构造性程序设计中一个相当新的课题。我们设计并实现了两种不同的方式，一种是使用接球/抛出机制，另一种是使用一类延续。然后我们从经典证明中提取算法，使用(2)-(4)中的系统，我们编写了许多编程(证明)例子。通常观察到，当程序的规范被严格地编写时，指定的程序被非常顺利地综合。因此，我们已经表明，建设性编程可以适用于比以前更广泛的目标，我们的系统可以是朝着真实行业中的建设性编程系统迈出的第一步。较少

In this two-year research project, we designed and implemented a prototypical software system which assists constructive programming. We also evaluated the system by making programming examples using it. In 1996, (1) we implemented an interpreter of a functional programming langauge LAMBDA which is a basis for all the software systems in this profect, and (2) we implemented an interactive theorem proving system for an intuitionistic first-order predicate calculus. Based on these results, in 1997, (3) we implemented an interactive theorem proving system for various logical systems such as many variants of modal logics, and (4) we implemented a constructive programming system for a classical logic.(2) : We implemented an interactive theorem proving system with a sophisticated graphical user interface based on X window system. A part of our implementation is written in the programming language JAVA,and our design aimed at distributed programming (distributed proving) by modules. (3) : We … More extended the system (2) so that the target logical system need not be an intuitionistic first-order logic. Our implementation includes many variants of modal logics such as T,S4, S5, B and so on. The system can be regarded as a system towards a proving strategy independent of specific logics. (4) : Extracting algorithmic contents from classical proofs is a quite recent topic in constructive programming. We designed and implemented two different ways, one uses the catch/throw mechanism, and the other uses the first-class continuation. We then extracted algorithms from classical proofs.Using the systems in (2)-(4), we wrote many programming (proving) examples. It is generally observed that, when specification of a program is rigidly written, the specified program is synthesized quite smoothly. As a result, we have shown that constructive programming can be applicable to much wider targets than befor, and our systems can be a first step towards a constructive programming system in the real industry. Less