Re: The simple essence of Proof Theoretic Semantics

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.

The requirements of a halt decider don't require that then input
be presented to the decider the way it is done above. For exmample,
a text file would be acceptable.

-- 
Mikko