Design and Implementation of Constructive Programming Systems

构造性编程系统的设计与实现

• 批准号: 08558023
• 负责人: SATO Masahiko
• 金额: $ 3.9万
• 依托单位: KYOTO UNIVERSITY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 1996
• 资助国家: 日本
• 起止时间: 1996 至 1997
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-08558023/
• 关键词: Constructive Programming; Interactive Proof System; Intuitionistic Logic; Classical Logic; Modal Logic; 証明支援システム; グラフィカルユーザインターフェース; 証明エンジン

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

在这个为期两年的研究项目中，我们设计并实现了一个辅助建设性编程的原型软件系统。我们还通过使用该系统进行编程示例来评估该系统。 1996 年，(1) 我们实现了函数式编程语言 LAMBDA 的解释器，它是本项目中所有软件系统的基础，(2) 我们实现了用于直观一阶谓词演算的交互式定理证明系统。基于这些结果，1997年，（3）我们为各种逻辑系统（例如模态逻辑的许多变体）实现了一个交互式定理证明系统，（4）我们为经典逻辑实现了一个构造性编程系统。（2）：我们实现了一个基于X窗口系统的具有复杂图形用户界面的交互式定理证明系统。我们的部分实现是用JAVA编程语言编写的，我们的设计旨在通过模块进行分布式编程（分布式证明）。 (3)：我们扩展了系统(2)，使得目标逻辑系统不必是直观的一阶逻辑。我们的实现包括模态逻辑的许多变体，例如 T、S4、S5、B 等。该系统可以被视为一个独立于特定逻辑的证明策略的系统。 (4)：从经典证明中提取算法内容是构造性编程中一个相当新的主题。我们设计并实现了两种不同的方式，一种使用catch/throw机制，另一种使用first-class continuation。然后我们从经典证明中提取算法。使用（2）-（4）中的系统，我们编写了许多编程（证明）示例。通常观察到，当程序的规范被严格地编写时，指定的程序被合成得相当顺利。结果，我们证明了构造性编程可以适用于比以前更广泛的目标，并且我们的系统可以成为现实行业中构造性编程系统的第一步。较少的

项目成果

Yukiyoshi Kameyama: "A New Formulation of the Catch/Throw Mechanism" Second Fuji International Workshop on Functional and Logic Programming,World Scientific. 106-122 (1997)

Yukiyoshi Kameyama：“捕捉/投掷机制的新公式”第二届富士函数和逻辑编程国际研讨会，世界科学。

Makoto Tatsuta: "Realizability for Constructive Theory of Functions and Classes and Its Application to Program Synthesis" Proc.Thirteenth Annual IEEE Symposium on Logic in Computer Science. (印刷中).

Tatsuta Makoto：“函数和类的构造理论的可实现性及其在程序综合中的应用”Proc。第十三届 IEEE 计算机科学逻辑研讨会（正在出版）。

Yukiyoshi Kameyama: "A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability" Proc.4th Australasian Theory Symposium. 20-3. 183-197 (1998)

Yukiyoshi Kameyama：“具有标签抽象及其强规范化性的经典接/投掷微积分”Proc.4th 澳大利亚理论研讨会。

Makoto Tatsuta: "Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis" Proc.Fourth International Conference on Mathematics of Program Construction,LNCS. (印刷中).

Makoto Tatsuta：“单调共导定义的实现及其在程序综合中的应用”Proc.第四届程序构造数学国际会议，LNCS（印刷中）。

沢村 一: "エージェント指向コンピューティングのための計算倫理学に向けて-公平性-" ソフトウェア工学の基礎IV. IV. 28-34 (1997)

Hajime Sawamura：“面向代理计算的计算伦理 - 公平 -”软件工程基础 IV 28-34 (1997)。