ポリモルフィズムの数学的構造

点击翻译按钮获取中文摘要

線形パラメトリシティを公理としてもつ体系と,その実現可能性解釈の開発を試みた.Reynoldsは1980年代に,ポリモルフィックなプログラミング言語に対して,パラメトリシティと呼ばれる概念を提唱した.線形パラメトリシティは,二階線形論理に対してこの概念を適用しようという試みである.パラメトリシティ原理を公理として仮定することの意味は,そこから再帰的データ型の存在が導かれることにある.1990年代に,高階の型付きラムダ計算に対するパラメトリシティ原理が盛んに研究されたのはこのような事情からであった.しかし,型付きラムダ計算に対するパラメトリシティ原理は,不動点演算子の存在と矛盾する.不動点演算子は,再帰的プログラミングに対応し,現実のプログラミング言語には存在するべきものであるが,これと矛盾してしまうのは,ある意味パラメトリシティ原理のもつ大きな欠点といえよう.われわれは,この原理を少し弱めた線形パラメトリシティ原理を考え,この矛盾を回避できることを主張した.具体的には,二階線形論理のモデルで,不動点演算子を持ち,さらに線形パラメトリシティと呼ぶにふさわしい性質を持つものを開発した.さらに,このモデルの性質を調べ,それが満たす線形パラメトリシティ原理を体系化しようと試みている.現在まだ完成はしていないが,その体系は次のような性質を満たすはずであることは分かっている.再帰的なデータ型の存在が,線形パラメトリシティというやや弱い原理からでも導かれること.不動点演算子の存在とあわせることによって,負の位置にパラメータが現れるような,一般的な再帰的データ型の存在も導出できること.始代数と終代数の一致が導け,これによりhylomorphismと呼ばれるプログラム変換の技法が自由に適用できるようになることである.