| 研究概要 |
本年度は,平成15年度の研究で提案した表現の理論をさらに改良した.
表現の理論は抽象操作と具体化操作を備えた構造を持っているが,その新しい点は、具体化操作は束縛変数の名前替えなしで行なわれるということである.この性質により,α同値性を変数の名前替えに依存しないで定義することが可能になり,α同値性の決定可能性の証明は非常に単純になった.通常の名前付き変数と束縛子を持った表現のシステムでは,自由変数の捕捉を避けるために局所変数を名前替えする必要があるが,我々のシステムでは,その外にある任意の変数を参照できるように変数参照の機構を導入したのである.以前の研究でも同様の機構を導入したが,環境の概念を拡張することにより,その定義を簡単化することができた.
この表現の理論を用いて,以前の研究で導入した判断と導出の理論を再構築した.この理論はNatural Framework (NF)の基礎となり,導出ゲームを用いて様々な数学的体系を定義することができた.以前の表現の理論はアリティの概念を持っていなかったので現在のものより単純である.しかし,以前の理論では導出ゲームを理論の対象物として定義することができなかったが,現在の理論では導出ゲームの規則を閉じた表現によって定義することが可能になっている.
以上の成果については,論文"A Simple Theory of Judgments and Derivations"で発表した.
さらに,明示的代入計算や部分計算への応用についても研究を行なった.
|
