Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: D correctly simulated by H cannot possibly halt --- templates and infinite sets
Date: Wed, 29 May 2024 12:14:35 +0300
Organization: -
Lines: 138
Message-ID: <v36rlr$13000$1@dont-email.me>
References: <v3501h$lpnh$1@dont-email.me> <v362eu$2d367$3@i2pn2.org> <v363js$vg63$2@dont-email.me> <v36803$2d368$3@i2pn2.org> <v368je$100kd$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 29 May 2024 11:14:35 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="12174c0476b29b50a8f25da96e0ea8af";
	logging-data="1146880"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1++MMqbIekap1gAaReDDUP2"
User-Agent: Unison/2.2
Cancel-Lock: sha1:DqKXsmiYEPBDNNUVlUUx8tJ6sME=
Bytes: 6234

On 2024-05-29 03:49:02 +0000, olcott said:

> On 5/28/2024 10:38 PM, Richard Damon wrote:
>> On 5/28/24 10:23 PM, olcott wrote:
>>> On 5/28/2024 9:04 PM, Richard Damon wrote:
>>>> On 5/28/24 12:16 PM, olcott wrote:
>>>>> typedef int (*ptr)();  // ptr is pointer to int function in C
>>>>> 00       int H(ptr p, ptr i);
>>>>> 01       int D(ptr p)
>>>>> 02       {
>>>>> 03         int Halt_Status = H(p, p);
>>>>> 04         if (Halt_Status)
>>>>> 05           HERE: goto HERE;
>>>>> 06         return Halt_Status;
>>>>> 07       }
>>>>> 08
>>>>> 09       int main()
>>>>> 10       {
>>>>> 11         H(D,D);
>>>>> 12         return 0;
>>>>> 13       }
>>>>> 
>>>>> When Ĥ is applied to ⟨Ĥ⟩
>>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
>>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>>>> 
>>>>> *Formalizing the Linz Proof structure*
>>>>> ∃H  ∈ Turing_Machines
>>>>> ∀x  ∈ Turing_Machines_Descriptions
>>>>> ∀y  ∈ Finite_Strings
>>>>> such that H(x,y) = Halts(x,x)
>>>> 
>>>> But since for x being the description of the H^ built from that H and y 
>>>> being the same, it turns out that no matter what answer H gives, it 
>>>> will be wrong.
>>>> 
>>> 
>>> We have not gotten to that point yet this post is so that
>>> you can fully understand what templates are and how they work.
>> 
>> But note, x, being a Turing Machine, is NOT a "template"
>> 
>> And H, isn't a "set of Turing Machines", but an arbitrary member of 
>> that set, so all we need to do is find a single x, y, possible 
>> determined as a function of H (so, BUILT from a template, but not a 
>> template themselves) that shows that particular H was wrong.
>> 
>> 
>> That is basically what Linz does.
>> 
>> Given a SPECIFIC (but arbitary) H, we can construct a specific H^ built 
>> from a template from H, that that H can not get right.
>> 
>> All the other H's might get this input right, but we don't care, we 
>> have shown that for every H we
>> 
>>> 
>>>> (And I think you have an error in your reference to Halts, I think you 
>>>> mean Halts(x,y) not Halts(x,x)
>>>> 
>>> 
>>> Yes good catch. I was trying to model embedded_H / ⟨Ĥ⟩
>>> and then changed my mind to make it more general.
>>> 
>>>>> 
>>>>> *Here is the same thing applied to H/D pairs*
>>>>> ∃H ∈ C_Functions
>>>>> ∀D ∈ x86_Machine_Code_of_C_Functions
>>>>> such that H(D,D) = Halts(D,D)
>>>> 
>>>> Not the same thing.
>>>> ∃H ∈ C_Functions
>>>> is not equivalent to
>>>> ∃H  ∈ Turing_Machines
>>>> 
>>>> as there are many C_Functions that are not the equivalent of Turing Machines.
>>>> 
>>> 
>>> The whole purpose here is to get you to understand what
>>> templates are and how they reference infinite sets.
>>> 
>> 
>> But the problem is that even in your formulation, H and D are, when 
>> doing the test, SPECIFIC PROGRAMS and not "templates" as Halts is 
>> defined on the domain of PROGRAMS.
>> 
>> Similarly, a "Template" doesn't have a specific set of 
>> x86_Machine_Code_of_C_function, at least not one with defined behavior 
>> since if it tries to reference code outside of itself, then Halts of 
>> that just isn't defined, only Halts of that code + the specific machine 
>> deciding it.
>> 
>>>> 
>>>>> 
>>>>> In both cases infinite sets are examined to see
>>>>> if any H exists with the required properties.
>>>>> 
>>>> 
>>>> Yes, but the logic of Turing Machines looks at them one at a time, and 
>>>> the input is a FULL INDEPENDENT PROGRAM.
>>>> 
>>> 
>>> ∃H  ∈ Turing_Machines
>>> That does not look at one machine it looks as an infinite set of
>>> machines. I am very happy to find out that you were not playing head
>>> games. Linz actually used the words that you referred to.
>> 
>> while the ∃H part can create a set of machines, each element of that 
>> set is INDIVIDUALLY TESTED in the following conditions, so, when we get 
>> to your test  H(x,y) = Halts(x,x), each of H, x, y are individual 
>> members of the set, and we THEN collect the set of all of them.
>> 
>> If we try to say
>> ∃x ∈ Natural Numbers, such that  x+x = 3
>> we can't say that x is both 1 and 2 and thus as a set meet the 
>> requirement. For the conditions, each qualifier select a single 
>> prospective element, and those are tested to see if that meet the 
>> requirement.
>> 
> 
> So it never was about any specific machine as Linz misleading words
> seemed to indicate. It was always about examining each element of an
> infinite set.
> 
> Likewise: ∃H ∈ C_Functions is about examining each element
> of an infinite set. A program template specifies a set of programs
> the same way that an axiom schema specifies a set of axioms.
> 
> I am very happy that the issue was the misleading words of Linz
> and not you playing head games.

In an inderect proof of an unversal claim the counter-hypothesis must
be about one example. Then the proof is about that specific example
until a contradiction is derived.

-- 
Mikko