| 研究概要 |
本年度は、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に基づくプログラム抽出の理論が全く自然に融合できることがわかった。
|
