Implementation of Constructive Programming Based on Classical Logic

基于经典逻辑的构造性规划的实现

• 批准号: 10480061
• 负责人: SATO Masahiko
• 金额: $ 2.94万
• 依托单位: KYOTO UNIVERSITY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 1998
• 资助国家: 日本
• 起止时间: 1998 至 1999
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-10480061/
• 关键词: Classical Logic; Constructive Programming; Type Theory; 算術; キャッチ・スロー機構

For the purpose of developing constructive programming based on classical logic, this research extended the functional programming language PAィイD2ctィエD2, which has catch/throw mechanism as exception processing, and made the following results.The head investigator Sato studied the notion of binding variables, which is the important notion for predicate logic and functional programming language. As the result of this study, he proposed a calculus which do not have renaming of bind variables. This result was presented in the 4th international conference on Typed Lambda Calculi and Application in 1999, at L'Aquia, Italy.The investigator Kameyama studied exception processing and partial contiunation in functional programming languages based on classical logic, and classified typical calculi with exception processing and partial continuation. He solved the problems of confluency and termination of such calculi. This results are to be published in 'Theoretical Computer Science'.The investigator Takeuti studied the relation between parametric polymorphism and mathematical induction. Mathematical induction is an important method to prove theorems in systems of constructive programming. He showed that system of parametricity derives various forms of mathematical induction. This result was published in 'Fundamenta Informaticae'.

本研究以基于经典逻辑的构造性编程为目的，扩展了函数式编程语言PA，将catch/throw机制作为异常处理，并取得了以下成果。 首席研究员佐藤提出了绑定变量的概念，即作为谓词逻辑和函数式编程语言的重要概念，他提出了一种不重命名绑定变量的演算。该结果在第四届类型 Lambda 演算和应用国际会议上发表。 1999年，在意大利L'Aquia。研究者Kameyama研究了基于经典逻辑的函数式编程语言中的异常处理和部分延续，并用异常处理和部分延续对典型演算进行了分类，他解决了汇合和终止的问题。这一结果将发表在《理论计算机科学》上。研究者 Takeuti 研究了参数多态性和数学归纳法之间的关系。数学归纳法是证明系统定理的重要方法。他证明了参数化系统导出了各种形式的数学归纳法。这一结果发表在“Fundamenta Informaticae”上。

项目成果

Sato Masahiko, Barstall Rod & Sakurai Taka-fumi: "Expicit Environment,"Proc. Typed Lambda Calcu-lus and Applications 1999, LNCS. vol.1581 Springer. 340-354 (1999)

佐藤正彦、巴斯托·罗德

Kameyama Yukiyoshi: "A Type System for Delimited Continuations,"JSSST Workshop on Program-ming and Programming Lan-guages'2000, March. (2000)

Kameyama Yukiyoshi：“用于定界延续的类型系统”，JSSST 编程和编程语言研讨会，2000 年，3 月。

亀山 幸義: "A Type System for Delimited Continnations"JSSST Workshop on Programming & Programming Languages. (掲載予定). (2000)

Yukiyoshi Kameyama：“定界连续的类型系统”JSSST 编程和编程语言研讨会（即将出版）。

佐藤 雅彦 他: "Explicit Environments"Lecture Notes in Computer Science. 1581. 340-354 (1999)

Masahiko Sato 等人：“显式环境”计算机科学讲义 1581. 340-354 (1999)。

Takeuti Izumi: "An axiomatic system of parametricity,"Fundamenta Informaticae. 33. 397-432 (1998)

Takeuti Izumi：“参数化的公理系统”，Fundamenta Informaticae。