×

zbMATH — the first resource for mathematics

Inhabitation of polymorphic and existential types. (English) Zbl 1225.03034
Summary: 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.

MSC:
03B70 Logic in computer science
03B15 Higher-order logic; type theory (MSC2010)
03B25 Decidability of theories and sets of sentences
03B40 Combinatory logic and lambda calculus
03C10 Quantifier elimination, model completeness and related topics
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Dowek, G.; Jiang, Y., Eigenvariables, bracketing and the decidability of positive minimal predicate logic, Theoretical computer science, 360, 1-3, 193-208, (2006) · Zbl 1106.03006
[2] Fujita, K., Explicitly typed \(\lambda \mu\)-calculus for polymorphism and call-by-value, (), 162-177 · Zbl 0933.03009
[3] Fujita, K., Galois embedding from polymorphic types into existential types, (), 194-208 · Zbl 1114.03009
[4] Hasegawa, M., Relational parametricity and control, Logical methods in computer science, 2, 3:3, 1-22, (2006) · Zbl 1126.68023
[5] Löb, M.H., Embedding first order predicate logic in fragments of intuitionistic logic, Journal of symbolic logic, 41, 4, 705-718, (1976) · Zbl 0358.02012
[6] Matthes, R., Non-strictly positive fixed-points for classical natural deduction, Annals of pure and applied logic, 133, 1-3, 205-230, (2005) · Zbl 1066.03057
[7] Y. Minamide, G. Morrisett, R. Harper, Typed closure conversion, in: Proceeding of 23rd ACM Symposium on Principles of Programming Languages, POPL’96, 1996, pp. 271-283.
[8] Mitchell, J.C.; Plotkin, G.D., Abstract types have existential type, ACM transactions on programming languages and systems, 10, 3, 470-502, (1988)
[9] Nakazawa, K.; Tatsuta, M.; Kameyama, Y.; Nakano, H., Undecidability of type-checking in domain-free typed lambda-calculi with existence, (), 478-492 · Zbl 1156.03316
[10] Tatsuta, M.; Mints, G., A simple proof of second-order strong normalization with permutative conversions, Annals of pure and applied logic, 136, 1-2, 134-155, (2005) · Zbl 1095.03057
[11] Tatsuta, M., Simple saturated sets for disjunction and second-order existential quantification, (), 366-380 · Zbl 1215.03068
[12] M. Tatsuta, K. Fujita, R. Hasegawa, H. Nakano, Inhabitance of existential types is decidable in negation – product fragment, in: Proceedings of 2nd International Workshop on Classical Logic and Computation, CLC2008, 2008.
[13] Troelstra, A.S., Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture notes in mathematics, 344, (1973) · Zbl 0275.02025
[14] Troelstra, A.S.; Schwichtenberg, H., Basic proof theory, (2000), Cambridge University Press · Zbl 0957.03053
[15] Urzyczyn, P., Inhabitation in typed lambda-calculi, (), 373-389 · Zbl 1063.03527
[16] Wells, J.B., Typability and type checking in system F are equivalent and undecidable, Annals of pure and applied logic, 98, 1-3, 111-156, (1999) · Zbl 0932.03017
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.