| 研究概要 |
本研究は何年かに渡って継続して行っているが,その最終的な目標は数学を形式的に記述するための体系を構築することであり,そのためにいくつかの層に分けて理論を構築している.一番上のレベルである数学(特に論理および計算)の理論は導出ゲームという形で記述し,その導出ゲームは判断と導出の理論という枠組の中で定義されている.そしてその判断と導出の理論は単純表現理論という理論を使って定義されている.これらの理論は計算機上でemacs lispを使ってインプリメントしており,単純表現理論はCAL,判断と導出の理論はNF(Natural Framework)というシステムとして実現している.
これらを実際に使用した経験を基にして,本年度は単純表現理論を改良し,判断と導出の理論を再構築した.単純表現理論は抽象操作と具体化操作を備えた構造を持っているが,具体化操作は束縛変数の名前替えなしで行なわれ,環境の概念を拡張することによりその操作を簡潔に定義できることが特徴となっている.またこの単純表現理論はアリティという概念を持っているが,本年度は,それをさらに改良し,カテゴリーという概念を導入した.アリティは引数の個数を高階にしたものに相当する概念であるが,カテゴリーは引数の種類を高階にしたものに相当する概念であり,より豊富な数学の概念を表現できるようになった.
また,単純表現理論をさらに拡張するときには,明示的代入を導入するのが自然である.しかし,明示的代入を有効に活用するには従来の合成規則では不十分であるので,明示的代入の合成規則を拡張する研究も行ない,これまでの合成規則ではできなかったメタレベルでの代入が体系内で実現でき,その強正規化性も証明した.
|
