Re: The simple essence of Proof Theoretic Semantics
Mikko <[email protected]>
| Newsgroups | comp.theory,comp.ai.philosophy,sci.logic,sci.math |
|---|---|
| Organization | A noiseless patient Spider |
| Message-ID | <[email protected]> |
On 09/07/2026 06:23, olcott wrote:
> On 7/8/2026 2:55 AM, Mikko wrote:
>> On 06/07/2026 18:30, olcott wrote:
>>> On 7/6/2026 3:24 AM, Mikko wrote:
>>>> On 04/07/2026 19:55, olcott wrote:
>>>>> On 7/4/2026 2:46 AM, Mikko wrote:
>>>>>> On 04/07/2026 04:52, olcott wrote:
>>>>>>> On 7/3/2026 5:51 PM, André G. Isaak wrote:
>>>>>>>> On 2026-07-03 16:37, olcott wrote:
>>>>>>>>> On 7/3/2026 1:47 PM, André G. Isaak wrote:
>>>>>>>>>> On 2026-07-03 12:36, olcott wrote:
>>>>>>>>>>> On 7/3/2026 1:18 PM, dbush wrote:
>>>>>>>>>>
>>>>>>>>>>>> If an algorithm takes an input and produces an output, that
>>>>>>>>>>>> is by definition a mapping.
>>>>>>>>>>> That only proves that the definition is incoherent.
>>>>>>>>>>> The coherent way that it actually works is that
>>>>>>>>>>> inputs are transformed into outputs by applying
>>>>>>>>>>> finite string transformation rules to inputs to
>>>>>>>>>>> derive outputs.
>>>>>>>>>>
>>>>>>>>>> Apparently you don't understand the difference between a
>>>>>>>>>> mapping and an algorithm. They are two different things.
>>>>>>>>>>
>>>>>>>>>> André
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> A function that ignores its input and only returns 0
>>>>>>>>> is not any sort of halt function.
>>>>>>>>
>>>>>>>> He was defining 'mapping', not 'halt function'.
>>>>>>>>
>>>>>>>> André
>>>>>>
>>>>>>> A actual halt function must compute the mapping from
>>>>>>> its actual input according to the operational semantics
>>>>>>> of this input to the behavior that this input actually
>>>>>>> specifies. No function can report on the behavior of
>>>>>>> its caller because it has no idea who its caller is.
>>>>>>
>>>>>> A function does not compute. An algrothm may compute a function.
>>>>>> However, no algrithm computes the halt function.
>>>>>>
>>>>>> The halt functions maps a computation to a truth value
>>>>>> but so do many other functions, too.
>>>>>
>>>>> When implemented as C functions
>>>>>
>>>>> typedef int (*ptr)();
>>>>> int HHH(ptr P);
>>>>>
>>>>> 01 int DD()
>>>>> 02 {
>>>>> 03 int Halt_Status = HHH(DD);
>>>>> 04 if (Halt_Status)
>>>>> 05 HERE: goto HERE;
>>>>> 06 return Halt_Status;
>>>>> 07 }
>>>>> 08
>>>>> 09 void main()
>>>>> 10 {
>>>>> 11 DD();
>>>>> 12 HHH(DD);
>>>>> 13 }
>>>>>
>>>>> The HP requires HHH to report on the DD() invoked
>>>>> in main(). This is impossible because HHH has no
>>>>> idea who its caller is and deciders are functions
>>>>> that only operate on their arguments.
>>>> The halting problem does not require anything unless the input
>>>> fully specifies a computation.
>>>>
>>>> The above DD calls HHH, which must be the same HHH as main calls if
>>>> DD halts. Therefore the bhaviour of HHH is a part of the computation
>>>> that the HHH would answer about if it were a halt decider.
>>>
>>> HHH(DD) can and does correctly report on its input.
>>> I just can get why it is taking so long for people
>>> to understand that DD executed in main is out-of-scope
>>> for HHH. It is like someone took actual brains apart
>>> and welded in short-circuits.
>>
>> It does not really matter. HHH and DD are not interesting and you
>> have never said anyting interesting about them.
>
> HHH/DD conclusively proves that the halting problem
> proof has always been incorrect.
No, it does not. Straw man is not a valid inference rule.
--
Mikko