# Is F<: with bottom undecidable?

We all know that F<: is undecidable: http://www.cse.chalmers.se/~abela/lehre/SS07/Typen/pierce93bounded.pdf

However, I have difficulties finding that anyone claiming the version with bottom added being also undecidable: https://www.cs.indiana.edu/pub/techreports/TR492.pdf

Intuitively F<: with bottom should be undecidable, but if one claims that without proving it, I feel it's just a sloppy belief. In particular, I think that the proof must involve showing S-BOT rule from the version with bottom must be either non-existent, or can be removed from the derivation tree, which doesn't seem immediate to me.

So I am wondering if there is any source actually showing adding bottom doesn't turn the calculus decidable (as expected)?

OK, fine. Since people seem to keep liking this question, I decide to answer this question myself.

TLDR : yes, F<:+bot is undecidable, as shown a proof of translation from it to F<: in the following link by myself: https://gitlab.com/JasonHuZS/AlgDotCalculus/blob/master/agda/FsubBot.agda

bot⇒full : ∀ {Γ S U} → List.map _* Γ ⊢ S * <: U * → Γ ⊢F S <: U
full⇒bot : ∀ {Γ S U} → Γ ⊢F S <: U → List.map _* Γ ⊢ S * <: U *


Despite such intuitive fact, I have to emphasize that, in the presence of subtyping, a syntactical extension of an undecidable language does not have to generate yet another undecidable language. More specifically, the decidability is a very global property of a language which depends on every interaction of the rules, and should not be assumed if a proof is not present.

In the case of F<:, the proof can easily discharge all usage of bot, merely because in F<:+bot, there isn't other creative way of using bot, to a point that it turns the translation of derivation tree to a non-trivial level.

In particular, I am working on another calculus (D<: in another source code), in which bot has so creative behavior to a point that the translation from it to F<: does not generally hold, and therefore, the calculus could be decidable, or, if it's undecidable, F<: does not reside in it as a sub-language.

• Cool! I agree that it's worth emphasizing that fact. There are a number of calculi where adding rules can turn an undecidable problem into a decidable one, e.g. adding a "universal type" $\Omega$ to an intersection type system: di.unito.it/~dezani/papers/wit02.pdf (though that example is somewhat trivial). I don't know of any simple way of avoiding the work you've done. – cody Feb 20 '19 at 13:39
• @cody when you said "decidable" did you mean decidable in terms of computation or in terms of formal theory? i don't see that paper claimed either though. am i misunderstanding anything? – Jason Hu Jun 14 '19 at 14:02
• I just meant that in the system with $\Omega$, typeability is trivially decidable: $\Gamma\vdash t : \Omega$ is always true. Remove that one rule, though, and you get undecidability. – cody Jun 14 '19 at 18:31