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

["ron.pr...@xxxxxxxxx" <ron.pressler@xxxxxxxxx>]

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

On Sunday, July 26, 2020 at 12:39:14 AM UTC+1 emanuel....@xxxxxxxxx wrote:

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

-- 
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/2b1a67eb-1e58-4b8d-9858-5a5aa61fce9dn%40googlegroups.com.