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

博弈论和编程语言语义

基本信息

批准号：
08780241
负责人：
赤間陽二
金额：
$ 0.7万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1996
资助国家：
日本
起止时间：
1996 至无数据
项目状态：
已结题

项目摘要

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

今年获得的结果是根据“ lambda-to-clanslation for for Ground归一化的”，λ计算和组合逻辑（组合逻辑）。 λ计算（称为λ部分）到组合逻辑（称为CL截面），并将其用于适用于λ截面的通风的足够的Cl。在这里，第t节满足通风的事实意味着t不能继续无限地简化t。 λ计算具有一个重要因素的函数抽象机制，因此可以轻松表达各种功能，但另一方面，λ计算部分在第一个地板逻辑框架中使用。相比之下，Schoenfinkel将1930年代的组合逻辑设计为设计的转换系统，以便可以以技术更易于处理的第一个逻辑的形式替换功能摘要的功能。根据一项常规研究，已知从λ计算部分到组合逻辑部分的平等性，该部分保留并反映了λ计算和组合逻辑中的特定代码。这项研究中新获得的响应还保留并反映了术语的新正常化。结果是由于对霍华德的讨论进行了详细检查，该讨论通过响应λo的顺序而导致通风的实质。此外，从减去逻辑和部分组合代数的各个方面得出的部分组合之间的关系源自整个有礼貌的λ部分。后者用于证明非常丰富的类型理论的不一致，可以说，由于我们的结果，前者可以用于目的。