[tlaplus] Re: Comparability Rules for TLC Values

["b.v.b@xxxxxx" <b.v.b@xxxxxx>]

I'm sorry, but I have to come back at this. I know that the general sentiment is not to fix things that are not broken, but if a community member would perform the necessary changes, would there be any chance a pull request is merged?

In defense of the rule update for functions (feel free to skip depending on how opposed you are to the idea):

Doing so is possible and reasonable. Take for example the proposition <<1,"2">> # <<2,2>>.

- Even if the exact set representation of functions is unspecified, the existence of some (infinitely many) that respect the proposition seems intuitive (not a good argument, I know).

- Common definitions of functions (though not necessarily compatible with TLA) agree on the validity of the proposition. In particular, TLAPS can prove it.

- It simplifies some tasks, such as the definition of complex, comparable structures.

I'm not promising I will do it, but I have finally overcome the reluctance of looking at sources of large projects for the first time and took a little dive into the TLAplus repo. I think I have an approach that would not only lead to a reasonably simple implementation of the new rule but also simplify existing code by unifying comparison and equality and eliminating unnecessary reimplementations of those methods for similar classes without compromising their optimizations.

In case of a positive answer, I will open a new issue on GitHub and link this conversation. This way, people know it's been suggested and approved but has to come from the community, similar to the proper handling of strings.

Cheers,

Benjamin

On Wednesday, July 28, 2021 at 8:18:35 PM UTC+2 Leslie Lamport wrote:

Generalizing the rule for sets would accomplish nothing, since TLC can only cope with sets all of whose elements are comparable with one another.    Generalizing the rule for functions seems too unlikely to be useful to warrant the complication it would add to TLC's implementation.

Leslie   

On Wednesday, July 28, 2021 at 3:17:33 AM UTC-7 b....@xxxxxx wrote:

G'day,

The comparability rule for functions from the SS book are as follows:

Two functions f and g are comparable iff (i) their domains are comparable
and (ii) if their domains are equal, then f [x] and g[x] are comparable for
every element x in their domain.

Is there a specific reason for them to be so strict other than simplicity? As far as I understand the existence of a single x for which f[x] # g[x] would in theory make them distinct (and thereby comparable).

Similarly for sets (of known structure) the existence of a single element in one of the sets that is not in the other one would make them distinct.

Cheers,

Benjamin

-- 
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 on the web visit https://groups.google.com/d/msgid/tlaplus/fc8adcb0-b8de-4704-8e92-be498435ef65n%40googlegroups.com.