User talk:Likebox/Incompletness

slight emendation

0. Halting problem: Given any computer program, there does not exist a computer testing-program which tells you whether or not the computer program under test eventually halts.^[1]

Turing's original expression of the same notion: "...there can be no machine E which, when supplied with the S.D. of an arbitrary machine M, will determine whether M ever printes a given symbol (0 say)'" (italics in original, Turing 1936-7 reprinted in Davis 1965:134)

The key here is the use of the ∀ in the in the formalization of this statement: ~(∃E(∀M...))

1. Kleene's separation lemma: there does not exists a ~~program~~ program ~~which~~ that tells you whether another computer program R returns a yes or a no.

Proof: construct SPITE to print its code, calculate the expected output, and do the opposite.

In recursion theory, Kleene's separation lemma is usually stated this way: "There is a subset S of a recursively enumerable set R which cannot be recursively separated from its complement R-S". R is the set of programs that return yes or no. S is the set of programs that return yes, and R-S is the set of programs that return no. ^{[citation needed]}^[2]

2. There does not exist a program which tells you whether any other computer program finishes in polynomial or exponential time.

Proof: construct SPITE(N) to ignore the input N, print its code, calculate the expected running time, then run an algorithm of the opposite running time on N. The first part does not depend on the input, and runs in fixed time.

3. word problem for groups: There does not exist a program which determines whether two elements in a finitely presented groups are equivalent. The decision problem was first posed by Max Dehn in 1911. Alan Turing proved that the problem for finitely presented monoids (no inverses) was equivalent to the halting problem and therefore undecidable, and the problem for groups was shown to be equivalent to the halting problem in 1952.^{[citation needed]}

4. Behavior of Cellular automata: There does not exist a program which can determine whether an arbitrary starting configuration of Conway's Game of Life will eventually reach the empty configuration.^{[citation needed]}

All the practical decision problems which have been shown to be undecidable, including all the ones above, are equivalent to the halting problem.^{[citation needed]}^[3] Turing showed that there are much stronger degrees of undecidablity (Turing 1939), while Post showed that there are weaker ones.^{[citation needed]} It remains an open question to find natural mathematical forms for these types of undecidable problems.^[4]

Footnotes

^ I reworded this into its correct formulation. Turing's original proof #1 upon which this proof #2 is built, is far more constructive than the common halting-problem proof devised by Davis. In that proof the testing program H gets locked into an infinitely-repeating circle and fails to print the diagonal number (of itself) when it finally comes to the test its own number. There is nothing whatever in Turing or thereafter in his lifetime about HALTING. This concept is attributable to Post (1936) and discussions of terminating algorithms in Church 1934 etc, and was finally used by Davis in his "halting problem" proof -- original to him -- in the mid-1950's in his text (I forget the year -- mid-1950's). Davis confirmed his first-use to me personally, and it also appears in the reference as cited on the halting problem page. I have verified this reference with my own eyes.
^ I don't doubt that this is true, I'm just looking for a source. I am very familiar with Kleene 1952.
^ Actually, all the undecidability proofs, including Godel's 1931 have a similar structure -- they all have diagonalization at their heart/core. I do have a published source for that observation, somewhere, if you need it. See the addition in the next section below, it's in one or the other of those two articles.
^ I do not have the vaguest idea of what this means. "Natural forms"? I do know that Post and Finser were looking for absolutely undecidable (unsolvable) problems as opposed to undecidable within "a system", cf Post 1941 finally published in Davis 1965:340). Is this what you mean?

Bill 19:35, 14 October 2007 (UTC)

See also the Talk:Entscheidungsproblem where I have been slowly developing a detailed historical look at "the decision problem". Basically, incompleteness is one expression of the notion of decision-problem. Folks have wondered why Godel didn't just go ahead and prove the "decision problem" undecidable: for an answer to this see the article-extension History of the Church-Turing thesis. Bill Wvbailey 21:31, 14 October 2007 (UTC)[reply]

Reply

I can't cite a source for most of the stuff, because I am lazy. But I'll do some research tomorrow and try to fix it up. Thanks for reading it over. Likebox 06:32, 15 October 2007 (UTC)[reply]

counter-machines, register-machines, RAMs and RASPS

I have a lot of the references re counter machine, RAM, and RASP in .pdf so if you see any that you want to read, lemme know at my talk page. Bill Wvbailey 19:28, 15 October 2007 (UTC)[reply]

[1] I reworded this into its correct formulation. Turing's original proof #1 upon which this proof #2 is built, is far more constructive than the common halting-problem proof devised by Davis. In that proof the testing program H gets locked into an infinitely-repeating circle and fails to print the diagonal number (of itself) when it finally comes to the test its own number. There is nothing whatever in Turing or thereafter in his lifetime about HALTING. This concept is attributable to Post (1936) and discussions of terminating algorithms in Church 1934 etc, and was finally used by Davis in his "halting problem" proof -- original to him -- in the mid-1950's in his text (I forget the year -- mid-1950's). Davis confirmed his first-use to me personally, and it also appears in the reference as cited on the halting problem page. I have verified this reference with my own eyes.

[2] I don't doubt that this is true, I'm just looking for a source. I am very familiar with Kleene 1952.

[3] Actually, all the undecidability proofs, including Godel's 1931 have a similar structure -- they all have diagonalization at their heart/core. I do have a published source for that observation, somewhere, if you need it. See the addition in the next section below, it's in one or the other of those two articles.

[4] I do not have the vaguest idea of what this means. "Natural forms"? I do know that Post and Finser were looking for absolutely undecidable (unsolvable) problems as opposed to undecidable within "a system", cf Post 1941 finally published in Davis 1965:340). Is this what you mean?

[1]

[2]

[3]

[4]