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

*From*: Jay Parlar <parlar@xxxxxxxxx>*Date*: Thu, 27 Jun 2019 18:14:21 -0700 (PDT)*References*: <68ae5b95-a7c2-4590-ab08-36e2074f403e@googlegroups.com> <9f67b0c4-3901-46ec-afb6-2e450bca646c@googlegroups.com> <1be823bd-9a61-43ee-999c-1d48422c1906@googlegroups.com>

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.

On Thursday, 27 June 2019 20:32:07 UTC-4, Mike O'Shea wrote:

-- 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**2I 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.

**Follow-Ups**:**Re: [tlaplus] Re: TLA+ Expressions - need clarification***From:*Matthew Singletary

**References**:**[tlaplus] TLA+ Expressions - need clarification***From:*Mike O'Shea

**[tlaplus] TLA+ Expressions - need clarification***From:*Jay Parlar

**[tlaplus] Re: TLA+ Expressions - need clarification***From:*Mike O'Shea

- Prev by Date:
**[tlaplus] Re: TLA+ Expressions - need clarification** - Next by Date:
**Re: [tlaplus] Re: TLA+ Expressions - need clarification** - Previous by thread:
**[tlaplus] Re: TLA+ Expressions - need clarification** - Next by thread:
**Re: [tlaplus] Re: TLA+ Expressions - need clarification** - Index(es):