Re: The simple essence of Proof Theoretic Semantics
Mikko <[email protected]>
| Newsgroups | comp.theory,sci.logic,sci.math,comp.ai.philosophy |
|---|---|
| Organization | A noiseless patient Spider |
| Message-ID | <[email protected]> |
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.
--
Mikko