2011 Fiscal Year Annual Research Report
| Project/Area Number |
21700013
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
|
|---|
| Keywords | ラムダ計算 / 型理論 / 多相型 / 型検査問題 / 型推論問題 |
|---|
| Research Abstract |
本研究ではラムダ計算の拡張体系について研究を行い、以下の成果を得た。
1.プログラムが二階量化子に関する型規則の情報を含み、関数の引数型を省略する形式であるドメインフリー形式において、多相型と関数型を含む型付ラムダ計算の型推論問題が決定不能であることを証明した。これは、既に決定不能であることが知られている型検査問題が同体系の型推論問題にチューリング還元可能であることを示すことによって証明した。また、同様のドメインフリー形式における、存在型・組型・継続型を含む型付ラムダ計算における型推論・型検査問題が、多相型・関数型を含む体系の型推論・型検査問題とチューリング還元可能性の意味で同値であることを証明した。この証明には、多相型、存在型を含む体系の間の相互の方向の継続渡し形式変換を利用している。型導出の情報なしで継続渡し形式が定義可能であるのはドメインフリー形式の特徴であり、この形式における体系の型検査・型推論問題についてはこの変換によってチューリング還元可能性の証明が可能であることを示す結果である。
2.ラムダ計算の拡張であるラムダ・ミュー計算に対するモデルとして、ストリーム・モデルを提案した。ストリーム・モデルはラムダ計算に対するラムダ・モデルの拡張となっており、ラムダ・ミュー計算がストリーム計算を表現しているという直観を反映したものになっている。さらに、ストリーム・モデルが、コンビナトリー代数のある拡張であ1る構造によって特徴づけられることを証明した。この拡張は、従来のコンビナトリー代数の関数適用を表す演算とS,K二つのコンビネータに加えて、ストリームに対する関数適用と、ストリームを操作する関数に対応する5つのコンビネータをi自加したものである、
|
