TLA+ Expressions - need clarification

[Mike O'Shea]

I'm working through the TLA+ Lecture 5 example and trying to nail down the notation as implemented by TLA+. I have looked at the TLA+ book and the "cheat sheet" of notation, but I'm having a hard time wrapping my head around a couple things.

The primary question is related to the "type" of "rmState" and how it is used in the spec as a variable. The other questions have to do with how/when to interpret the meaning of square brackets in the TLA expression syntax - in some cases they return a set of functions, in others they seem to represent a single function.

For example. This definition in the example spec:

TCTypeOK == rmState \in [RM -> {"working","prepared","committed","aborted"}]  

In the TLA documentation, the expression [S->T] is a "set of functions f, with f(x) /in T for x /in S".  

So, according to the definition given, I can interpret as:  S = RM and T = {"working","prepared","committed","aborted"}, and rmState is any function that maps S to T.  Correct?

Which leads me to this definition expression in the spec:

TCInit == rmState = [r \in RM |-> "working"]

Here the TLA documentation says the expression of form "[x in S |-> e]" is a "function f, such that f(x) = e for x in S". Even though we're seeing [] brackets - which implies a set of functions, that function which returns a specific (constant expression 'e') value for any x in S can really only be a constant function. In this case, rmState seems to be representing a function that returns "working" for all r in RM. Correct?

To summarize:

1. I think rmState's type, based on the above definitions/context, is "function". 

2. The square bracket notation can return or reference either a set of functions or a specific function.

Thanks for any clarification or support.

[Hillel Wayne]

[A -> B] is a set of functions, [x \in S |-> expr] is a specific function. Note the pipe in the second one: individual functions use |->, sets of functions use ->.

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/68ae5b95-a7c2-4590-ab08-36e2074f403e%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Jay Parlar]

I’ve found that it helps some people to see “Python equivalents” of these operators, to help build intuition.

I put together this cheat sheet awhile ago where I explain some key TLA+ operators in terms of Python: https://github.com/parlarjb/tla_workshop/blob/master/tla_cheatsheet.pdf

[Mike O'Shea]

Hi Jay. This is great. Python is one of my favorite languages, so this is a good resource. I will certainly go through this in some depth. Thanks!

I happened to run into the "SRC Technical Note - The Operators of TLA+" and encountered another explanation of this notation "[x \in D |-> e]"  as being TLA's equivalent to lambda expressions. Then it clicked for me a little more as this being a function generator.

In TLA+:

f = [x \in Nat |-> x^2 ]

In Python:

f = lamba x: x**2

I liked your take on that as well using a list comprehension. function == array mapping makes sense, but tough to break out of the programming mindset. Even Lamport seems to mix and match terms like "array expression" with "function" in his videos. I'm not yet able to "translate" synonymous terminology on the fly :)

[Jay Parlar]

It'll help to keep in mind the mathematical meaning of the word "function": It's a thing (relation) that associates an input to a single output.

Some functions have infinite domains. The TLA+ and Python functions you have below are examples of that. They take any value from the infinite set of natural numbers, and return a single output.

But then you can _also_ think of Python dictionaries as functions! They're functions with finite domains, namely, the keys in the dict. But each of those keys maps to a single output.

If you add/remove/modify a key/value pair in a Python dictionary, then you now have a _different_ function. But a dictionary at some point in time can definitely be viewed as a function.

This means arrays are also functions. The domain is the indices of the array, and each of those indices maps to a single output. 

So some mixing and matching of terms is ok, because all of these things are essentially functions.

[S -> T] vs [x \in S |-> T] can be confusing at first, because so much syntax is shared between them. They both use [ and ], and they both have "arrows". And they're both dealing with functions. But they mean _drastically_ different things :)

Jay P.

[Matthew Singletary]

On the note that dictionaries can be viewed as functions, in Clojure, Map (the near-equivalent of python's dict) actually implements their function interface, so clojure maps _are_ functions.

I imagine you might be able to do something similar in python, but I'm not sure how.

See https://clojure.org/reference/data_structures#Maps

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2d7daa81-cdca-4b80-a390-4b8465f58980%40googlegroups.com.