Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.prolog > #15650

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

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.
> 
> 
> Mild Shock schrieb:
>> 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?
>>>
>>
> 

Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Prolog Education Group clueless about the AI Boom? Mild Shock <janburse@fastmail.fm> - 2025-03-03 14:18 +0100
  Re: Prolog Education Group clueless about the AI Boom? Mild Shock <janburse@fastmail.fm> - 2025-03-03 14:20 +0100
    Salary Templates if you "Grok" ML / AI [PhDs Negotiate Salaries] (Re: Prolog Education Group clueless about the AI Boom?) Mild Shock <janburse@fastmail.fm> - 2025-03-03 18:03 +0100
  ILP is still dreaming of higher order (Was: Prolog Education Group clueless about the AI Boom?) Mild Shock <janburse@fastmail.fm> - 2025-03-07 23:58 +0100
    Re: ILP is still dreaming of higher order (Was: Prolog Education Group clueless about the AI Boom?) Mild Shock <janburse@fastmail.fm> - 2025-03-08 00:00 +0100
  FYI: Philip Zucker’s Co-Egraphs (Was: Prolog Education Group clueless about the AI Boom?) Mild Shock <janburse@fastmail.fm> - 2025-08-12 18:37 +0200
    Using Hopcroft & Karp (HK) everywhere (Was: FYI: Philip Zucker’s Co-Egraphs) Mild Shock <janburse@fastmail.fm> - 2025-08-14 12:31 +0200
      Confusing "decidable problem" and "complete algorithm" (Was: Using Hopcroft & Karp (HK) everywhere) Mild Shock <janburse@fastmail.fm> - 2025-08-14 14:31 +0200
        DFA algorithms in a Python library (Re: Confusing "decidable problem" and "complete algorithm") Mild Shock <janburse@fastmail.fm> - 2025-08-14 15:14 +0200
      Static Variable Shunting in Dogelog Player (Was: Using Hopcroft & Karp (HK) everywhere) Mild Shock <janburse@fastmail.fm> - 2025-08-16 11:22 +0200
        Dynamic Variable Shunting in WebPL (Was: Static Variable Shunting in Dogelog Player) Mild Shock <janburse@fastmail.fm> - 2025-08-16 11:34 +0200
          SWI-Prolog is still the OG of GC (Was: Dynamic Variable Shunting in WebPL) Mild Shock <janburse@fastmail.fm> - 2025-08-16 11:46 +0200
            Cyclic Term Unification is Accounted (Was: SWI-Prolog is still the OG of GC) Mild Shock <janburse@fastmail.fm> - 2025-08-16 11:59 +0200
            WebPL is an interesting project (Was: SWI-Prolog is still the OG of GC) Mild Shock <janburse@fastmail.fm> - 2025-08-17 18:00 +0200
              Head to Head Race with Scryer Prolog (Was: WebPL is an interesting project) Mild Shock <janburse@fastmail.fm> - 2025-08-17 18:24 +0200
                Does Variable Age make Sense? [Prolog Unification] (Was: Head to Head Race with Scryer Prolog) Mild Shock <janburse@fastmail.fm> - 2026-02-10 12:05 +0100
                Type systems for non-deterministic concurrency [Amir Pnueli] (Was: Does Variable Age make Sense? [Prolog Unification]) Mild Shock <janburse@fastmail.fm> - 2026-07-20 12:20 +0200
                Robin Milners fickle gives non-determinism in practice [Parallel π-WAM] (Was: Type systems for non-deterministic concurrency [Amir Pnueli]) Mild Shock <janburse@fastmail.fm> - 2026-07-20 12:34 +0200
  Sleepy Joe and the Poor South (Local AI Emacs Mode) (Re: Prolog Education Group clueless about the AI Boom?) Mild Shock <janburse@fastmail.fm> - 2025-11-12 12:59 +0100
    Beyond Sleepy Joe around the World (Was: Sleepy Joe and the Poor South (Local AI Emacs Mode)) Mild Shock <janburse@fastmail.fm> - 2025-11-12 13:12 +0100
  GENESIS MISSION: Loosing it over Deep Pokets [Business wants A-Life] (Was: Prolog Education Group clueless about the AI Boom?) Mild Shock <janburse@fastmail.fm> - 2025-11-26 18:07 +0100
  Vanilla Prolog: semi-decidable =\= decidable (Re: Prolog Education Group clueless about the AI Boom?) Mild Shock <janburse@fastmail.fm> - 2026-03-14 20:40 +0100
    Its on the Internet, so it must be true? (Was: Vanilla Prolog: semi-decidable =\= decidable) Mild Shock <janburse@fastmail.fm> - 2026-03-16 11:01 +0100
    Hack + Computed Goto = Leightweigh C_OR (Was: Vanilla Prolog: semi-decidable =\= decidable) Mild Shock <janburse@fastmail.fm> - 2026-07-04 16:58 +0200
      The stack and choice points as an after match (Re: Hack + Computed Goto = Leightweigh C_OR) Mild Shock <janburse@fastmail.fm> - 2026-07-04 17:07 +0200
        Introduction to AI Accelerator Prolog [π-WAM of Dogelog] (Was: The stack and choice points as an after match) Mild Shock <janburse@fastmail.fm> - 2026-07-17 10:49 +0200
          Not praying to the god of lambda calculus [π beats α] (Was: Introduction to AI Accelerator Prolog [π-WAM of Dogelog]) Mild Shock <janburse@fastmail.fm> - 2026-07-17 11:13 +0200
          pi in pi-WAM refers to pi-calculus (Re: Introduction to AI Accelerator Prolog [π-WAM of Dogelog]) Mild Shock <janburse@fastmail.fm> - 2026-07-18 01:22 +0200
            Milners fickle() in pi-WAM [For fun and profit] (Re: pi in pi-WAM refers to pi-calculus (Re: Introduction to AI Accelerator Prolog [π-WAM of Dogelog]) Mild Shock <janburse@fastmail.fm> - 2026-07-18 01:49 +0200
              Robin Milners pi calculus is typeless (Re: Milners fickle() in pi-WAM [For fun and profit]) Mild Shock <janburse@fastmail.fm> - 2026-07-18 11:00 +0200
                Can the Church Turing hypotheses be refuted? [TLo @ FOM] (Re: Robin Milners pi calculus is typeless) Mild Shock <janburse@fastmail.fm> - 2026-07-18 11:10 +0200
          Accelerate Lean! From Theorem 3.11 to Corollary 3.12 [ZMC] (Was: Introduction to AI Accelerator Prolog [π-WAM of Dogelog]) Mild Shock <janburse@fastmail.fm> - 2026-07-19 16:06 +0200
            ANN: Library Pegg, for π-E-graphs [Not EXWM] (Was: Accelerate Lean! From Theorem 3.11 to Corollary 3.12 [ZMC]) Mild Shock <janburse@fastmail.fm> - 2026-07-19 16:21 +0200

csiph-web