構成的プログラミング・システムの実現

1996 年度 実績報告書

• 研究課題/領域番号: 08558023
• 研究種目: 基盤研究(B)
• 応募区分: 試験
• 研究機関: 京都大学
• 研究代表者: 佐藤 雅彦 京都大学, 工学研究科, 教授 (20027387)
• 研究分担者: 大谷 武 富士通研究所, 研究員 ; 亀山 幸義 京都大学, 工学研究科, 助教授 (10195000) ; 龍田 真 京都大学, 理学研究科, 助教授 (80216994) ; 沢村 一 新潟大学, 工学部, 助教授 (40282991)
• キーワード: 構成的プログラミング / 証明支援システム / グラフィカルユーザインターフェース / 証明エンジン

研究概要

今年度の研究では,構成的プログラミング・システムの作成の基礎となるプログラム言語,および,証明支援システムの2点について検討を行い,プロトタイプシステムを作成した.
まず,関数型プログラム言語Aの処理系の作成を行った.Aは手続き型プログラム言語の特徴である代入文を持ちながら,関数型プログラム言語としての良い性質(参照透明性など)を持つというユニークな言語である.本年度の処理系は,インタープリンタであるが,Aのフルセットが動作し,次年度の構成的プログラミング・システム作成の基礎となるものである.
証明支援システムの作成については,グラフィカルユーザインターフェースを含めた対話型証明作成支援環境を実装した.大規模プログラムの開発を構成的プログラミングの手法で行うためには,証明作成が容易であることともに,モジュール化による分散プログラミング(分散証明)が可能でなければならないという考察をおこない,前者のためにSTk(Scheme+Tkツールキット)およびJAVAにより独立に対話型証明作成支援環境を実装した.
今年度は,証明作成エンジンとして直感主義一階述語論理のものを作成して利用したが,次年度には本格的な証明エンジンにいれかえて大規模プログラミングが可能な構成的プログラミングシステムを作成する予定である.

研究成果

• [文献書誌] Masahiko Sato: "Intutionistic and Classical Natural Deduction Systems with the catch and the throw rules" Theoretical Computer Science. (発表予定).
• [文献書誌] 山中淳彦: "参照透明な代入をもつ純関数型言語" コンピュータ・ソフトウェア. (発表予定).
• [文献書誌] Hajime Sawamura: "Intuitionistic Logic of Music and its Mechanization with the Hol Theorem Prover" Proc.Int'l Conf.on Comp.Music and Music Science. 68-83 (1996)
• [文献書誌] 大谷武: "汎用論証システムEUODHILOS-IIの設計と実装" 情報処理学会論文誌. 38・1. 9-22 (1997)
• [文献書誌] Mitsuru Tada: "The Function [a/m] in Sharply Bounded Arithmetic" Archive for Mathematical Logic. (発表予定).
• [文献書誌] Yukiyoshi Kameyama: "A New Formulation of the Catch/throw Mechanism" Proc.Int'l Workshop on Func.and Logic Programming. 56-64 (1996)