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

<p>TLDR : yes, F&lt;:+bot is undecidable, as shown a proof of translation from it to F&lt;: in the following link by myself: <a href="https://gitlab.com/JasonHuZS/AlgDotCalculus/blob/master/agda/FsubBot.agda" rel="nofollow noreferrer">https://gitlab.com/JasonHuZS/AlgDotCalculus/blob/master/agda/FsubBot.agda</a></p>

<pre><code>bot⇒full : ∀ {Γ S U} → List.map _* Γ ⊢ S * &lt;: U * → Γ ⊢F S &lt;: U
full⇒bot : ∀ {Γ S U} → Γ ⊢F S &lt;: U → List.map _* Γ ⊢ S * &lt;: U *
</code></pre>

<hr>

<p>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.</p>

<p>In the case of F&lt;:, the proof can easily discharge all usage of bot, merely because in F&lt;:+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.</p>

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

CC BY-SA 4.0
2019-02-20T13:39:37.853Z
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: http://www.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
CC BY-SA 4.0
2019-06-14T14:02:40.870Z
@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
CC BY-SA 4.0
2019-06-14T18:31:31.843Z
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
CC BY-SA 4.0
2019-02-19T23:33:30.073Z
2019-03-23T18:22:39.340Z
2019-03-23T18:22:39.340Z
Jason Hu
<p>We all know that F&lt;: is undecidable: <a href="http://www.cse.chalmers.se/~abela/lehre/SS07/Typen/pierce93bounded.pdf" rel="noreferrer">http://www.cse.chalmers.se/~abela/lehre/SS07/Typen/pierce93bounded.pdf</a></p>

<p>However, I have difficulties finding that anyone claiming the version with bottom added being also undecidable: <a href="https://www.cs.indiana.edu/pub/techreports/TR492.pdf" rel="noreferrer">https://www.cs.indiana.edu/pub/techreports/TR492.pdf</a></p>

<p>Intuitively F&lt;: 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.</p>

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

<pl.programming-languages>
Is F<: with bottom undecidable?
Jason Hu
# Is F<: with bottom undecidable?

(Asked by: username_0 on 2019-02-01)

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)?

**Tags:** pl.programming-languages

---

## 1 answers

### Answer by username_0 on 2019-02-19. Score: 5 | Accepted answer

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.

> **Comments:**
> **username_1**: 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: http://www.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.  
> **username_0**: @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?  
> **username_1**: 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.  

---

