What’s Decidable About (Atomic) Polymorphism?

DOI10.4230/LIPICS.FSCD.2021.27arXiv2105.00748OpenAlexW3187018013MaRDI QIDQ6159943FDOQ6159943

Authors: Paolo Pistone, Luca Tranchini 

Publication date: 23 June 2023

Abstract: Due to the undecidability of most type-related properties of System F like type inhabitation or type checking, restricted polymorphic systems have been widely investigated (the most well-known being ML-polymorphism). In this paper we investigate System Fat, or atomic System F, a very weak predicative fragment of System F whose typable terms coincide with the simply typable ones. We show that the type-checking problem for Fat is decidable and we propose an algorithm which sheds some new light on the source of undecidability in full System F. Moreover, we investigate free theorems and contextual equivalence in this fragment, and we show that the latter, unlike in the simply typed lambda-calculus, is undecidable.

Full work available at URL: https://arxiv.org/abs/2105.00748

Recommendations

• scientific article; zbMATH DE number 7577586
• Type inhabitation of atomic polymorphism is undecidable
• Typability and type checking in System F are equivalent and undecidable
• The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types
• THE UNDECIDABILITY OF TYPE RELATED PROBLEMS IN TYPE -FREE STYLE SYSTEM F

zbMATH Keywords

contextual equivalencepredicative polymorphismtype-checkingatomic system Ffree theoremsML-polymorphism

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx) Computer science (68-XX)

Cited In (3)

• The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
• Type inhabitation of atomic polymorphism is undecidable
• Title not available (Why is that?)

This page was built for publication: What’s Decidable About (Atomic) Polymorphism?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6159943)