Research Project
Grant-in-Aid for Exploratory Research
本研究の目的は、従来、PER model、categorical modelなどの意味論的枠組みの中だけで議論されてきた多相型のparametricityを、意味論なしで、形式的理論のadmissible ruleを使って表現することを試みることにあった。これを具体的に言えば「FefermanのT_0や、直観主義的集合論などの構成的形式系において定義可能な関数は、それが、すべての型Xに対して、Xからの入力αに対して、Xの値を返すものであれば、X→Xの恒等関数しかない」という定理を、一般の多相型に拡張することであったが、残念ながら、最終年度の今年度も、この拡張は達成できなかった。本年度の成果としては、この定理の特殊な場合の証明を与えるdoubling realizability interpretationの洗練と拡張がある。このinterpretationは、研究開始当初、それによって上記予想が解決できると期待されたものである。このrealizability interpretationは、実効値と意味値を並行に持って走るため、色々と面白い応用を持つものである。しかし、上記の目的を達成するためには充分でなかったのかもしれない。当初の計画では、このrealizability interpretationの持つ、性格を分析すれば、一般的型の、parametricityが得られるものを期待したが、実際には、それは困難であった。realizabilityは、高階型をサポートはするものの、本質的には1階の性格がつよい。多相型のparametoricityは1階的概念であると当初は予想していたが、実はX→Xのparametricityなどを除き、それは高階の要素が強い概念であったのかもしれない。今回の萌芽的研究は終了するが、今後も、引き続きLCMの技法なども援用して、この問題にアタックを続けたい。
