|
本研究では、多相型や存在型を含む型付きラムダ計算における型検査問題や型推論問題の決定可能性について考察し、それらが多くの形式化において決定不能であることを証明した。
論理における二階存在量化子に対応する存在型は、二階普遍量化子に対応する多相型の双対概念であり、それらの間の関係は証明の対称性の形で藤田によって明らかにされている。このため、古典論理とその対称性を考察する上で非常に重要な概念であるが、存在型を含む型付きラムダ計算の性質についてはまだ知られていない部分が多かった。
本研究では存在型を含むラムダ計算として、関数型(含意)を含む体系、および、継続型(否定)、組型(連言)を含む体系、の二つに対し、ドメインフリーと呼ばれる形式化における型検査問題、型推論問題がともに決定不能であることを証明した。ここで、型検査問題とは、与えられた項(プログラム)と型に対し、その項がその型を持つか否かを問う問題であり、型推論問題とは、与えられた項に対し、その項が何らかの型を持つか否かを問う問題である。
|
