权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

構成的プログラミングの手法による制御機構を持つプログラムの合成

使用构造性编程技术将程序与控制机制综合起来

基本信息

批准号：
09780266
负责人：
亀山幸義
金额：
$ 1.34万
依托单位：
Kyoto University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1997
资助国家：
日本
起止时间：
1997 至 1998
项目状态：
已结题

项目摘要

関数型プログラミング言語におけるコントロールオペレータとして昨年度の研究では主としてキャッチスロー機構について研究を行ってきたが,今年度の研究では,より強力なオペレータとして部分継続に着目し,その定式化を行った.部分継続は,継続をより洗練した機構であり,通常の継続が「残りの計算の全て」を表すオブジェクトを抽象するのに対して,部分継続は「残りの計算の一部」を表すオブジェクトを抽象する.一部を指定するために,control del1miter(制御限定子)をプログラム中の任意の場所に設定することができる.本年度の研究では,部分継続を型理論の枠組みの中で定式化した.特に,継続限定子と部分継続オペレータの対が従来の研究では1種類の限定していた制限を除去し,複数の種類の対を使うことができるよう拡張した.ここで定式化した体系の性質を調べ,合流性や型の安全性など望ましい性質が満たされることを証明した.また,この体系がCurry-Howardの同型対応のもとで古典論理に対応することを示し,この体系を古典論理の証明からのプログラム抽出に用いることができることを示した.一方,プログラミングの観点からの成果としては,まず,この計算系の処理系(イシタープリタ)を作成し,さらに,この枠組みでのプログラミングの実例を蓄積した.特に,部分継続を用いてcoroutineを自然に表現できることを示し,二分木の走査関数を用いたsaome-fringe問題の効率的なプログラミング例を示した.

The research conducted in the past year has been conducted by the main body of research on the relationship between the number of types of speech and the number of types of speech. This year's research has been conducted by the main body of research on the organization of speech. Some of them are "part of residual computation" and some of them are "part of residual computation". A part of the specification,control del1miter(control qualifier), any place in the list This year's research is aimed at formalizing some of the model theories. In particular, the definition of the sub-category of the study is to eliminate the limitation of the category of the study, and to expand the category of the study. The properties of these systems are regulated, and the safety of convergent systems is expected to be proved. This system is shown by the classical logic of the Curry-Howard congruence. This system is shown by the classical logic of the proof. On the other hand, the results of the optimization of the system are accumulated in the processing system of the computing system. In particular, part of the coroutine is used to show the natural behavior of the tree. The number of branches is used to show the efficiency of the saome-fringe problem.