Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > sci.math > #646843 > unrolled thread
| Started by | Mild Shock <janburse@fastmail.fm> |
|---|---|
| First post | 2026-07-20 12:20 +0200 |
| Last post | 2026-07-20 12:34 +0200 |
| Articles | 2 — 1 participant |
Back to article view | Back to sci.math
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.
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
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2026-07-20 12:20 +0200 |
| Subject | Type systems for non-deterministic concurrency [Amir Pnueli] (Was: Does Variable Age make Sense? [Prolog Unification]) |
| Message-ID | <113kspv$3l1m$1@solani.org> |
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, > > The WebPL shunting experiment still resonates. Dogelog > Players assumption is implicit shunting through > unification variable bind preferences, derived > > from how unification is called. So I rearranged > the implementation of member/2 a little bit, and > now I get, a less invasive version, doesn't modify L: > > /* Dogelog Player 2.1.5 Preview */ > > /* Not Invasive */ > ?- T = T, L = [X,Y,Z], member(T, L), write(L), nl, fail; true. > [_0, _1, _2] > [_0, _1, _2] > [_0, _1, _2] > true. > > /* Not Invasive */ > ?- L = [X,Y,Z], T = T, member(T, L), write(L), nl, fail; true. > [_3, _4, _5] > [_3, _4, _5] > [_3, _4, _5] > true. > > We can compare with SWI-Prolog: > > /* SWI-Prolog 10.1.1 */ > /* Invasive */ > ?- T = T, L = [X,Y,Z], member(T, L), write(L), nl, fail; true. > [_13280,_13294,_13300] > [_13288,_13280,_13300] > [_13288,_13294,_13280] > true. > > /* Not Invasive */ > ?- L = [X,Y,Z], T = T, member(T, L), write(L), nl, fail; true. > [_18762,_18768,_18774] > [_18762,_18768,_18774] > [_18762,_18768,_18774] > true. > > And the result for Scryer Prolog: > > /* Scryer Prolog 0.10 */ > /* Invasive */ > ?- T = T, L = [X,Y,Z], member(T, L), write(L), nl, fail; true. > [_112,_131,_138] > [_123,_112,_138] > [_123,_131,_112] > true. > > /* Invasive */ > ?- L = [X,Y,Z], T = T, member(T, L), write(L), nl, fail; true. > [_117,_125,_133] > [_117,_120,_133] > [_117,_125,_120] > true. > > Bye > > Mild Shock schrieb: >> Hi, >> >> Here some test results when testing >> Desktop and not the Web. With Desktop >> Prolog versions I find: >> >> /* SWI-Prolog 9.3.28 */ >> % 7,506,637 inferences, 0.578 CPU in 0.567 seconds >> >> /* Dogelog Player 1.3.6 for Java (16.08.2025) */ >> % Zeit 803 ms, GC 0 ms, Lips 9367988, Uhr 17.08.2025 18:03 >> >> /* Scryer Prolog 0.9.4-592 */ >> % CPU time: 0.838s, 7_517_613 inferences >> >> /* Trealla Prolog 2.82.12 */ >> % Time elapsed 2.315s, 11263917 Inferences, 4.866 MLips >> >> Bye >> >> Mild Shock schrieb: >>> Hi, >>> >>> The paper by Shalin and Carlson from 1991 >>> did not yet ring a bell. But it suggest testing >>> something with primes and freeze. Lets do >>> >>> primes as suggested but without freeze. SWI-Prolog >>> seems not to the OG of GC. Putting aside Shalin >>> and Carlson, its an typical example of a lot of >>> >>> intermediate results, that can be discarded by >>> a garbage collection. Every candidate number that >>> is not a prime number can be remove from the >>> >>> trail they get unreachable in the first clause >>> of search/3. Besides this obvious unreachability >>> task, I don't have statistics or don't see immediately >>> >>> where large variable instantiation chains are supposed >>> to be created. At least not in my Prolog system, since >>> a result variable is passed without binding it to a >>> >>> local variable, this "shunting" happens independent >>> of neck tests and the "shunting" there. The result variable >>> passing is extremly simple to implement and could >>> >>> be what is effective here besides the reachability thingy. >>> At least the 1 ms GC time in Dogelog Player show that >>> the reachability thingy is the minor effort or optimization >>> >>> to get nice performance: >>> >>> >>> /* WebPL GC */ >>> (1846.1ms) >>> >>> /* Dogelog Player 1.3.6 for JavaScript (16.08.2025) */ >>> % Zeit 2992 ms, GC 1 ms, Lips 2514202, Uhr 17.08.2025 17:44 >>> >>> /* SWI-Prolog WASM */ >>> (4204.2ms) >>> >>> /* Trealla Prolog WASM */ >>> (23568.9ms) >>> >>> The test code was: >>> >>> test :- >>> len(L, 1000), >>> primes(L, _). >>> >>> primes([], 1). >>> primes([J|L], J) :- >>> primes(L, I), >>> K is I+1, >>> search(L, K, J). >>> >>> search(L, I, J) :- >>> mem(X, L), >>> I mod X =:= 0, !, >>> K is I+1, >>> search(L, K, J). >>> search(_, I, I). >>> >>> mem(X, [X|_]). >>> mem(X, [_|Y]) :- >>> mem(X, Y). >>> >>> len([], 0) :- !. >>> len([_|L], N) :- >>> N > 0, >>> M is N-1, >>> len(L, M). >>> >>> Bye >> >
[toc] | [next] | [standalone]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Date | 2026-07-20 12:34 +0200 |
| Subject | Robin Milners fickle gives non-determinism in practice [Parallel π-WAM] (Was: Type systems for non-deterministic concurrency [Amir Pnueli]) |
| Message-ID | <113ktjm$3lig$1@solani.org> |
| In reply to | #646843 |
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, >> >> The WebPL shunting experiment still resonates. Dogelog >> Players assumption is implicit shunting through >> unification variable bind preferences, derived >> >> from how unification is called. So I rearranged >> the implementation of member/2 a little bit, and >> now I get, a less invasive version, doesn't modify L: >> >> /* Dogelog Player 2.1.5 Preview */ >> >> /* Not Invasive */ >> ?- T = T, L = [X,Y,Z], member(T, L), write(L), nl, fail; true. >> [_0, _1, _2] >> [_0, _1, _2] >> [_0, _1, _2] >> true. >> >> /* Not Invasive */ >> ?- L = [X,Y,Z], T = T, member(T, L), write(L), nl, fail; true. >> [_3, _4, _5] >> [_3, _4, _5] >> [_3, _4, _5] >> true. >> >> We can compare with SWI-Prolog: >> >> /* SWI-Prolog 10.1.1 */ >> /* Invasive */ >> ?- T = T, L = [X,Y,Z], member(T, L), write(L), nl, fail; true. >> [_13280,_13294,_13300] >> [_13288,_13280,_13300] >> [_13288,_13294,_13280] >> true. >> >> /* Not Invasive */ >> ?- L = [X,Y,Z], T = T, member(T, L), write(L), nl, fail; true. >> [_18762,_18768,_18774] >> [_18762,_18768,_18774] >> [_18762,_18768,_18774] >> true. >> >> And the result for Scryer Prolog: >> >> /* Scryer Prolog 0.10 */ >> /* Invasive */ >> ?- T = T, L = [X,Y,Z], member(T, L), write(L), nl, fail; true. >> [_112,_131,_138] >> [_123,_112,_138] >> [_123,_131,_112] >> true. >> >> /* Invasive */ >> ?- L = [X,Y,Z], T = T, member(T, L), write(L), nl, fail; true. >> [_117,_125,_133] >> [_117,_120,_133] >> [_117,_125,_120] >> true. >> >> Bye >> >> Mild Shock schrieb: >>> Hi, >>> >>> Here some test results when testing >>> Desktop and not the Web. With Desktop >>> Prolog versions I find: >>> >>> /* SWI-Prolog 9.3.28 */ >>> % 7,506,637 inferences, 0.578 CPU in 0.567 seconds >>> >>> /* Dogelog Player 1.3.6 for Java (16.08.2025) */ >>> % Zeit 803 ms, GC 0 ms, Lips 9367988, Uhr 17.08.2025 18:03 >>> >>> /* Scryer Prolog 0.9.4-592 */ >>> % CPU time: 0.838s, 7_517_613 inferences >>> >>> /* Trealla Prolog 2.82.12 */ >>> % Time elapsed 2.315s, 11263917 Inferences, 4.866 MLips >>> >>> Bye >>> >>> Mild Shock schrieb: >>>> Hi, >>>> >>>> The paper by Shalin and Carlson from 1991 >>>> did not yet ring a bell. But it suggest testing >>>> something with primes and freeze. Lets do >>>> >>>> primes as suggested but without freeze. SWI-Prolog >>>> seems not to the OG of GC. Putting aside Shalin >>>> and Carlson, its an typical example of a lot of >>>> >>>> intermediate results, that can be discarded by >>>> a garbage collection. Every candidate number that >>>> is not a prime number can be remove from the >>>> >>>> trail they get unreachable in the first clause >>>> of search/3. Besides this obvious unreachability >>>> task, I don't have statistics or don't see immediately >>>> >>>> where large variable instantiation chains are supposed >>>> to be created. At least not in my Prolog system, since >>>> a result variable is passed without binding it to a >>>> >>>> local variable, this "shunting" happens independent >>>> of neck tests and the "shunting" there. The result variable >>>> passing is extremly simple to implement and could >>>> >>>> be what is effective here besides the reachability thingy. >>>> At least the 1 ms GC time in Dogelog Player show that >>>> the reachability thingy is the minor effort or optimization >>>> >>>> to get nice performance: >>>> >>>> >>>> /* WebPL GC */ >>>> (1846.1ms) >>>> >>>> /* Dogelog Player 1.3.6 for JavaScript (16.08.2025) */ >>>> % Zeit 2992 ms, GC 1 ms, Lips 2514202, Uhr 17.08.2025 17:44 >>>> >>>> /* SWI-Prolog WASM */ >>>> (4204.2ms) >>>> >>>> /* Trealla Prolog WASM */ >>>> (23568.9ms) >>>> >>>> The test code was: >>>> >>>> test :- >>>> len(L, 1000), >>>> primes(L, _). >>>> >>>> primes([], 1). >>>> primes([J|L], J) :- >>>> primes(L, I), >>>> K is I+1, >>>> search(L, K, J). >>>> >>>> search(L, I, J) :- >>>> mem(X, L), >>>> I mod X =:= 0, !, >>>> K is I+1, >>>> search(L, K, J). >>>> search(_, I, I). >>>> >>>> mem(X, [X|_]). >>>> mem(X, [_|Y]) :- >>>> mem(X, Y). >>>> >>>> len([], 0) :- !. >>>> len([_|L], N) :- >>>> N > 0, >>>> M is N-1, >>>> len(L, M). >>>> >>>> Bye >>> >> >
[toc] | [prev] | [standalone]
Back to top | Article view | sci.math
csiph-web