• Type systems for non-deterministic concurrency [Amir Pnueli] (Was: Does Variable Age make Sense? [Prolog Unification])

    From Mild Shock@janburse@fastmail.fm to comp.lang.prolog,sci.math,sci.logic on Mon Jul 20 12:20:46 2026
    From Newsgroup: sci.math

    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

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

    the simplest first order bootstrapped types are:

    Product Type:
    A -> [-C]B

    Sum Type:
    A /\ <-C>B

    So we need more than only a ->-C 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]
    -a-a 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]
    -a-a 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 :-
    -a-a-a len(L, 1000),
    -a-a-a primes(L, _).

    primes([], 1).
    primes([J|L], J) :-
    -a-a-a primes(L, I),
    -a-a-a K is I+1,
    -a-a-a search(L, K, J).

    search(L, I, J) :-
    -a-a-a mem(X, L),
    -a-a-a I mod X =:= 0, !,
    -a-a-a K is I+1,
    -a-a-a search(L, K, J).
    search(_, I, I).

    mem(X, [X|_]).
    mem(X, [_|Y]) :-
    -a-a-a mem(X, Y).

    len([], 0) :- !.
    len([_|L], N) :-
    -a-a-a N > 0,
    -a-a-a M is N-1,
    -a-a-a len(L, M).

    Bye



    --- Synchronet 3.22a-Linux NewsLink 1.2
  • From Mild Shock@janburse@fastmail.fm to comp.lang.prolog,sci.math,sci.logic on Mon Jul 20 12:34:30 2026
    From Newsgroup: sci.math

    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

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

    the simplest first order bootstrapped types are:

    Product Type:
    A -> [-C]B

    Sum Type:
    A /\ <-C>B

    So we need more than only a ->-C 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]
    -a-a-a 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]
    -a-a-a 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 :-
    -a-a-a len(L, 1000),
    -a-a-a primes(L, _).

    primes([], 1).
    primes([J|L], J) :-
    -a-a-a primes(L, I),
    -a-a-a K is I+1,
    -a-a-a search(L, K, J).

    search(L, I, J) :-
    -a-a-a mem(X, L),
    -a-a-a I mod X =:= 0, !,
    -a-a-a K is I+1,
    -a-a-a search(L, K, J).
    search(_, I, I).

    mem(X, [X|_]).
    mem(X, [_|Y]) :-
    -a-a-a mem(X, Y).

    len([], 0) :- !.
    len([_|L], N) :-
    -a-a-a N > 0,
    -a-a-a M is N-1,
    -a-a-a len(L, M).

    Bye




    --- Synchronet 3.22a-Linux NewsLink 1.2