構成的プログラミングを実現する証明、検証、合成システム

1995 Fiscal Year Annual Research Report

• Project/Area Number: 06452387
• Research Institution: KYOTO UNIVERSITY
• Principal Investigator: 佐藤 雅彦 京都大学, 工学研究科, 教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): 龍田 真 東北大学, 電気通信研究所, 助教授 (80216994)
• Keywords: 構成的プログラミング / 構成的論理 / 証明システム / 関数型プロゲーム言語 / 代入文 / 遅延評価

Research Abstract

本研究の目的は,構成的プログラミングの基礎理論に関する理論的研究を深化させるとともに,構成的プログラミングを実現するための証明、検証、合成システムの試作システムを作成することである.このために,本研究では、関数型プログラミング言語Λの設計を行い,また,論理体系RPTの研究を深化させることを行った.本年度の研究では,特に,プログラミング言語Λの設計を通じて,いわゆるCatch/Throw機構を関数型言語に取りこむ事について検討した.Catch/Throw機構は,プログラムの実用上有用な機構であるが,論理的意味付けは,これまで,シーケント計算に基づくいくつかの研究があるだけであった.本研究では,既存の研究とは異なり,Catch/Throw機構が論理概念の拡張を伴わず,同じ論理概念に対する効率良い実行機構であることを示した.具体的には,直観主義命題論理の自然演繹体系にいくつかの規則を追加した簡単な体系を提案し,この拡張が保存的拡張であることを示した.また,この体系の証明図に対する簡約化を定義し,Curry-Howard同型対応に基づいて,証明図の簡約化から自然に定義されるプログラム言語が,Catch/Throw機構を含む関数型プログラム言語となっていることを示した.また,本研究で提案したCatch/Throw機構に対応する論理体系の強正規化可能性を証明した.この証明で用いた手法を用いて,過去に提案されていた体系の強正規化可能性の証明も簡潔に行えることを示した.

Research Products

• [Publications] 佐藤雅彦: "自己反映的証明体系RPTの理論と実現" コンピュータソフトウェア. 12-2. 32-51 (1995)
• [Publications] Masahiko Sato: "A Nootural Deduction System with Catch/Throw Rules" The Secerd Worksop on Starlard Logic and Cogical Aspects of Computpr Science. (1995)