[zekrioca]

Doesn't ℤ include negative natural numbers?

* Nevermind, I just saw you used the ">" sign in the definition. Is it why the definition only applies to positive numbers? In any case, you did not write it in your textual description, which looked confusing to me. I think it would be easier if one could define it as ℤ+ or something like that.

[Jtsummers]

The original from pron:

    f ≜ CHOOSE f ∈ [Int → Int] : 
       ∀ x ∈ Int : f[x] = -f[x]

You added the > in your quote of pron, he didn't have it in the original. There is no c in ℤ with c != 0 s.t. f(x) = c and f(x) = -f(x), that would imply that c = -c for non-zero integers which is not true. The only function that can satisfy pron's constraints is f(x) = 0 since c = 0 is the only time c = -c, or 0 = -0.

[zekrioca]

That’s true, my mistake. Thank you for the clarification! In this case, I have another question.

Why is this original definition different than say

f ≜ CHOOSE f ∈ [Int → Int]:

       ∀ x ∈ Int : f[x] = 0

If you want some function to be 0, just specify it. Why does one need to find this a broader but more complex way of specifying the possible “input” space in TLA+? How does it help is my question, I guess.

[pron]

Because sometimes you're not sure if your belief is correct. To show what TLA+ can do, I used a simple example where the truth of the proposition (f is the zero function) is pretty obvious yet behaves very differently from how programming works to show how you can prove things in TLA+:

    THEOREM fIsTheZeroFunction ≜
         f = [x ∈ Int ↦ 0]
    PROOF
      ⟨1⟩ DEFINE zero[x ∈ Int] ≜ 0
      ⟨1⟩1. ∃ g ∈ [Int → Int] : ∀ x ∈ Int : g[x] = -g[x] BY zero ∈ [Int → Int]
      ⟨1⟩2. ∀ g ∈ [Int → Int] : (∀ x ∈ Int : g[x] = -g[x]) ⇒ g = zero OBVIOUS
      ⟨1⟩3. QED BY ⟨1⟩1, ⟨1⟩2 DEF f

The TLAPS TLA+ proof-checker verifies this proof instantly.

You can then use that proof like so:

    THEOREM f[23409873848726346824] = 0 
       BY fIsTheZeroFunction

But when you specify a non-trivial thing, say a distributed system, you want to make sure that your proposition -- say, that no data can be lost even in the face of a faulty network and crashing machines -- is true but you're not sure of it in advance.

Writing deductive proofs like above can be tedious when they're not so simple, and the TLA+ toolbox contains another tool, called TLC, that can automatically verify certain propositions (with some caveats), especially those that arise when specifying computer systems (though it cannot automatically prove that f is zero everywhere).

So the purpose of my example wasn't to show something that is useful for engineers in and of itself, but to show that TLA+ works very differently from programming languages, and it is useful for different things: not to create running software but to answer important questions about software.

[zekrioca]

Thanks for the nice explanation, that makes a lot of sense! Would you have any good recommendations about where to start with TLA+?

Thanks again!

[pron]

I would recommend the TLA+ Video Course: https://lamport.azurewebsites.net/video/videos.html

There are other good resources (some somewhat updated, but not enough to matter) are listed here: https://lamport.azurewebsites.net/tla/learning.html

[auggierose]

This was just an example that TLA+ is not executable.

You didn't realise that f[x] = -f[x] implies f[x] = 0, and that is how it is often: You have some property, but you don't know what it entails exactly. TLA+ allows you to reason about that.

[zekrioca]

Thanks, that makes sense!