Inhabitation of polymorphic and existential types |
| |
Authors: | Makoto Tatsuta Ken-etsu Fujita Hiroshi Nakano |
| |
Affiliation: | a National Institute of Informatics, Japan b Department of Computer Science, Gunma University, Japan c Department of Mathematics, University of Tokyo, Japan d Department of Applied Mathematics and Informatics, Ryukoku University, Japan |
| |
Abstract: | This paper shows that the inhabitation problem in the lambda calculus with negation, product, polymorphic, and existential types is decidable, where the inhabitation problem asks whether there exists some term that belongs to a given type. In order to do that, this paper proves the decidability of the provability in the logical system defined from the second-order natural deduction by removing implication and disjunction. This is proved by showing the quantifier elimination theorem and reducing the problem to the provability in propositional logic. The magic formulas are used for quantifier elimination such that they replace quantifiers. As a byproduct, this paper also shows the second-order witness theorem which states that a quantifier followed by negation can be replaced by a witness obtained only from the formula. As a corollary of the main results, this paper also shows Glivenko’s theorem, Double Negation Shift, and conservativity for antecedent-empty sequents between the logical system and its classical version. |
| |
Keywords: | 03B15 03B70 |
本文献已被 ScienceDirect 等数据库收录! |
|