|
関数型プログラミングの言語モデルとして、2階の直観主義線形理論を考える。論理としての側面をとりあえず無視し、計算体系として考えるとき、不動点演算子は再帰的プログラミングをサポートするためにも必須の構造である。そこで不動点演算子を付け加えた体系を考え、その構造を明らかにすることが目標である。そのような演算子の存在は、構造を豊かにする一方で、モデルの構築を著しく難しいものにしている。われわれはtwinerと呼ばれる数学的概念を用いて、上記体系のモデルすなわち表示的意味論を構築する試みを続けている。Twinerはわれわれによって導入された新しい概念であり、それを用いたモデルが課題名にある組合せ論的数え上げモデルである。この名前は、数え上げ組合せ論で基本的な道具である母関数とtwinerが密接な関連をもつことからつけられた。このことはまた、数え上げ組合せ論で知られた数学的技法が、モデルの解析に利用できることを意味している。この観察を利用し、モデルの中での不動点演算子の解釈を詳細に解析した。2階の不動点演算子の解釈は上に述べたtwinerの構造を持つが、そこから対応する母関数を得ることができる。その結果得られた母関数は、ちょうどCayley関数と呼ばれる冪級数に対応していることがわかった。これは木の数え上げに現れる最も基本的な母関数であり、Lagrangeの逆関数公式を用いて具体的に係数が求められる典型的な例にもなっている。このことを用いて、不動点演算子の解釈の標準形の個数が決定され、その構造が完全に決定される。
|
