| 研究概要 |
本研究では存在型を含む型付きラムダ計算の型検査問題に関する研究を行い,以下の結果を得た.
1.ドメインフリー形式において,存在型と関数型を含むラムダ計算の型検査問題と型推論問題が,多相型ラムダ計算の問題にチューリング還元可能であることを証明した.証明はCPS変換を用いて,存在型の体系における型判断に対してそれと同値であるような多相型ラムダ計算における型判断が得られることを示すことによって行った.
2.ドメインフリー形式において,存在型と組型,継続型を含むラムダ計算の型検査問題が,多相型ラムダ計算の問題にチューリング還元可能であることを証明した.証明は1.と同様,CPS変換を用いた手法であるが,1.の場合の単純な応用では困難であるため,適当な型定数と項定数を導入することによって証明した.このため,この手法では型推論問題のチューリング還元可能性を直接証明できない.
3.以上の結果と,本研究の昨年度までの成果を含めた既存の結果と合わせることにより,ドメインフリー形式における三つの体系,存在型と関数型を含むラムダ計算,存在型と組型,継続型を含むラムダ計算,多相型ラムダ計算における型検査問題と型推論問題の計六つの問題が全て互いにチューリング同値であることが導かれる.
|
