*** SOLVABILITY OF THE HALTING PROBLEM ***

[|-|erc]

It's quite simple. First lets review the Halting proof.

Let Halt(TM#, input) = {'halts' IFF TM(input) eventually halts,
'runs_forever' otherwise}

We will call TM# the godel number of the test Turing Machine TM
but it can be any numerical representation of the program.

Let Loops(TM#) = IF Halt(TM#, TM#) = 'halts'
THEN x: GOTO x

Let Loops# be the godel number of Loops.

What is the value of Halt(Loops#, Loops#)?

If Halt(Loops#, Loops#) = 'halts' then
Loops(Loops#) -> IF Halt(Loops#, Loops#) = 'halts'
THEN x: GOTO x
-> x: GOTO x
-> Loops(Loops#) does not halt
-> Halt(Loops#, Loops#) = 'runs_forever'
-> CONTRADICTION

If Halt(Loops#, Loops#) = 'runs_forever' then
Loops(Loops#) -> IF Halt(Loops#, Loops#) = 'halts'
THEN x: GOTO x
-> Loops(Loops#) halts
-> Halt(Loops#, Loops#) = 'halts'
-> CONTRADICTION

Therefore Loops is not computable, which is based on Halt,
so Halt is not computable.

-----------------------------------------------------------

Now consider the function smartHalt!

Let sHalt(TM#, input) = {'dont_know' IFF TM# = input,
'halts' IF TM(input) eventually halts,
'runs_forever' otherwise}

Let sLoops(TM#) = IF sHalt(TM#, TM#) = 'halts'
THEN x: GOTO x

What is the value of sHalt(sLoops#, sLoops#)?

If sHalt(sLoops#, sLoops#) = 'halts' then
sLoops(sLoops#) -> IF sHalt(sLoops#, sLoops#) = 'halts'
THEN x: GOTO x
-> IF 'dont_know' = 'halts'
THEN x: GOTO x
-> sLoops(sLoops#) halts

There is no contradiction, we have a consistent solution!

Therefore, it may be possible to program a slightly restricted
3 valued Halting function.

Herc
--
~~~~~~~~~~~~~~~~~~~~~~~~~~~~

[The Ghost In The Machine]

In sci.logic, |-|erc
<h@r.c>
wrote
on Wed, 06 Aug 2008 02:27:23 GMT
<f_7mk.25836$IK1....@news-server.bigpond.net.au>:

Yes, that'll completely solve a modified problem. The
original problem was to construct Halt() that applies to
*all* valid Godel number/input pairs (assuming Valid(TM#)
is computable). This problem, as your proof shows above,
is unsolvable, leading to a contradiction.

Your modification solves completely the problem of defining
a function sHalt() that will only correctly compute only
a proper subset of all Godel number/input pairs. The
function

sLoops(TM#) = IF sHalt(TM#, TM# || NOP) = 'halts'
THEN x: GOTO x

(where || is defined in accordance with the Godel encoding)

is a trivial workaround, mangling your function. The proper
solution of this issue looks to be a fair amount of work.

>
> Therefore, it may be possible to program a slightly restricted
> 3 valued Halting function.

It *is* possible. Let

nHalt(TM#, input) = 'dont_know'.

be defined. Such a function satisfies all of your
requirements, although it's not horribly useful.

One can also define

lHalt(TM#, input) = IF pair<TM#, input> IS A KEY OF knowledgeLookupTable
THEN return knowledgeLookupTable[pair<TM#, input>]
ELSE return 'dont_know'

which is relatively uninteresting.

The most interesting implementation (IMO) of tHalt() I can
think of would analyze the program's static flow graph,
returning 'halts' if the flow graph is reducible and the
loops are all for-loops, which, if expressed in an idealized
assembly language [*], might mutate into the form

MOV startval, lvar(SP) \
... +-- these can swap
MOV termval, lterm(SP) /
...
L1:
...
COMPARE lterm(SP), lvar(SP)
JUMPIFLESS L1END
...
INCREMENT lvar(SP)
...
JUMP L1
L1END:

where '...' indicates a reducible block, or a variant which
replace lterm(SP) with #cterm, or a perturbation of either,
so long as INCREMENT is guaranteed to be hit exactly once
between L1 and the JUMP, and nothing else within the loop
modifies lterm(SP) or lvar(SP).

(One can do certain optimizations such as code-hoisting here.)

Obviously this is a proper subset of all programs, as
the muLoop:

L1:
...
CALL predicateFunction
COMPARE returnVal, #0
JUMPIFNOTEQUAL L1END
...
JUMP L1
L1END:

or the far less useful dumbLoop [+]:

L1:
...
JUMP L1

do not fit this form.

Exactly what problem are you trying to solve, TrueMan?

>
> Herc

[*] the syntax I'm using is vaguely reminiscent of VAX
assembler, with "MOV from, to" moving a piece of
data appropriately. Other language variants are of
course possible.

[+] if one assumes a program can be externally killed, the
dumbLoop can be useful; such is the case with a lot
of daemons whose sole purpose is to process input,
then loop around and wait for more. Without external
kill possibilities, however, one has to include a
test of some sort.

--
#191, ewi...@earthlink.net
If your CPU can't stand the heat, get another fan.
** Posted from http://www.teranews.com **

[|-|erc]

"The Ghost In The Machine" <ew...@sirius.tg00suus7038.net> wrote

>
> sLoops(TM#) = IF sHalt(TM#, TM# || NOP) = 'halts'
> THEN x: GOTO x
>
> (where || is defined in accordance with the Godel encoding)
>
> is a trivial workaround, mangling your function. The proper
> solution of this issue looks to be a fair amount of work.

It may be possible to get a contradiction yet.

Let sLoops1 = IF sHalt(TM#, TM# ) = 'halts'
THEN x: GOTO x

Let sLoops2 = IF sHalt(TM#, TM# ) = 'halts'
THEN x: NOP; GOTO x

What is the value of sHalt(sLoops1#, sLoops2#)?

too lazy to finish counter proof atm.

Herc