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

[tlaplus] Re: TLA+ Expressions - need clarification

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/1be823bd-9a61-43ee-999c-1d48422c1906%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.