Re: Foundation for a Formal Refutation of the Original Halting Problem?

From: Acme Diagnostics (LFinezapthis_at_partpostmark.net)
Date: 08/06/04

  • Next message: George Greene: "Re: The proof that I was referring to is on the website" 
    Date: 6 Aug 2004 12:39:05 -0500

    Owen Jacobson <angstrom@lionsanctuary.net> wrote:
    >
    >You might, just possibly, be able to prove that there can be a Halt
    >program that can accept any program that does not itself contain a Halt
    >program[0]. Such a proof would be of academic interest only, because
    >we already know it's possible to write Halt programs for well-defined
    >subsets of all Turing machines.
    >
    >[0] I did some quick checking on Google, and the consensus *seems* to
    >be that this is possible, but I couldn't find a formal proof that this
    >is true or false.

    I meant to thank you for posting this. It seems to address a question I
    had asked previously, though doesn't answer it directly:

    "Is there any *linkable* proof of the Halting Problem for a computer
    language that does not contrive a logic paradox and require
    self-reference to make the proof?"

    Is it fair to say that you were unable to find such a proof in your
    "quick checking on Google"?

    I'm not interested in Turing Machines at all, but only the proof "for
    a computer language." That distinction is made explicit on this page:

    http://www.csee.umbc.edu/~squire/cs451_l26.html

    (I am asking this same question of Marc in a companion post.)

    Larry

  • Next message: George Greene: "Re: The proof that I was referring to is on the website"

    Relevant Pages

    • Re: Foundation for a Formal Refutation of the Original Halting Problem?
      ... Owen Jacobson wrote: ... >You might, just possibly, be able to prove that there can be a Halt ... I'm not interested in Turing Machines at all, ... a computer language." ...
      (sci.logic)
    • Re: [PO] Re: Proving a negative is hard
      ... If Halt determines that it will halt, ... Undecidability ... > abstractions of Turing Machines, ... >> paradigm applies to the new paradigm. ...
      (comp.theory)
    • Re: [PO] Re: Proving a negative is hard
      ... If Halt determines that it will halt, ... Undecidability ... > abstractions of Turing Machines, ... >> paradigm applies to the new paradigm. ...
      (sci.logic)
    • Re: Largest provable BB(N)?
      ... If you define BB in terms of number of steps needed to halt, ... |And by "provable" I mean within the scope of known mathematics... ... and nonhalting of exactly the same Turing machines as ZFC can. ... Some of their favorite additional axioms are known as "higher axioms ...
      (sci.math)
    • Re: What is the Result from Invoking this Halt Function?
      ... No, it forms a logical contradiction, thus proving that WillHalt (a ... program that determines whether or not an arbitrary program halts) ... The concept of a halt analyser has to be applied to ... Turing Machines, standard C++ with particular implementation defined ...
      (sci.logic)