| 研究概要 |
本研究では,プログラムの正しさを保証するための検証システム,および,その検証自体の正しさを保証するメタ理論に関する議論をともに行うことのできるフレームワークの実装に向けて,自然枠組(Natural Framework,NF)の設計と構築を行っている.本年度は,NFを実装するためのプログラミング言語の仕様の詳細化を行った.より具体的には以下のとおりである.
この言語の中核部分で必要となる数学的対象は,それぞれ,ある基本的な「概念」(concept)を満足するものとして特徴づけられるという重要な性質をもつ.すなわち,個々の対象は,対象それ自体でなく,それが満たす固有の概念とともに存在すると考えられる.このような対象を「第一種の数学的対象」と呼び,その対象の集りがつくる数学的構造について研究をした.
今後は,この設計をもとに言語の実装を行い,このプログラミング言語の上でNFを実現することが期待される.
|
