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

[tlaplus] Re: TLA+ Expressions - need clarification



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.


On Thursday, 27 June 2019 20:32:07 UTC-4, Mike O'Shea wrote:
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 :)




--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
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.
For more options, visit https://groups.google.com/d/optout.