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

*From*: "ron.pr...@xxxxxxxxx" <ron.pressler@xxxxxxxxx>*Date*: Sun, 26 Jul 2020 05:39:13 -0700 (PDT)*References*: <0dd33769-a76b-4ffc-a201-ffaacad1e50eo@googlegroups.com> <2b1a67eb-1e58-4b8d-9858-5a5aa61fce9dn@googlegroups.com> <a95b6583-6bc5-44a5-9521-af3daa7c62fbo@googlegroups.com> <93aac454-a9d9-4e8e-b536-590232637700n@googlegroups.com>

P.S.

When I said that if a,b ∈ S then they're comparable, that applies to the canonical sets that are defined axiomatically: BOOLEAN, STRING, Nat, Int, Real. Obviously, it doesn't apply to the set Nat ∪ STRING, but I'm not sure about the status of that set in TLA+ (obviously Nat ∩ STRING isn't defined).

-- Ron

On Sunday, July 26, 2020 at 1:31:19 PM UTC+1 ron.pr...@xxxxxxxxx wrote:

Equality in set theory is defined as "same members" but while everything in TLA+ is a set, be it 1, "a", or [n ∈ Nat ↦ n + 1], the members of those sets aren't defined in the axioms of TLA+, and as we don't know what the members of 1 and "a" are, we cannot compare them. This is a good thing as it makes "nonsensical" propositions, such as 1 ∈ 3 undefined (indeterminable, really).We can compare objects on which equality is defined by the axioms of TLA+. In particular, if there is some set S such that a ∈ S and b ∈ S, then the truth of the proposition a = b is defined. And as Nat ⊆ Int ⊆ Real, all numbers can be compared. The rules for functions derived from that and from the fact that TLA+ defines the DOMAIN operator on all functions (so two functions are equal if their domains are equal and their mappings on the domain are equal), and that's how operators like Len work. Recursively, this means that sets with comparable members can be compared, and functions with comparable domains and ranges can be compared. This is why sequences with comparable elements can be compared, and why strings, which are also functions can be compared.-- RonOn Sunday, July 26, 2020 at 1:18:42 PM UTC+1 emanuel....@xxxxxxxxx wrote:Hi,This rises some more questions:* How is equality/unequality defined actually?** What about '1 = 2' and 1 /= 2?** What about '1.0 = 1' and 1.0 /= 1?** What about '3.14 = 1' and 3.14 /= 1?As far as I know, every value is a set in TLA+.We just don't care what the elmenets are in 1, 3.14 etc.Right?As far as I know, sets are equal if they have the same elements.This means, that we can't compare sets of unknown elements.* So what we can compare?* Why Len() from Sequences works as expected?Thanks,Emanuel

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/72b942a7-163d-4e33-9fce-2d363d10386cn%40googlegroups.com.

**References**:**[tlaplus] The rules of TLA+ do not imply that 1 /= "a" ?***From:*Emanuel Koczwara

**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?***From:*ron.pr...@xxxxxxxxx

**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?***From:*Emanuel Koczwara

**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?***From:*ron.pr...@xxxxxxxxx

- Prev by Date:
**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?** - Next by Date:
**[tlaplus] Variables with values unspecified but distinct from each other** - Previous by thread:
**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?** - Next by thread:
**[tlaplus] Variables with values unspecified but distinct from each other** - Index(es):