1997 Fiscal Year Annual Research Report
| Project/Area Number |
08680367
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| Keywords | プログラム検証 / プログラム合成 / 形式的技法 |
|---|
| Research Abstract |
本研究の当初計画では型のない関数型言語にもとづくPX systemそのものにBerardiの方法を適用する予定であったが、これはうまく行かなかった。これは、もともと、型理論に基づく方法を型の無い理論に強引に適用しようという計画であったので、本来無理があったのかもしれない。
そのため、第1年度より計画を変更し、PX systemの抜本的な再設計・再構築という道を選んだ。すなわち、Berardiの方法がそのまま適用できるように、Px自体をその基礎論理システムから再構築したのである。
この計画変更により、プログラム抽出部分と最適化部分を完全に独立したモジュールとしてもつシステムを構築することが可能となり、PX systemのad,hocな最適化の置換えと拡張という最終目標は、当初計画以上の成果を得ることができた。
また、本研究の研究途上、林は構成的プログラミングの全く新しい応用である“証明アニメーション"という構想を提唱した。このアイデアは、構成的プログラミングという大きなコンテキストののなかで得られたものであり、本研究の具体的研究計画の枠組を超えるものである。
しかし、このアイデアは本研究の具体的成果の一つとして得られたものであり、また、長期的展望にたてば、本来の研究計画の達成により、この新知見の方が遥かに大きな影響力を持つと予想される。
|
-
[Publications] Susumu Hayashi: "Constructive Programming -a personal view-" Combinatorics,Complexity,Logic,Proceedings of DMTCS '96,Springer-Verlag,Singapore. 38-51 (1996)
