<p>Old question, but I thought I'd offer this fairly simple proof:</p>
<p><strong>Yes</strong>, it is decidable, since one can constructively build an (admissible) model in <em>finite</em> <span class="math-container">$\omega$</span>-CPPOs.</p>
<p>Well, actually, this is a slight lie; <span class="math-container">$\omega$</span>-CPOs are tough constructively since chain-completeness of <span class="math-container">$\{0 \leq 1 \}$</span> is LPO. But classically, every finite poset is chain-complete and every monotone function on finite posets is chain-continuous, and it turns out everything we need works with finite posets with <span class="math-container">$\bot$</span> and a decidable ordering. The nontrivial parts are as follows:</p>
<ul>
<li>The (strict) function space: you can enumerate all set-theoretic functions and check each one to see if it's strict and monotone. <span class="math-container">$f \leq g$</span> is decidable since the domain is finite.</li>
<li>Fixpoints: Suppose we have <span class="math-container">$f : A \to A$</span>. Then you can iterate <span class="math-container">$f$</span> starting on <span class="math-container">$\bot$</span> until you find a fixed point; this terminates since before you have found a fixed point, <span class="math-container">$x \leq f(x)$</span>, and so <span class="math-container">$|\{y \in A : y \geq x\}|$</span> decreases each iteration.</li>
</ul>

CC BY-SA 4.0
2024-11-13T00:23:42.840Z
2024-11-13T00:23:42.840Z
Mark Barbone
<p>Is the halting problem decidable for finitary <a href="https://en.wikipedia.org/wiki/Programming_Computable_Functions" rel="noreferrer">PCF</a>? By &quot;halting problem&quot; I mean the problem of deciding whether a closed PCF term evaluates to bottom under the denotational semantics of PCF. <em>Finitary</em> PCF is a version of PCF whose only base type is the type of booleans (so every type is finite).</p>

CC BY-SA 4.0
2021-10-03T17:11:58.200Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-10-03T17:16:19.213Z
For PCF you can see here: https://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
CC BY-SA 4.0
2021-10-03T17:18:45.370Z
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?
Andrej Bauer
CC BY-SA 4.0
2021-10-03T17:22:27.297Z
Sure, thanks! I am a newbie...
PaR
CC BY-SA 4.0
2021-10-03T18:18:32.270Z
I fixed it up some more for you.
Andrej Bauer
CC BY-SA 4.0
2021-10-03T18:27:05.500Z
Are you aware of https://doi.org/10.1016/S0304-3975(00)00194-8?
Andrej Bauer
CC BY-SA 4.0
2021-10-03T18:48:47.347Z
Thanks for fixing the question. Yes, I am aware of Loader's paper. However, my understanding is that it answers a different question, namely the problem of deciding whether two finitary PCF terms are observationally equivalent.
PaR
CC BY-SA 4.0
2021-10-03T19:53:17.017Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-10-03T19:59:22.400Z
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.
Andrej Bauer
<computability><pl.programming-languages><semantics><undecidability>
Halting problem for finitary PCF
PaR
# Halting problem for finitary PCF

(Asked by: username_0 on 2021-10-03)

Is the halting problem decidable for finitary [PCF](https://en.wikipedia.org/wiki/Programming_Computable_Functions)? 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).

**Tags:** computability, pl.programming-languages, semantics, undecidability
> **Comments:**
> **username_1**: 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.  
> **username_0**: For PCF you can see here: https://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).  
> **username_1**: 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?  
> **username_0**: Sure, thanks! I am a newbie...  
> **username_1**: I fixed it up some more for you.  
> **username_1**: Are you aware of https://doi.org/10.1016/S0304-3975(00)00194-8?  
> **username_0**: Thanks for fixing the question. Yes, I am aware of Loader's paper. However, my understanding is that it answers a different question, namely the problem of deciding whether two finitary PCF terms are observationally equivalent.  
> **username_1**: 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.  
> **username_1**: 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.  

---

## 1 answers

### Answer by username_2 on 2024-11-13. Score: 1

Old question, but I thought I'd offer this fairly simple proof:

**Yes**, it is decidable, since one can constructively build an (admissible) model in *finite* $\omega$-CPPOs.

Well, actually, this is a slight lie; $\omega$-CPOs are tough constructively since chain-completeness of $\{0 \leq 1 \}$ is LPO. But classically, every finite poset is chain-complete and every monotone function on finite posets is chain-continuous, and it turns out everything we need works with finite posets with $\bot$ and a decidable ordering. The nontrivial parts are as follows:

* The (strict) function space: you can enumerate all set-theoretic functions and check each one to see if it's strict and monotone. $f \leq g$ is decidable since the domain is finite.
* Fixpoints: Suppose we have $f : A \to A$. Then you can iterate $f$ starting on $\bot$ until you find a fixed point; this terminates since before you have found a fixed point, $x \leq f(x)$, and so $|\{y \in A : y \geq x\}|$ decreases each iteration.


---

