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

Groups > sci.physics.relativity > #671491 > unrolled thread

Type systems for non-deterministic concurrency [Amir Pnueli] (Re: Creating a "European CMOS 2.0 Army")

Back to article view | Back to sci.physics.relativity

This discussion starts older than the indexed window; earlier articles aren't shown. The article labeled Started by below is the oldest one visible, not the original post.

Contents

  Type systems for non-deterministic concurrency [Amir Pnueli] (Re: Creating a "European CMOS 2.0 Army") Mild Shock <janburse@fastmail.fm> - 2026-07-20 12:23 +0200
    Robin Milners fickle gives non-determinism in practice [Parallel π-WAM] (Re: Type systems for non-deterministic concurrency [Amir Pnueli]) Mild Shock <janburse@fastmail.fm> - 2026-07-20 12:35 +0200
      Doing uux with pi-calculus and WAM (Re: Robin Milners fickle gives non-determinism in practice [Parallel π-WAM]) Mild Shock <janburse@fastmail.fm> - 2026-08-24 20:15 +0200
        Does it have a declarative reading? (Re: Doing uux with pi-calculus and WAM) Mild Shock <janburse@fastmail.fm> - 2026-08-24 20:44 +0200
          MCP = uux with streaming JSON (Re: Does it have a declarative reading?) Mild Shock <janburse@fastmail.fm> - 2026-08-24 22:28 +0200

#671491 — Type systems for non-deterministic concurrency [Amir Pnueli] (Re: Creating a "European CMOS 2.0 Army")

Hi,

Probably blinded by some academic remoteness
from the real world, some people really believe
nonsense like the following:

Deterministic Concurrency - Edward Lee
deterministic models as a central part of the engineering toolkit
https://icfp26.sigplan.org/track/icfp-2026-icfp-keynotes#event-overview

But hey Aristoteles present us already with
modal logic to talk about the future. So
if I have a process calculus, with expressions

π, that capture all my processes of interest,
I can have a modal logic of with modal operators
[π] and <π> that give necessity and possibility,

the simplest first order bootstrapped types are:

Product Type:
A -> [π]B

Sum Type:
A /\ <π>B

So we need more than only a ->π type? But even
with two types, is there an easy equivalent of
Curry Howard isomorphism?

In contrast Amir Pnueli's 1977 system of temporal
logic, another variant of modal logic sharing many
common features with dynamic logic, differs from all
of the above-mentioned logics by being what Pnueli
has characterized as an "endogenous" logic,
the others being "exogenous" logics.
https://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29

The Sea Battle and the Master Argument
Aristotle and Diodorus Cronus on the Metaphysics of the Future
https://www.degruyterbrill.com/de/document/doi/10.1515/9783110866346/html



Mild Shock schrieb:
> Hi,
> 
> For marketing purposes people
> typically look at the race towards
> 2nm, and we find:
> 
> A month ago, Apple lost its exclusivity
> on 3 nm smartphone processors with
> MediaTek’s Dimensity 9400 chip, integrated
> in the Vivo X200 Pro smartphone. Qualcomm
> is also in the race with its recently
> unveiled Snapdragon 8 Elite and set to
> power the Xiaomi 15 Pro in 2025. However,
> Apple should regain its position as innovation
> leader in 2026 with the release of the
> iPhone 18, which should feature the A20
> chip built on TSMC’s 2 nm process."
> 
> But there is a vertical vias revolution
> going on as well, some SOCs typically
> being at 18 layers now:
> 
> Zooming Into a CPU (It's Incredible)
> https://www.youtube.com/watch?v=Bez-2cvYja0
> 
> imec has coined the term CMOS 2.0:
> 
> LEUVEN (Belgium), MARCH 12th, 2026 — Imec,
> a world-leading research and innovation hub
> in advanced semiconductor technologies, has
> launched a first-of-its-kind consortium with
> 26 European university groups that will jointly
> work on the technology roadmap beyond
> CMOS scaling (CMOS 2.0).
> https://www.imec-int.com/en/press/imec-launches-university-consortium-around-next-generation-chips 
> 
> 
> So we might see more mobile grade GPUs.
> 
> Bye

[toc] | [next] | [standalone]

#671492 — Robin Milners fickle gives non-determinism in practice [Parallel π-WAM] (Re: Type systems for non-deterministic concurrency [Amir Pnueli])

Hi,

Hi take Robin Milners fickle:

?- emulate((between(1,2,Y),in(X),out(Y))).
: 0
1
: 0
2
fail.

If I use NUM=3, number of logical threads,
and common input [0, 0, 0, 0, 0, 0].

I might get this common output:

[1, 2, 1, 2, 1, 2]

Or this common output:

[1, 1, 2, 2, 1, 2]

Or this common output:

[1, 1, 1, 2, 2, 2]

What else? Did I miss some case?

Can be seen on GPU and CPU backend, depending
on launch parameters. (*)

Bye

(*) If logical threads are executed together in
work groups, certain guarantees of determinism
might hold. But modern GPUs usually support

multiple independent work groups, also my CPU
backend does support a notion of multiple
independent work groups. So that the determinism

guarantees only hold inside the work group.

Mild Shock schrieb:
> Hi,
> 
> Probably blinded by some academic remoteness
> from the real world, some people really believe
> nonsense like the following:
> 
> Deterministic Concurrency - Edward Lee
> deterministic models as a central part of the engineering toolkit
> https://icfp26.sigplan.org/track/icfp-2026-icfp-keynotes#event-overview
> 
> But hey Aristoteles present us already with
> modal logic to talk about the future. So
> if I have a process calculus, with expressions
> 
> π, that capture all my processes of interest,
> I can have a modal logic of with modal operators
> [π] and <π> that give necessity and possibility,
> 
> the simplest first order bootstrapped types are:
> 
> Product Type:
> A -> [π]B
> 
> Sum Type:
> A /\ <π>B
> 
> So we need more than only a ->π type? But even
> with two types, is there an easy equivalent of
> Curry Howard isomorphism?
> 
> In contrast Amir Pnueli's 1977 system of temporal
> logic, another variant of modal logic sharing many
> common features with dynamic logic, differs from all
> of the above-mentioned logics by being what Pnueli
> has characterized as an "endogenous" logic,
> the others being "exogenous" logics.
> https://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29
> 
> The Sea Battle and the Master Argument
> Aristotle and Diodorus Cronus on the Metaphysics of the Future
> https://www.degruyterbrill.com/de/document/doi/10.1515/9783110866346/html
> 
> 
> 
> Mild Shock schrieb:
>> Hi,
>>
>> For marketing purposes people
>> typically look at the race towards
>> 2nm, and we find:
>>
>> A month ago, Apple lost its exclusivity
>> on 3 nm smartphone processors with
>> MediaTek’s Dimensity 9400 chip, integrated
>> in the Vivo X200 Pro smartphone. Qualcomm
>> is also in the race with its recently
>> unveiled Snapdragon 8 Elite and set to
>> power the Xiaomi 15 Pro in 2025. However,
>> Apple should regain its position as innovation
>> leader in 2026 with the release of the
>> iPhone 18, which should feature the A20
>> chip built on TSMC’s 2 nm process."
>>
>> But there is a vertical vias revolution
>> going on as well, some SOCs typically
>> being at 18 layers now:
>>
>> Zooming Into a CPU (It's Incredible)
>> https://www.youtube.com/watch?v=Bez-2cvYja0
>>
>> imec has coined the term CMOS 2.0:
>>
>> LEUVEN (Belgium), MARCH 12th, 2026 — Imec,
>> a world-leading research and innovation hub
>> in advanced semiconductor technologies, has
>> launched a first-of-its-kind consortium with
>> 26 European university groups that will jointly
>> work on the technology roadmap beyond
>> CMOS scaling (CMOS 2.0).
>> https://www.imec-int.com/en/press/imec-launches-university-consortium-around-next-generation-chips 
>>
>>
>> So we might see more mobile grade GPUs.
>>
>> Bye
> 

[toc] | [prev] | [next] | [standalone]

#672374 — Doing uux with pi-calculus and WAM (Re: Robin Milners fickle gives non-determinism in practice [Parallel π-WAM])

Hi,

I find an early precendent of a command
in a unix system, which has an interesting
flavor, that goes beyond Web Prolog Trinity

RPC nonsense. Take this command:

uux merlin!wc < venus!/paper/*.tex > mars!/stats/*.txt
https://www.ibm.com/docs/en/aix/7.1.0?topic=u-uux-command

So basically wc, i.e. word count is executed
on merlin, takes data from venus and moves it
to marks. We can do the same with pi-WAM,

currently experimenting with a non-blocking
execute/1 built-in, spawn/2:

?- chan(In), chan(Out),
    spawn((recv(3,[Z]), wc(Z,T), send(4,[T])), [comm([In,Out])]),
    venus(X),
    send(In,[X]), repeat, recv(Out,[Y]),
    mars(Y).

But maybe introducing in/1 and out/1 options
to spawn/2, would be more easier to write,
now I have split spawn/2 into prepare/3 and run/1.

?- chan(In), chan(Out),
    prepare(wc(X,Y)), [in(X), out(Y)], P),
    venus(X),
    run(P),
    mars(Y).

But the point is to do prepare/3 only once,
and do mars and venus later. It also reflects
the ordering on a uux command:

1               2                    3
uux merlin!wc < venus!/paper/*.tex > mars!/stats/*.txt

But we wouldn't do it alone for this cosmetic.
The idea is that the spawned process is using
its channels, to do more than only one job.

Bye


Mild Shock schrieb:
> Hi,
> 
> Hi take Robin Milners fickle:
> 
> ?- emulate((between(1,2,Y),in(X),out(Y))).
> : 0
> 1
> : 0
> 2
> fail.
> 
> If I use NUM=3, number of logical threads,
> and common input [0, 0, 0, 0, 0, 0].
> 
> I might get this common output:
> 
> [1, 2, 1, 2, 1, 2]
> 
> Or this common output:
> 
> [1, 1, 2, 2, 1, 2]
> 
> Or this common output:
> 
> [1, 1, 1, 2, 2, 2]
> 
> What else? Did I miss some case?
> 
> Can be seen on GPU and CPU backend, depending
> on launch parameters. (*)
> 
> Bye
> 
> (*) If logical threads are executed together in
> work groups, certain guarantees of determinism
> might hold. But modern GPUs usually support
> 
> multiple independent work groups, also my CPU
> backend does support a notion of multiple
> independent work groups. So that the determinism
> 
> guarantees only hold inside the work group.
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Probably blinded by some academic remoteness
>> from the real world, some people really believe
>> nonsense like the following:
>>
>> Deterministic Concurrency - Edward Lee
>> deterministic models as a central part of the engineering toolkit
>> https://icfp26.sigplan.org/track/icfp-2026-icfp-keynotes#event-overview
>>
>> But hey Aristoteles present us already with
>> modal logic to talk about the future. So
>> if I have a process calculus, with expressions
>>
>> π, that capture all my processes of interest,
>> I can have a modal logic of with modal operators
>> [π] and <π> that give necessity and possibility,
>>
>> the simplest first order bootstrapped types are:
>>
>> Product Type:
>> A -> [π]B
>>
>> Sum Type:
>> A /\ <π>B
>>
>> So we need more than only a ->π type? But even
>> with two types, is there an easy equivalent of
>> Curry Howard isomorphism?
>>
>> In contrast Amir Pnueli's 1977 system of temporal
>> logic, another variant of modal logic sharing many
>> common features with dynamic logic, differs from all
>> of the above-mentioned logics by being what Pnueli
>> has characterized as an "endogenous" logic,
>> the others being "exogenous" logics.
>> https://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29
>>
>> The Sea Battle and the Master Argument
>> Aristotle and Diodorus Cronus on the Metaphysics of the Future
>> https://www.degruyterbrill.com/de/document/doi/10.1515/9783110866346/html
>>
>>
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> For marketing purposes people
>>> typically look at the race towards
>>> 2nm, and we find:
>>>
>>> A month ago, Apple lost its exclusivity
>>> on 3 nm smartphone processors with
>>> MediaTek’s Dimensity 9400 chip, integrated
>>> in the Vivo X200 Pro smartphone. Qualcomm
>>> is also in the race with its recently
>>> unveiled Snapdragon 8 Elite and set to
>>> power the Xiaomi 15 Pro in 2025. However,
>>> Apple should regain its position as innovation
>>> leader in 2026 with the release of the
>>> iPhone 18, which should feature the A20
>>> chip built on TSMC’s 2 nm process."
>>>
>>> But there is a vertical vias revolution
>>> going on as well, some SOCs typically
>>> being at 18 layers now:
>>>
>>> Zooming Into a CPU (It's Incredible)
>>> https://www.youtube.com/watch?v=Bez-2cvYja0
>>>
>>> imec has coined the term CMOS 2.0:
>>>
>>> LEUVEN (Belgium), MARCH 12th, 2026 — Imec,
>>> a world-leading research and innovation hub
>>> in advanced semiconductor technologies, has
>>> launched a first-of-its-kind consortium with
>>> 26 European university groups that will jointly
>>> work on the technology roadmap beyond
>>> CMOS scaling (CMOS 2.0).
>>> https://www.imec-int.com/en/press/imec-launches-university-consortium-around-next-generation-chips 
>>>
>>>
>>> So we might see more mobile grade GPUs.
>>>
>>> Bye
>>
> 

[toc] | [prev] | [next] | [standalone]

#672376 — Does it have a declarative reading? (Re: Doing uux with pi-calculus and WAM)

Hi,

Sorry I forget to specify the site for wc.
Lets just write it as follows, the site
somehow encoded in a the predicate name,

and forget about a lot of (!)/2 details:

?- prepare(merlin(X,Y)), [in(X), out(Y)], P),
    venus(X),
    run(P),
    mars(Y).

Does it have a declarative reading? Besides
the benefit of shipping merlin/1 only once?
Of course we can interpret it as follows:

?- venus(X),
    merlin(X,Y),
    mars(Y).

This would be much more also in the spirit of a
Jens Ottens theorem provers, that ultimately end
in connection proof problems, when they have

decended down. Maybe the Trinity system can
somehow avoid the multiple shipping of the merlin
payload through caching. But the problem is it

will see merlin(foo, Y), merlin(bar, Y),
merlin(baz, Y). So it doesn't know what was
the input. It cannot create a single logical

thread on the executing site.

Bye

Mild Shock schrieb:
> Hi,
> 
> I find an early precendent of a command
> in a unix system, which has an interesting
> flavor, that goes beyond Web Prolog Trinity
> 
> RPC nonsense. Take this command:
> 
> uux merlin!wc < venus!/paper/*.tex > mars!/stats/*.txt
> https://www.ibm.com/docs/en/aix/7.1.0?topic=u-uux-command
> 
> So basically wc, i.e. word count is executed
> on merlin, takes data from venus and moves it
> to marks. We can do the same with pi-WAM,
> 
> currently experimenting with a non-blocking
> execute/1 built-in, spawn/2:
> 
> ?- chan(In), chan(Out),
>     spawn((recv(3,[Z]), wc(Z,T), send(4,[T])), [comm([In,Out])]),
>     venus(X),
>     send(In,[X]), repeat, recv(Out,[Y]),
>     mars(Y).
> 
> But maybe introducing in/1 and out/1 options
> to spawn/2, would be more easier to write,
> now I have split spawn/2 into prepare/3 and run/1.
> 
> ?- chan(In), chan(Out),
>     prepare(wc(X,Y)), [in(X), out(Y)], P),
>     venus(X),
>     run(P),
>     mars(Y).
> 
> But the point is to do prepare/3 only once,
> and do mars and venus later. It also reflects
> the ordering on a uux command:
> 
> 1               2                    3
> uux merlin!wc < venus!/paper/*.tex > mars!/stats/*.txt
> 
> But we wouldn't do it alone for this cosmetic.
> The idea is that the spawned process is using
> its channels, to do more than only one job.
> 
> Bye
> 
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Hi take Robin Milners fickle:
>>
>> ?- emulate((between(1,2,Y),in(X),out(Y))).
>> : 0
>> 1
>> : 0
>> 2
>> fail.
>>
>> If I use NUM=3, number of logical threads,
>> and common input [0, 0, 0, 0, 0, 0].
>>
>> I might get this common output:
>>
>> [1, 2, 1, 2, 1, 2]
>>
>> Or this common output:
>>
>> [1, 1, 2, 2, 1, 2]
>>
>> Or this common output:
>>
>> [1, 1, 1, 2, 2, 2]
>>
>> What else? Did I miss some case?
>>
>> Can be seen on GPU and CPU backend, depending
>> on launch parameters. (*)
>>
>> Bye
>>
>> (*) If logical threads are executed together in
>> work groups, certain guarantees of determinism
>> might hold. But modern GPUs usually support
>>
>> multiple independent work groups, also my CPU
>> backend does support a notion of multiple
>> independent work groups. So that the determinism
>>
>> guarantees only hold inside the work group.
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Probably blinded by some academic remoteness
>>> from the real world, some people really believe
>>> nonsense like the following:
>>>
>>> Deterministic Concurrency - Edward Lee
>>> deterministic models as a central part of the engineering toolkit
>>> https://icfp26.sigplan.org/track/icfp-2026-icfp-keynotes#event-overview
>>>
>>> But hey Aristoteles present us already with
>>> modal logic to talk about the future. So
>>> if I have a process calculus, with expressions
>>>
>>> π, that capture all my processes of interest,
>>> I can have a modal logic of with modal operators
>>> [π] and <π> that give necessity and possibility,
>>>
>>> the simplest first order bootstrapped types are:
>>>
>>> Product Type:
>>> A -> [π]B
>>>
>>> Sum Type:
>>> A /\ <π>B
>>>
>>> So we need more than only a ->π type? But even
>>> with two types, is there an easy equivalent of
>>> Curry Howard isomorphism?
>>>
>>> In contrast Amir Pnueli's 1977 system of temporal
>>> logic, another variant of modal logic sharing many
>>> common features with dynamic logic, differs from all
>>> of the above-mentioned logics by being what Pnueli
>>> has characterized as an "endogenous" logic,
>>> the others being "exogenous" logics.
>>> https://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29
>>>
>>> The Sea Battle and the Master Argument
>>> Aristotle and Diodorus Cronus on the Metaphysics of the Future
>>> https://www.degruyterbrill.com/de/document/doi/10.1515/9783110866346/html 
>>>
>>>
>>>
>>>
>>> Mild Shock schrieb:
>>>> Hi,
>>>>
>>>> For marketing purposes people
>>>> typically look at the race towards
>>>> 2nm, and we find:
>>>>
>>>> A month ago, Apple lost its exclusivity
>>>> on 3 nm smartphone processors with
>>>> MediaTek’s Dimensity 9400 chip, integrated
>>>> in the Vivo X200 Pro smartphone. Qualcomm
>>>> is also in the race with its recently
>>>> unveiled Snapdragon 8 Elite and set to
>>>> power the Xiaomi 15 Pro in 2025. However,
>>>> Apple should regain its position as innovation
>>>> leader in 2026 with the release of the
>>>> iPhone 18, which should feature the A20
>>>> chip built on TSMC’s 2 nm process."
>>>>
>>>> But there is a vertical vias revolution
>>>> going on as well, some SOCs typically
>>>> being at 18 layers now:
>>>>
>>>> Zooming Into a CPU (It's Incredible)
>>>> https://www.youtube.com/watch?v=Bez-2cvYja0
>>>>
>>>> imec has coined the term CMOS 2.0:
>>>>
>>>> LEUVEN (Belgium), MARCH 12th, 2026 — Imec,
>>>> a world-leading research and innovation hub
>>>> in advanced semiconductor technologies, has
>>>> launched a first-of-its-kind consortium with
>>>> 26 European university groups that will jointly
>>>> work on the technology roadmap beyond
>>>> CMOS scaling (CMOS 2.0).
>>>> https://www.imec-int.com/en/press/imec-launches-university-consortium-around-next-generation-chips 
>>>>
>>>>
>>>> So we might see more mobile grade GPUs.
>>>>
>>>> Bye
>>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#672378 — MCP = uux with streaming JSON (Re: Does it have a declarative reading?)

Hi,

Amazing turn of events, Model Context Protocol
(MCP) can be viewed as uux using streaming
JSON, so as to obtain message boundaries

even on stdin/stdout:

 > **Newline-delimited JSON**
{"some":"thing\n"}⏎
{"may":{"include":"nested","objects":["and","arrays"]}}⏎
https://en.wikipedia.org/wiki/JSON_streaming#Newline-delimited_JSON

Well if we ignore some SOAP add on, i.e.
JSON-RPC envelopes, but I guess they are not
mandatory on the transport level to

keep this level lean?

Bye

Mild Shock schrieb:
> Hi,
> 
> Sorry I forget to specify the site for wc.
> Lets just write it as follows, the site
> somehow encoded in a the predicate name,
> 
> and forget about a lot of (!)/2 details:
> 
> ?- prepare(merlin(X,Y)), [in(X), out(Y)], P),
>     venus(X),
>     run(P),
>     mars(Y).
> 
> Does it have a declarative reading? Besides
> the benefit of shipping merlin/1 only once?
> Of course we can interpret it as follows:
> 
> ?- venus(X),
>     merlin(X,Y),
>     mars(Y).
> 
> This would be much more also in the spirit of a
> Jens Ottens theorem provers, that ultimately end
> in connection proof problems, when they have
> 
> decended down. Maybe the Trinity system can
> somehow avoid the multiple shipping of the merlin
> payload through caching. But the problem is it
> 
> will see merlin(foo, Y), merlin(bar, Y),
> merlin(baz, Y). So it doesn't know what was
> the input. It cannot create a single logical
> 
> thread on the executing site.
> 
> Bye
> 
> Mild Shock schrieb:
>> Hi,
>>
>> I find an early precendent of a command
>> in a unix system, which has an interesting
>> flavor, that goes beyond Web Prolog Trinity
>>
>> RPC nonsense. Take this command:
>>
>> uux merlin!wc < venus!/paper/*.tex > mars!/stats/*.txt
>> https://www.ibm.com/docs/en/aix/7.1.0?topic=u-uux-command
>>
>> So basically wc, i.e. word count is executed
>> on merlin, takes data from venus and moves it
>> to marks. We can do the same with pi-WAM,
>>
>> currently experimenting with a non-blocking
>> execute/1 built-in, spawn/2:
>>
>> ?- chan(In), chan(Out),
>>     spawn((recv(3,[Z]), wc(Z,T), send(4,[T])), [comm([In,Out])]),
>>     venus(X),
>>     send(In,[X]), repeat, recv(Out,[Y]),
>>     mars(Y).
>>
>> But maybe introducing in/1 and out/1 options
>> to spawn/2, would be more easier to write,
>> now I have split spawn/2 into prepare/3 and run/1.
>>
>> ?- chan(In), chan(Out),
>>     prepare(wc(X,Y)), [in(X), out(Y)], P),
>>     venus(X),
>>     run(P),
>>     mars(Y).
>>
>> But the point is to do prepare/3 only once,
>> and do mars and venus later. It also reflects
>> the ordering on a uux command:
>>
>> 1               2                    3
>> uux merlin!wc < venus!/paper/*.tex > mars!/stats/*.txt
>>
>> But we wouldn't do it alone for this cosmetic.
>> The idea is that the spawned process is using
>> its channels, to do more than only one job.
>>
>> Bye

[toc] | [prev] | [standalone]

Back to top | Article view | sci.physics.relativity

csiph-web