| 研究概要 |
本年度は,本研究を通して目的としている自然枠組(Natural Framework, NF)の構築に向けて,NFの基礎となる「式の理論」を与えるために、抽象(abstraction)操作について考察した.
数学を形式的に記述するときに変数による抽象操作は必須となる基本的な操作である.この操作は,与えられた変数xと表現Mから,表現abs(x, M)を構成する操作であり,その結果はMのxによる抽象と呼ばれる.この操作の「逆操作」は具体化(instantiation)と呼ばれ,抽象Aを表現Nで具体化した結果はinst(A,N)と書かれる.抽象と具体化の間には以下の関係がある:
Inst(abs(x,M),N)=[N/x]M.
本研究では,これらの性質をもつ抽象操作を実現する具体的な新しい方法を提案した.この手法はNFの「式の理論」に組み込まれ,NFにおける抽象操作の理論的基盤を与えることが期待されるが,本手法自体はNFに限らない,一般の抽象操作を表現できるものである.
|
