| 研究概要 |
存在型を含むラムダ計算における型付け問題について考察し,以下の結果を得た.
型付け問題には,与えられた項が与えられた型を持つか否かを判定する「型検査問題」(Type Checking, TC)と,与えられた項が何らかの型を持つか否かを検査する「型付け可能性問題」(Type Inferece, TI)がある.本研究ではドメインフリー(Domain Free)と呼ばれる形式化における,存在型と関数型を含むラムダ計算の体系,および,存在型と組型と継続型を持つラムダ計算の体系について考察を行なった.これらの体系におけるTCとTIが決定不可能であることは本研究代表者によって既に証明されていたが,本研究では新たに,それぞれの体系においてTCとTIが同値であることを証明したここで,二つの決定問題のクラスが同値であるとは,各問題のクラスがもう一方にTuring還元可能であること,すなわち,各問題のインスタンスをもう一方の問題の同値なインスタンスに変換する計算可能関数が(両方向に)存在することを言う.
また,この結果は存在型を含むラムダ計算における型付け可能性問題の決定不可能性に対する新たな証明を与える.
|
