[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Wed, 28 Jul 2021 11:18:35 -0700 (PDT)*References*: <82dee55b-3952-4a90-b0d2-8367e8e4961dn@googlegroups.com>

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.v.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/cab564dd-9ae9-4c61-aad1-fc9bebfcef93n%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Comparability Rules for TLC Values***From:*b.v.b@xxxxxx

- Prev by Date:
**Re: [tlaplus] Re: Model checking a mutually recursive definition of a tree** - Next by Date:
**[tlaplus] Re: Comparability Rules for TLC Values** - Previous by thread:
**Re: [tlaplus] Re: How to obtain the value in a function** - Next by thread:
**[tlaplus] Re: Comparability Rules for TLC Values** - Index(es):