| 研究概要 |
本研究では,プログラムの正しさを保証するための検証システム,および,その検証自体の正しさを保証するメタ理論に関する議諭をともに行うことのできるフレームワークの実装に向けて,自然枠組(Natural Framework, NF>の設計と構築を行っている.本年度は,NFを実装するためのプログラミング言語のプロトタイプの実装を行った.より具体的には以下のとおりである.
この言語の中核部分で必要となる数学的対象は,それぞれ,ある基本的な「概念」(concept)を満足するものとして特徴づけられるという重要な性質をもつ.このような対象を「第一種の数学的対象」と呼び,その対象の集りがつくる数学的構造についての研究を前年度に引き続き研究した.このような対象の多くは,単射的な帰納的定義により比較的容易に構築することができる.しかしながら,命題や証明を第一種の数学的対象として構築するのには単射的でない帰納的定義が必要になる.今年度は,命題や証明同士の等しさが決定可能であるという基本性質を満足した上で.これらを第一種の数学的対象として定義することに成功した.
今後は,この設計をもとに言語の実装を行い,このプログラミング言語の上でNFを実現することが期待される.
|
