限定継続の計算系と論理

2001 Fiscal Year Annual Research Report

• Project/Area Number: 13680411
• Research Institution: University of Tsukuba
• Principal Investigator: 亀山 幸義 筑波大学, 電子・情報工学系, 助教授 (10195000)
• Keywords: コントロール・オペレータ / カリー・ハワードの対応 / 古典論理 / 型理論 / 関数型プログラム言語 / 限定継続

Research Abstract

制御演算子(コントロール・オペレータ)を持つ計算系を型理論および論理の視点から観察することにより,その妥当な定式化や意味についての理論を展開することが我々の研究の目標である.その理論に基づき,仕様を表す論理式が与えられた時,その仕様を満たす,制御演算子を持つ関数型プログラムを作成するという手法へ応用することも目標である.本研究では,control delimiter(制御限定子)を持つ継続の体系,すなわち,限定継続の制御演算子の妥当な定式化を目的としている.特に,従来の我々の研究では静的な限定継続の制御演算子を対象としていたが,より簡便なCPS意味論を持ち広く応用されている動的な限定継続の制御演算子を定式化することが本研究の課題である.そのため,本年度は,限定継続より簡単な制御演算子である「例外」機構を取りあげ,動的な例外機構を論理の枠組みで定式化する事について検討し,以下の成果を得た.動的な例外機構は,カリー・ハワードの同型対応に基づく従来の理論ではうまく定式化ができず,従って論理体系との対応も存在しなかった.しかし,関数型A→Bに,例外型の集合を添付した型を新たに導入することにより,静的な型システムで定式化可能である.この定式化は極めて素直なアイディアに基づくものであるが,ML言語の例外機構にもよく対応し,動的制御演算子の定式化として妥当なものである.また,既に知られている中野のキャッチ・スローの体系の定式化への変換も簡単に与えられる.本研究では,この型システムと動的意味論のもとで体系の性質を調べ,型の健全性,合流性,強正規化可能性,正規形に関する性質など種々の性質が全て成立することを示した.

Research Products

• [Publications] Yukiyoshi Kameyama: "Strong Normalizability of the Non-deterministic Catch/Throw Calculi"Theoretical Computer Science. 272:1-2. 223-245 (2002)
• [Publications] Yukiyoshi Kameyama: "Dynamic Control Operators in Type Theory"Proc. Second Asian Workshop on Programming Languages and Systems. 1-11 (2001)
• [Publications] A. A. Taha, M. Sato, Y. Kameyama: "A Second Order Context Caculus"Computer Software. 3月号(発表予定). (2002)