26

I was just reading another explanation of the halting problem, and it got me thinking all the problems I've seen that are given as examples involve infinite sequences. But I never use infinite sequences in my programs - they take too long. All the real world applications have lower and upper bounds. Even reals aren't truly reals - they are approximations stored as 32/64 bits etc.

So the question is, is there a subset of programs that can be determined if they halt? Is it good enough for most programs. Can I build a set of language constructs that I can determine the 'haltability' of a program. I'm sure this has been studied somewhere before so any pointers would be appreciated. The language wouldn't be turing complete, but is there such a thing as nearly turing complete which is good enough?

Naturally enough such a construct would have to exclude recursion and unbounded while loops, but I can write a program without those easily enough.

Reading from standard input as an example would have to be bounded, but that's easy enough - I'll limit my input to 10,000,000 characters etc, depending on the problem domain.

tia

[Update]

After reading the comments and answers perhaps I should restate my question.

For a given program in which all inputs are bounded can you determine if the program halts. If so what are the constraints of the language and what are the limits of the input set. The maximal set of these constructs would determine a language which can be deduced to halt or not. Is there some study that's been done on this?

[Update 2]

here's the answer, it's yes, way back in 1967 from http://www.isp.uni-luebeck.de/kps07/files/papers/kirner.pdf

That the halting problem can be at least theoretically solved for finite-state systems has been already argued by Minsky in 1967 [4]: “...any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine...”

(and so if you stick to finite turing machines then you can build an oracle)

daven11
  • 769
  • 5
  • 11
  • 20
    "infinite sequences... take too long". Made me laugh out loud. – Bryan Oakley Dec 19 '11 at 03:35
  • http://scienceblogs.com/goodmath/2008/12/my_favorite_strange_number_cla.php - This wouldn't be the post read in question? –  Dec 19 '11 at 03:38
  • @World - it was indeed - it popped up on hacker news – daven11 Dec 19 '11 at 04:48
  • 3
    I believe SQL92 and Regular Expressions are examples of languages that are guaranteed to halt. – Elian Ebbing Dec 19 '11 at 13:24
  • 2
    Please post "Update2..." as an answer. – S.Lott Dec 19 '11 at 16:38
  • There are an infinite number of subsets of programs which avoid the halting problem. – Peter Taylor Dec 19 '11 at 22:38
  • A duplicate: http://stackoverflow.com/questions/8412741/existence-of-a-programming-language-guaranteed-termination – SK-logic Dec 20 '11 at 11:31
  • 2
    You do not need to exclude recursion. If you limit the recursion to strict sub-terms of the callee arguments you'll always be able to prove termination. It is a sufficient requirement - no "bounded loops" and alike are necessary, as long as you're using the Church numerals. – SK-logic Dec 20 '11 at 11:49
  • 1
    The language Idris uses dependent typing and a proof checker to prove your programs terminate before running them. It's similar to Haskell and allows recursion, but not *general* recursion - only recursion that it can prove (through the dependent types) leads to some terminal state. – Jack Dec 16 '14 at 00:52
  • See NASA's 10 Rules for Developing Safety-Critical Code: https://en.wikipedia.org/wiki/The_Power_of_10:_Rules_for_Developing_Safety-Critical_Code (full text: http://web.eecs.umich.edu/~imarkov/10rules.pdf). It classifies programs into two categories: halting and never-halting. – Dávid Horváth Jun 03 '21 at 09:50
  • [**Halting problem proofs refuted on the basis of software engineering**](https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering) – polcott Jul 05 '22 at 16:27
  • _"Can I build a set of language constructs that I can determine the 'haltability' of a program."_ It's funny how every supposed way around the halting problem inherently bring it all back to needing to do precisely what the halting problem tells you that you can't do. Part of the observation whether that a program halts or not is that you are _independently_ able to verify it. Depending on a language construct to do it for you infringes on that independent verification. [..] – Flater Jul 12 '22 at 14:09
  • [..] The question isn't whether the runtime is ended, it's whether the _algorithm_ would _choose_ to end itself. This is not "solved" by considering non-finite integers due to an implementation constraint of not being able to house literally infinite binary digits in computer memory. The heat death of the universe, the finite battery that a computer runs on, number overflow due to memory constraints, or blind trust in a language construct is not a valid "halt" in this sense. – Flater Jul 12 '22 at 14:11

9 Answers9

12

First off, consider what would happen if we had a halting detector. We know from the diagonal argument that there exists at least one program that would cause a halting detector to either never halt or give a wrong answer. But that's a bizarre and unlikely program.

There is another argument though that a halting detector is impossible, and that is the more intuitive argument that a halting detector would be magical. Suppose you want to know if Fermat's Last Theorem is true or false. You just write a program that halts if it is true and runs forever if it is false, and then run the halting detector on it. You don't run the program, you just run the halting detector on the program. A halting detector would enable us to immediately solve a huge number of open problems in number theory just by writing programs.

So, can you write a programming language that is guaranteed to produce programs whose halting can be always determined? Sure. It just cannot have loops, conditions and use arbitrarily much storage. If you're willing to live with no loops, or no "if" statements, or a strictly restricted amount of storage, then sure, you can write a language whose halting is always determinable.

Eric Lippert
  • 45,799
  • 22
  • 87
  • 126
  • 3
    One can have the if statement if the jump always has to be forward, never backwards. I am thinking of a restricted subset of BASIC language, where "GOTO X" means go to the line number currentLine + X, and X must be greater than 0. If the line is invalid, then halt. This would up the storage demands, but would allow for some non-trivial logic. This is probably equivalent to a finite state machine where the vertices form a graph and that graph may not have any cycles, or else the FSM is invalid. Also, any state that is a dead end must be an accepting state. – Job Dec 19 '11 at 03:56
  • 3
    it could have bounded loops - for i=1 to 10 for example, likewise well behaved iterators. So is there a class of finite problems that can be solved - fermats theorem is again involved in the infinite sequence of reals. But if we restrict the domain to numbers less than 1 000 000 then it does halt. – daven11 Dec 19 '11 at 04:51
  • 2
    Why not conditions? It seems that conditions without jumps can be shown to always halt... – Billy ONeal Dec 19 '11 at 05:41
  • I think your "intuitive argument" is a bit weak: It is possible to write a program that will find a proof for any problem that's provable or disprovable. No magic needed, just a lot of time. It's the propositions like the continuum hypotheses that can't be proven or proven wrong (at least in some axiom systems) that are the problem: If you wrote a program for such a problem, the halting detector would have to decide after a finite amount of time that the CH is provable or disprovable. And it would be wrong in either case. – nikie Dec 19 '11 at 07:48
  • @BillyONeal how would a condition without a jump work? –  Dec 19 '11 at 09:35
  • @nikie: It would be easy to write a brute-force program to test Goldbach's Conjecture, for example (that all even numbers > 2 are the sum of two primes). If we could determine whether it halts, that would be a proof or disproof. If we put any limits on it (necessary to avoid the halting problem) we know if it's true on numbers smaller than some specific one, not in general. Similarly, a computer-generated proof could wind up being arbitrarily lengthy, and not generatable on a specific finite system. – David Thornley Dec 19 '11 at 15:10
  • 3
    @nikie: Of course it is a weak argument. The point is that such a halting detector would be able to prove or disprove such statements **without necessarily finding the proof**. The intuition that I'm intending the reader to develop here is that a language for which a trivial halting detector could be written is a language that cannot represent even simple problems in number theory like Fermat's Last Theorem or Goldbach's Conjecture, and therefore probably is not a very useful language. – Eric Lippert Dec 19 '11 at 15:12
  • @Eric Lippert: It probably wouldn't be a very useful *general purpose* language. But if you were writing e.g. some function called in from the inner loop of a pacemaker, not being able to write an unbounded while-loop might be a minor inconvenience, compared to the additional security – nikie Dec 19 '11 at 16:09
  • @nikie: Sure. Or you could consider programming languages like HTML that are entirely declarative (leaving JavaScript out of the mix). Those are certainly useful languages for their specific domains. Of course, it often does not take very many additional features for even a simple DSL to become Turing-complete. – Eric Lippert Dec 19 '11 at 16:22
  • @Thorbjørn Ravn Andersen: I suppose there's a jump there; but it's restricted in that a condition can never jump backwards, and therefore can't be used to build looping-like constructs (and therefore can't cause the system to not halt) – Billy ONeal Dec 19 '11 at 19:46
  • @EricLippert These are interesting problems, but again they operate on the reals which are infinite. If you use the reals as implemented in a machine then you can find if it halts or not it seems. I was thinking more about applications implemented on machines - not proving mathematical theorems. – daven11 Dec 19 '11 at 21:59
  • 1
    @daven11: They operate on the *integers*, not the *reals*. What's the difference in your mind between writing "applications" and writing programs that do "math"? As far as I'm concerned, *they are the same thing*. An axiomatic proof system is just a list of legal start states (axioms) and rules for determining new "valid" states from old ones. That's all a program is; you start with a particular program state and the rules of the program determine what legal future states are. The history of the state of any particular program is a *proof* that the state is possible. – Eric Lippert Dec 19 '11 at 22:14
  • @EricLippert again integers are infinite, not as infinite as reals but still infinite. Integers (and reals) are abstractions, what a computer uses are approximations to these. Integers in a machine are bounded to the bit size used to represent them. So any machine that calculates integer values has bounds and so can be determined to halt it seems. – daven11 Dec 19 '11 at 22:27
  • 1
    @daven11: What prevents computers from allocating arbitrarily many bits for an integer? Why can't I have a thousand-bit integer or a million-bit integer? The BigInteger class in C# does exactly that. The fact that some hardware happens to be *optimized* for 32 bit math is irrelevant. – Eric Lippert Dec 19 '11 at 22:31
  • @EricLippert: But there's still a limit, available memory is a limit, or if you can page out then available disk space is a limit. Nowadays it's a big limit but still a limit. In the absolute limit it's the number of available quantum states in the universe - a fairly large number I'll grant but still a limit. – daven11 Dec 20 '11 at 00:31
  • @daven11: I'll grant you that the universe is large but finite. I'm not seeing your point. You don't need to posit computers the size of the sun with atoms for bits; a "computer" made out of a thousand scrabble tiles pushed around on a tabletop is already too big for us to analyze practically. – Eric Lippert Dec 20 '11 at 00:41
  • @EricLippert: I'm not sure what my point is at this stage, though it's an interesting discussion. The original question was re the halting problem for finite machines, and that seems to be answered. I'm starting to wonder if there's something more fundamental in the discussion about infinite numbers - they're not realisable in a finite universe. A solution may still be NP hard though. So is there something more fundamental in this in the fact that all numbers we can use are finite no matter how big the computing device. – daven11 Dec 20 '11 at 01:17
  • @daven11: heck, you can't even write a computer program that *names* the transfinite ordinals, much less does *math* on them. If you're interested in problems in the space of "things computers can't do", you could do worse than to study the transfinite ordinals. – Eric Lippert Dec 20 '11 at 08:24
  • @EricLippert: Did a course on them many years ago - I thought it was one of the most elegant pieces of logic I'd ever come across, though I could never figure out what to do with them. My thinking is coming from the other way - if the universe can't contain infinity, then maybe we're looking at it wrong, what this means though I have no idea. – daven11 Dec 20 '11 at 08:41
  • 3
    @EricLippert: Wrong. Such a language will have loops, proper storage and many other useful things. It is possible to code *almost* anything in it. Behold, here it is: http://coq.inria.fr/ – SK-logic Dec 20 '11 at 11:29
  • @Job: forward jumping is not enough http://esolangs.org/wiki/SMITH – Thomas Eding Dec 16 '14 at 05:06
  • You could have a language that is just the same as whatever you use today, but automatically halts after 10^1000 steps. Halting problem solved. – gnasher729 Jul 12 '22 at 10:00
12

The issue isn't on the input (obviously, with unbounded input, you can have unbounded running time just to read the input), it is on the number of internal states.

When the number of internal state is bounded, theoretically you can solve the halting problem in all cases (just emulate it until you reach halting or the repetition of a state), when it isn't, there are cases where it isn't solvable. But even if the number of internal states is in practice bounded, it is also so huge that the methods relying of the boundedness of the number of internal states are useless to prove the termination of any but the most trivial programs.

There are more practical ways to check the termination of programs. For instance, express them in a programming language which hasn't recursion nor goto and whose looping structures have all a bound on the number of iterations which has to be specified on entry of the loop. (Note that the bound hasn't to be really related to the effective number of iterations, a standard way to prove the termination of a loop is to have a function which you prove is strictly decreasing from one iteration to the other and your entry condition ensure is positive, you could put the first evaluation as your bound).

AProgrammer
  • 10,404
  • 1
  • 30
  • 45
7

I recommend you to read Gödel, Escher, Bach. It's a very fun and illuminating book that, among other things, touches on Gödel's incompleteness theorem and the halting problem.

To answer your question in a nutshell: the halting problem is decidable as long as your program does not contain a while loop (or any of its many possible manifestations).

Jon Purdy
  • 20,437
  • 7
  • 63
  • 95
zvrba
  • 3,470
  • 2
  • 23
  • 22
  • Sorry, I misread you. I deleted my comment but I'll restate the recommendation of GEB. – AProgrammer Dec 19 '11 at 14:17
  • @zvrba That's been on my reading list for some time - probably time to dive in. – daven11 Dec 19 '11 at 22:28
  • You can allow any loops where an upper limit for the number of iterations is calculated before the loop starts. And other loops, like anything where some state has a complete ordering, the loop ends when the state is "small" enough, and each iteration of the loop leads to an earlier state in the ordering; this lets you write a program for the Big Ackermann function which is guaranteed to halt. (in theory). – gnasher729 Jul 12 '22 at 10:05
5

For every program that works on a limited amount of memory (including storage of all kind), the halting problem can be solved; i.e. an undecidable program is bound to take more and more memory on the run.

But even so, this insight doesn't mean that it can be used for real-world problems, since a halting program, working on just a few kilobytes of memory, can easily take longer than the remaining lifetime of the universe to halt.

user281377
  • 28,352
  • 5
  • 75
  • 130
3

To (partially) answer your question "Is there a subset of programs that avoid the halting problem": yes, in fact there is. However, this subset is amazingly useless (note that the subset I'm talking about is a strict subset of the programs that halt).

The study of the complexity of problems for 'most inputs' is called generic-case complexity. You define some subset of the possible inputs, prove that this subset covers 'most inputs' and give an algorithm that solves the problem for this subset.

For instance, the halting problem is solvable in polynomial time for most inputs (in fact, in linear time, if I understand the paper correctly).

However, this result is rather useless because of three side notes: firstly, we talk about Turing machines with a single tape, rather than real-world computer programs on real-world computers. As far as I know, no one knows whether the same holds for real-world computers (even though real world computers may be able to compute the same functions as Turing machines, the number of allowed programs, their lengths and whether they halt may be completely different).

Secondly, you have to watch out what 'most inputs' means. It means that the probability that a random program of 'length' n can be checked by this algorithm tends to 1 as n tends to infinity. In other words, if n is large enough, then a random program of length n can almost surely be checked by this algorithm.

Which programs can be checked by the approach described in the paper? Essentially, all programs that halt before repeating a state (where 'state' roughly corresponds to a line of code in a program).

Even though nearly all programs can be checked in this way, none of the programs that can be checked in this way are very interesting and they usually won't be designed by humans, so this is of no practical value whatsoever.

It also indicates that generic-case complexity will probably not be able to help us with the halting problem, as nearly all interesting programs are (apparently) hard to check. Or, alternatively phrased: nearly all programs are uninteresting, but easy to check.

Alex ten Brink
  • 2,121
  • 15
  • 14
  • 2
    -1, This is wrong on so many levels... – user281377 Dec 19 '11 at 20:19
  • 1
    First, real-worlds computers cannot compute anything that a Turing machine can't. Till now, nobody has shown a real-world computer more capable (in terms of computablity) than a Turing machine. Second, if a program repeats it's state, it won't halt, so the halting problem is solved for that program and input. Remember: The halting problem is about deciding whether or not a program will halt on given input. An infinite loop is ok once you positively detect it. Finally: There is a large set of useful programs for which the halting problem is solvable: Those operating on limited storage. – user281377 Dec 19 '11 at 20:26
  • As for your first issue: as remarked in the paper, showing that some model of computation is Turing complete does not preserve how many programs exactly halt, so the result they prove does not immediately mean anything for other models of computation. I'm well aware of Turing completeness, and I'm not completely sure why it makes my answer 'wrong'. – Alex ten Brink Dec 19 '11 at 21:50
  • As for your second issue: the states I'm talking about is not the same as the 'state of a machine' one usually talks about (which involves the state of everything that can have state), but rather the state the finite state automaton used to control the Turing machine is in, which roughly corresponds to the line of code a program is working on at any point during execution. On repeating a line of code the contents of your memory may be different, so this does not immediately imply halting at all. I'll update my answer to make this more clear. – Alex ten Brink Dec 19 '11 at 21:51
  • @ammoQ: No, the halting problem is not solvable if you are talking about real-world systems with limited storage, as that would mean building a real-world system that can handle combinations of states. As the number of possible register states in most CPUs exceeds the number of atoms in the Universe, you aren't going to be able to do that. – David Thornley Dec 19 '11 at 22:52
  • David: On a computer with n bits of storage, a program can run at most through 2^n different states before either looping or halting. While it is infeasible to build a computer with a 2^n bits (so you can mark each state that has been reached), all it really takes is a n bit counter; on every clock tick of the target system, just increase the counter by one. If it overruns, we have detected a loop. So we need a little bit of overhead for the program that handles the counter, but that is not the problem. We need some time, though, so the heat death of the universe might become an issue. – user281377 Dec 20 '11 at 07:42
  • Alex: Ok, now it's more clear what you mean. It should be more clearly said that the method described in the paper depends on the turing machine. I thought it was a general statement about the halting problem. The second issue is more clear now, too. So I'll take back the -1. – user281377 Dec 20 '11 at 08:05
  • It is somewhat insulting to call languages like Agda2 and Coq "amazingly useless". For example, there is a complete C compiler written in Coq. Is it a "useless" application for a language? – SK-logic Dec 20 '11 at 11:52
  • @ammoQ: That's similarly infeasible. Counting to something as low as 2^128 with anything resembling conventional computing would take more energy than the Sun will put out in the future. Theoretically, we're dealing with computers of essentially infinite power, and cannot in general solve the Halting Problem. Practically, we're dealing with computer of limited size, which means the HP is solvable on a theoretical computer of infinite power, but can't be solved with only the resources in the known Universe. – David Thornley Dec 20 '11 at 15:15
  • @SK-logic: I'm not sure what you mean. Presuming your comment was aimed at me: I don't call any programming language 'amazingly useless'. I merely think that the algorithm presented in the paper is amazingly useless, since the set of programs it works on correctly is highly uninteresting. That has nothing to do with programming languages. – Alex ten Brink Dec 20 '11 at 23:15
  • @Alex ten Brink, you said that "the subset (of the always terminating programs) is amazingly useless", it was not clear that it is about some specific algorithm. – SK-logic Dec 21 '11 at 00:09
  • David: True, but the "practical halting problem" is a completely different kind of beast than the theoretical problem anyway. For example, as you have pointed out, a program counting to 2^128 won't complete its job in this solar system. On the other hand, from the theoretical point of view, there is no doubt that this is a program that eventually halts! A program that just writes 1s to the tape inevitably crashes in the real world with an out of memory exception, but never halts in the theoretical model. – user281377 Dec 21 '11 at 06:40
3

There is, and in fact there are programs in real life that solve the halting problem for other problems all the time. They are part of the operating system you are running your computer on. Undecidability is a weird claim that only says that there isn't such a program that works for ALL other programs.

One person correctly stated that the halting proof seems to be the only program for which it cannot be solved, as it infinitely traces itself like a mirror. This same person also stated that if there was a halting machine, it would be magic because it would tell us hard math problems by telling us ahead of time if it's solver algorithm would halt.

The assumption in both of these cases is that the halting machine doesn't trace because there is no proof that it traces. However, in reality it actually does trace/ run the program it is run on with the input given.

The logical proof at least is simple. If it didn't need to trace at least the first step, it wouldn't need the input along with the program it's run on. In order to make any use of the information, it has to at least trace the first step before trying to analyze where that path is going.

The hard math problems mentioned in the top answer are ones where you cannot fast forward to figure out the answer, which means the halting problem would have to continue tracing until some pattern was recognizable.

So the only practical argument to get from the halting problem is that a halting machine can't determine the outcome of an optimized problem solver faster than the problem solver can finish.

Giving a formal proof for this reasoning is harder, and although I believe I could, attempting to explain it to anyone an academia will result in them throwing an ape like temper-tantrum and swinging from the chandelier. It's best just not to argue with those people.

Terrence Kwasha
  • 39
  • 2
1

here's the answer, it's yes, way back in 1967 from http://www.isp.uni-luebeck.de/kps07/files/papers/kirner.pdf

That the halting problem can be at least theoretically solved for finite-state systems has been already argued by Minsky in 1967 [4]: “...any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine...”

(and so if you stick to finite turing machines then you can build an oracle)

Of course how long this takes is another question

daven11
  • 769
  • 5
  • 11
0

is there a subset of programs that can be determined if they halt?

Yes.

Is it good enough for most programs?

Define "most".

Can I build a set of language constructs that I can determine the 'haltability' of a program?

Yes.

is there such a thing as nearly turing complete which is good enough?

Define "nearly".

Many folks write Python without using while statement or recursion.

Many folks write Java using only the for statement with simple iterators or counters that can be trivially proven to terminate; and they write without recursion.

It's pretty easy to avoid while and recursion.

For a given program in which all inputs are bounded can you determine if the program halts?

No.

If so what are the constraints of the language and what are the limits of the input set.

Um. The Halting problem means the program can't ever determine things about programs as complex as itself. You can add any one of a large number of constraints to get past the halting problem.

The standard approach to the halting problem is to allow proofs using a slightly "richer" set of mathematical formalisms than are available in the programming language.

It's easier to extend the proof system than it is to restrict the language. Any restriction leads to arguments for the one algorithm that's difficult to express because of the restriction.

The maximal set of these constructs would determine a language which can be deduced to halt or not. Is there some study that's been done on this?

Yes. It's called "Group Theory". A set of values closed under a set of operations. Pretty well understood stuff.

S.Lott
  • 45,264
  • 6
  • 90
  • 154
  • "nearly" is the bit I'm asking. Is there are finite class of problems for which a program can be said to halt and how limited is the problem set? For instance the statement if(i<10) then print(i) does halt for all i. If I restrict the domain of i to 32 bit integers then it too halts. – daven11 Dec 19 '11 at 04:54
  • Keep in mind a `for` loop *is* a while loop, and people often put more complicated things in the condition term than just `x < 42`. – Billy ONeal Dec 19 '11 at 05:38
  • @BillyONeal: Good point. In Python a `for` loop is very, very tightly constrained to work through an iterator. A more general `for` loop in Java, however, can include extra conditions that invalidate simple use of an iterator. – S.Lott Dec 19 '11 at 14:11
  • "Is there are finite class of problems for which a program can be said to halt?" The answer remains yes. "how limited is the problem set?" Um. Finite is finite. If you give up on trying to approximate real numbers and stick to natural numbers, closed under all mathematical operations, you're doing ordinary group theory. Modular arithmetic. Nothing special. It's not clear what you're asking. Are you asking what modular arithmetic is? – S.Lott Dec 19 '11 at 14:15
  • @S.Lott I mean numbers as represented in a machine, not numbers in the abstract sense. So think of numbers as a fixed number of bits. These numbers have slightly different rules from the integers and reals. Hope that makes sense. – daven11 Dec 19 '11 at 22:50
  • "numbers as a fixed number of bits. These numbers have slightly different rules from the integers". False. Group theory describes abstract numbers in a finite domain. Completely. – S.Lott Dec 19 '11 at 22:51
  • @S.Lott. Yes you're right - that's interesting, I'll have to reread this stuff. Thanks. – daven11 Dec 20 '11 at 02:10
0

For many programs P, we can write a decider which halts on any input X, and tells us correctly whether P(X) halts or not. That is especially true for all programs with finite state. It is true for programs without loops, or with loops that have a structure that the decider is capable of analysing well enough.

An example: Let S be a state with a complete and discrete ordering and a smallest value. If S is initialised before the loop starts, and becomes smaller at each iteration of the loop, and the loop stops when the state is small enough, then the loop finishes and cannot stop P from halting. This allows to prove for example that the calculation of the big Ackermann function halts (in theory obviously. In practice the universe will be long gone before calculating A(4) would finish).

There are programs P where writing the correct decider takes some very hard maths, possibly beyond what we have now. On the borderline: I can easily write a program P where P(n) halts if n ≥ 0 and there are 0 < a < b < c such that $a^n + b^n = c^n$. Only quite recently there has been enough progress in maths to write a correct and very simple decider. (P will halt if and only if n = 1 or n = 2).

Note that a correct decider would have been possible without proving Fermat's last theorem. For example if someone had proved "there are no solutions with n ≥ 3 where a, b, c are co-prime and c > n^10000", that wouldn't prove Fermats Last Theorem, but would allow us to write a decider for the program P.

gnasher729
  • 42,090
  • 4
  • 59
  • 119