The halting problem is decidable on a set of asymptotic probability one (2006)
projecteuclid.org
projecteuclid.org
I managed to solve all BF programs up to length 12. The longest running but stopping short program that I've found was this: >+[>++>+++[-<]>>], it stopped after 9212 steps.
With 8 possible instructions, that is equivalent to all programs up to 12 * log 8 = 36 bits. Curiously, that exactly matches how far we were able to analyze the behaviour of a functional busy beaver [1].
> it stopped after 9212 steps.
The largest output of a 36 bit lambda term is a whopping 578960446186580977117854925043439539266349923328202820197287920039565648199686 bits long though...
I've never properly learned brainfuck, so the answer to this might be trivial without needing to write a solver, but what's the shortest non-halting program you found?
Brainfuck's state consists of an array of integers, an index into that array, a program counter, and some bookkeeping required to track which "[" corresponds to which "]".
Let's assume the array a[:] is zeroed and the index i is set to 0 before the program begins executing.
Then `+` increments the cell in the array a at index i, i.e. `a[i] += 1`; `[` begins a while loop, equivalent to `while a[i] != 0 {`; and `]` ends the while loop: `}` .
So the program `+[]` is equivalent to something like
a := (allocate a length N array of bytes, set to zero)
i := 0
a[i] += 1
while a[i] != 0 {
}
Why is this the shortest?
`]` is the only instruction that might decrease the program counter, otherwise the program counter always increases by one or more. Therefore, a non-halting brainfuck program must include at least one `]`. Brainfuck programs are syntactically incorrect unless there is exactly one `]` occurring somewhere in the program after each `[`. So the shortest non-halting brainfuck program must have at least two instructions.
There is only one syntactically valid brainfuck program with two instructions that might not halt: `[]`. But this will halt, assuming that the array `a` is initialised to zero before execution begins. So the shortest non-halting brainfuck program contains three instructions.
In practice it may not there may not be enough resources to build something to enumerate all the states on all inputs, but we are talking theoretically here. Theoretically, there is no halting problem in a finite world. And we humans live in what looks to be a locally finite world, so it doesn't apply to us.
The halting problem is actually a statement on whether it's possible to always determine if a finite set of rules that have infinite memory will halt on all inputs. The answer is famously no. Thus the halting problem illustrates a property of infinities. It's a subtlety that's rarely mentioned.
It is an interesting property. One thing it says to me is there are things in an infinite world a finite computation machine (like our human brains) will never be able to understand. While locally (say within the Milky Way) we live in a finite world the Universe itself may well be infinite. Ergo, there may be some aspects of the Universe we can never understand, and some things may happen that we can never predict.
You could try defining H to only work on input machines smaller than itself. However there’s still problems.
If you don’t limit input size (aka the I in H(M,I) does machine M halt on input I), your code would still get tricked if M is just a tiny emulator and the input is the whole self defeating H program. So M and I both must be limited.
Anyway that’s not to say a finite H would work even if the input size is limited. You’d have to prove it’s impossible to self recurse - so you’d need good compression.
That’s all assuming self recursion is the only problem with the halt programs. Maybe it’s not, and it seems difficult to rule out other problems and see how they’d affect finitely bound TMs.
I’m just spitballing here. For a while I was infatuated by the idea of snuffing out self recursion or otherwise somehow making a variant of halting programs possible. But self referential poison seems really, really tough to prove the non existence of.
Anyways, I’m of the attitude that the proof for halting problem undecidability is a dumb trick. I’m simply fine with a halting program that doesn’t work correctly in self referential cases. As above though, that just leaves the whole problem vague aka don’t know about other issues and there’s the problem of actually solving it anyways (aka solving all of mathematics at once).
So it's definitely possible to decide halt problem for a bounded computer (any physical computer), it's just not practical in most cases, e.g. amount of memory needed to store graph of all states be bigger than amount of matter in the universe, etc.
The inputs to a halting decider TM is an infinite set (all TMs and all inputs to them) so that’s another reason why a finite graph can’t be represented. Even something like integer addition isn’t a finite graph if you enumerate all inputs
Sure one can say input is coming from a network stream then what? For practical issues then we can limit input size to N bits ... For theoretical issues we can discuss if there is a difference between halting or waiting for more input :)
It's a pretty trivial question in any language, it tends to just be while(true); or similar in that language.
For combinatory logic with the usual {S,K} basis, it's S S K (S (S S K).
Just for a short taste, in the lambda calculus the base entity is an abstract function that can be applied to a variable and return a result. You are probably familiar with formulae like `f(x) = x`. In the lambda calculus formalism, this is written as `\lambda x.x`. However, it's important to note that there is no direct equivalent to something like `f(x) = x + 1` - addition or numbers are not a part of the lambda calculus directly. Instead, you can define numbers and then addition in terms of functions and variables.
Instead, the lambda calculus has rules for how function application should work to reduce complex formulae to simpler ones. For example, `(\lambda x.x) y` reduces to `y` [equivalent to f(x) = x; f(y) = ? => y]. Or, `(\lambda x.y) z` reduces to `y` [equivalent to f(x) = y; f(z) = ? => y]. And, if we go on to more complex expressions: `(\lambda x.x) (\lambda x.y) z` reduces to y by applying the reductions above successively (first we reduce the initial expression to `(\lambda x.x) y` then we reduce this to just `y`.
It can be shown that this model of how to reduce the formulae of lambda calculus is in fact equivalent to the model of the Turing machine that can write a symbol on its tape.
- https://www.cs.cornell.edu/courses/cs3110/2008fa/recitations...
> Proof of the Main Theorem Using the standard model
> let B be the set of programs that on input 0 either halt before repeating a state or fall off the tape before repeating a state. Clearly, B is polynomial time decidable, since we need only run a program p for at most n steps, where n is the number of states in p, to determine whether or not it is in B. It is equally clear that the halting problem is polynomial time decidable for programs p in B, since again we need only simulate p for n steps to know whether it halted or fell off. What remains is to prove that this behavior occurs with asymptotic probability one.
The proof also makes use of this
> Lemma 2.5 (Polya [2], see also, e.g., [1])
> In the random walk with equal likelihood of moving left or right on a semi-infinite tape, beginning on the left-most cell, the probability of eventually falling off the left edge is 1.
This suggests that the result crucially depends on having a one-sided infinite tape rather than the two-sided infinite tape that's used in the Turing Machine busy beaver.
It would be interesting to determine whether the result also holds for that other computational model, i.e. what about the set of lambda calculus terms with or without a normal form?
> Clearly, B is polynomial time decidable, since we need only run a program p for at most n steps, where n is the number of states in p, to determine whether or not it is in B.
Couldn't program p have an exponential number of states, e.g. 2^|p| distinct program states? Then running the program for O(2^|p|) steps is clearly not polynomial time decidable in the size of the instance. I thought polynomial time, for the decision algorithm, meant O(|p|^c) for some c. Am I mistaken about something?
This theorem is not about programs B whose tape contents is linear in the length of the encoding of the program.
It’s a misreading of the halting problem to think of it as a ‘barrier’ of some sort. What it really means is that there are some computer programs where the only way to find out what they will do is to actually run them. There’s not a ‘better trick’ you can pull to get the answer. This is kind of intuitive, since we know there are problems we run into where the easiest way we can think of to solve them is to write a program and run it. The halting problem tells us that it’s plausible that that instinct is right - that for some programs, you really can’t do some other analysis of the program that tells you what it’s going to do. You have to just run it.
Like: take a random complex number with magnitude < 2. Keep squaring it and adding the original number. Will you ever get a number with magnitude > 2?
For some numbers you can take a shortcut and say yes or no. But for others the only way to find out is to keep doing it.
This isn't quite right. The halting problem says that you can't just run it. If you just run it, you will not learn whether or not it halts after any finite amount of time.
Also I don't see how this is related to uncertainty bounds.
If it halts within a finite amount of time, you will.
So, we agree!
I don't think this is correct. In fact, in certain systems, the Heisenberg uncertainty can get amplified as the number of particles increases - which is why we end up needing the addition of the Born rule in QM to predict classical observations, and can't just deduce them from the base equations. And also why we end up predicting a particle can go either left with some probability or right with one minus that probability, instead of being able to say "that particle will go right".
The point of the analogy was that the halting problem - like the uncertainty principle - is a result that says that you can’t know certain things about systems - and with small systems in particular figuring that out can be as complex as the system itself. But they don’t prevent us from doing useful things with larger systems. It struck me as a similar result to this paper - though only by analogy, not like, in some deep way.
The fact that classical objects have deterministic trajectories is not a consequence of statistics + Heisenberg uncertainty, it is explicitly in contradiction to Heisenberg uncertainty, requiring an extra element to be added to the theory (the Born rule).
This certainly makes intuitive sense, since it explains why we don't have trouble measuring both the speed and position of objects in everyday life with fairly high precision.
Anyways, if anyone is interested is a more complete survey of similarly flavored computability/density results, this paper is good: https://faculty.math.illinois.edu/~jockusch/DensityCE_JML.pd...
There is even some pure combinatorics involved, for example I remember lemma 6.7 from my combinatorics class back in undergrad
This relates nicely to the earlier discussion of SAT: while SAT is NP-complete, many instances can be solved in reasonable time. Similarly, we can verify that many actual programs will halt even if the problem is, in general, undecidable.
[1] https://mathwithbaddrawings.com/2016/12/28/why-the-number-li...
[2] There’s a finite set of programs of a fixed length, thus (countable union of finite sets) a countable set of all programs, thus only at most a countable set of numbers they can compute.
[3] Every countable set has Lebesgue measure zero: cover point #n by a blot of measure ε / 2^n (that could even intersect other blots) to prove all of them have measure at most ε > 0, take ε as small as desired.
b) Neither is equality computable for the reals. Nothing is lost here.
c) Differentiation is computable for the functions of computable reals if you have a computable rate of convergence.
In a sense. You would end up with https://en.wikipedia.org/wiki/Automatic_differentiation.
The amount of functions you can construct in this manner is massive, along with their derivatives, but it is not an operator that given an arbitrary computable function gives you its derivative.
There isn’t a single universally appropriate choice here, and sometimes even the direction of the axis is not obvious (real numbers lack solutions for algebraic equations; complex numbers lack smooth functions nonzero only in a finite region), but usually a simple family of eldritch objects is easier to deal with than an byzantine clan of cuddly objects.
Could you do simple physics and more generally ordinary differential equations over the computable numbers? You probably could to some extent, but it’s unlikely you’d get the nice intuitive geometry you get over the reals (see e.g. Arnold’s ODE textbook). The (basic) geometry of surfaces parametrized by real coordinates is fairly straightforward (differential geometry); the geometry of surfaces parametrized by rational coordinates is famously mind-blowingly abstract (algebraic geometry). The (basic) theory of real or complex functions is mostly understandable (analysis); the theory of natural or rational functions is horrifying (number theory).
Also, as a sibling reply mentions, it’s not like computable numbers will solve every problem: even though arithmetic over them is decidable, order still isn’t, and computable transcendental functions aren’t exactly a cakewalk either.
It doesn’t mean the computable reals aren’t worth knowing about, but, well, we live in a world where mandatory education has violently rejected[2] every advance in mathematical thought since Otto von Bismarck left office, and reduced the ones it accepted to a desiccated husk[3], so there are a great many things in that category. (I cannot help but remember the SMBC patriotism vs nationalism comic[4]: “Now I am mathematics.”)
[1] https://ncatlab.org/nlab/show/dichotomy+between+nice+objects...
[2] http://www.ams.org/notices/201201/rtx120100031p.pdf
[3] https://www.maa.org/external_archive/devlin/devlin_03_08.htm...
[4] https://www.smbc-comics.com/comic/an-important-distinction
You are also going to encounter other funny things. One of De Morgan’s laws failing could seem troubling but ultimately theoretical—how, then, about the distinction about countable and constructively countable[3]? The set of all programs is countable; the set of all terminating programs is a subset of it, but can’t constructively be proven to itself be countable—after all, that would imply a solution to the halting problem! (Neither can it constructively be proven to not be such, as it is such in a consistent extension, namely classical mathematics.) Thus you get the new and exciting notion of subcountable sets. And that’s one of the mildest things that you’re going to encounter in your shiny new theory of cardinals.
(Anybody who can explain to me what the hell constructive Hahn—Banach[4] is about gets a beverage of their choice if we are ever in the same city. Without HB, you cannot do any functional analysis worth a damn, and without that you can’t really talk about Green’s functions / fundamental solutions to linear PDEs, which are in turn a basic tool for any electodynamics or quantum mechanics worth speaking about. Unless you want to forgo proof or the natural sciences, you need it, is my point.)
None of this is to say that I think intuitionistic logic is useless, mind you. It’s interesting and useful[5]! But so far it seems that you need to learn at least some logic (as a piece of mathematics and not mere terminology, so including scary words like “metalogic”) before you can really understand how it comes together.
[1] It seems categorical logic[2] says useful things about what the One True Definition should be? But I don’t understand it well enough to tell, and in any case the constructivist tradition predates not only it but category theory in general.
[2] https://mikeshulman.github.io/catlog/catlog.pdf
[3] https://ncatlab.org/nlab/show/constructive+mathematics
[4] https://www.cse.chalmers.se/~coquand/hahn1.pdf
[5] https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016...
As for Hahn—Banach I can only site the book “Techniques of Constructive Analysis” by Douglas S. Bridges:
For example, our proof of the Hahn-Banach theorem (Theorem 5.3.3) is, as it stands, a valid algorithmic proof of the classical Hahn Banach theorem. Moreover and this is one advantage of a constructive proof in general our proof embodies an algorithm for the construction of the functional whose existence is stated in the theorem. This algorithm can be extracted from the proof, and, as an undeserved bonus, the proof itself demonstrates that the algorithm is correct or, in computer science parlance, "meets its specifications". …
The Hahn-Banach theorem enables us to extend a normed linear functional, with an arbitrarily small increase in norm, from a subspace of a normed space to the entire space. This fundamental result has numerous applications throughout functional analysis.
In the constructive context we deal only with the extension of linear functionals on subspaces of a separable normed space. The standard classical proofs extending the theorem to nonseparable normed spaces depend on Zorn's lemma and are therefore nonconstructive. … The classical Hahn-Banach theorem says that we can extend a bounded linear functional v from Y to a functional u on the whole space X with exact preservation of norm. In general, as Exercise 5 shows, we cannot do this constructively. But, as we shall see, if we impose extra conditions on the norm of X, then we can make the extension norm-preserving.
I thought this had to do with the difference between being computable and computably enumerable.
[0] Looking back, the core of my confusion was this. I had thought: I can visualize what ℵ0 means; that’s just the infinity of integers. I can also visualize what C=2^ℵ0 means; that’s the infinity of points on a line. Those, therefore, are the two bedrocks of clarity in this discussion. By contrast, I can’t visualize a set of intermediate cardinality between ℵ0 and C. The intermediate infinity, being weird and ghostlike, is the one that shouldn’t exist unless we deliberately “force” it to.
Turns out I had things backwards. For starters, I can’t visualize the uncountable infinity of real numbers. I might think I’m visualizing the real line—it’s solid, it’s black, it’s got little points everywhere—but how can I be sure that I’m not merely visualizing the ℵ0 rationals, or (say) the computable or definable reals, which include all the ones that arise in ordinary math?
The continuum C is not at all the bedrock of clarity that I’d thought it was. Unlike its junior partner ℵ0, the continuum is adjustable, changeable—and we will change it when we build different models of ZFC. What’s (relatively) more “fixed” in this game is something that I, like many non-experts, had always given short shrift to: Cantor’s sequence of Alephs ℵ0, ℵ1, ℵ2, etc.
Suppose you have one undecidable statement, U, out of s possible statements. A random program of length n contains U at least once with probability 1-(1-1/s)^n. If the program is of infinite length, it contains U with probability 1. So I would have thought the chances of undecidability increase as the program gets longer.
Clearly my intuition is wrong, per the paper, but I don't think the result is immediately obvious.
So if you make a random TM, it's almost guaranteed that it'll get eventually "trapped" in one of these easily decidable infinite loops.
There isn't really a single undecidable statement, it would be a complex subroutine. My intuition would be its much more likely a halt or indef loop (both relatively simple) would appear before program control would transfer to the undecidable part, in most cases.
I.e. if something undecidable requires 60 symbols in a row in correct order, but halting requires one, than probability of a halt at any given spot seems much higher on average.
For non-random instances the ratio of clauses to variables in is utterly meaningless.
Also look up Buridan’s Principle by Leslie Lamport. I emailed him and “argued” with him for a while after reading his paper, but in a theoretical sense and some practical subsets it is correct!
For example, in classical thermodynamics there is a nonzero probability that all the air molecules in a room will happen to travel to one side, violating many laws of fluid mechanics. In quantum mechanics the situation is even worse, where basically anything can happen with nonzero probability.
It took me some time to realize that that's what "HitchHiker's Guide to Galaxy" was about.
It would be interesting to see how long we are capable of running even just a while true
The power might go out, some electronic component might fail, or the cooling system, etc
What is the longest that we are actually capable of keeping the most simple system running?
You could argue that the timekeeping of TAI (https://en.wikipedia.org/wiki/International_Atomic_Time) could be seen as a distributed computation (where different entities are counting the same value and running manual and automated protocols to keep the value synchronized), and that has been running since 1972. It almost certainly hasn't been running continuously on any individual hardware device, but there have always been devices that represented its value and always been efforts to maintain continuity between calculations.
Although I guess the same logic could argue for civil timekeeping in any calendar, because people have actively tracked it as "the same computation" and cared about it for centuries or millennia. Maybe the distinctive argument for TAI is that it's presumably been continually represented digitally in programmable computers since 1972.
This makes the result a lot less interesting. Sure random programs will typically halt before long, but with an illegal memory access ( in the parlance of the article, they read from the left of the turing tape)
"For the purposes of defining the halting problem H, one should specify whether it officially counts as halting or not if the head should happen to fall off the left edge of the tape. Although the truth of the main theorem will not depend on these details, provided we adopt a uniform answer, let us be definite and regard such computations as having not officially halted, as the halt state was not reached."
> For the purposes of defining the halting problem H, one should specify whether it officially counts as halting or not if the head should happen to fall off the left edge of the tape. Although the truth of the main theorem will not depend on these details, provided we adopt a uniform answer, let us be definite and regard such computations as having not officially halted, as the halt state was not reached.
Any other machine that can simulate a turing machine can simulate failing in those same ways. You can't escape the problems of turing completeness without losing it.
So, if you want to prove something about the limits of computation, a Turing machine is usually the right choice.
[0]: https://en.wikipedia.org/wiki/Interaction_nets [1]: https://github.com/HigherOrderCO/HVM
It seems to me a more complex lambda calculus.
So, most likely, the real reason nobody is interested is that the numbers are too large.
The fallacy in this argument lies in the assumption that Beta is computable. It would be true if we could enumerate the computable sequences by finite means, but the problem of enumerating computable sequences is equivalent to the problem of finding out whether a given number is the D.N of a circle-free machine, and we have no general process for doing this in a finite number of steps.[1]
[1] On computable numbers https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf