| 研究概要 |
変換系であるところのさまざまなλ計算に対して、その項から組合せ論理の項への翻訳があり、その翻訳が項の強正規性を保存し反映することが知られている(e.g.[Akama,A Lambda-to-CL Translation for strong Normalization,1996])。それらのλ計算の強正規な項全体を特徴づけるために、組合せ論理の強正規な項全体が交型理論を用いて特徴づけた[Akama,SN combinators and Partial Combinatory Algebras 1998]。この交型理論のモデルとして、高階型理論・値呼び出しのλ計算のモデルを生成することが知られている、部分組合せ代数を選び、部分組合せ代数全体のクラスに対する完全性を証明した。ここで、部分組合せ代数はため重要である。また、この交型理論の正準的なモデルにより、ある部分組合せ代数のfinal collapseを表現できることを証明した。
本年度の2番目の結果としては、プログラミング言語Schemeのプリミティブthe-environmentを抽象した変換系で西崎が導入したλenvに着目した。
CurienやAbadiたちが導入した代入明示なλ計算と異なり、環境を一級市民として扱い項と同じソ-トである。このthe-environmentを使うとデバッガが容易に書けることが知られている。我々は、λenvの変換系としての性質(合流性など)を証明し、外延的な意味を型なしλ計算への翻訳を介して与えた。そこでは、環境は、変数の「名前」をもらうとその変数に束縛されている項を返す関数に翻訳される。型なしλ計算は計算力を十分持つためこの翻訳の計算量は無視可能であり、自然な意味論となっている。
|
