On recursion again: does Apalache handle Fold operators over collections well?

[timimin]

Hello.
I have another question on recursive operators. In the previous post you said:

We have found that, in practice, using the folds defined by the Apalache module, recursive operators are almost always unnecessary, and it's very likely that we will end up restricting their use in the future.

I've been thinking for a while and found it difficult abstaining from using folds in some cases. I guess it is possible to express an effect of almost any map operation in terms of pure logic terms but when it comes to some reduce algorithm with an accumulator... Say i want to model an abstract semantics on a finite lattice structure. I have defined the partial order, the least upper bound (LUB) and the greatest lower bound (GLB) binary operators. Now i want to define the least upper bound operator on a subset.
It seems i have two options:

1. I can do it algorithmically:

LUB4Set (s) == FoldSet(LAMBDA x, y: LUB(x,y), min, s)

2. Or declaratively using the formal definition, smth like:

LUB4Seq (s) == CHOOSE p \in PolSet: /\  \A x \in s: compareItem(x, p)
                                    /\ ~\E y \in PolSet: y # p
                                              /\ \A z \in s: compareItem(z, y)
                                              /\ compareItem(y, p)

where PolSet - is the lattice, compareItem - is the partial order.

In the second option i have to explicitly define the PolSet which may be large enough.
The question is what is the best choice? Does the fold operator has that bad impact on the Apalache effectiveness? What can we do if it is impossible to implement the accumulator pattern declaratively? Should we abstract away such computations in our model?

Thanks in advance. Alex.

[shonfeder]

Does the fold operator has that bad impact on the Apalache effectiveness?

On the contrary! Our plans to depreciate explicit recursions is motivated in part by our conviction that folds are nice and good, and the best option for enabling iteration over collections.

I think you may have misread @konnov's remark, but I can see how the confusion arose. When Igor wrote,

We have found that, in practice, using the folds defined by the Apalache module, recursive operators are almost always unnecessary, and it's very likely that we will end up restricting their use in the future.

He meant that, recursive operators (i.e., operators defined using explicit recursion) are unnecessary because folds work so well, and suffice for all cases of interest. IIUC, you read Igor to be saying instead "recursive operators, including folds, are unnecessary".

So, fold away! We are fond of folds 😉 If, however, you find a case where you think you need explicit recursion, and a FOLD cannot suffice, please do let us know :)

[Kukovec]

We have found that, in practice, using the folds defined by the Apalache module, recursive operators are almost always unnecessary, and it's very likely that we will end up restricting their use in the future.

This was phrased poorly. The thing being restricted are RECURSIVE-defined operators, not folds (we plan on supporting folds for the foreseeable future, and in fact encourage their use).

In the second option i have to explicitly define the PolSet which may be large enough. The question is what is the best choice? Does the fold operator has that bad impact on the Apalache effectiveness? What can we do if it is impossible to implement the accumulator pattern declaratively? Should we abstract away such computations in our model?

IMO, folds are the vastly superior choice here. They have a direct encoding (i.e. they are treated by Apalache as if they were language-level operators and are not expanded to an equivalent TLA+ definition and then encoded) and are probably the most efficient way of doing iteration. So by all means, keep using folds.

[timimin]

Thanks a lot, friends. It is my fault, i've read it again and now see the point. -- Отправлено из Mail.ru для Android воскресенье, 12 декабря 2021г., 23:59 +03:00 от Kukovec ***@***.*** :

…

>>We have found that, in practice, using the folds defined by the Apalache module, recursive operators are almost always unnecessary, and it's very likely that we will end up restricting their use in the future. This was phrased poorly. The thing being restricted are RECURSIVE-defined operators, not folds (we plan on supporting folds for the foreseeable future, and in fact encourage their use). >In the second option i have to explicitly define the PolSet which may be large enough. The question is what is the best choice? Does the fold operator has that bad impact on the Apalache effectiveness? What can we do if it is impossible to implement the accumulator pattern declaratively? Should we abstract away such computations in our model? IMO, folds are the vastly superior choice here. They have a direct encoding (i.e. they are treated by Apalache as if they were language-level operators and are not expanded to an equivalent TLA+ definition and then encoded) and are probably the most efficient way of doing iteration. So by all means, keep using folds. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub , or unsubscribe . Triage notifications on the go with GitHub Mobile for iOS or Android .