Comparability Rules for TLC Values

[b....@gmx.at]

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

[Leslie Lamport]

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   

[b....@gmx.at]

Not to say that this behavior is up to spec, but TLC is quite happy to evaluate expressions like 1 \in {1,"a"} (though naturally not 1 \in {"a",1} ;D ) and I think it is a good thing, since it is obviously true and (if fully supported) could be even useful at times (e.g. in some function domains, when writing in the TLA subset which is supported both by TLC and TLAPS). Thus I wouldn't say there is no application of those less strict rules. I have to admit though, that this niche is probably rather small. And of course implementing the necessary checks for such sets with partially undefined properties would probably be quite a complex task.

Thanks for sating my curiosity! (And sorry for my pedantry)

Cheers,

Benjamin

[b....@gmx.at]

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: