13 votes
Accepted

Is there a good notion of non-termination and halting proofs in type theory?

Because one of the principal applications of Type Theory in formalizations has been to study programing languages and computation in general, a lot of thought has gone into ways of representing ...
user avatar
  • 13.2k
11 votes

"Berman-Hartmanis Conjecture Separates NP From All Super-Poly. DTIME Classes" -- Worthy of arXiv.org?

I'm glad you are interested in complexity but there are some issues in your paper. Your techniques relativize and there is an oracle relative to which the Berman-Hartmanis conjecture is true and NP = ...
user avatar
10 votes
Accepted

How good can a halting detector be?

This isn't a "nice" property, because whether it's true or false depends upon the encoding. See David et al's Asymptotically almost all $\lambda$-terms are strongly normalizing, which proves what it ...
user avatar
9 votes
Accepted

What is the reference for the proof Gödel's first incompleteness theorem based on the undecidability of the halting problem?

I believe that some version of this connection can be tied back to Turing's seminal paper on computability. Namely, Turing makes the following two claims: "The results of Section 8 have some ...
user avatar
  • 1,633
8 votes
Accepted

For a specific unbounded Turing machine, is its Halting problem undecidable?

It depends in which sense you mean "undecidable". If you evaluate $M$ on the empty input, and want only to find a yes/no answer, then the algorithmic problem is trivially decidable, as answered by ...
user avatar
  • 7,653
6 votes
Accepted

Can the halting problem be solved probabilistically?

It is well known that any language or function computable by a probabilistic algorithm is also computable deterministically. Here, we require that with probability $>1/2$, the algorithm outputs the ...
user avatar
6 votes
Accepted

Uniform mortality problem for Turing Machines

The mortality problem is undecidable (P.K. Hooper, Th eUndecidability of the Turing Machine Immortality Problem (1966)) The uniform mortality problem undecidability follows from the following: ...
user avatar
6 votes
Accepted

Program equivalence wherein the programs are known to always halt

As a counter-example to this, consider the Context-Free Equivalence problem: it's undecidable to determine, given two context free languages, whether they accept the same set. If your problem were ...
user avatar
6 votes

Polynomial-time reductions between undecidable languages

Gödel's incompleteness theorem can be thought of as a reduction from the Halting problem to the language $\langle \varphi \mid \varphi \text{ is a true sentence in number theory}\rangle$, and a ...
user avatar
  • 2,295
6 votes

Is there a sensible notion of an approximation algorithm for an undecidable problem?

This is answering the title of the question more than its content, but you can also consider "approximations" of the halting problem as algorithms which will give you a correct answer on "almost all" ...
user avatar
  • 329
5 votes

What is the "nearest" problem to the Collatz conjecture that has been successfully resolved?

Consider the function $T: \mathbb N \rightarrow \mathbb N$, where $T(n)=n/2$ when $n$ is even and $T(n)=n+1$ when $n$ is odd. Then it is known that for any $n \in \mathbb N$, there exists a $k \in \...
user avatar
5 votes

For a specific unbounded Turing machine, is its Halting problem undecidable?

For every concrete Turing machine $M$, the halting problem (Problem $P_M$ without input: "Does the Turing machine $M$ halt on the empty input $\varepsilon$?") is decidable. The corresponding decision ...
user avatar
  • 5,722
4 votes
Accepted

Turing meta-oracle

Such an $H$ would let us solve the halting problem: We begin by running $H(H(P))$ until it halts (which it does by assumption on $H$). If the output of $H(H(P))$ is "doesn't halt," then we know $H(P)...
user avatar
4 votes
Accepted

Are all turing machines paths predictable?

This is another way to prove that not all Turing machines are predictable. First it's easy to note that: all halting machines are predictable; all machines that loop forever on a finite portion of ...
user avatar
4 votes
Accepted

Practical approaches to solving whether programs will halt

Yes, an example of a system that performs this task is T2. It does not solve the halting problem but instead it only attempts to solve certain special cases. A overview is at https://en.wikipedia.org/...
user avatar
4 votes

Program equivalence wherein the programs are known to always halt

Consider programs $e_1$, $e_2$ and numbers of time steps $t$. Let $f_i(t)$ be the output of $e_i$ after $t$ steps, and let $f_i(t)$ output a special message like "none" if there's no output yet. ...
user avatar
3 votes

Are All Turing-Uncomputable Sets Isomorphic to the Halting Problem?

No, there is a whole hierarchy of Turing undecidability: http://en.wikipedia.org/wiki/Turing_degree In particular, the language L_min consisting of all minimal Turing machine encodings is not ...
user avatar
  • 10.1k
3 votes
Accepted

Is this a weaker or stronger form of the halting problem

The standard proof that the halting problem $L$ is undecidable also gives an efficient algorithm for constructing an instance on which a given Turing machine $H$ fails to solve the halting problem. ...
user avatar
  • 1,733
2 votes

Is this a good definition of computability?

First of all, the place for this question is cs.se, not here. But since I've already written an answer, I'll leave it. There is a formal definition of computability: a function $f$ is computable if ...
user avatar
  • 5,261
2 votes

Are all turing machines paths predictable?

If I understood your question correctly, the answer is NO. Let $M$ be any TM and $w$ any input string, and define the TM $M'$ as follows: it reserves the leftmost square of the tape as "special" (e.g.,...
user avatar
  • 10.1k
2 votes

Halting problem for finite tape TM

"Easy to check" is the understatement of the century: can you actually carry out your proposed plan of "just" writing down all the registers/RAM cells, etc? You're right that it takes finite time, but ...
user avatar
  • 10.1k
2 votes

Automated proving that a program doesn't halt

In contradiction with Gurkenglas' answer, there actually is a community of scientists who work on proving non-termination of programs in various language and formalisms. An obvious approach would be ...
user avatar
  • 13.2k
1 vote

Automated proving that a program doesn't halt

Since the Halting problem is undecidable, whatever approach I use to answer the question must eventually be unhelpful in the real world. There's a sequence of sets of programs such that each set is ...
user avatar
1 vote

Constructive proof of the Halting Problem

I think if we want to answer this problem constructively, then we should be able propose problem constructively. Let language of arithmetic be $L=\{0,S,+,\cdot \}$ and $\phi(n,x,y)$ be kleene ...
user avatar
1 vote
Accepted

Undecidable Single Programs

One way to look at your question is the Busy Beaver Numbers. What we will do is restrict a Turing Machine so that: The blank symbol is a $0$ The tape alphabet is $\{0, 1\}$ The input to our turing ...
user avatar
  • 1,102

Only top scored, non community-wiki answers of a minimum length are eligible