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

Groups > comp.lang.prolog > #14719

At least 3 methods for Bisimilarity [Python BisPy] (Was: Bonus: Prolog Systems with Strings, Bigints, etc.. )

Show all headers | View raw

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
>>>
>>
> 

Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Fathers of Bisimulation: Robin Milner (1934–2010) Mild Shock <janburse@fastmail.fm> - 2025-07-21 14:28 +0200
  From Bisimulation to Bisimilarity: A Complete Inference System (Was: Fathers of Bisimulation: Robin Milner (1934–2010)) Mild Shock <janburse@fastmail.fm> - 2025-07-21 22:44 +0200
    Bonus: Prolog Systems with Strings, Bigints, etc.. (Re: From Bisimulation to Bisimilarity: A Complete Inference System) Mild Shock <janburse@fastmail.fm> - 2025-07-21 23:04 +0200
      At least 3 methods for Bisimilarity [Python BisPy] (Was: Bonus: Prolog Systems with Strings, Bigints, etc.. ) Mild Shock <janburse@fastmail.fm> - 2025-07-21 23:25 +0200
        sets or tuples? be warned (Re: At least 3 methods for Bisimilarity [Python BisPy]) Mild Shock <janburse@fastmail.fm> - 2025-07-21 23:36 +0200
  The Original Ganster (OG) of Bisimilarity are Hopcroft and Karp (1971) (Re: Fathers of Bisimulation: Robin Milner (1934–2010)) Mild Shock <janburse@fastmail.fm> - 2025-07-22 00:50 +0200
    All-in-One DAM-GT: Wuhan, Hopcroft and Attention (Was: The Original Ganster (OG) of Bisimilarity are Hopcroft and Karp (1971)) Mild Shock <janburse@fastmail.fm> - 2025-08-06 15:10 +0200

csiph-web