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

  • 2
    $\begingroup$ 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. $\endgroup$ Oct 3, 2021 at 17:11
  • $\begingroup$ 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). $\endgroup$
    – PaR
    Oct 3, 2021 at 17:16
  • 2
    $\begingroup$ 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? $\endgroup$ Oct 3, 2021 at 17:18
  • 1
    $\begingroup$ 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. $\endgroup$ Oct 3, 2021 at 19:53
  • 1
    $\begingroup$ 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. $\endgroup$ Oct 3, 2021 at 19:59


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.