When have you come upon the halting problem in the field?

Language AgnosticFieldTheoryTuring MachinesHalting Problem

Language Agnostic Problem Overview


When have you ever personally come upon the https://en.wikipedia.org/wiki/Halting_problem">halting problem in the field? This can be when a co-worker / boss suggested a solution which would violate the fundamental limits of computation, or when you realized yourself that a problem you were trying to solve was, in fact, impossible to solve.

The most recent time I came up with it was when studying type checkers. Our class realized that it would be impossible to write a perfect type checker (one that would accept all programs that would run without type errors, and reject all programs that would run with type errors) because this would, in fact, solve the halting problem. Another was when we realized, in the same class, that it would be impossible to determine whether a division would ever occur by zero, in the type-checking stage, because checking whether a number, at run-time, is zero, is also a version of the halting problem.

Language Agnostic Solutions


Solution 1 - Language Agnostic

I literally got assigned the halting problem, as in "write a monitor plugin to determine whether a host is permanently down". Seriously? OK, so I'll just give it a threshold. "No, because it might come back up afterward."

Much theoretical exposition ensued.

Solution 2 - Language Agnostic

Years ago, I remember reading a review (in Byte magazine, I believe) of a product called Basic Infinite Loop Finder or BILF. BILF was supposed to scan your Microsoft Basic source code and find any loops which didn't terminate. It claimed to be able any find any infinite loops in the code.

The reviewer was savvy enough to point out that for that program to work in all cases, it would have to solve the halting problem and went so far as to provide a mathematical proof of why it couldn't work in all cases.

In the next issue, they published a letter from a company representative explaining that the problem would be fixed in the next release.

Update: I ran across an image of the article on imgur. I remembered the wrong magazine. It was Creative Computing, not Byte. Otherwise, it's pretty much as I remembered it.

You can see a hi-res version of it on imgur.

enter image description here enter image description here

Solution 3 - Language Agnostic

The project I'm working on right now has undecidable problems all over it. It's a unit test generator, so in general what it tries to accomplish is to answer the question "what this program does". Which is an instance of a halting problem. Another problem that came up during development is "are given two (testing) functions the same"? Or even "does the order of those two calls (assertions) matter"?

What's interesting about this project is that, even though you can't answer those questions in all situations, you can find smart solutions that solve the problem 90% of the time, which for this domain is actually very good.

Other tools that try to reason about other code, like optimizing compilers/interpreters, static code analysis tools, even refactoring tools, are likely to hit (thus be forced to find workarounds to) the halting problem.

Solution 4 - Language Agnostic

Example 1. How many pages in my report?

When I was learning to program I played with making a tool to print out pretty reports from data. Obviously I wanted it to be really flexible and powerful so it would be the report generator to end all report generators.

The report definition ended up being so flexible that it was Turing complete. It could look at variables, choose between alternatives, use loops to repeat things.

I defined a built-in variable N, the number of pages in the report instance, so you could put a string that said "page n of N" on each page. I did two passes, the first one to count the pages (during which N was set to zero), and the second to actually generate them, using the N obtained from the first pass.

Sometimes the first pass would compute N, and then the second pass would generate a different number of pages (because now the non-zero N would change what the report did). I tried doing passes iteratively until the N settled down. Then I realised this was hopeless because what if it didn't settle down?

This then leads to the question, "Can I at least detect and warn the user if the iteration is never going to settle on a stable value for the number of pages their report produces?" Fortunately by this time I had become interested in reading about Turing, Godel, computability etc. and made the connection.

Years later I noticed that MS Access sometimes prints "Page 6 of 5", which is a truly marvelous thing.

Example 2: C++ compilers

The compilation process involves expanding templates. Template definitions can be selected from multiple specialisations (good enough to serve as a "cond") and they can also be recursive. So it's a Turing complete (pure functional) meta-system, in which the template definitions are the language, the types are the values, and the compiler is really an interpreter. This was an accident.

Consequently it is not possible to examine any given C++ program and say whether the compiler could in principle terminate with a successful compilation of the program.

Compiler vendors get around this by limiting the stack depth of template recursive. You can adjust the depth in g++.

Solution 5 - Language Agnostic

Many many moons ago I was assisting a consultant for our company who was implementing a very complex rail system to move baskets of metal parts in and out of a 1500-degree blast furnace. The track itself was a fairly complex 'mini-railyard' on the shop floor that intersected itself in a couple of places. Several motorized pallets would shuttle baskets of parts around according to a schedule. It was very important that the furnace doors were open for as short a time as possible.

Since the plant was in full production, the consultant was unable to run his software in 'real time' to test his scheduling algorithms. Instead, he wrote a pretty, graphic-y simulator. As we watched virtual pallets move around on his on-screen track layout, I asked "how will you know if you have any scheduling conflicts?"

His quick answer, "Easy - the simulation will never stop."

Solution 6 - Language Agnostic

Sophisticated static code analysis can run into the halting problem.

For example, if a Java virtual machine can prove that a piece of code will never access an array index out-of-bounds, it can omit that check and run faster. For some code this is possible; as it gets more complex it becomes the halting problem.

Solution 7 - Language Agnostic

This is still a problem for shaders in GPU applications. If a shader has an infinite loop (or a very long calculation), should the driver (after some time limit) stop it, kill the fragment, or just let it run? For games and other commercial stuff, the former is probably what you want, but for scientific/GPU computing, the latter is what you want. Worse, some versions of windows assume that since the graphics driver has been unresponsive for some time, it kills it, which artificially limits the computing power when doing computation on the GPU.

There's no API for a application to control how the driver should behave or set the timeout or something, and there's certainly no way for the driver to tell if your shader is going to finish or not.

I don't know if this situation has improved recently, but I'd like to know.

Solution 8 - Language Agnostic

Another common version of this is "we need to eliminate any deadlocks in our multi-threaded code". A perfectly-reasonable request, from the management perspective, but in order to prevent deadlocks in the general case, you have to analyse every possible locking state that the software can get into, which is, no surprise, equivalent to the halting problem.

There are ways to partially "solve" deadlocks in a complex system by imposing another layer on top of the locking (like a defined order of acquisition), but these methods are not always applicable.


Why this is equivalent to the halting problem:

Imagine you have two locks, A and B, and two threads, X and Y. If thread X has lock A, and wants lock B also, and thread Y has lock B and wants A too, then you have a deadlock.

If both X and Y have access to both A and B, then the only way to ensure that you never get into the bad state is to determine all of the possible paths that each thread can take through the code, and the order in which they can acquire and hold locks in all those cases. Then you determine whether the two threads can ever acquire more than one lock in a different order.

But, determining all of the possible paths that each thread can take through the code is (in the general case) equivalent to the halting problem.

Solution 9 - Language Agnostic

Perl's testing system maintains a test counter. You either put the number of tests you're going to run at the top of the program, or you declare that you're not going to track it. This guard against your test exiting prematurely, but there are other guards so it's not all that important.

Every once in a while somebody tries to write a program to count the number of tests for you. This is, of course, defeated by a simple loop. They plow ahead anyway, doing more and more elaborate tricks to try and detect loops and guess how many iterations there will be and solve the halting problem. Usually they declare that it just has to be "good enough".

Here's a particularly elaborate example.

Solution 10 - Language Agnostic

I was once working on an integration project in the ATM (Automated Teller Machines) domain. The client requested me to generate a report from my system for transactions sent by the country switch which were not received by my system!!

Solution 11 - Language Agnostic

I found a Berkeley paper: Looper: Lightweight Detection of Infinite Loops at Runtime http://www.eecs.berkeley.edu/~jburnim/pubs/BurnimJalbertStergiouSen-ASE09.pdf

LOOPER may be useful since most infinite loops are trivial errors. However, this paper doesn't even mention the halting problem!

What do they say about their limitations?

> [LOOPER] typically cannot reason about loops where non-termination > depends on the particulars of heap mutation in every loop iteration. > This is because our symbolic execution is conservative in > concretizing pointers, and our symbolic reasoning insufficiently > powerful. We believe combining our techniques with shape analysis > and more powerful invariant generation and proving would be valuable > future work.

In other words, "the problem will be fixed in the next release".

Solution 12 - Language Agnostic

From the Functional Overview of (Eclipse) Visual Editor:

> The Eclipse Visual Editor (VE) can be > used to open any .java file. It then > parses the Java source code looking > for visual beans. ... > > Some visual editing tools will only > provide a visual model of code that > that particular visual tool itself has > generated. Subsequent direct editing > of the source code can prevent the > visual tool from parsing the code and > building a model. > > Eclipse VE, however, ... can either be > used to edit GUIs from scratch, or > from Java files that have been > 'hardcoded' or built in a different > visual tool. The source file can > either be updated using the Graphical > Viewer, JavaBeans Tree or Properties > view or it can be edited directly by > the Source Editor.

Maybe I should stick with Matisse for now.

Unrelated, here's someone asking for the halting problem within Eclipse.

To be fair, VE's domain is quite limited, and it probably won't go crazy over tricky things like reflection. Still, the claim to build GUI out of any java file seems halt-ish.

Solution 13 - Language Agnostic

"How can you assure me your code is 100% free of bugs?"

Attributions

All content for this solution is sourced from the original question on Stackoverflow.

The content on this page is licensed under the Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) license.

Content TypeOriginal AuthorOriginal Content on Stackoverflow
QuestionClaudiuView Question on Stackoverflow
Solution 1 - Language AgnosticKirk StrauserView Answer on Stackoverflow
Solution 2 - Language AgnosticFerruccioView Answer on Stackoverflow
Solution 3 - Language AgnosticMichał KwiatkowskiView Answer on Stackoverflow
Solution 4 - Language AgnosticDaniel EarwickerView Answer on Stackoverflow
Solution 5 - Language Agnosticn8wrlView Answer on Stackoverflow
Solution 6 - Language AgnosticJason CohenView Answer on Stackoverflow
Solution 7 - Language AgnosticjoeldView Answer on Stackoverflow
Solution 8 - Language AgnosticMark BesseyView Answer on Stackoverflow
Solution 9 - Language AgnosticSchwernView Answer on Stackoverflow
Solution 10 - Language AgnosticJaywalkerView Answer on Stackoverflow
Solution 11 - Language AgnosticKevin KostlanView Answer on Stackoverflow
Solution 12 - Language AgnosticGeoffrey ZhengView Answer on Stackoverflow
Solution 13 - Language AgnosticzaratustraView Answer on Stackoverflow