| 研究概要 |
本研究では,プログラムの正しさを保証するための検証システム,および,その検証自体の正しさを保証するメタ理論に関する議論をともに行なうことができるフレームワークの実装に向けて,自然枠組(Natural Framework, NF)の設計と構築を行なっているが,本年度は,NFを実装するためのプログラミング言語の設計を行なった.より具体的には以下のとおりである.
昨年度までに,NFのための理論的基盤を与えるために,とくにその構文論的基礎を与える式の理論に関する考察を行なってきたが,本年度はこの中で得られた知見をもとに,NFをコンピュータ上で実現するためのプログラミング言語設計を行なった.この言語の中核部分で必要となる数学的対象は,それぞれ,ある基本的な「概念」(concept)を満足するものとして特徴づけられ,そのため抽象化の操作を必要としない帰納的な記号操作でこれらの数学的対象が構成できることを示した.
今後は,この設計をもとに実装を行ない,このプログラミング言語の上でNFを実現し,プログラム検証およびそのメタ理論に関する議論をコンピュータ上の同じ枠組みで行なえる環境が構築されることが期待される.
|
