Relations

[Karolis Petrauskas]

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

[Markus Kuppe]

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