3
$\begingroup$

Halting Problem is (theoretically) decidable for such algorithms which termination may be proved in First Order Logic (FOL) because all true statements in FOL are recursively enumerable. It is correct?

I'm talking about programs in Turing-complete languages and use "realworldiness" property not in the sense of finiteness but in the sense of "be designed to some real purpose" and "be not specially cooked to require HOL for termination proof" (that allows potentially to require unprovable statements for termination proof).

As for argument that FOL is adequate for working with ordinary programs is a fact that there are plenty systems designed for industrial application for proving program properties that use only FOL (TLA+, for example).

To be precise, let set of real world programs be all programs that humans write for their utility for entire human history to the end of times.

Perhaps I must say even more precise: Can such property be existing that limits Turing-complete language in such way that termination of any program in language with that property can be proved in FOL but no programmer will be disturbed by that limitation?

And interesting satellite question: is absolutely minimal restriction of Turing-complete languages possible such that Halting Problem become decidable for restricted languages?

  • 3
    This is a fairly confused question. The set of programs that halt is already recursively enumerable, without needing proofs. The problem is that the set of non-halting programs is not recursively enumerable. You can definitely enumerate all the programs for which a proof exists that the program halts, yes. It would also be really helpful if you could define more clearly what you mean by "real world" examples.2011-05-28
  • 0
    @Thomas Andrews: I'm enumerating FOL theorems, not programs; I'm enumerating them until termination proof for given program will be found. What about "real world", I've add update.2011-05-28
  • 0
    I'm enumerating them until termination _or nontermination_ proof will be found.2011-05-28
  • 1
    Well, no program that any person ever writes is ever in a Turing complete language, since it only runs in machines that have finite memory. That said, a simple program that a person might want to write is to search for a proof of a theorem. If you could solve the halting problem, then the set of provable and disprovable theorems would be a recursive set, which it is not.2011-05-28
  • 0
    @Thomas Andrews: "Well, no program that any person ever writes is ever in a Turing complete language, since it only runs in machines that have finite memory". It is incorrect because you confused language and its implementation. Implementation is finite, language is Turing-complete.2011-05-28
  • 0
    @Thomas Andrews: set of theorems is recursively enumerable set, for all formal systems ever, by definition.2011-05-28
  • 0
    Depends on the language. As a consequence of 6.2.6 Representation of Types, the C language explicitly specifies a non-Turing-complete computation model (the number of possible addressable storage units, in memory and in files, is bounded due to the representation of pointers and file offsets having a fixed size expressible in the program with `sizeof`).2011-05-28
  • 0
    @R.. : Indeed. So we will talk only about "programming languages which level is high enough so they can manipulate unbounded lists" as I said explicitly in the question.2011-05-28
  • 0
    It's recursively enumerably, but you can't solve the problem: "Will the search for a proof of theorem X halt?" You asked for a real-world collection of problems for which the halting problem cannot be solved.2011-05-28
  • 0
    @Thomas Andrews: No, all true statements are provable in FOL (Godel Completeness Theorem) so the search process is certainly terminates.2011-05-28
  • 0
    Yes, some languages are *theoretically* Turing complete, but in the real world, the actual programs are not, because the actual programs are run on computers with finite space.2011-05-28
  • 0
    Programs in assembly or machine code are not Turing-complete because of fixed pointer width. Programs in high level languages are. Please, stop confusing languages and their implementations. Programming Language is (syntax,semantics). Syntax is described by grammar and static semantics. Semantics is mathematical theory (often alleged) from which for every program and corresponding input its output may be derived.2011-05-28
  • 0
    While talking about programs in some language only its syntax and semantics is important, not our universe nor physical laws nor computers nor implementations. Programming language is very theoretical thing.2011-05-28
  • 0
    Sorry, but did I say first order logic? I might want to solve more general problems than FOL allows. Then we cannot solve the halting problem in general.2011-05-28
  • 0
    @Thomas Andrews: Well, this is the gist of my question. If FOL is really adequate for reasoning about usual programs, Halting Problem is decidable for these usual programs. If it can be shown that no unprovable truths in HOL required to prove programs termination and HOL is enough then Halting Problem is decidable.2011-05-28
  • 0
    Okay, if you don't like that pedantry, then take this pedantry: I assert the set of all programs that any person will ever write is finite, so necessarily there exists a program that will determine whether any particular one of these will halt.2011-05-28
  • 0
    I do not see why finiteness of number of programs per se implies existing of termination decider.2011-05-28
  • 0
    "Perhaps I must say even more precise: Can such property be existing that limits Turing-complete language in such way that termination of all programs in this language can be proved in FOL?" Update.2011-05-28
  • 0
    Implicitly, if the halting of a class of enumerable programs $\phi_i$ cannot be determined, then that class implicitly needs to require more than $FOL.$ But there are certainly problems and programs that were not initially thought to be beyond FOL that turned out to be beyond FOL. Hilbert's tenth problem is essentially asking for a solution to a halting problem on a class of programs. That it turned out to be unsolvable was not intially obvious.2011-05-28
  • 0
    To make things clear about "theoretical" and "practical" issues: actually all issues are purely theoretical; the difference is just what set of assumptions are considered: finiteness of energy, boundedness of time, Turing-completeness, etc. After the point which fixes all assumptions no additional assumptions must be added: If I'm talking about Turing-complete programming language it is incorrect to mention finiteness of the world.2011-05-28
  • 0
    @Thomas Andrews: explain please why you talking about "enumerable programs", not just "programs"? What is supposed to meant?2011-05-28
  • 0
    @Thomas Andrews: So this is absolutely impossible to predict what logic may be required to prove termination of software complex no matter how mundane it looks if it isn't already written in that way that it can be translated to language with power low enough to make its HP decidable? Am I correctly understood your point?2011-05-28
  • 0
    By enumerable class of programs, say you have an encoding $\phi_e$ of the set $P$ of all the programs in your language. Then any subset of $P$ corresponds to a subset of $\mathbb{N}$, but if that subset is not $r.e.$, then it isn't, in a sense, a useful class of programs. For example, we could take the set of all $\phi_e$ such that $\phi_e(0)$ halts. Then we could certainly solve the halting problem for that class, but that's not a meaningful result.2011-05-28
  • 0
    Ultimately, what it means for a class of programs to be enumerable is really that there is a universal program which can be used to calculate all the programs in the class.2011-05-28
  • 0
    For example, under your definition of "real world program," it's not at all clear that the set is enumerable, if it is infinite, unless the universe itself is merely Turing-complete :)2011-05-28
  • 0
    @Thomas Andrews: "under your definition of "real world program," it's not at all clear that the set is enumerable" Oh! Thanks, I've missed that fact. But it still have no relation to the topic: using my algorithm you can determine termination of any program is our class regardless of enumerability of the class.2011-05-29

2 Answers 2