Theory of Constructive Programming

构造性规划理论

• 批准号: 08458068
• 负责人: SATO Masahiko
• 金额: $ 4.67万
• 依托单位: KYOTO UNIVERSITY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 1996
• 资助国家: 日本
• 起止时间: 1996 至 1997
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-08458068/
• 关键词: Constructive Programming; Catch; Throwcontrd; Type Theory; Catch; Throw機構

This project had three large subjects, which are listed in the following.The first was to construct logical systems corresponding to catch-throw mechanism. The investigators researched for characteristics and semantics of logical systems corresponding to catch/throw mechanism. As the result of that the investigators constructed the logical systems MJct and NKct, and proved that the logical systems NJct and NKct are conservative extensions of NJ and NK, respectively. The investigators also showed that these systems are useful for constructive programming. This subject was mainly developed by Sato and Kameyama.The second was on realizability interpretations of untyped calculation theory. The investigations was aimed at giving realizability interpretations for logical systems with untyped calculus, and applying it to constructive programming. As the result of that, the investigators gave a realizability interpretation for logical system for a set theory. This realizability interpretation is very much improved as compared to the former ones, which used double variables. The investigators also gave a realizability interpretation for a system with co-induction, and showed an application of this realizability interpretation to constructive programming. This subject was mainly developed by Tatsuta.The third was on constructivew logical systems for polymorphism. The investigators made a research pn parametricity of polymorphic calculation systems, such as SYstem F, second order lambda calculus. As the result of that, the investigators gave logical systems ; one of them is for parametric polymorphism of System F, and another is for cyclic structure. This subject was mainly developed by Takeuti.

本课题有三大课题，分别是：第一，构建与接抛机制相对应的逻辑体系;研究者对与catch/throw机制相对应的逻辑系统的特征和语义进行了研究。在此基础上，构造了逻辑系统MJct和NKct，并证明了逻辑系统NJct和NKct分别是NJ和NK的保守扩张。研究人员还表明，这些系统对建设性编程很有用。这一课题主要是由佐藤和龟山发展起来的。第二个是关于非类型计算理论的可实现性解释。这些研究的目的是给出非类型演算逻辑系统的可实现性解释，并将其应用于构造性编程。由此，研究者对集合论的逻辑系统给出了可实现性解释。这种可实现性解释与以前使用双变量的解释相比有了很大的改进。研究人员还给出了一个系统的可实现性解释与共同感应，并显示了这种可实现性解释的建设性编程的应用。第三个是关于多态性的构造性新逻辑系统。研究者们对多态计算系统如SYstem F、二阶lambda演算等的参数化进行了研究。作为结果，研究者给出了逻辑系统，其中之一是系统F的参数多态性，另一个是循环结构。这个主题主要由Takeuti开发。

项目成果

Makoto Tatsuta: "Realizability of Coinductive THeory of Functions and Classes and its Application to Program Synthesis" Lecture Notes in Computer Science. 13. (1998)

Makoto Tatsuta：“函数和类的共归纳理论的实现及其在程序综合中的应用”计算机科学讲义。

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

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

Makoto Tatsuta: "Realizability of Monotone Coindudive Definitions and its Application to Program Synthesis" Lecture Notes in Computer Science. (発表予定).

Makoto Tatsuta：“单调共融定义的可实现性及其在程序综合中的应用”计算机科学讲义（待提交）。

Izumi Takeuti: "An Axiomatic System of Parametricity" Lecture Notes in Computer Science. 1210. 354-372 (1997)

Izumi Takeuti：“参数化公理系统”计算机科学讲义。

Izumi Takeuti: "A Type Theory for Cyclic Structure" Proc.3rd Fuji Int'l Symp.on Func.and logic Programing. 3(発表予定). (1998)

Izumi Takeuti：“循环结构的类型理论”Proc.3rd Fuji Intl Symp.on Func.and 逻辑编程 3（即将发表）。