|
本研究の目的は、従来、PER model、categorical modelなどの意味論的枠組みの中だけで議論されてきた多相型のparmetricityを、意味論なしで、形式的理論のadmissible ruleを使って表現することを試みることにある。
これを具体的に言えば「FefermanのT_0や、直観主義的集合論などの構成的形式系において定義可能な関数は、それが、すべての型Xに対して、Xからの入力aに対して、Xの値を返すものであれば、X→Xの恒等関数しかない」という定理を、一般の多相型に拡張することである。
今年度は、上記の特殊な型の場合の定理の証明の細部を完成させることに専念した。その証明のkeyとなるアイデアは、一般には項が値をもたないlogic of partial termsにおいて、subtermの値の存在を保証するために、わざと冗長なconstructionを型に置くという方法である。そして、その方法を使いつつ、実現子として、二つの項を準備し、それらを連動して動かすことにより、実際の計算を担う項は極力冗長性を削ぎながら、もう一方は論理的性質を保証する冗長性を持たせるという、矛盾した要請を実現することができることを示した。このように新しいdoubling realizabilityの理論の細部を完成させたが、この方法を一般のシステムの場合に拡張するまでにはいたらなかった。これは来年度以後の課題としたい。
|
