ゲーム理論とプログラム言語の意味論

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

本年度は得られた成果は次の題の論文としてまとめられている."A Lambda-to-CL Translation for Strong Normalization"では,λ計算と組合せ論理(combinatory logic)という簡約系の項の強正規化性という性質に着目し,λ計算の項(λ項と呼ぶ)から組合せ論理の項(CL項と呼ぶ)への新しい対応を定義し、それを使ってλ項の強正規性を適当なCL項の強正規性に還元する新しい方法を示した。ここで、項tが強正規化性を満たすとは,tを無限回、簡約し続けることができないということである。λ計算は、その重要な要素として関数抽象の機構を持っているため、いろいろな関数を容易に表現することができるが、その反面、1階述語論理の枠組でλ計算の項をそのまま扱うことはできない。これに対して、技術的により扱いやすい1階述語論理の項の形で、関数抽象の機能を巧みに代用できるよう工夫された変換系として、Schoenfinkelが組合せ論理を1930年台に考案している。従来までの研究により、λ計算・組合せ論理に特有な符号を保存・反映するような、λ計算の項から組合せ論理の項への対等が知られていた。本研究で新しく得られた対応は、加えて、新たに、項の強正正規化をも保存・反映する。この結果は、λ項にεoまでの順序数を対応させることによってその強正規性導くHowardの議論を子細に検討した結果得られたもので、これによってλ項、CL項、及び順序数の間に、これまでより見通しの良い関係が確立されたことになる。また、強正規な組合せ論理の項全体から導かれる部分組合せ代数と、強正規なλ項全体から導かれる部分組合せ代数との関係を調べた。後者は、表現力が極めて豊かな型理論の無矛盾性を証明するのに使われるものであり、われわれの結果により、前者もその目的に使えることが言える。