構成的プログラミングにおける非局所脱出機構を持つプログラムの合成

构造性编程中具有非局部转义机制的程序综合

• 批准号: 08780232
• 负责人: 亀山 幸義
• 金额: $ 0.7万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1996
• 资助国家: 日本
• 起止时间: 1996 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-08780232/
• 关键词: 構成的プログラミング; 非局所脱出機構; Catch; Throw機構; 強正規化可能性

関数型プログラム言語における非局所脱出機構を取り上げ,構成的論理との対応を調べた.まず,Common Lispなどにおける非局所脱出機構であるCatch/Throw機構を取り上げ,CatchとThrowのそれぞれに対応する推論規則を持つ型理論的体系について検討した.型理論の体系では最も興味深い性質の1つである停止性(強正規化可能性)が,従来提案されていた体系に対して成立することを,強いreducibilityという概念を新たに用いることにより証明した.次に,従来提案されていた体系では,プログラムの記述力が弱く,高階関数プログラミングを自然に展開することができないことを指摘し,停止性が成立する範囲内でどこまで体系の表現力を上げることができるか検討した.その結果,新たに,「データの型(関数型構成子を使わないで構成できる型)に対するCatch/Throwは無制限に使ってよい,という緩い制限のもとでも,型理論的体系が構成でき,停止性も成立することを示した.現実のプログラムの中で発生するCatch/Throwは,基礎データの受け渡しに使われることが大部分であるため,この制限は非常に合理的である.新しく提案したCatch/Throw機構を持つ体系において,多くのプログラム例を記述し,提案した体系が構成的プログラミングの観点から有用なものであることを示した.本研究では主としてCatch/Throw機構を扱ったが,関数型言語MLにおける非局所脱出機構であるException機構も,同様に,本研究での体系で記述することができる.そこで,Exception機構を用いた例も作成した.

The logic of the system consists of two parts: one is the logic of the system, the other is the logic of the system. Common Lisp is a system of non-local escape mechanisms, catch and Throw mechanisms, inference rules, and theoretical systems. The system of type theory is the most interesting and the property is the stopping property (strong normalization possibility). Second, in the future, the system's descriptive power is weak, and the high-level relationship between the system and the system is natural. As a result, the new model (related to the number of sub-components in the composition of the model) corresponds to the Catch/Throw unlimited limit, and the type of theoretical system is composed of the following elements: Catch/Throw is the most reasonable way to control the situation. New proposal Catch/Throw mechanism to maintain the system in the middle of the process, a number of examples to describe, proposal system to constitute the process of the process, the point to use the process to show. This study focuses on Catch/Throw mechanism, which is related to numerical speech ML. The Exception mechanism is used to create the exception.

项目成果

亀山 幸義: "型付けされたプログラム言語と停止性" 京都大学大学院工学研究科情報工学専攻、情報工学研究談話会. 第156回. 1-13 (1996)

Yukiyoshi Kameyama：《类型化编程语言和终止》京都大学大学院工学研究科信息工程研究讨论会第156期（1996年）。

Yukiyoshi Kameyama: "A New Formulation of the Catch/Throw Mechanism" Proc.Inpl Workshop on Func.and Logic Programming. 56-64 (1996)

Yukiyoshi Kameyama：“捕捉/抛出机制的新公式”Proc.Inpl Func.and Logic 编程研讨会。