parametric polymorphismの新しい枠組

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12878049
• Research Institution: Kobe University
• Principal Investigator: 林 晋 神戸大学, 工学部, 教授 (40156443)
• Keywords: 多相型 / admissible rule

Research Abstract

本研究の目的は、従来、PER model、categorical modelなどの意味論的枠組みの中だけで議論されてきた多相型のparametricityを、意味論なしで、形式的理論のadmissible ruleを使って表現することを試みることにある。
これを具体的に言えば「FefermanのT_oや、直観主義的集合論などの構成的形式系において定義可能な関数は、それが、すべての型Xに対して、Xからの入力aに対して、Xの値を返すものであれば、X→Xの恒等関数しかない」という定理を、一般の多相型に拡張することである。
昨年度はT_o系列の形式的体系について、上記の特殊な型の場合の定理の証明の細部を完成させたが、それにはT_o独特の形式的体系の特徴である「型(クラス)も、データである」という機能が使われていた。本年度は、これを一般の2階論理に拡張することを試みた。この場合、実は第一に問題になるのは、一般の2階論理では、むしろparametricであることが自明であり、林がparametricでない型システムの特徴として使った、「特殊な型の場合にのみ、関数を変える」というadhoc polymorphismを実現し難いという点にある。つまり、parametricという特徴を表現することが難しいのであるが、これは林が現在開発中のLCM理論における弱い排中律を導入することにより、「型が、1,2を含めば値をスワップ、そうでない値に対しては、恒等関数」という関数などの存在を許す形式系を作れることが分った。しかし、その形式系では、full comprehensionがなり立たない。この問題は、まだ、解決できていないが、LCM理論と再帰的関数論により、Fefermanのpredicative polymorphismは実現可能と予想して研究を進めている。