|
関数型プログラミングの言語モデルとして、2階線形論理を考える。論理としての側面を無視して、計算体系として考えるとき、不動点演算子は再帰プログラミングをサポートするために必須の構造である。そこで2階線形論理に不動点演算子をつけ加えた体系を考え、その計算体系としての構造を究明するのが目標である。不動点演算子の存在は、構造を豊かにする一方で、モデルの構成を著しく困難にしている。不動点演算子の解釈にまつわる様々な性質を研究対象とした。抽象的な圏論モデルの中での不動点演算子の振る舞いと、実モデルにおける具体的な分析をあわせて行った。圏論モデルにおいては、線形論理のモデルのもつexponential comonadによるcofree coalgebraの作るco-Eilenberg-Moore圏の部分圏上でのトレース演算子から不動点演算子が作られる。以前の研究で行ったトレースの構成は、この観点から自然に再現できるものである。また、具体的な実例として、twinerという新たな数学的概念からモデルを構成することを試みている。この実モデルにおける不動点演算子の解釈の具体的な構造を分析した。数え上げ組合せ論で基本的な道具である母関数とtwinerは直接的な関係がある。このことはまた、数え上げ組合せ論で利用される数学的手法が、モデルの解析に利用できることを示している。この観察を応用して、不動点演算子の構造を調べることができる。その結果として、不動点演算子を解釈するtwinerに付随する母関数が、Cayley関数と呼ばれるベキ級数に対応することがわかった。この関数はLagrangeの逆関数公式を用いて具体的に係数が決定できる典型例にもなっている。このことから、2階不動点演算子の解釈の標準形の個数が決定される。
|
