Remove CHOOSE and recursive operators from TLA+ in favor of new FoldSet language primitive

@konnov:

[It] makes me wonder, whether we need CHOOSE, if we assume that we are working only with finite sets (as both TLC and Apalache do). I have an impression that “FoldSet” together with the other set operators of TLA+ could be powerful enough to replace reasonable recursive operators and CHOOSE over finite sets.

@xxyzzn:

I think we do. How would you write a recursive definition of the cardinality of a set without being able to choose a single element from the set? Since specs are Boolean-valued formulas, it's possible that one could rewrite any spec written in terms of Cardinality using only its properties and removing its definition. (Stephan might know if that's always possible.) But it would produce unreadable specs.

In practice, you can get pretty far using CHOOSE to avoid recursive definitions--e.g., for defining the maximum of a set of numbers or even the length of a sequence. This is useful because engineers who have never used a functional programming language have a hard time dealing with recursion."

@konnov:

ight. What I meant is that we could have FoldSet as a primitive operator in the set of operators as an alternative to bounded CHOOSE and recursive operators. Currently, FoldSet is defined as follows in [1], I just inlined the auxiliary definition:

RECURSIVE FoldSet(_,_,_)
FoldSet( Op(_,_), v, S ) ==
  IF S = {} THEN v
  ELSE LET w == CHOOSE x \in S: TRUE IN
    LET T == S \ {w} IN FoldSet( Op, Op(v, w), T )

We would still have to impose a fixed but unknown order of iteration over a set. Having FoldSet as a primitive, which means that we would have to define its semantics without using CHOOSE and recursive operators, we could define bounded CHOOSE as follows:
MyChoose(S, P(_)) ==
LET Iter(res, elem) ==
IF res[1]
THEN res
ELSE <<P(elem), elem>>
IN    
LET res == FoldSet(Iter, <<FALSE>>, S) IN
res[2]
The good thing about FoldSet is that it is obviously terminating and one still can write plenty of things with iteration. I know that FoldSet would not be expressive enough to replace all terminating recursive operators. I guess, we would not be able to express the Ackermann function with it. But I have always been curious about how powerful a single transition of a state machine should be.

In practice, you can get pretty far using CHOOSE to avoid recursive definitions--e.g., for defining the maximum of a set of numbers or even the length of a sequence. This is useful because engineers who have never used a functional programming language have a hard time dealing with recursion.

I agree that CHOOSE can help a lot when someone is stuck. It is just that recursive operators and CHOOSE have been a pain point in Apalache from the beginning. I understand that this is how TLA+ was designed. The question is whether you absolutely need CHOOSE and recursive operators to write a good and understandable specification.

@xxyzzn:

The fundamental goal of TLA+ is not to provide tools for finding bugs. It's to teach people a better way to think about systems. Tools are needed to accomplish that, but they are a means not an end. We were recently told that Amazon has realized this, and that they want people to use TLA+ because it improves the way they think.

The reason TLA+ does that has to do with its simplicity and elegance. CHOOSE is a TLA+ primitive and FoldSet isn't because CHOOSE is simpler and more elegant than FoldSet. [...]

@lemmy:

For what it's worth, out of the ~20 TLA+ projects I sampled (a search for TLA+ language) on Github, about 1/3 use recursive operators.

tlaplus / rfcs

Remove CHOOSE and recursive operators from TLA+ in favor of new FoldSet language primitive #3