From Newsgroup: sci.logic

Take this test case:

test1(X) :- X = f(g(X,_B),_A).

test2(X) :- Y = g(f(Y,A),_B), X = f(Y,A).

Now try this (numbervars/3):

/* SWI-Prolog 9.3.26 */
?- test1(X), numbervars(X,0,_).
X = f(g(X, A), B).

?- test2(X), numbervars(X,0,_).
X = f(_S1, A), % where
_S1 = g(f(_S1, A), B).

And try this (nonground/2):

?- test1(X), nonground(X, V).
X = f(g(X, V), _).

?- test2(X), nonground(X, V).
X = f(_S1, V), % where
_S1 = g(f(_S1, V), _).

And try this (term_variables/2):

?- test1(X), term_variables(X, [V,W]).
X = f(g(X, V), W).

?- test2(X), term_variables(X, [V,W]).
X = f(_S1, V), % where
_S1 = g(f(_S1, V), W).

All 3 predicates suffer from an similar anomaly,
namely, in the first query V appears 2nd
argument of g/2, and in the second query V

appears 2nd argument of f/2. Can this be fixed?
--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: sci.logic


Here is an implementation that doesnrCOt suffer from
the same anomaly. I get these results:

?- test1(X), term_vars(X, [V,W]).
X = f(g(X, W), V).

?- test2(X), term_vars(X, [V,W]).
X = f(_S1, V), % where
_S1 = g(f(_S1, V), W).

Only the algorithm is a little expensive. Whats
annonying that I backtrack over a bisimulation
equals. And can only collect the union find store

during a sucesss. But a failure of the bisimulation
equals does a local union find store rollback, without
keeping any partial union find results that were

from successful sub-equals calls:

term_vars(T, L) :-
term_vars([], T, []-[], L-_).

% term_vars(+List, +Term, +Pair, -Pair)
term_vars(_, V, L-P, L-P) :- var(V),
member(W, L), W == V, !.
term_vars(_, V, L-P, [V|L]-P) :- var(V), !.
term_vars(M, T, L-P, L-Q) :- compound(T),
member(S, M), equals(T, S, P, Q), !.
term_vars(M, T, L, R) :- compound(T), !,
T =..[_|A],
foldl(term_vars([T|M]), A, L, R).
term_vars(_, _, L, L).

The bisimulation equals itself is:

equals(X, Y) :-
equals(X, Y, [], _).

% equals(+Term, +Term, +List, -List)
equals(X, Y, L, R) :- compound(X), compound(Y), !,
union_find(X, L, Z),
union_find(Y, L, T),
equals2(Z, T, L, R).
equals(X, Y, L, L) :- X == Y.

equals2(X, Y, L, L) :-
same_term(X, Y), !.
equals2(X, Y, _, _) :-
functor(X, F, N),
functor(Y, G, M),
F/N \== G/M, !, fail.
equals2(X, Y, L, R) :-
X =.. [_|A],
Y =.. [_|B],
foldl(equals, A, B, [X-Y|L], R).

And the union find trivially:

union_find(X, L, T) :-
member(Y-Z, L),
same_term(X, Y), !,
union_find(Z, L, T).
union_find(X, _, X).

Mild Shock schrieb:

Take this test case:

test1(X) :- X = f(g(X,_B),_A).

test2(X) :- Y = g(f(Y,A),_B), X = f(Y,A).

Now try this (numbervars/3):

/* SWI-Prolog 9.3.26 */
?- test1(X), numbervars(X,0,_).
X = f(g(X, A), B).

?- test2(X), numbervars(X,0,_).
X = f(_S1, A), % where
-a-a-a _S1 = g(f(_S1, A), B).

And try this (nonground/2):

?- test1(X), nonground(X, V).
X = f(g(X, V), _).

?- test2(X), nonground(X, V).
X = f(_S1, V), % where
-a-a-a _S1 = g(f(_S1, V), _).

And try this (term_variables/2):

?- test1(X), term_variables(X, [V,W]).
X = f(g(X, V), W).

?- test2(X), term_variables(X, [V,W]).
X = f(_S1, V), % where
-a-a-a _S1 = g(f(_S1, V), W).

All 3 predicates suffer from an similar anomaly,
namely, in the first query V appears 2nd
argument of g/2, and in the second query V

appears 2nd argument of f/2. Can this be fixed?

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: sci.logic

Hi,

All-in-One: Wuhan, Hopcroft and Attention:

DAM-GT: Dual Positional Encoding-Based Attention
Masking Graph Transformer for Node Classification https://arxiv.org/abs/2505.17660v1

LoL

Bye

Mild Shock schrieb:

The Original Ganster (OG) of Bisimilarity are
Hopcroft and Karp (1971). These hand-outs discuss a
coalgebra with the compound ->(_,_) and the atom -.
Coalgebra seem to have the feature that both vertices

and edges have labels. The algorithm does attack a ~ b,
and nf(a) respectively nf(b) at the same time by using
union find. The algorithm is space linear, can be

implemented with an extra pointer in each Prolog compound
for the union find. Mostlikely what SWI-Prolo gdoes
with reference to Folk Knowledge and Bart Demoen. The

algorithm is also almost time linear:

Bisimulation and Equirecursive Equality -2014 https://www.cs.cornell.edu/courses/cs6110/2014sp/Lectures/lec35a.pdf

Mild Shock schrieb:

Hi,

Despite these efforts:

The development of concurrent logic programming
was given an impetus when Guarded Horn Clause was
used to implement KL1, the systems programming
language of the Japanese Fifth Generation
Project (FGCS). The FGCS Project was a $400M
initiative by Japan's Ministry of International
Trade and Industry, begun in 1982, to use
massively parallel computing/processing for
artificial intelligence applications.
https://en.wikipedia.org/wiki/Concurrent_logic_programming

And relation ship to rational trees, in
Alain Colmerauers WINDOW PRINCIPLE, mostlikely
Bisimulation has a more lasting impact.

But who were the founding fathers of bisimulation?

Robin Milner (1934rCo2010)
Primary founder of the concept of bisimulation. Introduced
the idea in the context of Calculus of Communicating
Systems (CCS) in the late 1970s and early 1980s. Bisimulation
became central to his work on concurrency theory. He won
the Turing Award in 1991, partly for this work.

Gordon Plotkin
While not the originator of bisimulation itself,
Plotkin worked closely with Milner and contributed
significantly to the theoretical foundations of
operational semantics and domain theory, which
intersect with bisimulation.

David Park
Credited with influencing the notion of bisimulation.
His unpublished manuscript (c. 1981) and personal
communications inspired MilnerrCOs formalization.
He clarified the distinction between simulation
and bisimulation.

Bye

--- Synchronet 3.21a-Linux NewsLink 1.2