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

*From*: Matthew Singletary <matt.singletary@xxxxxxxxx>*Date*: Fri, 28 Jun 2019 11:39:29 -0400*References*: <68ae5b95-a7c2-4590-ab08-36e2074f403e@googlegroups.com> <9f67b0c4-3901-46ec-afb6-2e450bca646c@googlegroups.com> <1be823bd-9a61-43ee-999c-1d48422c1906@googlegroups.com> <2d7daa81-cdca-4b80-a390-4b8465f58980@googlegroups.com>

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.

On Thu, Jun 27, 2019 at 9:14 PM Jay Parlar <parlar@xxxxxxxxx> wrote:

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

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/CAAJ-tZLvShqFxKoLO7CMvrn%2B7hXbY%2BxkWFQyguYQ3EjDQm0m0A%40mail.gmail.com.

For more options, visit https://groups.google.com/d/optout.

**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

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

- Prev by Date:
**[tlaplus] Re: TLA+ Expressions - need clarification** - Next by Date:
**[tlaplus] Making PlusCal a first-class language for TLC** - Previous by thread:
**[tlaplus] Re: TLA+ Expressions - need clarification** - Next by thread:
**[tlaplus] Making PlusCal a first-class language for TLC** - Index(es):