| Deutsch English Français Italiano |
|
<105mbs9$2l46g$1@solani.org> View for Bookmarking (what is this?) Look up another Usenet article |
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: sets or tuples? be warned (Was: At least 3 methods for Bisimilarity [Python BisPy]) Date: Mon, 21 Jul 2025 23:36:09 +0200 Message-ID: <105mbs9$2l46g$1@solani.org> References: <105lbr7$2idvv$2@solani.org> <105m9ap$2l2uv$1@solani.org> <105m9u7$2l38j$2@solani.org> <105mba6$2l3t3$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:36:09 -0000 (UTC) Injection-Info: solani.org; logging-data="2789584"; 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:eSyzx+9/2NuRPmE/UyJS4Z1y7rk= In-Reply-To: <105mba6$2l3t3$2@solani.org> X-User-ID: eJwFwYEBwCAIA7CXwNEq5wiW/09Ygo/O3kEwMBhmBW/BrMcRKWvwrsgudYa/Nf02z5nzyrbplgSXPiVr8QddihYq **Disclaimer:** I didn't double check what graphs BisPy supports, bisimulation for sets might be more complex than bisimulation for tuples, so be warned. Mild Shock schrieb: > 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 >>> >> >