# Tag Info

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

### "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 = ...
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 ...
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 ...
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 ...
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 ...
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: ...
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 ...

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

### 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" ...

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

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

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

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

### 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.,...

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

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

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