Halting problem for finitary PCF

Is the halting problem decidable for finitary PCF? By "halting problem" I mean the problem of deciding whether a closed PCF term evaluates to bottom under the denotational semantics of PCF. Finitary PCF is a version of PCF whose only base type is the type of booleans (so every type is finite).

• What is finitary PCF? Please ask questions in a (mostly) self-contained way. There are experts here, but for the most part they are not mind readers. Oct 3 '21 at 17:11
• For PCF you can see here: en.wikipedia.org/wiki/Programming_Computable_Functions. Finitary PCF is a version of PCF whose only type has a finite number of values (for example, the Boolean type).
– PaR
Oct 3 '21 at 17:16
• Please edit your question, not write more comments. And explain what "finitary" means, please. While you are at it, what is the halting problem for a programming language? Oct 3 '21 at 17:18
• Right, we can reduce $x = \bot$ to $x \leq \bot$, but it's not so clear how to reduce $x \leq y$ to $\bot$-testing. Oct 3 '21 at 19:53
• My first instinct is to say that it's decidable, because we ought to be able to tell how many times we need to unfold a $\mathsf{fix} \, e$ by looking at the types of subexpressions of $e$. But these things can be tricky. Oct 3 '21 at 19:59