Re: [tlaplus] Relations

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Hi Karolis,

I don’t know if there is an answer to your question because I wouldn’t know how to select a "winner" among the various representations.  However, I want to mention that a similar challenge exists in how we represent directed and undirected graphs [1,2,3].  In my view, the best approach is to just aim for consistency across the standard modules, CommunityModules, and TLAPS-provided modules.  We should also determine ownership rules for modules [4].  Additionally, we can improve interop by introducing convenience operators that translate between different representations (see, for example, [4]).

Markus

[1] https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla
[2] https://github.com/tlaplus/CommunityModules/blob/master/modules/UndirectedGraphs.tla#L4
[3] https://github.com/tlaplus/CommunityModules/blob/master/modules/GraphViz.tla
[4] https://github.com/tlaplus/CommunityModules/issues/60
[5] https://github.com/tlaplus/CommunityModules/commit/73a56dcd77042c72d72b1a6811aaa884f85573f8

> On Dec 21, 2024, at 2:02 AM, Karolis Petrauskas <k.petrauskas@xxxxxxxxx> wrote:
> 
> Hi all,
> 
> Recently, I tried to extract some parts of my proofs on relations to a separate module and then realized an overlap with the existing modules.
> 
>     • In my case, I modeled relations as a binary operator over a set.
>     • In the StdLib WellFoundedInduction.tla considers a relation as a set of pairs. Also, an operator OpToRel translates an operator to the set representation.
>     • The CommunityModules repo contains Relation.tla, which represents relations as a binary function to booleans.
> 
> I wonder which representation should be considered the "main one"? It would be easier to consolidate results if a common base is clear.
> 
> Karolis

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/4A95DC24-5CA0-4D94-873F-FBF2D9CF49D2%40lemmster.de.