[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: Comparability Rules for TLC Values
- From: Leslie Lamport <tlaplus.ll@xxxxxxxxx>
- Date: Wed, 28 Jul 2021 11:18:35 -0700 (PDT)
- Ironport-hdrordr: A9a23:bKSjl6ka0+T+pA/AK2ynNJehzvHpDfKn3DAbv31ZSRFFG/Fw9vre4MjzsCWf5Qr5N0tQ/exoVJPwJk80sKQFmbX409+ZLX/bUEXBFvAU0WKg+UySJ8XGntQtoZuICpIOQeEYbmIK8PoTVWKDYqYdKae8gdmVbLzlvgZQpGhRAskKnmVE40SgYzZLrW99dOQE/bWnifavzADQA0j/AP7LYEXsnoD41r72fVHdDyLuxSRK1OE/5gnYnYIS3yL44v/vOAk/vovKOFKk4mnEz5Tmieiyzlv31mPY7Zha3PvnjvVZAtCU4/JlWAnRtg==
- References: <firstname.lastname@example.org>
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.
On Wednesday, July 28, 2021 at 3:17:33 AM UTC-7 b.v.b@xxxxxx wrote:
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.
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.