Path: nntp.eternal-september.org!news.eternal-september.org!eternal-september.org!feeder3.eternal-september.org!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: At least 3 methods for Bisimilarity [Python BisPy] (Re: Bonus: Prolog
 Systems with Strings, Bigints, etc.. )
Date: Mon, 21 Jul 2025 23:26:30 +0200
Message-ID: <105mba6$2l3t3$2@solani.org>
References: <105lbr7$2idvv$2@solani.org> <105m9ap$2l2uv$1@solani.org>
 <105m9u7$2l38j$2@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 21 Jul 2025 21:26:30 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2789283"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101
 Firefox/128.0 SeaMonkey/2.53.21
Cancel-Lock: sha1:mtMTc61mLAntPZBqVMkUjOWCFxs=
In-Reply-To: <105m9u7$2l38j$2@solani.org>
X-User-ID: eJwFwQkBwDAIA0BLsIZPDtDGv4Td2XH1Dbg5jEbqSORUX7mU76zfa6wFx6VeP18EVDBfZi9UWVG2yZBD9A9qXRXJ

Hi,

There are at least 3 methods to decide
Bisimilarity, namely:

- Run into a ~ b using some loop checking
- Use a normal form and check nf(a) = nf(b)
- Or use a global partition method

The global partition method would look
at the full graph, that contains both a
and b. I suspect this Python package does that:

BisPy is a Python package for the computation
of the maximum bisimulation of directed graphs.
At the moment it supports the following algorithms:

- Paige-Tarjan
- Dovier-Piazza-Policriti
- Saha

https://github.com/fandreuz/BisPy

Have Fun!

Bye

Mild Shock schrieb:
> Hi,
> 
> My modelling for atomic Prolog types was a little
> overkill, since most Prolog systems are still fond
> of atom tables and stuff, but I had a edge with
> 
> label 0, between the adress of atomic Prolog type,
> and the "value" of an atomic Prolog type. Ok
> lets turn this overkill into a bonus:
> 
>  > So we can study two things under the same umbrella,
>  > inside the bisimulation framework of Robin Milner:
>  >
>  > - Lower Level adresses, such as *1, *2, *3, etc..
>  >
>  > - Higher Level Prolog terms, such as f(a,b), a, b, etc..
> 
> Add the following item:
> 
> - Prolog Systems with Strings, Bigints, etc.. (*)
> 
> When atomic things with different adresses
> can be still equal, but same_term/2 as
> realized in SWI-Prolog might not give that
> 
> information. Don’t know what it does…
> 
> Bye
> 
> Mild Shock schrieb:
>>
>> Bisimilarity has an interesting history, I
>> only figured out today. 1981 David Park
>> mentioned it in a appendix “Unresolved problems.”
>>
>> Concurrency and Automata on Infinite Sequences
>> David Park - 1981
>> https://scispace.com/pdf/concurrency-and-automata-on-infinite-sequences-3eilumrkv0.pdf 
>>
>>
>> 1983 Robin Milner had a more grown up theory
>> about it. With findings such as “Charts C1,
>> and C2, are congruent if they possess a bisimulation;
>> Congruence of charts is an equivalence relation.”
>>
>> A Complete Inference System for a Class of Regular Behaviours
>> Robin Milner - 1982
>> https://www.pure.ed.ac.uk/ws/portalfiles/portal/15159317/A_Complete_Inference_System_for_a_Class_of_Regular_Behaviours.pdf 
>>
>>
>> But how view syntactic Prolog terms as
>> infinte trees respective graphs. First of
>> all you need graphs that are labeled in their
>> edges, and also labeled in their nodes,
>>
>> so take a term: f(a,b):
>>
>>                      *1   (label f)
>>                     /  \
>>    (label 1)       /    \       (label 2)
>>                   /      \
>>    (label a)     *2       *3    (label b)
>>
>> The *1, *2 and *3 are some memory addresses.
>> The Robin Milner paper does bisimulation
>> when there are labels in the edges, he
>> doesn’t show bisimulation if there are
>> labels in the vertices as well,
>>
>> but one could use arg(0) for the functor,
>> actually effectively most Prolog systems
>> implement a compound as such, a Prolog compound
>> f(a,b) is basically internally some tupel (f,a,b):
>>
>>                   *1
>>     (label 0)  /  |  \
>>               /   |  (label 1)
>>             /     |      \       (label 2)
>>            f      *2      *3
>>                   |        |
>>        (label 0)  |        |    (label 0)
>>                   |        |
>>                   a        b
>>
>> So we can study two things under the same
>> umbrella, inside the bisimulation
>> framework of Robin Milner:
>>
>> - Lower Level adresses, such as *1, *2, *3, etc..
>>
>> - Higher Level Prolog terms, such as f(a,b), a, b, etc..
>>
>> Attention: The “Variables” in Robin Milners
>> paper are not Prolog Variables, they are more
>> like bread crumbs from Hänsel and Gretel,
>> to flee the Witch from the Forest.
>>
>> 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 (1934–2010)
>>> 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 Milner’s formalization.
>>> He clarified the distinction between simulation
>>> and bisimulation.
>>>
>>> Bye
>>
>