Possible new language constructs for TLA+3?

188 views
Skip to first unread message

Andrew Helwer

unread,
Apr 7, 2018, 1:20:28 PM4/7/18
to tlaplus
TLA+ as a language is pretty much perfect, but there are a couple scenarios where I wish for additional language constructs/features:

Combined set-builder notation

When defining a set with set-builder notation, we have two options:
  • Mapping: {f(x) : x \in S}
  • Filtering: {x \in S : p(x)}

I often find myself wanting to both map and filter at the same time, which requires the following somewhat cumbersome expression:

  • Map & Filter: {f(x) : x \in {y \in S : p(y)}}

I think this would be much improved in readability if we had a language-level construct similar to:

  • Combined: {f(x) : x \in S WHERE p(x)}

This is similar to set comprehensions in Python, which is probably my favorite feature of that language.


EXCEPT support for nested functions


Many of the specs I write are of distributed systems, so I'll usually have one or more variables of this type:

  • distributedData \in [Node -> [Key -> Value]]

When I want to update a single value in distributedData, I use this notation:

  • distributedData' = [distributedData EXCEPT ![node] = [@ EXCEPT ![key] = value]]

It would be nicer if we could write it something like this:

  • distributedData' = [distributedData EXCEPT ![node][key] = value]

I recall this also as a common point of confusion among TLA+ course attendees, who intuitively tried this notation at first.


I'm not sure whether either of these suggestions violate some bedrock principle in the TLA+ construction (I could see that for the latter) but they certainly would both make my life simpler and reduce the cognitive overhead of reading/writing TLA+.


New standard module: Query


Not a fully fleshed-out idea, but it might be nice to have a new standard module that implements something like relational algebra for easy manipulation of sets of records, in addition to other common higher-level functions like fold and zip.


Anyone else have suggestions of their own?

Leslie Lamport

unread,
Apr 8, 2018, 12:43:21 PM4/8/18
to tlaplus

Hi Andrew,


   Perfection is achieved not when there is nothing more to add,
   but when there is nothing left to take away.
                                                  Saint-Exupery


Except for the proof language, I'm interested in removing things from
TLA+ rather than adding them.  In fact, I've stopped mentioning
constructs with free tuples such as {<<x, y>> \in S : p(x, y)},
intending to remove them from the de facto language as a prelude
to possibly removing them from the supported language.  I think


   {f(x) : x \in {y \in S : p(y)}}


can be expressed well enough with


   LET T == {y \in S : p(y)}
   IN  {f(x) : x \in T}


so there's no need to add the language feature you propose.


----


The expression


   [distributedData EXCEPT ![node][key] = value]


is already legal TLA+, as are things like


   [e EXCEPT ![a].b[c]]


The ability to write such expressions is a major reason that
I prefer EXCEPT to other notations that have been proposed
for writing  [e EXCEPT ![a] = b].


----


The main reason for making something a standard module is so its
operators can be implemented in Java.  It's fairly easy to write your
own Java implementations of operators in a module.  For any module
Foo, you just have to add a file Foo.java to the appropriate
directory.  You can look up the java files corresponding to the
current standard modules to see how it's done.  Anyone proposing a
standard module should try it out and see how much it speeds
execution.  It might be better to modify the Toolbox and TLC to
make it easy to share such modules and their implementations
rather than to grow the set of standard modules. 


Leslie

Ron Pressler

unread,
Apr 9, 2018, 7:11:38 AM4/9/18
to tlaplus
Hi.

Can you elaborate some more on the motivation? Minimalism is certainly a virtue, but surely something can be said for convenience of reading. Syntax sugar doesn't add new concepts, so it adds little in the way of a mental burden (and it can be desugared from the AST by the parser, keeping tools simple), and IF it is intuitive it can assist with readability. Free tuples are a great example. Not only is the syntax intuitive, but it is so in line with ordinary mathematical notation that even if not taught, users may guess it is supported and try it.

Using a LET to simplify nested comprehensions requires the spec writer to name some intermediary set that may not be meaningful on its own, and requires the reader to at least read the name and maybe ponder its significance. It's not a show-stopper, but it does add some small mental road-bump.

As to standard modules, I can think of some more reasons. By given common idioms standard names they can make it easier to read other people's specs without studying their definitions. They can also ensure that the definitions are correct. Finally, they can then serve as a common ground for reusable theorem modules. Obviously, it's not a good idea that have the standard modules contain any possibly useful definition, but some very common idioms could be added. For example, I think many definitions in the standard TLAPS modules may be candidates.

Ron

Leslie Lamport

unread,
Apr 9, 2018, 5:45:36 PM4/9/18
to tlaplus
It's easy to find useful things to add to a language.  I expect if I asked 100 TLA+ users, I could get 10 reasonable suggestions.  And any single addition adds little in the way of mental burden.  It requires ruthless discipline to keep the sum of those little additions from becoming burdensome.  All the constant operators appear in Tables 1 and 2 of "Specifying Systems".  There are already too many of them, as evidenced by Andrew being unaware of "EXCEPT ![a][b]". 

I remember many years ago listening to a talk in which someone described a project that led them to propose additions to the TLA logic.  I remarked that they had spent 6 months adding things to TLA that it had taken me 15 years to learn how to get rid of.

I suggest that instead of thinking of things to add to TLA+, it would be much more useful (and much harder) to come up with things that can be removed.  I'd love to see temporal logic removed, but I don't know anything better to replace it with.

Leslie
Reply all
Reply to author
Forward
0 new messages