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

1997 Fiscal Year Annual Research Report

• Project/Area Number: 08558023
• Research Institution: KYOTO UNIVERSITY
• Principal Investigator: 佐藤 雅彦 京都大学, 工学研究科, 教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): 大谷 武 (株)富士通研究所, 研究員 ; 竹内 泉 新潟大学, 工学研究科, 助手 (20264583) ; 沢村 一 新潟大学, 工学部, 助教授 (40282991) ; 亀山 幸義 京都大学, 工学研究科, 助教授 (10195000) ; 龍田 真 京都大学, 理学研究科, 助教授 (80216994)
• Keywords: 構成的プログラミング / 古典論理 / 様相論理 / 証明支援システム

Research Abstract

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

Research Products

• [Publications] Masahiko Sato: "Classical Brouner-Heyting-Kolmogorov Interpretation" Lecture Notes in Artificial Intelligence. 1316. 176-196 (1997)
• [Publications] Makoto Tatsuta: "Realizability for Constructive theory of Functions and Classes and its Application to Program Synthesis" Proc.13th IEEE Symp.on Logic in Computer Science. 13. (1998)
• [Publications] Yukiyoshi Kameyama: "A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability" Proc.4th Australasian Theory Symposium. 20-3. 183-197 (1998)
• [Publications] Izumi Takeuti: "An Axiomatic System of Parametricity" Lecture Notes in Computer Science. 1210. 354-372 (1997)
• [Publications] 沢村 一: "エイジェント指向コンピューティングのための計算倫理学に向けて-公平性-" ソフトウェア工学の基礎IV. IV. 28-34 (1997)
• [Publications] 大谷 武: "汎用論証支援システムEUQDHILOS-IIの設計と実装" 情報処理学会論文誌. 38-1. 9-22 (1997)