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

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

基本信息

批准号：
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機構を用いた例も作成した.

我们采用了功能编程语言中的非本地逃生机制，并研究了与本构逻辑的对应关系。首先，我们采用了捕获/投掷机制，这是LISP和其他领域的非本地逃生机制，并检查了一种类型的理论系统，其推理规则对应于捕获和投掷。我们证明了类型理论系统的最有趣的属性之一，即停止（强有力的可能性），对于先前提出的系统是正确的，它通过使用新的可降低性概念。接下来，我们指出，该程序的写作能力是薄弱的，并且不能自然地开发高阶功能编程，并且我们检查了在建立停止功率的范围内可以增加系统表现力量。结果，我们新引入了用于数据类型的新CAT（可以在不使用功能构造函数的情况下构造的类型）。已经表明，即使在宽松的限制下，CH/THRD可以在不限制的情况下使用，也可以使用CH/TORP而不限制，并且也可以停止。这种限制非常合理，因为在实际程序中发生的捕获/投掷主要用于传递基本数据。在具有捕获/投掷机制的新提出的系统中，描述了许多程序的示例，并且从本构编程的角度看，该系统被证明是有用的。在这项研究中，我们主要处理捕获/投掷机制，但是本研究中的系统中也可以描述异常机制，一种功能语言ML的非本地逃生机制。因此，还创建了一个使用异常机制的示例。