構成的プログラミングの新局面の研究

1995 Fiscal Year Annual Research Report

• Project/Area Number: 06680333
• Research Institution: Kobe University
• Principal Investigator: 林 晋 神戸大学, 工学部・情報知能工学科, 教授 (40156443)
• Co-Investigator(Kenkyū-buntansha): 小林 聡 龍谷大学, 理工学部・数理情報学科, 助手 (70234820)
• Keywords: 構成的プログラミング / プログラム検証 / プログラム論理

Research Abstract

本年度は、PXの再設計・再実現を行い、新しいPXのversion P2X をほぼ完成するとともに、evaluation modalityについての研究を進めた。
PXはLisp上の基本推論関数の集合として定義され、また、Lisp readerの変更と動的型チェックにより基本推論関数以外は新しいオブジェクトを生産させないようにすることにより証明を安全に構築していた。これをMIZARやICOT-PDLなどと同様に、独自の証明記述言語を設計し、そのインタプリタを実現する方式に改めた。以前の方式は拡張性に優れている半面、マクロの展開が多発するため、エラー発生時にエラーの原因を同定することが困難であった。新しい方式においては、エラーへの対処が極めて的確かつ簡単に行えるようになった。また、P2Xは、AUC-TeX, ispellなどのEMACS環境と類似の使用環境を持ち、これにより構成的プログラミングに不可欠の証明開発の工程が非常に楽に行えるようになった。
また、構成的プログラミングに応用可能で、なおかつできるだけ表現力の高い様相論理を開発するため、A. Pittsのevaluation modalityについて研究した。その結果、Pittsによるもともとのevaluation logicの体系は真に構成的とは言えず、構成的プログラミングに応用するには修正を要することが判明した。そこで修正法を探るうちに、evaluation modalityをnon-informative quantifierの自然な拡張ととらえられることがわかった。これによって、林によるnon-informative quantifierの理論と小林による monadに基づくプログラム抽出の理論が全く自然に融合できることがわかった。

Research Products

• [Publications] S. Hayashi and S. Kobayashi: "A new formalization of Feferman's system of functions and classes and its relation to Frege structure" International Journal of Foundations of Computer Secience. 6. 187-202 (1995)
• [Publications] 小林聡: "Constructive Evaluation Logic" 日本ソフトウェア科学会第12回大会論文集. 97-100 (1995)
• [Publications] 林晋: "プログラム検証論" 共立出版, 208 (1995)