| 研究分担者 |
大谷 武 (株)富士通研究所, 研究員
竹内 泉 新潟大学, 工学研究科, 助手 (20264583)
沢村 一 新潟大学, 工学部, 助教授 (40282991)
亀山 幸義 京都大学, 工学研究科, 助教授 (10195000)
龍田 真 京都大学, 理学研究科, 助教授 (80216994)
|
|---|
| 研究概要 |
今年度の研究は2年計画の最終年度であり,構成的プログラミングの実用化へ向けて,(i)多様な論理体系への対応と証明戦略の検討,(ii)古典論理を用いた構成的プログラミング,という2点について研究し,プロトタイプシステムを作成した.
まず,直観主義論理/古典論理/各種の様相論理(T,S4,S5,Bなど)といった多様な論理体系に対応した証明支援システムを作成した.前年度は,直観主義一階述語論理という特定の論理体系を対象にして,グラフィカル・ユーザインターフェイスを重視した対話的環境を構築したが,本年度は,多様な論理体系への対応,及び個々の論理体系に依存しない共通した証明戦略の構築を目的としたソフトウェアを作成した.これらは,前年度に引き続き,STk(Scheme+Tkツールキット)およびJAVAを用いて実装した.
さらに,構成的プログラミングの手法における最新の話題として,古典論理の証明からのアルゴリズム抽出を関して2種類の異なるアプローチから研究し,計算機上に実装した.具体的には,catch/throw機構を導入した型付ラムダ計算の体系に基づいた算術の体系PA_<c/t>のシステムを実装し,このシステム上での古典論理の証明の構築,アルゴリズムの抽出をおこなった.一方,継続計算の型理論的解釈に基づいたシステムにおいても古典論理の証明からのアルゴリズム抽出が行えることが知られており,これを多相型を持つMLの型体系に基づいて実装した.
これらの研究成果およびソフトウェアにより,構成的プログラミングの適用範囲が従来より広がり,より実用的な構成的プログラミング・システムの実現に向けての一歩となることができた.
|
