研究課題
若手研究(B)
本研究では、二階存在量化子をもつ計算体系について、とくにプログラムが部分的な型情報を持つ形式の型付ラムダ計算の体系において、その型付可能性に対する決定問題に関する以下の結果を得た。(1)プログラムが部分的な型情報を持つ形式において、多相型に関する型検査問題・型推論問題が存在型に関する型検査問題・型推論問題にチューリング還元可能であることを示し、これらの問題の決定不能性を証明した。(2)ドメインフリーと呼ばれる形式化において、二階存在型を含むいくつかの断片において型検査問題と型付可能性問題がチューリング同値であることを証明した。これにより、存在型をもつドメインフリーラムダ計算の型付可能性問題の決定不能性に対する別証を得た。(3)さらにドメインフリー形式において二階存在型をもつ体系における型検査・型付可能性問題が、多相型をもつ体系における型検査・型付可能性問題と、それぞれチューリング同値であることを証明した。
すべて 2011 2010 2009
すべて 雑誌論文 (3件) 学会発表 (5件)
Theoretical Computer Science
巻: 412(44) ページ: 6193-6207
18th International Workshop on Functional and(Constraint) Logic Programming(WFLP 2009)
巻: 5979 ページ: 96-110
Special Issue : Selected papers from 2009 Computing : The Australasian Theory Symposium(CATS2009)
巻: 7
