2024-03-28T21:55:47Z
https://repository.nii.ac.jp/oai
oai:repository.nii.ac.jp:00001243
2023-01-05T08:32:22Z
136
NII Technical Report (NII-2008-005E):Inhabitance of Existential Types is Decidable in Negation-Product Fragment
龍田, 真
Tatsuta, Makoto
藤田, 憲悦
Fujita, Ken-etsu
長谷川, 立
Hasegawa, Ryu
中野, 洋
Nakano, Hiroshi
テクニカルレポート
Technical Report
This paper shows the inhabitance in the lambda calculus with negation, product, and existential types is decidable. This is proved by showing existential quantification can be eliminated and reducing the problem to provability in intuitionistic propositional logic. By the same technique, this paper also shows existential quantification followed by negation can be replaced by a specific witness in both that system and the system with implication and bottom.
国立情報学研究所
2008-04-04
eng
departmental bulletin paper
https://doi.org/10.20736/0000001243
https://repository.nii.ac.jp/records/1243
10.20736/0000001243
1346-5597
NIIテクニカル・レポート
NII Technical Report
1
13
https://repository.nii.ac.jp/record/1243/files/08-005E.pdf
application/pdf
249.4 kB
2019-03-12