<p>From a memorable talk of a person that implemented an algorithm that solves an undecidable problem: "It takes 2-3 seconds for all the inputs I tried".</p>

CC BY-SA 2.5
2011-01-04T13:25:00.730Z
2011-01-04T13:25:00.730Z
Sariel Har-Peled
<p>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" programs.</p>

<p>The notion of "almost all" programs only makes sense if your model of computation is optimal (in the same sense that for <a href="https://en.wikipedia.org/wiki/Kolmogorov_complexity" rel="noreferrer">Kolmogorov's complexity</a>), to avoid situations where the majority of your programs are trivial.</p>

<p>Given an optimal machine $M$ and an integer $n$, can you give a correct answer to the halting problem for all programs of size $\lt n$, except a fraction $\epsilon$, for arbitrarily small $\epsilon$? Lynch proved in the 70s that <a href="https://pdfs.semanticscholar.org/1465/0acb7306411c3501656d69965ff26332b939.pdf" rel="noreferrer">no, you can't</a>. A few years ago, colleagues and I proved a <a href="https://arxiv.org/pdf/1505.00731.pdf" rel="noreferrer">stronger version</a> of this result, allowing the algorithm to make mistakes or to not halt on a small proportion of inputs, or only requiring a probabilistic approximation with probability $p\gt 0$ (allowing the algorithm to flip coins).</p>

<p>Along the way, we proved a bunch of interesting things about the properties of the sequence $\rho_n$, where $\rho_n$ is the ratio of programs of size $&lt;n$ which halt (turns out, this sequence is <em>very weird</em>). If the paper above is too dense, you can check out <a href="https://desfontain.es/PDFs/SlidesICALP.pdf" rel="noreferrer">my slides</a> from when we presented the results at ICALP.</p>

CC BY-SA 4.0
2018-05-15T15:13:05.033Z
2018-05-15T15:13:05.033Z
Ted
<p>In the case of the halting problem, the answer is "not yet". The reason is that the standard logical method for characterizing how hard a program's termination proof is (eg, ordinal analysis) tends to lose too much combinatorial and/or number-theoretic structure.  </p>

<p>The state of the art in practical termination analysis of imperative programs is something called "rank-function synthesis" (Byron Cook has a forthcoming book, Proving Program Termination, on the subject from CUP). The idea is to compute a linear function of the program's variables' values now and at the previous step, which serves as a termination metric. (One cool thing about this method is that it uses Farkas's lemma, which gives a neat geometric viewpoint to what's going on.) The interesting thing is that the tools built on this approach can do things like show the termination of the Ackerman function (which is non primitive recursive), but you can construct non-nested while loops which can defeat them (which only needs $\omega$ to show termination). </p>

<p>This means that there isn't a neat relationship between the proof-theoretic strength of the metalogic in which you show termination (this is very important in rewriting theory, for example) and the functions that techniques like rank-function synthesis can show termination for. </p>

<p>For the lambda calculus, we have a precise characterization of termination in terms of typability: a lambda term is strongly normalizing if and only if it is typeable under the intersection type discipline. Of course, this means that full type inference for intersection types is impossible, but it may also give a way of comparing partial inference algorithms. </p>

CC BY-SA 2.5
2010-12-30T12:11:18.827Z
2010-12-30T12:11:18.827Z
Neel Krishnaswami
<p>Certain problems are known to be undecidable, but it is nevertheless possible to make some progress on solving them.  For example, the halting problem is undecidable, but practical progress can be made on creating tools for detecting potential infinite loops in your code.  Tiling problems are often undecidable (e.g., does this polyomino tile some rectangle?) but again it is possible to advance the state of the art in this area.</p>

<p>What I am wondering is if there is any decent theoretical method of measuring progress on solving undecidable problems, that resembles the theoretical apparatus that has been developed for measuring progress on NP-hard problems.  Or does it seem that we are stuck with ad hoc, I-know-progress-when-I-see-it assessments of how much particular breakthroughs advance our understanding of undecidable problems?</p>

<p><b>Edit</b>: As I think about this question, it occurs to me that perhaps parameterized complexity may be relevant here.  An undecidable problem may become decidable if we introduce a parameter and fix the value of the parameter.  I'm not sure if this observation is of any use, though.</p>

CC BY-SA 3.0
2013-10-11T23:19:42.017Z
propose a concept of ["quasialgorithms"](http://cs.stackexchange.com/questions/4856/algorithm-to-solve-turings-halting-problem/4866#4866) with some research in the area
vzn
CC BY-SA 3.0
2016-07-06T02:03:01.793Z
Kolmogorov complexity can be considered an optimization problem so is a candidate for approximation algorithms. I suspect that it is not approximable if you use worst-case approximation error, or trivially approximable if you use expected approximation error.
Andrew
CC BY-SA 4.0
2018-05-16T21:09:17.150Z
One possibly stupid definition: we know that determining whether a (multivariate) polynomial equation has integer/rational solutions is undecidable, but one can ask for either integers that are "almost solutions" or (computable representations of) real numbers that are solutions and are "close to an integer/rational" in some sense. Perhaps there are notions of closeness for which this problem is decidable and still interesting.
Noah Stephens-Davidowitz
CC BY-SA 4.0
2018-05-19T13:45:08.273Z
@NoahStephens-Davidowitz : Interesting suggestion. Note, however, that Hilbert's tenth problem over $\mathbb{Q}$ is still unsolved (and in particular, not known to be undecidable).
Timothy Chow
CC BY-SA 2.5
2010-12-30T07:00:06.447Z
..reminds me of the theory of Abstract Interpretation.
Jagadish
CC BY-SA 2.5
2010-12-30T11:32:58.893Z
[Along with Jagadish's comment]: You may take a look at the MIT course [16.399: Abstract Interpretation](http://web.mit.edu/16.399/www/). Specially, [Lecture 3](http://web.mit.edu/16.399/www/lecture_03-proofs/Cousot_MIT_2005_Course_03_4-1.pdf) might be useful for your case.
Sadeq Dousti
CC BY-SA 2.5
2010-12-30T16:07:23.040Z
The obvious measure which you probably you won't like is to simply order various partial solutions according to their domains (i.e., the set of inputs on which they work). What would you like to use the measure for?
Andrej Bauer
CC BY-SA 2.5
2010-12-31T21:19:16.467Z
@Andrej: Let me answer your question indirectly.  In the realm of NP-hard problems, we sometimes have very nice results of the form, "Such-and-such an approximation ratio is attainable, and any further improvement is impossible unless P = NP."  Being able to prove analogous results for interesting undecidable problems would be nice.  It would give us some sense of whether there's some intrinsic barrier to further progress.
Timothy Chow
<computability><approximation-algorithms><parameterized-complexity><halting-problem>
Is there a sensible notion of an approximation algorithm for an undecidable problem?
Timothy Chow
# Is there a sensible notion of an approximation algorithm for an undecidable problem?

(Asked by: username_0 on 2010-12-29)

Certain problems are known to be undecidable, but it is nevertheless possible to make some progress on solving them. For example, the halting problem is undecidable, but practical progress can be made on creating tools for detecting potential infinite loops in your code. Tiling problems are often undecidable (e.g., does this polyomino tile some rectangle?) but again it is possible to advance the state of the art in this area.

What I am wondering is if there is any decent theoretical method of measuring progress on solving undecidable problems, that resembles the theoretical apparatus that has been developed for measuring progress on NP-hard problems. Or does it seem that we are stuck with ad hoc, I-know-progress-when-I-see-it assessments of how much particular breakthroughs advance our understanding of undecidable problems?

**Edit**: As I think about this question, it occurs to me that perhaps parameterized complexity may be relevant here. An undecidable problem may become decidable if we introduce a parameter and fix the value of the parameter. I'm not sure if this observation is of any use, though.

**Tags:** computability, approximation-algorithms, parameterized-complexity, halting-problem
> **Comments:**
> **username_4**: ..reminds me of the theory of Abstract Interpretation.  
> **username_5**: [Along with Jagadish's comment]: You may take a look at the MIT course [16.399: Abstract Interpretation](http://web.mit.edu/16.399/www/). Specially, [Lecture 3](http://web.mit.edu/16.399/www/lecture_03-proofs/Cousot_MIT_2005_Course_03_4-1.pdf) might be useful for your case.  
> **username_6**: The obvious measure which you probably you won't like is to simply order various partial solutions according to their domains (i.e., the set of inputs on which they work). What would you like to use the measure for?  
> **username_0**: @Andrej: Let me answer your question indirectly.  In the realm of NP-hard problems, we sometimes have very nice results of the form, "Such-and-such an approximation ratio is attainable, and any further improvement is impossible unless P = NP."  Being able to prove analogous results for interesting undecidable problems would be nice.  It would give us some sense of whether there's some intrinsic barrier to further progress.  
> **username_1**: propose a concept of ["quasialgorithms"](http://cs.stackexchange.com/questions/4856/algorithm-to-solve-turings-halting-problem/4866#4866) with some research in the area  
> **username_2**: Kolmogorov complexity can be considered an optimization problem so is a candidate for approximation algorithms. I suspect that it is not approximable if you use worst-case approximation error, or trivially approximable if you use expected approximation error.  
> **username_3**: One possibly stupid definition: we know that determining whether a (multivariate) polynomial equation has integer/rational solutions is undecidable, but one can ask for either integers that are "almost solutions" or (computable representations of) real numbers that are solutions and are "close to an integer/rational" in some sense. Perhaps there are notions of closeness for which this problem is decidable and still interesting.  
> **username_0**: @NoahStephens-Davidowitz : Interesting suggestion. Note, however, that Hilbert's tenth problem over $\mathbb{Q}$ is still unsolved (and in particular, not known to be undecidable).  

---

## 3 answers

### Answer by username_9 on 2010-12-30. Score: 32 | Accepted answer

In the case of the halting problem, the answer is "not yet". The reason is that the standard logical method for characterizing how hard a program's termination proof is (eg, ordinal analysis) tends to lose too much combinatorial and/or number-theoretic structure.

The state of the art in practical termination analysis of imperative programs is something called "rank-function synthesis" (Byron Cook has a forthcoming book, Proving Program Termination, on the subject from CUP). The idea is to compute a linear function of the program's variables' values now and at the previous step, which serves as a termination metric. (One cool thing about this method is that it uses Farkas's lemma, which gives a neat geometric viewpoint to what's going on.) The interesting thing is that the tools built on this approach can do things like show the termination of the Ackerman function (which is non primitive recursive), but you can construct non-nested while loops which can defeat them (which only needs $\omega$ to show termination).

This means that there isn't a neat relationship between the proof-theoretic strength of the metalogic in which you show termination (this is very important in rewriting theory, for example) and the functions that techniques like rank-function synthesis can show termination for.

For the lambda calculus, we have a precise characterization of termination in terms of typability: a lambda term is strongly normalizing if and only if it is typeable under the intersection type discipline. Of course, this means that full type inference for intersection types is impossible, but it may also give a way of comparing partial inference algorithms.


---

### Answer by username_7 on 2011-01-04. Score: 7

From a memorable talk of a person that implemented an algorithm that solves an undecidable problem: "It takes 2-3 seconds for all the inputs I tried".


---

### Answer by username_8 on 2018-05-15. Score: 6

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

The notion of "almost all" programs only makes sense if your model of computation is optimal (in the same sense that for [Kolmogorov's complexity](https://en.wikipedia.org/wiki/Kolmogorov_complexity)), to avoid situations where the majority of your programs are trivial.

Given an optimal machine $M$ and an integer $n$, can you give a correct answer to the halting problem for all programs of size $\lt n$, except a fraction $\epsilon$, for arbitrarily small $\epsilon$? Lynch proved in the 70s that [no, you can't](https://pdfs.semanticscholar.org/1465/0acb7306411c3501656d69965ff26332b939.pdf). A few years ago, colleagues and I proved a [stronger version](https://arxiv.org/pdf/1505.00731.pdf) of this result, allowing the algorithm to make mistakes or to not halt on a small proportion of inputs, or only requiring a probabilistic approximation with probability $p\gt 0$ (allowing the algorithm to flip coins).

Along the way, we proved a bunch of interesting things about the properties of the sequence $\rho\_n$, where $\rho\_n$ is the ratio of programs of size $very weird). If the paper above is too dense, you can check out [my slides](https://desfontain.es/PDFs/SlidesICALP.pdf) from when we presented the results at ICALP.


---

