Show simple item record

dc.contributor.authorWells, J. B.en_US
dc.date.accessioned2011-10-20T04:37:42Z
dc.date.available2011-10-20T04:37:42Z
dc.date.issued1996-03-09
dc.identifier.citationWells, J.B.. "Typability is Undecidable for F+Eta", Technical Report BUCS-1996-022, Computer Science Department, Boston University, March 9, 1996. [Available from: http://hdl.handle.net/2144/1598]
dc.identifier.urihttps://hdl.handle.net/2144/1598
dc.description.abstractSystem F is the well-known polymorphically-typed λ-calculus with universal quantifiers ("∀"). F+η is System F extended with the eta rule, which says that if term M can be given type τ and M η-reduces to N, then N can also be given the type τ. Adding the eta rule to System F is equivalent to adding the subsumption rule using the subtyping ("containment") relation that Mitchell defined and axiomatized [Mit88]. The subsumption rule says that if M can be given type τ and τ is a subtype of type σ, then M can be given type σ. Mitchell's subtyping relation involves no extensions to the syntax of types, i.e., no bounded polymorphism and no supertype of all types, and is thus unrelated to the system F≤("F-sub"). Typability for F+η is the problem of determining for any term M whether there is any type τ that can be given to it using the type inference rules of F+η. Typability has been proven undecidable for System F [Wel94] (without the eta rule), but the decidability of typability has been an open problem for F+η. Mitchell's subtyping relation has recently been proven undecidable [TU95, Wel95b], implying the undecidability of "type checking" for F+η. This paper reduces the problem of subtyping to the problem of typability for F+η, thus proving the undecidability of typability. The proof methods are similar in outline to those used to prove the undecidability of typability for System F, but the fine details differ greatly.en_US
dc.description.sponsorshipNational Science Foundation (CCR-9113196, CCR-9417382)en_US
dc.language.isoen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-1996-022
dc.titleTypability is undecidable for F+Etaen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record