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.

  • $\begingroup$ 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. $\endgroup$
    – cody
    Feb 20 '19 at 13:39
  • $\begingroup$ @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? $\endgroup$
    – Jason Hu
    Jun 14 '19 at 14:02
  • $\begingroup$ 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. $\endgroup$
    – cody
    Jun 14 '19 at 18:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.