多相型ラムダ計算の構造とその数学的特徴付けの研究

不動点演算子を持つ多相型線型ラムダ計算は、不動点演算子を持つ多相型ラムダ計算の重要なメタ言語である。Girardによって研究がはじめられた相互作用の幾何学(Geometry of Interaction)は多相型線型ラムダ計算の意味論の一つである。相互作用の幾何学は、多くの言語に対しての完全抽象性を満たす意味論を与えているゲーム意味論との類似性がある一方で、その圏論的背景がゲーム意味論に比べてよく研究されている。平成22年度はこの相互作用の幾何学の不動点演算子を持つ多相型線型ラムダ計算の意味論としての側面の研究を行った。相互作用の幾何学による不動点演算子の解釈に関する研究はGirardによるものとHackieによるものの二つがあるが、いずれも与えた解釈が適切性(adequacy)を満たすかについての議論を行っていない。適切性を満たす意味論は、ラムダ計算の性質を調べる上で非常に強力な道具である。本研究者は標準的な相互作用の幾何学が不動点演算子をもつ多相型線型ラムダ計算に対して適切性を満たさないことを指摘し、その問題を実現可能性解釈を用いることで解決した。まず相互作用の幾何学から構成されるlinear combinatory algebraといわれる代数を用いて実現可能性解釈から多相型線型ラムダ計算の圏論的意味論を構成しその適切性を証明した。この圏論的意味論から相互作用の幾何学の多相型線型ラムダ計算に対する新たな解釈を与えた。ここで与えた新たな解釈が適切性を満たす事は実現可能性解釈から構成した圏論的意味論の適切性から従う。この研究で用いた手法は他のラムダ計算に対しても適用可能なものである。

不動点演算子を持つ多相型線型ラムダ計算は、不動点演算子を持つ多相型ラムダ計算の重要なメタ言語である。Girardによって研究がはじめられた相互作用の幾何学(Geometry of Interaction)は多相型線型ラムダ計算の意味論の一つである。相互作用の幾何学は、多くの言語に対しての完全抽象性を満たす意味論を与えているゲーム意味論との類似性がある一方で、その圏論的背景がゲーム意味論に比べてよく研究されている。平成22年度はこの相互作用の幾何学の不動点演算子を持つ多相型線型ラムダ計算の意味論としての側面の研究を行った。相互作用の幾何学による不動点演算子の解釈に関する研究はGirardによるものとHackieによるものの二つがあるが、いずれも与えた解釈が適切性(adequacy)を満たすかについての議論を行っていない。適切性を満たす意味論は、ラムダ計算の性質を調べる上で非常に強力な道具である。本研究者は標準的な相互作用の幾何学が不動点演算子をもつ多相型線型ラムダ計算に対して適切性を満たさないことを指摘し、その問題を実現可能性解釈を用いることで解決した。まず相互作用の幾何学から構成されるlinear combinatory algebraといわれる代数を用いて実現可能性解釈から多相型線型ラムダ計算の圏論的意味論を構成しその適切性を証明した。この圏論的意味論から相互作用の幾何学の多相型線型ラムダ計算に対する新たな解釈を与えた。ここで与えた新たな解釈が適切性を満たす事は実現可能性解釈から構成した圏論的意味論の適切性から従う。この研究で用いた手法は他のラムダ計算に対しても適用可能なものである。