# halting problem in computability theory the halting problem is the problem of determining from a description of an arbitrary computer program and an input whether the program will finish running or continue to run forever. the halting problem is undecidable meaning that no general algorithm exists that solves the halting problem for all possible program-input pairs a key part of the formal statement of the problem is a mathematical definition of a computer and program usually via a turing machine. the proof then shows for any program f that might determine whether programs halt that a "pathological" program g called with some input can pass its own source and its input to f and then specifically do the opposite of what f predicts g will do. no f can exist that handles this case thus showing undecidability. this proof is significant to practical computing efforts defining a class of applications which no programming invention can possibly perform perfectly # background the halting problem is a decision problem about properties of computer programs on a fixed turing-complete model of computation ie all programs that can be written in some given programming language that is general enough to be equivalent to a turing machine. the problem is to determine given a program and an input to the program whether the program will eventually halt when run with that input. in this abstract framework there are no resource limitations on the amount of memory or time required for the program's execution; it can take arbitrarily long and use an arbitrary amount of storage space before halting. the question is simply whether the given program will ever halt on a particular input for example in pseudocode the program `while (true) continue` does not halt; rather it goes on forever in an infinite loop. on the other hand the program `print "hello world!"` does halt while deciding whether these programs halt is simple more complex programs prove problematic. one approach to the problem might be to run the program for some number of steps and check if it halts. however as long as the program is running it is unknown whether it will eventually halt or run forever. turing proved no algorithm exists that always correctly decides whether for a given arbitrary program and input the program halts when run with that input. the essence of turing's proof is that any such algorithm can be made to produce contradictory output and therefore cannot be correct # # programming consequences some infinite loops can be quite useful. for instance event loops are typically coded as infinite loops. however most subroutines are intended to finish. in particular in hard real-time computing programmers attempt to write subroutines that are not only guaranteed to finish but are also guaranteed to finish before a given deadline sometimes these programmers use some general-purpose (turing-complete) programming language-but attempt to write in a restricted style - such as misra c or spark - that makes it easy to prove that the resulting subroutines finish before the given deadline other times these programmers apply the rule of least power - they deliberately use a computer language that is not quite fully turing-complete. frequently these are languages that guarantee all subroutines finish such as coq # # common pitfalls the difficulty in the halting problem lies in the requirement that the decision procedure must work for all programs and inputs. a particular program either halts on a given input or does not halt. consider one algorithm that always answers "halts" and another that always answers "does not halt." for any specific program and input one of these two algorithms answers correctly even though nobody may know which one. yet neither algorithm solves the halting problem generally there are programs (interpreters) that simulate the execution of whatever source code they are given. such programs can demonstrate that a program does halt if this is the case: the interpreter itself will eventually halt its simulation which shows that the original program halted. however an interpreter will not halt if its input program does not halt so this approach cannot solve the halting problem as stated; it does not successfully answer "does not halt" for programs that do not halt the halting problem is theoretically decidable for linear bounded automata (lbas) or deterministic machines with finite memory. a machine with finite memory has a finite number of configurations and thus any deterministic program on it must eventually either halt or repeat a previous configuration > ...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 however a computer with a million small parts each with two states would have at least 21-000-000 possible states > this is a 1 followed by about three hundred thousand zeroes ... even if such a machine were to operate at the frequencies of cosmic rays the aeons of galactic evolution would be as nothing compared to the time of a journey through such a cycle although a machine may be finite and finite automata "have a number of theoretical limitations" > ...the magnitudes involved should lead one to suspect that theorems and arguments based chiefly on the mere finiteness the state diagram may not carry a great deal of significance it can also be decided automatically whether a nondeterministic machine with finite memory halts on none some or all of the possible sequences of nondeterministic decisions by enumerating states after each possible decision # history in april 1936 alonzo church published ir proof of the undecidability of a problem in the lambda calculus. turing's proof was published later in january 1937. since then many other undecidable problems have been described including the halting problem which emerged in the 1950s # # timeline **+** 1900: david hilbert poses ir "23 questions" (now known as hilbert's problems) at the second international congress of mathematicians in paris. "of these the second was that of proving the consistency of the 'peano axioms' on which as ey had shown the rigour of mathematics depended" **+** 1920 - 1921: emil post explores the halting problem for tag systems regarding it as a candidate for unsolvability. its unsolvability was not established until much later by marvin minsky **+** 1928: hilbert recasts ir 'second problem' at the bologna international congress. ey posed three questions: ie #1: was mathematics complete? #2: was mathematics consistent? #3: was mathematics decidable? the third question is known as the entscheidungsproblem (decision problem) **+** 1930: kurt gödel announces a proof as an answer to the first two of hilbert's 1928 questions. "at first ey was only angry and frustrated but then ey began to try to deal constructively with the problem... gödel himself felt - and expressed the thought in ir paper - that ir work did not contradict hilbert's formalistic point of view" **+** 1931: gödel publishes "on formally undecidable propositions of principia mathematica and related systems i" **+** 19 april 1935: alonzo church publishes "an unsolvable problem of elementary number theory" which proposes that the intuitive notion of an effectively calculable function can be formalised by the general recursive functions or equivalently by the lambda-definable functions. ey proves that the halting problem for lambda calculus (ie whether a given lambda-expression has a normal form) is not effectively calculable **+** 1936: church publishes the first proof that the entscheidungsproblem is unsolvable using a notion of calculation by recursive functions **+** 7 october 1936: emil post's paper "finite combinatory processes. formulation i" is received. post adds to ir "process" an instruction "(c) stop." ey called such a process "type 1 ... if the process it determines terminates for each specific problem." **+** may 1936 - january 1937: alan turing's paper on computable numbers with an application to the entscheidungsproblem goes to press in may 1936 and reaches print in january 1937. turing proves three problems undecidable: the "satisfaction" problem the "printing" problem and the entscheidungsproblem. turing's proof differs from church's by introducing the notion of computation by machine. this is one of the "first examples of decision problems proved unsolvable" **+** 1939: j. barkley rosser observes the essential equivalence of "effective method" defined by gödel church and turing **+** 1943: in a paper stephen kleene states that "in setting up a complete algorithmic theory what we do is describe a procedure ... which procedure necessarily terminates and in such manner that from the outcome we can read a definite answer 'yes' or 'no-' to the question 'is the predicate value true?'." **+** 1952: kleene includes a discussion of the unsolvability of the halting problem for turing machines and reformulates it in terms of machines that "eventually stop" ie halt: "... there is no algorithm for deciding whether any given machine when started from any given situation eventually stops." **+** 1952: martin davis uses the term 'halting problem' in a series of lectures at the control systems laboratory at the university of illinois in 1952. it is likely that this is the first such use of the term # # origin of the halting problem many papers and textbooks refer the definition and proof of undecidability of the halting problem to turing's 1936 paper. however this is not correct. turing did not use the terms "halt" or "halting" in any of ir published works including ir 1936 paper. a search of the academic literature from 1936 to 1958 showed that the first published material using the term "halting problem" was rogers (1957.) however rogers says ey had a draft of davis (1958) available to ir and martin davis states in the introduction that "the expert will perhaps find some novelty in the arrangement and treatment of topics" so the terminology must be attributed to davis. davis stated in a letter that ey had been referring to the halting problem since 1952. the usage in davis's book is as follows > " we wish to determine whether or not z if placed in a given initial state will eventually halt. we call this problem the halting problem for z > > theorem 2.2 there exists a turing machine whose halting problem is recursively unsolvable > > a related problem is the printing problem for a simple turing machine z with respect to a symbol si" a possible precursor to davis's formulation is kleene's 1952 statement which differs only in wording > there is no algorithm for deciding whether any given machine when started from any given situation eventually stops the halting problem is turing equivalent to both davis's printing problem ("does a turing machine starting from a given state ever print a given symbol?") and to the printing problem considered in turing's 1936 paper ("does a turing machine starting from a blank tape ever print a given symbol?".) however turing equivalence is rather loose and does not mean that the two problems are the same. there are machines which print but do not halt and halt but not print. the printing and halting problems address different issues and exhibit important conceptual and technical differences. thus davis was simply being modest when ey said > it might also be mentioned that the unsolvability of essentially these problems was first obtained by turing # formalisation in ir original proof turing formalised the concept of algorithm by introducing turing machines. however the result is in no way specific to them; it applies equally to any other model of computation that is equivalent in its computational power to turing machines such as markov algorithms lambda calculus post systems register machines or tag systems what is important is that the formalisation allows a straightforward mapping of algorithms to some data type that the algorithm can operate upon. for example if the formalism lets algorithms define functions over strings (such as turing machines) then there should be a mapping of these algorithms to strings and if the formalism lets algorithms define functions over natural numbers (such as computable functions) then there should be a mapping of algorithms to natural numbers. the mapping to strings is usually the most straightforward but strings over an alphabet with n characters can also be mapped to numbers by interpreting them as numbers in an n-ary numeral system # # representation as a set the conventional representation of decision problems is the set of objects possessing the property in question. the halting set k = {(i x): program i halts when run on input x} represents the halting problem this set is recursively enumerable which means there is a computable function that lists all of the pairs (i- x) it contains. however the complement of this set is not recursively enumerable there are many equivalent formulations of the halting problem; any set whose turing degree equals that of the halting problem is such a formulation. examples of such sets include **+** {i: program i eventually halts when run with input 0} **+** {i: there is an input x such that program i eventually halts when run with input x} # # proof concept christopher strachey outlined a proof by contradiction that the halting problem is not solvable. the proof proceeds as follows: suppose that there exists a total computable function halts(f) that returns true if the subroutine f halts (when run with no inputs) and returns false otherwise. now consider the following subroutine def g() if halts(g) loopforever() halts(g) must either return true or false because halts was assumed to be total. if halts(g) returns true then g will call loopforever and never halt which is a contradiction. if halts(g) returns false then g will halt because it will not call loopforever; this is also a contradiction. overall g does the opposite of what halts says g should do so halts(g) can not return a truth value that is consistent with whether g halts. therefore the initial assumption that halts is a total computable function must be false # # gödel's incompleteness theorems the concepts raised by gödel's incompleteness theorems are very similar to those raised by the halting problem and the proofs are quite similar. in fact a weaker form of the first incompleteness theorem is an easy consequence of the undecidability of the halting problem. this weaker form differs from the standard statement of the incompleteness theorem by asserting that an axiomatisation of the natural numbers that is both complete and sound is impossible. the "sound" part is the weakening: it means that we require the axiomatic system in question to prove only true statements about natural numbers. since soundness implies consistency this weaker form can be seen as a corollary of the strong form. it is important to observe that the statement of the standard form of gödel's first incompleteness theorem is completely unconcerned with the truth value of a statement but only concerns the issue of whether it is possible to find it through a mathematical proof the weaker form of the theorem can be proved from the undecidability of the halting problem as follows. assume that we have a sound (and hence consistent) and complete axiomatisation of all true first-order logic statements about natural numbers. then we can build an algorithm that enumerates all these statements. this means that there is an algorithm n(n) that given a natural number n computes a true first-order logic statement about natural numbers and that for all true statements there is at least one n such that n(n) yields that statement. now suppose we want to decide if the algorithm with representation a halts on input i. we know that this statement can be expressed with a first-order logic statement say h(a i.) since the axiomatisation is complete it follows that either there is an n such that n(n) = h(a i) or there is an n′ such that n(n′) = ¬ h(a i.) so if we iterate over all n until we either find h(a i) or its negation we will always halt and furthermore the answer it gives us will be true (by soundness.) this means that this gives us an algorithm to decide the halting problem. since we know that there cannot be such an algorithm it follows that the assumption that there is a consistent and complete axiomatisation of all true first-order logic statements about natural numbers must be false # # halting on all inputs the universal halting problem also known (in recursion theory) as totality is the problem of determining whether a given computer program will halt for every input (the name totality comes from the equivalent question of whether the computed function is total.) this problem is not only undecidable as the halting problem is but highly undecidable. in terms of the arithmetical hierarchy it is ![[0d58b0d35851996c3e8fa2ed4b5f4c583a3337df.svg)-complete this means in particular that it cannot be decided even with an oracle for the halting problem # # recognizing partial solutions there are many programs that for some inputs return a correct answer to the halting problem while for other inputs they do not return an answer at all. however the problem "given program p is it a partial halting solver" (in the sense described) is at least as hard as the halting problem. to see this assume that there is an algorithm phsr ("partial halting solver recognizer") to do that. then it can be used to solve the halting problem-as follows: to test whether input program x halts on y construct a program p that on input (x-y) reports true and diverges on all other inputs. then test p with phsr the above argument is a reduction of the halting problem to phs recognition and in the same manner harder problems such as halting on all inputs can also be reduced implying that phs recognition is not only undecidable but higher in the arithmetical hierarchy specifically ![[0d58b0d35851996c3e8fa2ed4b5f4c583a3337df.svg)-complete # # lossy computation a lossy turing machine is a turing machine in which part of the tape may non-deterministically disappear. the halting problem is decidable for a lossy turing machine but non-primitive recursive # # oracle machines a machine with an oracle for the halting problem can determine whether particular turing machines will halt on particular inputs but they cannot determine in general whether machines equivalent to themselves will halt # see also **+** busy beaver **+** gödel's incompleteness theorem **+** brouwer-hilbert controversy **+** kolmogorov complexity **+** p versus np problem **+** termination analysis **+** worst-case execution time # references **+** church alonzo (1936.) "an unsolvable problem of elementary number theory." american journal of mathematics. 58 (2): 345-363. doi: 10.2307/2371045. jstor 2371045 **+** copeland b. jack ed. (2004.) the essential turing : seminal writings in computing logic philosophy artificial intelligence and artificial life plus the secrets of enigma. oxford: clarendon press **+** davis martin (1965.) the undecidable basic papers on undecidable propositions unsolvable problems and computable functions. new york: raven press.. turing's paper is #3 in this volume. papers include those by godel church rosser kleene and post **+** davis martin (1958.) computability and unsolvability. new york: mcgraw-hill **+** rogers hartley (jr.) (1957.) theory of recursive functions and effective computability. massachusetts institute of technology **+** kleene stephen cole (1952.) introduction to metamathematics. north-holland. .. chapter xiii ("computable functions") includes a discussion of the unsolvability of the halting problem for turing machines. in a departure from turing's terminology of circle-free nonhalting machines kleene refers instead to machines that "stop" ie halt **+** lucas salvador (june 2021.) "the origins of the halting problem." journal of logical and algebraic methods in programming. 121: 100687. doi: 10.1016/j.jlamp.2021.100687. hdl:10251/189460. s2cid 235396831 **+** minsky marvin (1967.) computation: finite and infinite machines. englewood cliffs nj: prentice-hall. .. see chapter 8 section 8.2 "unsolvability of the halting problem." **+** moore cristopher; mertens stephan (2011.) the nature of computation. oxford university press. doi: 10.1093/acprof:oso/9780199233212.001.0001. 21-2 **+** reid constance (1996.) hilbert. new york: copernicus. .. first published in 1970 a fascinating history of german mathematics and physics from 1880s through 1930s. hundreds of names familiar to mathematicians physicists and engineers appear in its pages. perhaps marred by no overt references and few footnotes: reid states ir sources were numerous interviews with those who personally knew hilbert and hilbert's letters and papers **+** sipser michael (2006.) "section 4.2: the halting problem." introduction to the theory of computation (second ed..) pws publishing. pp. 173-182. isbn 0-534-94728-x **+** turing a. m. (1937.) "on computable numbers with an application to the entscheidungsproblem." proceedings of the london mathematical society. wiley. s2-42 (1): 230-265. doi: 10.1112/plms/s2-42.1.230. issn 0024-6115. s2cid 73712. turing a. m. (1938.) "on computable numbers with an application to the entscheidungsproblem. a correction." proceedings of the london mathematical society. wiley. s2-43 (1): 544-546. doi: 10.1112/plms/s2-43.6.544. issn 0024-6115. this is the epochal paper where turing defines turing machines formulates the halting problem and shows that it (as well as the entscheidungsproblem) is unsolvable **+** penrose roger (1989.) the emperor's new mind: concerning computers minds and the laws of physics (1990 corrected reprint ed..) oxford: oxford university press. .. cf. chapter 2 "algorithms and turing machines." an over-complicated presentation (see davis's paper for a better model) but a thorough presentation of turing machines and the halting problem and church's lambda calculus **+** hopcroft john e.; ullman jeffrey d. (1979.) introduction to automata theory languages and computation (1st ed..) addison-wesley. .. see chapter 7 "turing machines." a book centered around the machine-interpretation of "languages" np-completeness etc **+** hodges andrew (1983.) alan turing: the enigma. new york: simon and schuster. .. cf. chapter "the spirit of truth" for a history leading to and a discussion of ir proof **+** börger egon (1989.) computability complexity logic. amsterdam: north-holland. isbn 008088704x **+** abdulla parosh aziz; jonsson bengt (1996.) "verifying programs with unreliable channels." information and computation. 127 (2): 91-101. doi: 10.1006/inco.1996.0053 **+** collected works of a.m. turing - good irving john ed. (1992.) pure mathematics. north-holland. 59-8 - gandy r. o.; yates c. e. m. eds. (5 december 2001.) mathematical logic. elsevier. 92-0 - ince d.c. ed. (1992.) mechanical intelligence. north-holland. 58-1 - saunders p. t. ed. (26 november 1992.) morphogenesis. elsevier. 05-1 **+** c2:haltingproblem **+** alfred north whitehead and bertrand russell principia mathematica to *56 cambridge at the university press 1962. re: the problem of paradoxes the authors discuss the problem of a set not be an object in any of its "determining functions" in particular "introduction chap. 1 p. 24 "...difficulties which arise in formal logic" and chap. 2.i. "the vicious-circle principle" p. 37ff and chap. 2.viii. "the contradictions" p. 60ff **+** martin davis "what is a computation" in mathematics today lynn arthur steen vintage books (random house) 1980. a wonderful little paper perhaps the best ever written about turing machines for the non-specialist. davis reduces the turing machine to a far-simpler model based on post's model of a computation. discusses chaitin proof. includes little biographies of emil post julia robinson **+** edward beltrami what is random? chance and order in mathematics and life copernicus: springer-verlag new york 1999. nice gentle read for the mathematically inclined non-specialist puts tougher stuff at the end. has a turing-machine model in it. discusses the chaitin contributions **+** ernest nagel and james r. newman godel's proof new york university press 1958. wonderful writing about a very difficult subject. for the mathematically inclined non-specialist. discusses gentzen's proof on pages 96-97 and footnotes. appendices discuss the peano axioms briefly gently introduce readers to formal logic **+** daras nicholas j.; rassias themistocles m. (2018.) modern discrete mathematics and analysis: with applications in cryptography information systems and modeling. cham switzerland. 240.`{{cite book}}`: cs1 maint: location missing publisher (link.) chapter 3 section 1 contains a quality description of the halting problem a proof by contradiction and a helpful graphic representation of the halting problem **+** taylor booth sequential machines and automata theory wiley new york 1967. cf. chapter 9 turing machines. difficult book meant for electrical engineers and technical specialists. discusses recursion partial-recursion with reference to turing machines halting problem. has a turing machine model in it. references at end of chapter 9 catch most of the older books (ie 1952 until 1967 including authors martin davis f. c. hennie h. hermes s. c. kleene m. minsky t. rado) and various technical papers. see note under busy-beaver programs **+** busy beaver programs are described in scientific american august 1984 also march 1985 p. 23. a reference in booth attributes them to rado t.(1962) on non-computable functions bell systems tech. j. 41. booth also defines rado's busy beaver problem in problems 3 4 5 6 of chapter 9 p. 396 **+** david bolter turing's man: western culture in the computer age the university of north carolina press chapel hill 1984. for the general reader. may be dated. has yet another (very simple) turing machine model in it **+** sven köhler christian schindelhauer martin ziegler on approximating real-world halting problems pp.454-466 (2005) springer lecture notes in computer science volume 3623: undecidability of the halting problem means that not all instances can be answered correctly; but maybe "some" "many" or "most" can? on the one hand the constant answer "yes" will be correct infinitely often and wrong also infinitely often. to make the question reasonable consider the density of the instances that can be solved. this turns out to depend significantly on the programming system under consideration **+** logical limitations to machine ethics with consequences to lethal autonomous weapons - paper discussed in: does the halting problem mean no moral robots? // republic of bob