The rules of TLA+ do not imply that 1 /= "a" ?

[Emanuel Koczwara]

Hi,

  In the book on page 81, chapter 7, section 7.3, Some Further Hints, there is a statement:

    Don't assume values that look different are unequal.

  And then:

    The rules of TLA+ do not imply that 1 /= "a".

  I need some explanations here. How? Why? I'm confused.

Thanks,

Emanuel

[ron.pr...@gmail.com]

This seemingly simple question actually boils down to fairly complex issues of formal logic, so first let me try to give the practical ramifications -- i.e. what you should care about -- and then give some intuition for why this is so.

In TLA+, it is neither true nor false that 1 is equal to "a". The proposition 1 = "a" is simply one that cannot be proven or falsified. This means that the two are incomparable, and that you should never attempt to compare them. Because this question has no answer, when trying to evaluate such an expression, TLC will throw an error.

As to the intuition for why that is so, let me give an analogy from software. Suppose that the way you check if computer objects are equal or not is by comparing the files that contain their encoding. I then ask you, is Tolstoy's Anna Karenina equal to a cat picture or not? There is no way to answer this question. It's certainly possible that some image format happens to encode some particular cat picture as a file that happens to be the same encoding as the text of Anna Karenina.

This issue doesn't come up in programming often because either your programming language is typed in such a way that 1 = "a" is a syntax error or definitionally equal to false, or it has an object tag system (AKA dynamic typing), that attaches a "type" name to every object. In such languages, 1 or "a" are either syntactically or dynamically much more complex objects than they are in "ordinary" mathematics, and TLA+ is mathematics. In math, the question is 1 equal to "a" is nonsensical. TLA+, being formal, has to precisely define what "nonsensical" means, and in TLA+ it means "indeterminable", or "we don't know and we don't care".

Hope this helps.

-- Ron

[Emanuel Koczwara]

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

[ron.pr...@gmail.com]

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.

-- Ron

[ron.pr...@gmail.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