4
$\begingroup$

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

$\endgroup$
  • $\begingroup$ What are the $\varphi$s? ​ ​ $\endgroup$ – user6973 May 12 '17 at 7:58
  • $\begingroup$ @RickyDemer An effective enumeration of all computable functions. Thanks, i will edit the question, and add it $\endgroup$ – Andrea Asperti May 12 '17 at 8:00
  • $\begingroup$ My understanding is that usually, they are defined as either going from {0,1}$^*$ to itself or from {0,1,2,3,...} to itself. ​ In particular, letting $\hspace{.04 in}f$ be a subscript for the constant $1$ function would work. ​ ​ ​ ​ $\endgroup$ – user6973 May 12 '17 at 8:03
  • $\begingroup$ @RickyDemer That is the type PC of partial computable functions. \varphi: N -> PC. Typical notation of computability theory. $\endgroup$ – Andrea Asperti May 12 '17 at 8:09
  • 1
    $\begingroup$ What specifies the codomain of the type you're using? ​ ​ $\endgroup$ – user6973 May 12 '17 at 8:15
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Andrea Asperti May 13 '17 at 8:08
  • $\begingroup$ 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. $\endgroup$ – Andrea Asperti May 13 '17 at 8:28
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer May 13 '17 at 8:31
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer May 13 '17 at 8:33
  • $\begingroup$ 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. $\endgroup$ – Andrea Asperti May 13 '17 at 8:42
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.