コントロール・オペレータの計算系とプログラム合成

1999 Fiscal Year Annual Research Report

• Project/Area Number: 11780213
• Research Institution: Kyoto University
• Principal Investigator: 亀山 幸義 京都大学, 大学院・情報学研究科, 助教授 (10195000)
• Keywords: コントロール・オペレータ / 古典論理 / プログラム合成

Research Abstract

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

Research Products

• [Publications] Y.Kameyama: "A Type System for Delimited Continuations"Proc.Workshop on Prog and Prog Lang.. (発表予定). (2000)
• [Publications] Furusawa,Kameyama et al.: "On Soundness and Completeness of Simulations wrt Refinement"Proc.Workshop on Refinement&Abstraction. (発表予定). (2000)