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 :)