<p>Suppose there were a computable $f$ as described in the question. Then we could solve the Halting problem as follows.</p>

<p>Given a Turing machine $T$, consider the computable function $g$, defined by
$$g(k) = \begin{cases}
1 &amp; \text{if $T$ halts in $\leq k$ steps} \\
0 &amp; \text{otherwise}
\end{cases}$$
This is a computable, nondecreasing and total function. Therefore, we may use $f$ to establish that the range of $g$ is decidable. But now we just check whether $1$ is in the range to figure out whether $T$ halts.</p>

<p>Notice that I never used the finite/infinite distinction. The above argument works even if we assume that $f$ enumerates a finite set. Are you sure you got your theorem correct? The one I know says that an infinite set is decidable if it can be enumerated by a computable <em>strictly increasing</em> function. There is of course another theorem stating that every finite set can (obviously) be enumerated in increasing order.</p>

<p><strong>Supplemental:</strong> Let us look at the matter from a constructive point of view. We have two constructive theorems, assuming Markov principle (which is generally used in computability theory):</p>

<blockquote>
  <p><strong>Theorem 1:</strong> If a finite set can be enumerated in non-decreasing order then it is decidable.</p>
</blockquote>

<p>(A set is said to be finite if it is isomprhic to $\{0, 1, \ldots, n-1\}$ for some $n \in \mathbb{N}$, so the extra conditions in the theorem does not actually help, as every finite set is decidable.)</p>

<blockquote>
  <p><strong>Theorem 2:</strong> If a non-finite set can be enumerated in non-decreasin order then it is decidable.</p>
</blockquote>

<p>However, we cannot just stick these two together into "any set enumerated in increasing order is decidable" because the following is <em>not</em> a constructive theorem:</p>

<blockquote>
  <p><strong>Theorem (classical):</strong> Every set is finite or non-finite.</p>
</blockquote>

<p>In fact, in computability theory there are counter-examples. An <em>immune</em> set is infinite, but it does not contain any infinite computable sequence.</p>

CC BY-SA 3.0
2017-05-13T08:08:53.760Z
Yes. If the set is finite it is obviously decidable, and if it is infinite then c(x)=let a = \mu y.f y >= x in a == x is total. But the proof is not constructive.
Andrea Asperti
CC BY-SA 3.0
2017-05-13T08:28:43.760Z
I don't see why you want to stick to a constructive point ot view. See e.g. theorem III(a) pag. 59 in Rogers.
Andrea Asperti
CC BY-SA 3.0
2017-05-13T08:31:04.110Z
I don't understand what you are talking about. *You* are bringing in constructivity, and I am just responding to it. I explicitly answered your question, and I identified the source of non-constructivity in the usual proof as the fact that not every set is finite or infinite.
Andrej Bauer
CC BY-SA 3.0
2017-05-13T08:33:36.273Z
But to explain what anything has to do with constructivity: Theorems 1 and 2 in the internal language of the effective topos amount precisely to what we are talking about.
Andrej Bauer
CC BY-SA 3.0
2017-05-13T08:42:56.197Z
The point is that you questioned the correctness of the theorem. The theorem is correct, but the proof is not constructive. Everything else if fine, i liked your proof.
Andrea Asperti
CC BY-SA 3.0
2017-05-13T08:57:45.237Z
I *questioned* correctness. You can just say "nope, it's correct". You don't have to admonish me for mentioning constructivity :-)
Andrej Bauer
CC BY-SA 3.0
2017-05-12T09:31:53.843Z
2017-05-13T08:33:59.580Z
2017-05-13T08:33:59.580Z
Andrej Bauer
<p>I have an answer to a closely related question.</p>

<blockquote>
  <p>Hopcroft &amp; Ullman -79, p.170:  </p>
  
  <p><strong>Theorem 7.8</strong> <span class="math-container">$L$</span> is recursive if and only if <span class="math-container">$L$</span> is generated in canonical order</p>
</blockquote>

<p>The last line of the proof reads</p>

<blockquote>
  <p>Note that in general we cannot exhibit a particular halting TM that accepts <span class="math-container">$L$</span>, but the theorem merely states that one such TM exists.</p>
</blockquote>

<p>It's not explained whether this is by necessity or if it's just a shortcoming of this particular proof.</p>

<p>The question is if there could be an algorithm <span class="math-container">$M_?$</span> that when given a canonical order enumerator as input produces a corresponding decider as output. (We don't put any restrictions on what the algorithm does if presented with other input.)</p>

<p>I think there is a simple argument that this is not possible:</p>

<ol>
<li><p>By a simple trick it's possible to enumerate the decidable languages with canonical order enumerators.</p></li>
<li><p>By a standard diagonalization argument it's <strong>not</strong> possible to enumerate the decidable languages with deciders.</p></li>
<li><p>If <span class="math-container">$M_?$</span> existed, then we could convert an enumeration of the decidable languages by canonical order enumerators (possible) into an enumeration by deciders (impossible).</p></li>
</ol>

<p><em>1. explained:<br>
We start with an enumeration of all TM enumerators, which is possible, since given a string it's (easily) decidable whether it encodes an enumerator or not. We modify each <span class="math-container">$M_E$</span> in that enumeration into a <span class="math-container">$M'_E$</span> that skips the outputs that break the canonical order.</em></p>

<p><em>This can be done by letting <span class="math-container">$M'_E$</span> simulate <span class="math-container">$M_E$</span> on one of its work tapes. <span class="math-container">$M'_E$</span> only writes to its output tape the words generated by <span class="math-container">$M_E$</span> that don't break the canonical order. Alternatively we could modify each <span class="math-container">$M_E$</span> to a <span class="math-container">$M''_E$</span> that stops outputting words altogether if <span class="math-container">$M_E$</span> generates a word that breaks the canonical order.</em></p>

<p><em>Those <span class="math-container">$M_E$</span> in the original enumeration that are already canonical order enumerators will go relatively unscathed through this modification process. <span class="math-container">$M'_E$</span> will in those cases generate the same words in the same order as <span class="math-container">$M_E$</span>, so <span class="math-container">$M'_E$</span> will represent the same (decidable) language as <span class="math-container">$M_E$</span>.</em></p>

<p>Canonical order enumerators and deciders are in a sense equivalent objects, but yet not equivalent, since it's only possible to go constructively in one direction.</p>

CC BY-SA 4.0
2019-12-12T14:32:41.057Z
2019-12-17T00:46:32.420Z
2019-12-17T00:46:32.420Z
sixpanbass
<p>It is well known that a set of numbers enumerable in nondecreasing order is
decidable. However, the typical proof, by cases on the finiteness of the
enumerated set, is not constructive. In general, it does not seem possible
to effectively derive the decider from the enumeration function (and its properties): can this be proved?</p>

<p>Here is a possible formalization of the problem. Let $\varphi$ be an effective enumeration of all computable functions.
Let $c_A$ be the characteristic function of $A$, Let $f$ be a function such that</p>

<p>$$\varphi_{f(i)} =
\begin{cases}
c_{cod{(\varphi_i})} &amp; \mbox{if $\varphi_i$ is total and non decreasing}\\
                 \mbox{arbitrary} &amp; \mbox{otherwise}
\end{cases}
$$
Prove that no such $f$ is computable (or that it is indeed computable).</p>

CC BY-SA 3.0
2017-05-12T08:00:37.760Z
@RickyDemer An effective enumeration of all computable functions. Thanks, i will edit the question, and add it
Andrea Asperti
CC BY-SA 3.0
2017-05-12T08:09:10.510Z
@RickyDemer That is the type PC of partial computable functions. \varphi: N -> PC. Typical notation of computability theory.
Andrea Asperti
CC BY-SA 3.0
2017-05-12T08:19:39.540Z
@RickyDemer The codomain is just the set of possible outputs of the function. Again, this is STANDARD terminology in computability theory.
Andrea Asperti
CC BY-SA 3.0
2017-05-12T08:40:56.667Z
@RickyDemer Since functions are partial, domain and codomain do not have the standard meaning. Use range, if you prefer.
Andrea Asperti
<computability><decidability><constructive-mathematics><enumeration>
About the decidability of sets enumerated in non decreasing order
Andrea Asperti
# About the decidability of sets enumerated in non decreasing order

(Asked by: username_0 on 2017-05-12)

It is well known that a set of numbers enumerable in nondecreasing order is
decidable. However, the typical proof, by cases on the finiteness of the
enumerated set, is not constructive. In general, it does not seem possible
to effectively derive the decider from the enumeration function (and its properties): can this be proved?

Here is a possible formalization of the problem. Let $\varphi$ be an effective enumeration of all computable functions.
Let $c\_A$ be the characteristic function of $A$, Let $f$ be a function such that

$$\varphi\_{f(i)} =
\begin{cases}
c\_{cod{(\varphi\_i})} & \mbox{if $\varphi\_i$ is total and non decreasing}\\
\mbox{arbitrary} & \mbox{otherwise}
\end{cases}
$$
Prove that no such $f$ is computable (or that it is indeed computable).

**Tags:** computability, decidability, constructive-mathematics, enumeration
> **Comments:**
> **username_0**: @RickyDemer An effective enumeration of all computable functions. Thanks, i will edit the question, and add it  
> **username_0**: @RickyDemer That is the type PC of partial computable functions. \varphi: N -> PC. Typical notation of computability theory.  
> **username_0**: @RickyDemer The codomain is just the set of possible outputs of the function. Again, this is STANDARD terminology in computability theory.  
> **username_0**: @RickyDemer Since functions are partial, domain and codomain do not have the standard meaning. Use range, if you prefer.  

---

## 2 answers

### Answer by username_1 on 2017-05-12. Score: 4

Suppose there were a computable $f$ as described in the question. Then we could solve the Halting problem as follows.

Given a Turing machine $T$, consider the computable function $g$, defined by
$$g(k) = \begin{cases}
1 & \text{if $T$ halts in $\leq k$ steps} \\
0 & \text{otherwise}
\end{cases}$$
This is a computable, nondecreasing and total function. Therefore, we may use $f$ to establish that the range of $g$ is decidable. But now we just check whether $1$ is in the range to figure out whether $T$ halts.

Notice that I never used the finite/infinite distinction. The above argument works even if we assume that $f$ enumerates a finite set. Are you sure you got your theorem correct? The one I know says that an infinite set is decidable if it can be enumerated by a computable *strictly increasing* function. There is of course another theorem stating that every finite set can (obviously) be enumerated in increasing order.

**Supplemental:** Let us look at the matter from a constructive point of view. We have two constructive theorems, assuming Markov principle (which is generally used in computability theory):

> **Theorem 1:** If a finite set can be enumerated in non-decreasing order then it is decidable.

(A set is said to be finite if it is isomprhic to $\{0, 1, \ldots, n-1\}$ for some $n \in \mathbb{N}$, so the extra conditions in the theorem does not actually help, as every finite set is decidable.)

> **Theorem 2:** If a non-finite set can be enumerated in non-decreasin order then it is decidable.

However, we cannot just stick these two together into "any set enumerated in increasing order is decidable" because the following is *not* a constructive theorem:

> **Theorem (classical):** Every set is finite or non-finite.

In fact, in computability theory there are counter-examples. An *immune* set is infinite, but it does not contain any infinite computable sequence.

> **Comments:**
> **username_0**: Yes. If the set is finite it is obviously decidable, and if it is infinite then c(x)=let a = \mu y.f y >= x in a == x is total. But the proof is not constructive.  
> **username_0**: I don't see why you want to stick to a constructive point ot view. See e.g. theorem III(a) pag. 59 in Rogers.  
> **username_1**: I don't understand what you are talking about. *You* are bringing in constructivity, and I am just responding to it. I explicitly answered your question, and I identified the source of non-constructivity in the usual proof as the fact that not every set is finite or infinite.  
> **username_1**: But to explain what anything has to do with constructivity: Theorems 1 and 2 in the internal language of the effective topos amount precisely to what we are talking about.  
> **username_0**: The point is that you questioned the correctness of the theorem. The theorem is correct, but the proof is not constructive. Everything else if fine, i liked your proof.  
> **username_1**: I *questioned* correctness. You can just say "nope, it's correct". You don't have to admonish me for mentioning constructivity :-)  

---

### Answer by username_2 on 2019-12-12. Score: 0

I have an answer to a closely related question.

> Hopcroft & Ullman -79, p.170:
>
> **Theorem 7.8** $L$ is recursive if and only if $L$ is generated in canonical order

The last line of the proof reads

> Note that in general we cannot exhibit a particular halting TM that accepts $L$, but the theorem merely states that one such TM exists.

It's not explained whether this is by necessity or if it's just a shortcoming of this particular proof.

The question is if there could be an algorithm $M\_?$ that when given a canonical order enumerator as input produces a corresponding decider as output. (We don't put any restrictions on what the algorithm does if presented with other input.)

I think there is a simple argument that this is not possible:

1. By a simple trick it's possible to enumerate the decidable languages with canonical order enumerators.
2. By a standard diagonalization argument it's **not** possible to enumerate the decidable languages with deciders.
3. If $M\_?$ existed, then we could convert an enumeration of the decidable languages by canonical order enumerators (possible) into an enumeration by deciders (impossible).

*1. explained:  
We start with an enumeration of all TM enumerators, which is possible, since given a string it's (easily) decidable whether it encodes an enumerator or not. We modify each $M\_E$ in that enumeration into a $M'\_E$ that skips the outputs that break the canonical order.*

*This can be done by letting $M'\_E$ simulate $M\_E$ on one of its work tapes. $M'\_E$ only writes to its output tape the words generated by $M\_E$ that don't break the canonical order. Alternatively we could modify each $M\_E$ to a $M''\_E$ that stops outputting words altogether if $M\_E$ generates a word that breaks the canonical order.*

*Those $M\_E$ in the original enumeration that are already canonical order enumerators will go relatively unscathed through this modification process. $M'\_E$ will in those cases generate the same words in the same order as $M\_E$, so $M'\_E$ will represent the same (decidable) language as $M\_E$.*

Canonical order enumerators and deciders are in a sense equivalent objects, but yet not equivalent, since it's only possible to go constructively in one direction.


---

