2
$\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).

|cite|improve this question
$\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.

|cite|improve this answer
$\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

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.