On 4/26/2026 3:09 AM, Mikko wrote:Which is not quite correct. The input should be rejected as incompleteOn 25/04/2026 15:25, olcott wrote:>>>>>> That does not help if it is not known whether such sequence ofOn 4/25/2026 3:20 AM, Mikko wrote:typedef int (*ptr)();>inference steps exists.>
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
The halting problem counter-example is grounded. One of the following
statements is true per the definition of "halting decider":
- The proposed decider accepts the counter-example.
- The proposed decider rejects the counter-example.
- The proposed decider is not a halting decider.
It is not necessary to know which one is true. Each one is sufficient
to infer that the propsed decider is not a halting decider.
>
Whether a halting oracle is possible is another problem. Accordint to
the CHurch-Turing thesis it isn't but there is no known proof.
>
int HHH(ptr P);
int DD()
{
int Halt_Status = HHH(DD);
if (Halt_Status)
HERE: goto HERE;
return Halt_Status;
}
int main()
{
HHH(DD);
}
Proof theoretic halt prover HHH is fully operational
code since 2022 can correctly rejects its input DD
as lacking a well-founded justification tree.
(unless the exact meaning of HHH is a part of the input language).
It does not make sense to say that the input ahs or lacks a
justification tree (just like it does not make sense that the
input "25 + 79" to an addition program has or lacks a justification
tree). There is nothing in the input that requires a justification
tree. The output must have a justification tree, though usually a
decider is not required to show it. Also the justification tree
(or some other form of proof) of the correctness is often required.
HHH is on line 1081If HHH in DD is interpreted to mean that routime then the question
https://github.com/plolcott/x86utm/blob/master/Halt7.c
whether a call to DD ever returns (instead of looping forever or
aborting for stack or heap overflow or some other reason) is valid.
HHH is a proof-theoretic-semantics halt prover:It does not count as a prover as it does not output a proof.
it accepts exactly those programs whose simulation
admits a finite, well-founded justification tree,
and rejects those whose simulation is non-well-founded.
For a halting computation the excution trace is almost all
of a proof but for a non-halting computation it isn't.
Under the operational semantics of C as implemented--
by HHH, the simulation of DD induces a recursive
self-reference cycle; therefore, no finite, well-founded
justification tree exists for DD under HHH.
Mikko
Les messages affichés proviennent d'usenet.