解析関手と理論計算機科学

ラムダ計算の不動点演算子と,解析や数え上げ組み合わせ論に現れるLagroge-Goodの公式との,関連を調べた.この公式は,形式的幕級数の逆関数を計算するときや,木構造の数え上げの問題などに用いられる式で,ある種の不動点を計算するものである.また,ラムダ計算の不動点演算子は,再帰的呼び出しをもつ関数プログラムをラムダ計算の中で表現するのに用いられる.本年の研究では,ラムダ計算のモデル論を用いて,Lagrange-Goodの公式の別証を与えることを行った.既存の証明としては,留数を用いたものや,数え上げ組み合わせ論を用いたものが知られているが,今回の結果は,まったく異なったアプローチによっていて,理論計算機科学の中で得られた結果を用いている.特に,最近知られるようになった,ラムダ計算の不動点演算子と,トレースとの関係を有効に用いている.この研究の意義は,理論計算機科学と,解析学や数え上げ組み合わせ論というまったく異なる分野に現れる不動点が密接に結びついていることを示した点にあるといえよう.これらを結びつけるのに用いた道具が解析関手である.この結果は,1998年8月にチェコ共和国のBrnoで開かれた国際会議Fixpointsin Computer Scienceで発表された.また,1999年1月に京都大学でひらかれた短期共同研究「二階算術の諸体系の研究」で,詳細な解説を行った.前年の成果とあわせて書かれた論文が,Theoretical Computer Science誌に投稿中である.

ラムダ計算の不動点演算子と,解析や数え上げ組み合わせ論に現れるLagroge-Goodの公式との,関連を調べた.この公式は,形式的幕級数の逆関数を計算するときや,木構造の数え上げの問題などに用いられる式で,ある種の不動点を計算するものである.また,ラムダ計算の不動点演算子は,再帰的呼び出しをもつ関数プログラムをラムダ計算の中で表現するのに用いられる.本年の研究では,ラムダ計算のモデル論を用いて,Lagrange-Goodの公式の別証を与えることを行った.既存の証明としては,留数を用いたものや,数え上げ組み合わせ論を用いたものが知られているが,今回の結果は,まったく異なったアプローチによっていて,理論計算機科学の中で得られた結果を用いている.特に,最近知られるようになった,ラムダ計算の不動点演算子と,トレースとの関係を有効に用いている.この研究の意義は,理論計算機科学と,解析学や数え上げ組み合わせ論というまったく異なる分野に現れる不動点が密接に結びついていることを示した点にあるといえよう.これらを結びつけるのに用いた道具が解析関手である.この結果は,1998年8月にチェコ共和国のBrnoで開かれた国際会議Fixpointsin Computer Scienceで発表された.また,1999年1月に京都大学でひらかれた短期共同研究「二階算術の諸体系の研究」で,詳細な解説を行った.前年の成果とあわせて書かれた論文が,Theoretical Computer Science誌に投稿中である.