Can the Church Turing hypotheses be refuted? [TLo @ FOM] (Was: Robin Milners pi calculus is typeless)

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	sci.logic
Subject	Can the Church Turing hypotheses be refuted? [TLo @ FOM] (Was: Robin Milners pi calculus is typeless)
Date	2026-07-18 11:08 +0200
Message-ID	<113ffq2$3lu$1@solani.org> (permalink)
References	(4 earlier) <113e1rb$32lvt$1@dont-email.me> <113ed4k$9agb$1@solani.org> <113ef4u$9bi1$2@solani.org> <sJKcnV_XQuEwp8b3nZ2dnZfqnPqdnZ2d@giganews.com> <113ff5p$32l$1@solani.org>

Show all headers | View raw

Hi,

Ha Ha, TLo @ FOM schrieb:
 > Lastly--there is the Church-Turing-thesis itself.
 > I cannot imagine what form a proof could have. But at
 > least a refutation is conceivable, if extremely far-fetched.

Can the Church Turing hypotheses be refuted? Well
since it is stricly speaking only a hypothesis and
not a thesis, it cannot be that much refuted,

since it is a kind of exhaustion argument defining
a category by examples. The history goes as follows:

> In 1935–36,[7] Alonzo Church formalized the 
 > concept of effectively calculable functions by proposing
 > that they are general recursive functions, or,
 > equivalently, λ-definable functions.
https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis

Does his λ-definable include types? Nope. Do
we need large cardinal axioms? It depends.
Church λ-computable was syntactically defined,

it didn't have a semantic referent. The search
for a semantic referent gave rise to certain
additional problems of set theory and type theory.

Have Fun!

Bye

Mild Shock schrieb:
> Hi,
> 
> Mild Shock schrieb:
>  > The π-calculus is a universal model of computation.
>  > This was first observed by Milner in his paper
>  > "Functions as Processes",[10] in which he presents
>  > two encodings of the lambda-calculus in the π-calculus.
>  > https://en.wikipedia.org/wiki/%CE%A0-calculus
> 
> Ross Finlayson schrieb:
>  > Of course the lambda-calculus and pi-calculus
>  > are great things for models of types and communicating
>  > sequential processes.
>  >
>  > Roberto di Cosmo has a great book on types,
>  > and more than one.
>  >
>  > 
> https://books.google.com/books/about/Isomorphisms_of_Types.html?id=cdJZRjIxavwC 
> 
> 
> When a 1970s paper claims a relation ship between
> pi-calculus and lambda calculus, then both calculi
> refer to a typeless calculi.
> 
> Types are a later invention. The original lambda
> calculus was typeless. Church encodings came later,
> but for example the Church Turing hypotheses is
> 
> formulated along typeless lambda calculus.
> 
> Bye
> 
> P.S.: Prolog is also typeless. I do not intend to
> add any types to pi-WAM either.
> 
> Ross Finlayson schrieb:
>> On 07/17/2026 04:50 PM, Mild Shock wrote:
>>> Hi,
>>>
>>> Milners fickle() is here:
>>>
>>> Functions as processes
>>> https://inria.hal.science/inria-00075405
>>>
>>> After Theorem 7.7:
>>>
>>> So in P we construct a fickle ‘function’ which
>>> behaves differently on successive calls.
>>>
>>> Here is a pi-WAM run in Dogelog Player, using the emulator:
>>>
>>> Dogelog Spieler 2.2.4, Oracle Corporation, Java 26.0.1
>>> (c) 1985-2026, XLOG Technologies AG, Schweiz
>>> ?- ensure_loaded(library(edge/brainfog)).
>>> true.
>>> ?- emulate((between(1,2,Y),in(X),out(Y))).
>>> : 0
>>> 1
>>> : 0
>>> 2
>>> fail.
>>>
>>> The emulator is portable, can be run every Prolog
>>> system. But it is only 1 process. So its better
>>> to use the n process backends for CPU or GPU.
>>>
>>> Which are less portable, not anymore pure Prolog,
>>> a great deal of thread start and join infrastructure
>>> as well, and a native Hack VM.
>>>
>>> The comms across process is not yet implemented.
>>> But the in/1 and out/1 instructions are already
>>> there. But they currently go to stdin/stdout.
>>>
>>> Bye
>>>
>>> Mild Shock schrieb:
>>>> Hi,
>>>>
>>>> The pi in pi-WAM refers to pi-calculus.
>>>> pi-calculus has not atomic(i32).
>>>>
>>>> The π-calculus is a universal model of computation.
>>>> This was first observed by Milner in his paper
>>>> "Functions as Processes",[10] in which he presents
>>>> two encodings of the lambda-calculus in the π-calculus.
>>>> https://en.wikipedia.org/wiki/%CE%A0-calculus
>>>>
>>>> LoL
>>>>
>>>> Bye
>>>>
>>>> Chris M. Thomasson schrieb:
>>>>> On 7/17/2026 2:16 AM, Mild Shock wrote:
>>>>>> Hi,
>>>>>>
>>>>>> Maybe I should write a blog post, titled
>>>>>> Introduction to AI Accelerator Prolog:
>>>>>>
>>>>>> - specialized jobs π-WAM (currently integerish stuff)
>>>>>> - π-WAM uses no atomics, only comms
>>>>>> - π-WAM uses warp, 30-40% more speed
>>>>>> - π-WAM runs on GPU and CPU
>>>>>> - π-WAM runs from within JavaScript, Python and Java
>>>>>
>>>>> [...]
>>>>>
>>>>> No atomic fetch-and-add?
>>>>
>>>
>>
>> So he partial-computes his alpha to alpha_alpha
>> in his Futamura projection, yet, that's partial computation,
>> why not make Minsky counter-machines using the bottom-up
>> approach of making arithmetizations and DFA's.
>>
>>
>> Of course the lambda-calculus and pi-calculus are great
>> things for models of types and communicating sequential processes.
>>
>> Roberto di Cosmo has a great book on types, and more than one.
>>
>> https://books.google.com/books/about/Isomorphisms_of_Types.html?id=cdJZRjIxavwC 
>>
>>
>>
>

Thread

Paul Tarau versus Mr. Taskmanager, who would win? [A PDP-11 Humunkulus from 1979] Mild Shock <janburse@fastmail.fm> - 2026-04-24 02:46 +0200
  AI dooms day escape: Güttinger Wald (Re: Paul Tarau versus Mr. Taskmanager, who would win?) Mild Shock <janburse@fastmail.fm> - 2026-04-25 14:06 +0200
    Elmos Fascist Dreams of a 365 Prolog (Was: AI dooms day escape: Güttinger Wald) Mild Shock <janburse@fastmail.fm> - 2026-05-09 12:52 +0200
      Even the Buddos are clueless [Did Tarau see Liliputians?] (Re: Elmos Fascist Dreams of a 365 Prolog) Mild Shock <janburse@fastmail.fm> - 2026-05-09 15:19 +0200
        Halfing the AI Laptop Budget: Ne-Meow sold out! (Re: Even the Buddos are clueless [Did Tarau see Liliputians?]) Mild Shock <janburse@fastmail.fm> - 2026-05-10 09:09 +0200
    Prolog Expert Ginis (PEGs) on a Keychain (Re: AI dooms day escape: Güttinger Wald) Mild Shock <janburse@fastmail.fm> - 2026-06-20 13:04 +0800
      Chatbot Classified as a Weapon (Re: Prolog Expert Ginis (PEGs) on a Keychain) Mild Shock <janburse@fastmail.fm> - 2026-06-21 05:39 +0800
      Introduction to AI Accelerator Prolog [π-WAM of Dogelog] (Re: Prolog Expert Ginis (PEGs) on a Keychain) Mild Shock <janburse@fastmail.fm> - 2026-07-17 11:16 +0200
        Not praying to the god of lambda calculus [π beats α] (Re: Introduction to AI Accelerator Prolog [π-WAM of Dogelog]) Mild Shock <janburse@fastmail.fm> - 2026-07-17 11:17 +0200
        Re: Introduction to AI Accelerator Prolog [π-WAM of Dogelog] (Re: Prolog Expert Ginis (PEGs) on a Keychain) "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2026-07-17 13:03 -0700
          pi in pi-WAM refers to pi-calculus (Was: Introduction to AI Accelerator Prolog [π-WAM of Dogelog] ) Mild Shock <janburse@fastmail.fm> - 2026-07-18 01:16 +0200
            Milners fickle() in pi-WAM [For fun and profit] (Re: pi in pi-WAM refers to pi-calculus) Mild Shock <janburse@fastmail.fm> - 2026-07-18 01:50 +0200
              Re: Milners fickle() in pi-WAM [For fun and profit] (Re: pi in pi-WAM refers to pi-calculus) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-18 01:34 -0700
                Robin Milners pi calculus is typeless (Was: Milners fickle() in pi-WAM [For fun and profit]) Mild Shock <janburse@fastmail.fm> - 2026-07-18 10:57 +0200
                Can the Church Turing hypotheses be refuted? [TLo @ FOM] (Was: Robin Milners pi calculus is typeless) Mild Shock <janburse@fastmail.fm> - 2026-07-18 11:08 +0200
    AI Laptops are just strange novel xBoxes (Was: AI dooms day escape: Güttinger Wald) Mild Shock <janburse@fastmail.fm> - 2026-07-08 20:44 +0200
      Re: AI Laptops are just strange novel xBoxes (Was: AI dooms day escape: Güttinger Wald) "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2026-07-08 15:22 -0700
        TDR solutions --> work slicing (Was: AI Laptops are just strange novel xBoxes) Mild Shock <janburse@fastmail.fm> - 2026-07-09 09:47 +0200
          Thinking of Chris M. Thomasson: From shadertoys to computetoys? (Re: TDR solutions --> work slicing) Mild Shock <janburse@fastmail.fm> - 2026-07-09 09:52 +0200
    FYI: Unified Memory Architecture (UMA) (Re: Implementing Gas for a Compute Shader [Avoid TDR]) Mild Shock <janburse@fastmail.fm> - 2026-07-09 19:43 +0200
      The Wider von Neumann Neck (Re: FYI: Unified Memory Architecture (UMA)) Mild Shock <janburse@fastmail.fm> - 2026-07-10 07:51 +0200
        The new MIMD Warp is the cherry on top (Re: The Wider von Neumann Neck) Mild Shock <janburse@fastmail.fm> - 2026-07-10 08:08 +0200
        Dumbwit, just run it on your RTX 5070 trash (Re: The Wider von Neumann Neck) Mild Shock <janburse@fastmail.fm> - 2026-07-10 15:49 +0200
          We are still waiting for results! [Confused Dumbwit] (Re: We are waiting Dumbwit: 1 Month, 3 Months, .. [node.js dawn]) Mild Shock <janburse@fastmail.fm> - 2026-07-10 22:45 +0200
            404 Brain not Found [GPU saturation] (Re: We are still waiting for results! [Confused Dumbwit]) Mild Shock <janburse@fastmail.fm> - 2026-07-10 23:40 +0200
              I nowhere talked about 10GB/s (Re: 404 Brain not Found [GPU saturation]) Mild Shock <janburse@fastmail.fm> - 2026-07-10 23:41 +0200
                I nowhere said something about AI (Re: I nowhere talked about 10GB/s) Mild Shock <janburse@fastmail.fm> - 2026-07-10 23:52 +0200
                What do you not understand in "budget"? (Re: I nowhere said something about AI) Mild Shock <janburse@fastmail.fm> - 2026-07-11 00:08 +0200
                SWI makes only MLips not GLips (Re: What do you not understand in "budget"?) Mild Shock <janburse@fastmail.fm> - 2026-07-11 00:09 +0200
                micro penis got hurt by "budget" (Re: SWI makes only MLips not GLips) Mild Shock <janburse@fastmail.fm> - 2026-07-12 19:20 +0200
  Micro Penis Nemesis: Shoe String Budget π-WAM (Was: Paul Tarau versus Mr. Taskmanager, who would win?) Mild Shock <janburse@fastmail.fm> - 2026-07-12 19:26 +0200
    micro penis struggels with mobile grade GPU concept [Redmi Note 14 Pro+ Results] (Re: Micro Penis Nemesis: Shoe String Budget π-WAM) Mild Shock <janburse@fastmail.fm> - 2026-07-12 21:32 +0200
      Micro Penis Existential Crisis: DeepSeek on a Mobile GPU (Re: micro penis struggels with mobile grade GPU concept [Redmi Note 14 Pro+ Results]) Mild Shock <janburse@fastmail.fm> - 2026-07-12 21:47 +0200
        Micro Penis is worse than Sleepy Joe (Re: Micro Penis Existential Crisis: DeepSeek on a Mobile GPU) Mild Shock <janburse@fastmail.fm> - 2026-07-12 23:00 +0200
          Maybe change your pampers? (Was: Micro Penis is worse than Sleepy Joe) Mild Shock <janburse@fastmail.fm> - 2026-07-12 23:01 +0200
            herpes blister rossy boy is confused (Re: Maybe change your pampers?) Mild Shock <janburse@fastmail.fm> - 2026-07-13 06:54 +0200
              nothing gets blocked except your brain [LPDDR5X-RAM] (Re: herpes blister rossy boy is confused) Mild Shock <janburse@fastmail.fm> - 2026-07-13 13:21 +0200
                flogging a dead horse PCI VRAM graphic cards (Re: nothing gets blocked except your brain [LPDDR5X-RAM]) Mild Shock <janburse@fastmail.fm> - 2026-07-13 13:52 +0200
  I'm a spinner, I'm a sinner [Dmitry Vyukov for pi-WAM] (Re: Paul Tarau versus Mr. Taskmanager, who would win? [A PDP-11 Humunkulus from 1979] Mild Shock <janburse@fastmail.fm> - 2026-07-19 11:55 +0200

csiph-web