| 研究概要 |
本研究では,関数型プログラミング言語におけるコントロールオペレータと,古典論理の関係について研究し,古典論理の証明からのプログラム作成を目標としている.本年度は,そのための基礎となる体系として,部分継続の一種であるcontrol delimiter(制御限定子)を持つ体系について検討し,以下の成果を得た.制御限定子を持つ部分継続体系に対して,本研究代表者が過去の研究で提案した体系は,型の健全性,合流性など良い性質を持つが,Normal Form Propertyと呼ばれる性質は成立しないことを指摘し,この性質を持つ部分継続の体系を提案した.Normal Form Propertyは,計算が終了した項は必ずcanonical formであるという性質であり、canonical formを「計算結果」と考えると,「計算が途中で止まらない」ことを意味する重要な性質である.古典論理に対応する多くの計算体系ではこの性質は成立しないが,プログラム言語と見なした場合にこの性質は極めて重要である.本年度の研究では,制御限定子の持つ型を原始型に制限すればNormal Form Propertyが成立することを示し,また,この制限の範囲内でも,古典論理からのプログラム作成には十分な力があることを示した.この事は,制限された体系がCurry-Howardの同型対応のもとで古典論理に対応することの証明と,Murthyらによる先行研究において,古典論理の証明から抽出されたプログラムでは,制限限定子に相当する部分の型が原始型のみ(実は,矛盾型しか使っていない)であるという観測から導かれた.
|
