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

1997 Fiscal Year Annual Research Report

• Project/Area Number: 09780266
• Research Institution: Kyoto University
• Principal Investigator: 亀山 幸義 京都大学, 大学院・工学研究科, 助教授 (10195000)
• Keywords: キャッチ・スロー機構 / 構成的プログラミング / 古典論理 / 強正規化可能性

Research Abstract

関数型プログラミング言語におけるキャッチスロー機構は,実行時におけるエラー処理など,非局所脱出の機構として有用なものである.キャッチスロー機構に対する型理論的解釈としては、中野のL_<c/t>という体系がある.本研究では、L_<c/t>におけるラムダ抽象導入時の制限をはずした体系LK_<c/t>を提案し,この体系が古典論理と対応することを示した.L_<c/t>が直観主義論理に対応し,従来型のプログラミング例題のみを与えるのに対し,古典論理に対応するLK_<c/t>は表現力の点で大幅に拡張されていることを示した.具体的には,論理積・論理和などの論理記号を定義できること,高階関数においてキャッチスロー機構を自由に使うことができること,および,Murthyらによる古典的証明からの計算的意味の抽出例題が記述できること,の3点を示した.特に重要な点は,Parigotのλμ計算系や継続を定式化した計算系に比べて計算能力が弱いとされていたキャッチスロー機構でも,古典的証明からの計算的意味の抽出が十分に可能であることを示したことである.
このほか,体系LK_<c/t>の性質の解析も行い,型の健全性や強正規化可能性などの望ましい性質が成立することを証明した.この種の体系の強正規化可能性はこれまで解決されていなかったが,LK_<c/t>に欠けていた除去規則を加える手法により肯定的に解決した.この手法は,キャッチスローおよびタグの抽象化を持つ体系に対して一般的に通用するものであり,たとえば,佐藤のNK_<c/t>の強正規化可能性の証明にも適用できることを示した.

Research Products

• [Publications] 亀山 幸義: "Control Delimiterと Full Functional Jumpの計算系" 日本ソフトウェア科学会第14回大会論文集. 14. 281-284 (1997)
• [Publications] Yukiyoshi Kameyama: "Strong Normalizability of Classical Catch/Throw Calculus" RIMS Kokyuroku,Kyoto University. 1023. 42-56 (1998)
• [Publications] Yukiyoshi Kameyama: "A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability" Proc.4th Australasian Theory Symposium,Springer. 20-3. 183-197 (1998)