On 10/10/2026 22:57, olcott wrote:
On 10/10/2026 3:31 AM, Mikko wrote:
On 09/10/2026 14:40, olcott wrote:
On 10/9/2026 3:18 AM, Mikko wrote:
On 07/10/2026 15:25, polcott wrote:
On 10/7/2026 5:40 AM, Mikko wrote:
On 02/10/2026 15:28, olcott wrote:
On 10/1/2026 10:05 PM, dart200 wrote:
On 10/1/26 5:28 PM, Chris M. Thomasson wrote:
On 10/1/2026 3:54 PM, dart200 wrote:
[...]
Are you saying that the halting problem is not solvable? If >>>>>>>>>> so, so what?
it is solvable for an enumerable set of machines that includes >>>>>>>>> all possible output sequences, it is not solvable for all
possible machines
The key mistake of the halting theorem is that
it requires a halt decider to report on the behavior
of the direct execution of DD() from main()
No, it isn't. The halting problem says nothing about "DD()" or
"main()".
The halting problem asks "How can one determine whether a
computation
halts?"
Here is the same thing from Linz where H and Ĥ.embedded_H are
also based on UTM simulation of their inputs.
*From the bottom of page 319 has been adapted to this*
Earlier on that page Linz says: "Simply stated, the problem is: given >>>>> the description of a Turing machine M and an input w, does M, when
started in the initial configuration qow, perform a computation that >>>>> eventually halts?"
At the bottom of the page, continuing to the next page, is a formal
definition of the solution of the halting problem, which Linz defines >>>>> as a Turing machine.
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.∞, // accept state
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn // reject state
There is no "embedded_H" in Linz's definition.
<Linz text>
From H' we construct another Turing machine Ĥ.
That is later in the text, not in the definition 12.1, so irrelevant
to this discussion.
I am ONLY talking about the Linz machine that totally
implements the Halting Problem counter-example input.
You are trying to cheat with a switch of topid and a pretension that
what was said abaut one topic be true about the other.
The topic was the definition of the "halting problem" and in particular
how Linz defines it. As long as you don't understand or can't express
that there is no point to go further.
Good. Then we have finally isolated the disagreement completely.
You now explicitly require not merely:
H's answer must be correct.
but:
H's answer must be obtained through a particular
semantically approved sequence of inference steps.
You even say:
"It cannot even be a correct guess."
That is an EXTRA requirement.
Computability theory normally asks whether a computation computes the correct mapping:
input -> output
It does not additionally require every intermediate inference step to constitute a proof of the semantic fact represented by the output.
For example, if two programs return exactly the same correct answer on
every input, they compute the same function even if one uses simulation,
one uses theorem proving, and one uses a lookup table.
So your logical target is now extremely precise:
You must prove that semantic correctness of the OUTPUT
requires semantic correctness, in your special sense,
of the particular INFERENCE PATH used to obtain it.
Neither Post's finite-string model nor operational semantics gives you
that requirement.
You have added it.
And this matters far beyond DD: without that new requirement, your distinction between HHH(DD)==0 and HHH1(DD)==1 cannot redefine the
halting predicate.
So before moving to the much larger goal of making
"true on the basis of meaning expressed in language"
computable, this much smaller proposition needs a formal proof.
Otherwise "correct transformation" is simply being defined as "a transformation following the semantics
I require",
and then used to--
prove that only those transformations are correct.
That is circular.
There is an even more fundamental problem with saying that a lookup
table "computes no mapping".
Go down to the hardware implementation of arithmetic itself.
A binary half-adder implements exactly this finite mapping:
inputs outputs
A B SUM CARRY
0 0 -> 0 0
0 1 -> 1 0
1 0 -> 1 0
1 1 -> 0 1
A full adder does the same thing with an additional carry input, giving eight cases.
Now this can be implemented with logic gates.
But it can ALSO be implemented literally as a tiny ROM:
address bits = A,B
stored bits = SUM,CARRY
Then the physical operation is simply:
apply address -> retrieve stored bits
In other words, a hardware lookup table.
Nothing inside that ROM performs an additional semantic proof that
1 + 1 = 10 binary.
Yet by composing these elementary mappings we construct an arithmetic
unit that computes addition.
So if you maintain that lookup-table B "computes no mapping", where
exactly does the REAL computation of addition begin?
You cannot answer "some earlier process constructed the table", because
the same issue recurs at the lowest hardware level.
Ultimately the machine consists of physical mechanisms implementing elementary mappings.
We call the resulting process "addition" because the composition of
those mappings realizes the mathematical addition function.
The hardware does not additionally prove that its output is semantically entailed by arithmetic.
This exposes the distinction I have been making:
SEMANTICS specifies the mapping we require.
COMPUTATION implements that mapping.
PROOF establishes that the implementation
satisfies the specification.
Those are three different things.
Your argument is effectively requiring COMPUTATION itself to contain PROOF.
That is not something you get from Post plus operational semantics.
And if a ROM implementing the truth table above "computes no mapping",
then your definition has the remarkable consequence that the elementary components from which actual arithmetic computers are constructed do not compute their mappings either.
Peter,
This actually clarifies the disagreement considerably.
I wrote:
Your argument is effectively requiring COMPUTATION itself to contain
PROOF.
and you answered:
Yes.
Good. Then this is now the precise point that needs justification.
In standard computability theory, a machine transition
C -> C'
is not required to be a semantic entailment
C |= C'
nor a proof step from stipulated axioms.
It is simply a transition specified by the machine's transition function.
Of course one can DESIGN a computation whose transitions encode valid inference steps. A theorem prover does exactly that. But it does not
follow that every computation must be such a proof.
Your arithmetic example makes the problem especially clear.
Consider two 8-bit adders.
A is constructed conventionally from gates and full adders.
B is a ROM containing all 65536 mappings
(x,y) -> (x+y) mod 256.
For every possible input,
A(x,y) = B(x,y).
Now either B computes addition or it does not.
If it does, then lookup tables can compute mappings, which was my point.
If it does not, then you need to explain why two machines implementing exactly the same input/output function differ as to whether they
"compute" that function.
And appealing to "stipulated axiom finite strings" does not solve this.
I can simply stipulate the 65536 ROM entries as finite-string axioms:
ADD(0,0)=0
ADD(0,1)=1
...
ADD(255,255)=254
The ROM lookup is then direct application of one of your stipulated
finite strings.
If those entries must themselves be derived from something else before
their use counts as computation, then they were not foundational
stipulated axioms after all, and the same question merely moves back one level.
So we have finally isolated the issue.
You are defining computation to require syntactically represented
semantic entailment from stipulated axioms.
That is a perfectly possible definition of a particular kind of formal inference process.
What has not been established is that this is the definition of
computation used by Post, Turing, or standard computability theory.
Saying
"that is the way ... it has always worked"
does not establish that.
Please identify the definition or theorem in Post, Turing, or standard operational semantics from which the following implication follows:
valid computational transition
=>
syntactically represented semantic entailment
from stipulated axiom finite strings.
That implication is now the entire issue.
Without it, your argument does not refute the halting theorem. It
changes the definition of computation and then proves a result about the changed definition.
BTW, have you read Greg Egan's novels and short stories?
It is not. It is my improvement of what they said built
on top of my generic paraphrase of Post.
Then we agree on an important point: your requirement that computation consist of syntactically specified semantic entailment is not a
requirement of Post, Turing, or standard computability theory. It is a
new requirement introduced by your own theory.
That is perfectly legitimate as a research proposal, but it means that results obtained from that additional requirement do not, by themselves, overturn results about Turing computation.
There is also a problem with your new Axiom 2:
Random answers to specific questions are never correct.
Literally, that is false. If I randomly answer YES or NO to
Is 2+2=4?
I may randomly answer YES, which is correct.
What I think you mean is:
Arbitrary answers provide no guarantee of correctness.
That is true, but it does not imply:
Computation requires every transformation to be
a semantically entailed transformation.
Those are very different propositions.
The ROM example exposes the difference.
Suppose I manufacture a 16-bit-address, 8-bit-output ROM whose contents,
by sheer accident, happen to satisfy
ROM[x,y] = (x+y) mod 256
for every x,y.
No previous process computed the table. Nothing was "off-loaded." We
simply discovered afterward that this physical device implements the 8-
bit addition function.
When presented with (23,42), it returns 65.
Does this device compute the 8-bit addition function?
If not, then your definition of "computes" depends not merely on the machine's structure and behavior, but on the causal history by which its contents came to exist.
That would be a radically different concept from computation in computability theory.
Also:
Table look up is not maximum algorithm compression
Agreed, but that is a different question.
Whether an implementation computes a function and whether it is a
maximally compressed algorithm for that function are not equivalent questions.
Finally:
Even the category of a counter-example cannot possibly exist.
MECE cannot establish that.
MECE can describe how you partition a domain. It cannot prove that your premises are true or that your proposed categories correctly model the phenomenon under investigation.
Indeed, if a theory concludes in advance that the category of counterexamples "cannot possibly exist,"
that is precisely where I would
look hardest for an unstated assumption.
So I think we have made substantial progress.
We no longer need to debate whether Post requires your notion of
semantic computation: you have now explicitly said that he does not.
The question is therefore much simpler:
Can you derive
computation
=>
correct semantic entailment from stipulated axioms
rather than simply defining "computation" to mean that?
Because if it is a definition, you have introduced a new class of
processes.
If it is a theorem about computation generally, it needs a proof
independent of that definition.
BTW, since you mentioned that you had never heard of Greg Egan, I think--
you might genuinely enjoy some of his work. He is unusually interested
in exactly the boundary between computation, implementation, semantics, identity and physical realization that we keep running into here.
A few suggestions, roughly in the order I would recommend them to you:
* **"Learning to Be Me"** (short story, in *Axiomatic*) — probably the most directly relevant. People have neural "jewels" implanted that learn
to reproduce their brains' input/output behavior until they can replace
the biological brain. It raises almost exactly the question: when does reproducing a mapping become reproducing the process or person that generated it?
* **Permutation City** — simulated minds, computational identity, and
the question of what it means for a computation to be physically instantiated. If two implementations realize the same computational structure, what makes one of them "real"? This is probably the Egan
novel most relevant to our disagreement.
* **"Axiomatic"** (short story) — asks what happens when apparently foundational beliefs and values can themselves be technologically
modified. Given your interest in foundational axioms, you may appreciate
the joke implicit in the title.
* **Diaspora** — begins with the creation of an artificial mind and then goes much further into questions of mathematical description, physical reality, simulated environments and post-human intelligence.
* **"Luminous"** — especially relevant if you are interested in the relationship between formal systems, mathematical truth and physical computation. It plays with the rather disturbing idea that mathematics itself might not be as implementation-independent as we normally assume.
* **"Oracle"** — deals with artificial intelligence, computability, mathematics and an alternate-history confrontation over the intellectual consequences of advanced computation.
* **"Singleton"** — explores quantum mechanics, computation and personal identity, including the consequences of trying to construct an
artificial intelligence.
* **"Crystal Nights"** — artificial life is evolved inside a
computational environment, raising the question of whether entities generated by a computational process acquire meanings, purposes and interests that were not explicitly supplied by their programmers.
If you only try three, I would suggest:
Learning to Be Me
Permutation City
Luminous
Egan is a programmer as well as a science-fiction writer, and unlike a
great deal of SF that merely uses computation as decoration, he tends to take the computational and mathematical premises seriously and then
follow their consequences somewhere uncomfortable.
I suspect you will disagree with him quite a lot, which is one reason I think you might find him interesting.
Peter,
I guess that we have to construe the circuitry as
equivalent to a proof.
I think that sentence exposes exactly the problem.
Equivalent to WHAT proof, in WHAT formal system?
An adder circuit implements a function. We can construct a proof that
the circuit implements addition correctly, but the circuit and that
proof are not the same thing.
For example, let C be an 8-bit adder circuit. We may prove:
for all x,y:
C(x,y) = (x+y) mod 256
Here we have three distinct objects:
specification: (x,y) -> (x+y) mod 256
implementation: C
proof: C satisfies the specification
Calling C itself "equivalent to a proof" simply collapses those three distinctions by definition.
And it immediately brings us back to the ROM problem.
Suppose C is implemented with gates.
Now synthesize exactly the same Boolean function into LUTs.
Or implement it as a ROM containing its truth table.
All three devices implement exactly the same mapping.
So if the gate circuit is "equivalent to a proof", is the LUT
implementation also equivalent to a proof?
Is the ROM?
If not, precisely what proof-theoretic property disappeared during the transformation?
This is not merely hypothetical. FPGA LUTs are literally small stored
truth tables used to implement Boolean functions. Logic synthesis
routinely moves between Boolean descriptions and LUT implementations.
So I think "the circuitry is equivalent to a proof" does not solve the problem. It makes the circularity more visible:
Why is this a computation?
Because it embodies a proof.
Why does it embody a proof?
Because it correctly computes the function.
Correctness of an implementation can be PROVED.
It does not follow that the implementation IS a proof.
A CPU executing
return x + y;
does not have to prove arithmetic before it can add x and y.
We may have to prove that the CPU's adder is correct.--
That is our proof about the computation, not the computation's proof of itself.
Peter,
I think your latest reply reveals a very important change in the subject
of the discussion.
You wrote:
Sheer accident provides zero basis for knowledge.
My system's domain is general knowledge expressed
as relations between finite strings.
But I did not ask whether the accidental ROM provides a basis for
KNOWLEDGE.
I asked whether it COMPUTES the function.
Those are different questions.
Suppose the ROM happens to satisfy
ROM[x,y] = (x+y) mod 256
for every possible input.
Then there are at least three separate questions:
1. Does the device implement the addition mapping?
2. Do we know that it implements the addition mapping?
3. Can we prove that it implements the addition mapping?
The answer to (1) can be yes while the answers to (2) and (3) are no.
Indeed, that was precisely the purpose of the accidental-ROM example.
You replied that accident provides no basis for knowledge.
Agreed.
But that answers (2), not (1).
This also explains why I don't think the Prawitz reference establishes
what you need.
Proof-theoretic semantics is indeed concerned with explaining meaning in terms of proof, and Prawitz discusses the connection between knowing
that a mathematical sentence is true and having a proof of it.
But that is an epistemological/semantic claim about mathematical
assertion and proof.
It does not establish:
computation = justified knowledge
or:
every computational transition = semantic inference.
In fact, your latest formulation seems increasingly to describe a theory
of justified inference rather than a theory of computation.
There is another interesting development in your answer.
Previously, you said that lookup does not itself perform the computation because the computation was "off-loaded."
Now you say:
All of your table lookups are stipulated.
So my system remains correct and coherent.
and:
ROM is stipulated relations.
I am happy to accept that for the sake of argument.
But then any finite function can be represented as stipulated relations.
For a finite domain
A = {a1,...,an}
and any function f, I can stipulate
a1 -> f(a1)
a2 -> f(a2)
...
an -> f(an)
and implement exactly those stipulated relations in a ROM.
So the distinction between gate computation and ROM lookup has
disappeared from your criterion.
This also connects directly to actual computer hardware.
The same finite Boolean function can be implemented as:
gates
PLA
FPGA LUTs
ROM
and representations can be mechanically transformed between these forms.
If ROM relations qualify because they are "stipulated", then there is no longer any reason to say that computation was performed elsewhere and
merely stored in the ROM. The ROM itself implements the stipulated mapping.
More importantly, however, your present definition appears to be:
acceptable transformation =
semantically entailed transformation
OR
stipulated transformation.
That may define a formal system of justified transformations.
But why should that be identified with COMPUTATION?
Your Prawitz quotation may provide motivation for identifying
mathematical knowledge with proof under a proof-theoretic conception of meaning.
It does not provide the missing implication:
computation
=>
knowledge
=>
proof
=>
semantic entailment or stipulation.
And your final statement makes the problem especially clear:
It seems to me that the only category of proof that
I will be able to provide is self-evidence:
proven true on the basis of meaning.
I think this is exactly where we need to be extremely careful.
If your crucial foundational claim is:
Computation requires correct rather than
arbitrary finite string transformations
we need to distinguish two readings of "correct".
Reading A:
The machine actually produces the value specified
by the function.
Then the accidental ROM is correct, regardless of whether anybody knows
or can prove that it is correct.
Reading B:
The transformation is justified as correct by
semantic entailment or stipulation.
Then you have changed "correct computation" into "justified computation".
That is an epistemic notion.
And the Halting Theorem is not a theorem about what we can justify as knowledge. It is a theorem about what Turing machines can compute.
This distinction becomes especially important when you say:
Undecidability ceases to exist within this new foundation.
It may instead be that you have defined a new notion of "decision" under which only semantically justified transformations count as decisions.
If so, undecidability has not been eliminated.
You have changed the meaning of "decider".
Before claiming that the Halting Theorem has been overturned, I
therefore think you need to establish one very specific bridge:
standard Turing computation
=>
your semantically justified computation.
And "self-evidence" cannot establish that bridge if the self-evidence
comes from the meaning you have assigned to the word "computation".
Otherwise the reasoning is:
I define computation as correct justified transformation.
Therefore every computation is a correct justified transformation.
Therefore the standard theory of computation is wrong
whenever it permits transformations not satisfying my
justification criterion.
That conclusion follows from the new definition, not from a discovery
about Turing computation.
So I think we have now reached an even more fundamental question than
the ROM example:
Are you proposing a new theory of COMPUTATION,
or a new theory of JUSTIFIED KNOWLEDGE represented by finite strings?
Those are not the same project.
Peter,
I think this sentence finally identifies the fundamental difference
between your system and computability theory:
If we have no way to determine whether or not
X is true then X is necessarily outside of the
body of knowledge, thus outside of the domain
of my system.
That is perfectly coherent as a restriction on the domain of your system.
But then I don't see how you can conclude that you have eliminated undecidability.
You have excluded it.
Suppose I define
D = { propositions whose truth can be determined
by the permitted methods of my system }.
Then naturally:
for every X in D,
the truth of X can be determined by my system.
But this does not establish:
for every X,
the truth of X can be determined.
It establishes the first statement by restricting D.
In particular, consider HALT:
HALT(P,I) =
TRUE if program P halts on input I
FALSE otherwise.
The standard Halting Theorem says that there is no Turing machine H such that, for every P and I,
H(P,I) = HALT(P,I).
function LoopIfYouSayItHalts (bool YouSayItHalts):
if YouSayItHalts () then
while true do {}
else
return false;
Does this program Halt?
(Your (YES or NO) answer is to be considered
translated to Boolean as the function's input
parameter)
Please ONLY PROVIDE CORRECT ANSWERS!
Now suppose some instances of HALT cannot be determined by your
permitted semantic methods.
An [incorrect question] is defined as any question such that
a correct answer does not exist from the set of all possible
answers.
According to what you have just written, those instances are:
outside of the domain of my system.
Fine.
But then your system has not decided HALT.
It has declined to include those cases in its domain.
There is an enormous difference between:
"There are no undecidable propositions in my domain"
and:
"There are no undecidable propositions."
The first can be obtained simply by defining the domain to contain only propositions for which an accepted determination exists.
The second is the extraordinary mathematical claim that would contradict standard undecidability results.
Your statement appears explicitly to give us the first, not the second.
This also clarifies something about our hardware discussion.
You now say:
Circuitry / lookup tables are type (1).
and type (1) is:
Stipulated relation foundational axioms.
That resolves our previous disagreement about ROM versus gates inside
your system: you are now treating both as stipulated relations.
But consider again the accidental ROM.
Suppose a ROM happens, completely accidentally, to contain the complete 8-bit addition mapping.
At time T1 nobody knows this.
We then exhaustively examine all 65536 entries and discover:
ROM[x,y] = (x+y) mod 256
for every x,y.
At time T2 we know that it implements addition.
Nothing whatsoever has changed inside the ROM between T1 and T2.
So did the ROM become an "axiom" at T2?
If so, "axiom" is not describing a computational property of the ROM.
It is describing our epistemic relationship to the ROM.
That seems consistent with your statement:
My system's domain is general knowledge
and also with the Prawitz passage concerning what it means to KNOW that
a sentence is true.
But that would make your project fundamentally a theory of knowledge/ justification, rather than a replacement foundation for computability.
And I think this distinction is now crucial.
Proof-theoretic semantics may tell us something about:
what justifies asserting X?
Computability theory asks:
what function does this machine compute?
Those are different questions.
There is also a smaller point about the carry-lookahead example.
You wrote:
Even a look-ahead carry generator implements conventional
elementary school 1st grade arithmetic.
Certainly it implements arithmetic.
But "implements arithmetic" is precisely the distinction I have been
making.
A carry-lookahead adder need not reproduce the elementary-school
sequential procedure. It uses generate/propagate logic specifically to reorganize carry dependencies so that they can be evaluated much more in parallel.
Different algorithms and radically different circuits can implement the
same mathematical function.
That is why I distinguish:
mathematical function/specification
implementation/computation
proof of correctness
But I think the domain issue is now much more fundamental than our
hardware examples.
So let me ask one very precise question.
Consider a particular HALT instance X for which your permitted methods provide no determination.
You have just said that such an X is outside the domain of your system.--
Does your system nevertheless return TRUE or FALSE for X?
If YES, please specify how it obtains the correct answer.
If NO, then X remains undecided.
Calling X "outside the domain" has not eliminated its undecidability.
It has only eliminated X from the set of questions your system
undertakes to decide.
Peter,
I think your latest reply reveals a very important change in the subject
of the discussion.
You wrote:
Sheer accident provides zero basis for knowledge.
My system's domain is general knowledge expressed
as relations between finite strings.
But I did not ask whether the accidental ROM provides a basis for
KNOWLEDGE.
I asked whether it COMPUTES the function.
Those are different questions.
Suppose the ROM happens to satisfy
ROM[x,y] = (x+y) mod 256
for every possible input.
Then there are at least three separate questions:
1. Does the device implement the addition mapping?
2. Do we know that it implements the addition mapping?
3. Can we prove that it implements the addition mapping?
The answer to (1) can be yes while the answers to (2) and (3) are no.
Indeed, that was precisely the purpose of the accidental-ROM example.
You replied that accident provides no basis for knowledge.
Agreed.
But that answers (2), not (1).
This also explains why I don't think the Prawitz reference establishes
what you need.
Proof-theoretic semantics is indeed concerned with explaining meaning in terms of proof, and Prawitz discusses the connection between knowing
that a mathematical sentence is true and having a proof of it.
But that is an epistemological/semantic claim about mathematical
assertion and proof.
It does not establish:
computation = justified knowledge
or:
every computational transition = semantic inference.
In fact, your latest formulation seems increasingly to describe a theory
of justified inference rather than a theory of computation.
There is another interesting development in your answer.
Previously, you said that lookup does not itself perform the computation because the computation was "off-loaded."
Now you say:
All of your table lookups are stipulated.
So my system remains correct and coherent.
and:
ROM is stipulated relations.
I am happy to accept that for the sake of argument.
But then any finite function can be represented as stipulated relations.
For a finite domain
A = {a1,...,an}
and any function f, I can stipulate
a1 -> f(a1)
a2 -> f(a2)
...
an -> f(an)
and implement exactly those stipulated relations in a ROM.
So the distinction between gate computation and ROM lookup has
disappeared from your criterion.
This also connects directly to actual computer hardware.
The same finite Boolean function can be implemented as:
gates
PLA
FPGA LUTs
ROM
and representations can be mechanically transformed between these forms.
If ROM relations qualify because they are "stipulated", then there is no longer any reason to say that computation was performed elsewhere and
merely stored in the ROM. The ROM itself implements the stipulated mapping.
More importantly, however, your present definition appears to be:
acceptable transformation =
semantically entailed transformation
OR
stipulated transformation.
That may define a formal system of justified transformations.
But why should that be identified with COMPUTATION?
Your Prawitz quotation may provide motivation for identifying
mathematical knowledge with proof under a proof-theoretic conception of meaning.
It does not provide the missing implication:
computation
=>
knowledge
=>
proof
=>
semantic entailment or stipulation.
And your final statement makes the problem especially clear:
It seems to me that the only category of proof that
I will be able to provide is self-evidence:
proven true on the basis of meaning.
I think this is exactly where we need to be extremely careful.
If your crucial foundational claim is:
Computation requires correct rather than
arbitrary finite string transformations
we need to distinguish two readings of "correct".
Reading A:
The machine actually produces the value specified
by the function.
Then the accidental ROM is correct, regardless of whether anybody knows
or can prove that it is correct.
Reading B:
The transformation is justified as correct by
semantic entailment or stipulation.
Then you have changed "correct computation" into "justified computation".
That is an epistemic notion.
And the Halting Theorem is not a theorem about what we can justify as knowledge. It is a theorem about what Turing machines can compute.
This distinction becomes especially important when you say:
Undecidability ceases to exist within this new foundation.
Peter,
What is the correct return value that a halt decider
can provide for a program that does the opposite of
whatever value it returns?
Neither value.
And that is exactly the proof of the Halting Theorem.
An [incorrect question] is defined as any question such that a correct answer does not exist from the set of all possible answers.
Assume H is a correct total halt decider, and construct D so that:
if H(D) says HALTS:
D loops forever
if H(D) says DOES NOT HALT:
D halts
Now ask H(D).
If H(D) says HALTS, it is wrong.--
If H(D) says DOES NOT HALT, it is wrong.
Therefore there is no value H can return while remaining a correct halt decider.
But notice what follows logically.
It is NOT:
therefore D is an "incorrect question".
It is:
therefore the assumed correct total H does not exist.
That is the reductio.
We assumed:
H exists and correctly decides every program.
From that assumption we constructed D and derived:
H(D) cannot be correct.
Therefore the assumption is false.
In symbols:
Assume H exists.
Construct D using H.
H(D) = HALTS
=> D does not halt
=> H is wrong.
H(D) = DOES_NOT_HALT
=> D halts
=> H is wrong.
Therefore H cannot satisfy its assumed specification.
That is precisely the Halting Theorem.
Your question therefore does not expose a misconception in the proof.
It reproduces the contradiction used by the proof.
The only way to obtain a different conclusion is to explain why the contradiction should be attributed to the QUESTION rather than to the assumption that H exists.
And that requires an independent argument.
You cannot simply define:
a question for which no correct answer can be
returned by H is an "incorrect question"
because the entire purpose of the diagonal construction is to prove that
no such universally correct H exists.
Doing that would transform:
Assume H exists.
Derive contradiction.
Therefore H does not exist.
into:
Assume H exists.
Derive contradiction.
Therefore exclude the case producing the contradiction
from H's domain.
But that simply protects the original assumption by restricting its domain.
And then H is no longer a halt decider for all programs.
So to answer your simplified question as directly as possible:
What correct value can H return for D?
NONE.
And the standard conclusion is:
therefore a total correct H cannot exist.
If your conclusion is instead:
therefore D is outside H's domain,
then you have conceded the standard result:
H cannot decide halting for every program.
You have simply given the undecidable case a different name.
Peter,
I followed the x86utm link and read the README, and I think this finally gives us a very precise technical point to examine.
Your README says:
The key mistake of the halting problem proofs is that they
require a halt decider to report on the behavior of something
other than the behavior specified by its finite string input.
and Axiom 2 says:
The only correct finite string transformation rules that HHH
is allowed to apply to its finite string input DD is specified
by the operational semantics of the C programming language.
This requires DD to be simulated by HHH according to these rules.
I think the second statement is exactly where your argument departs from
the Halting Theorem.
A hypothetical halt decider is NOT required to determine termination by simulating its input.
Peter,
I think we have now achieved an important clarification, and I want to preserve it rather than continue arguing past it.
I wrote:
Then you have changed "correct computation"
into "justified computation".
That is an epistemic notion.
and you answered:
Yes. That is a correct clarification.
Good.
You have also now accepted that the ROM itself implements its stipulated mapping. So I think our hardware disagreement is essentially resolved.
The remaining issue is much narrower.
You write:
Deciders must apply finite string transformations that are
semantically relevant to the decision criteria.
I think your three recent replies now identify the exact point on which
we disagree.
You say:
A halt decider is required to derive its result through
the application of finite string transformations to its
finite string input. The halting theorem totally ignores
this.
and:
A halt decider is also implicitly required to limit these
finite string transformations to those relevant to determining
the halting property specified by this finite string input.
The halting theorem totally ignores this.
and:
The halting theorem is framed as the impossibility of
a halt decider returning a correct value to its caller
that is not even its input.
I don't think the Halting Theorem ignores any of these issues.
I think you are conflating three different things:
1. the finite representation of a program P,
2. the computation denoted by that representation,
3. the context in which that computation is executed.
These are related, but they are not identical.
Consider an ordinary static analyzer A.
I can give A the finite source code:
int f() {
return 17;
}
The INPUT to A is a finite string representing f.
What A is asked to determine is a property of the computation denoted by that finite string.
There is no contradiction here between:
static finite string input
and:
executing process.
The finite string REPRESENTS the program whose possible execution we are reasoning about.
That distinction is fundamental to essentially all program analysis.
Likewise, there is no "mutual exclusivity" between a program being the caller of a function during one execution and a representation of that
same program being the input data of that function.
Assume H exists.
Then construct D:
D():
if H(<D>) == HALTS:
loop forever
else:
halt
Now ask H(<D>).
If H says HALTS, D does not halt.
If H says DOES_NOT_HALT, D halts.
You call this an "incorrect question".
function LoopIfYouSayItHalts (bool YouSayItHalts):
if YouSayItHalts () then
while true do {}
else
return false;
Does this program Halt?
(Your (YES or NO) answer is to be considered
translated to Boolean as the function's input
parameter)
Please ONLY PROVIDE CORRECT ANSWERS!
An [incorrect question] is defined as any question such that
a correct answer does not exist from the set of all possible
answers.
Peter,
I think your latest example makes the disagreement extremely precise:
int main()
{
DD(); // is neither the input to HHH nor a finite static string
}
I completely agree with the comment.
DD() executing in main is NOT the input to HHH.
But the Halting Theorem does not require it to be.
Peter,
When both of your own answers are wrong this proves
that I am correct.
No. It proves exactly the Halting Theorem.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,142 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 94:08:02 |
| Calls: | 14,704 |
| Calls today: | 2 |
| Files: | 186,497 |
| D/L today: |
2,661 files (886M bytes) |
| Messages: | 2,551,683 |