Mutually Recursive Higher Order Terms Syntax Error

[Victor Miraldo]

Hello TLA+,

I'm currently developing a tool that generates TLA+ from SystemF. This morning I came across some interesting generated code, which was rejected by TLA. After minimizing it I came up with the following:

11| RECURSIVE Do(_,_,_)
12| DoubleDo(op(_,_), a) == Do(op,a,a)
13| Do(op(_,_), a, b) == op(a, b)

TLA talls me that "line 12: The operator op requires 2 arguments". This behavior is surprising to me because I cannot say "RECURSIVE Do(_(_,_), _, _)", which means I can't declare "Do" with the correct type before its usage.

Sure, in the snippet above I could always swap the definitions of Do and DoubleDo, but in general, this happens with mutually recursive function definitions that actually use each other in their bodies, so regardless of which definition you put first you'd get an error.

I also tried eta-expanding:

12| DoubleDo(op(_,_), a) == Do(LAMBDA x,y: op(x,y),a,a)

but this didn't fool TLA either.

Does anyone have a suggesting for handling higher order mutually recursive definitions?

On a similar note, we thought of representing all higher-order'ness through TLA functions, which in this example, would be:

11| RECURSIVE Do(_,_,_)
12| DoubleDo(op, a) == Do(op,a,a)
13| Do(op, a, b) == op[a, b]

And this works like a charm! Is there a reason to prefer operators to functions or could we simply use functions everywhere? It's worth mentioning we generate thousands of lines of TLA+, so performance is a must. Do operators perform better than functions?

Thank you!

Victor

[Markus Kuppe]

https://github.com/tlaplus/tlaplus/issues/57

M.

[Victor Miraldo]

Thank you Markus and Leslie,

First I'd like to paste the answer I got from Leslie on my e-mail, then I'd like to ask some followup questions.

> Hi Victor,
>
> I approved the message you sent to the group, but I haven’t received a copy of it so I’m afraid something may have gone wrong.  To answer your question, the reason recursive definitions of higher-order operators are not allowed in TLA+ is because I don’t know what they would mean and it has not seemed to be worth the effort to try to find out.  If someone provides a satisfactory definition of their semantics, they can be added to the language.  Since we have limited manpower, whether they are then implemented in the parser and in TLC would depend on how difficult it is and how important it seems.  To understand what is involved, see
>
>    http://lamport.azurewebsites.net/pubs/recursive-ops.pdf
>
> Since others may have the same question, I hope that your message does eventually appear.  If it has been lost, please repost a suitable message containing your question and its answer.  If just the copy sent to me has been lost, perhaps you can post the answer yourself.

>

> Thanks,

> Leslie Lamport

@Markus, thanks for the link. I couldn't figure out whether the issue you linked meant to say the support will disappear or whether there is more interest in supporting it. It surely doesn't help that the `SetReduce` appears on the https://learntla.com/tla/operators/ page.

@Leslie, thank you for the message and the explanation. I fully appreciate the difficulty with recursion of any form. IIRC, in the simply typed lambda calculus with fix, one can define a generalized fix combinator and handle mutual recursion with that, but I have no idea how that all would work within TLA+, I barely just started learning TLA+.

This brings me to my next question. Seems like I'll have to either (A) remove the mutual recursion before outputting TLA+ or (B) rely on passing TLA+ functions and "faking" the higher-order'ness. I

can always wrap an operator into a function and this seems to trick TLA+ into accepting my definitions:

11| RECURSIVE Do(_,_,_)
12| DoubleDo(op, a) == Do(op,a,a)
13| Do(op, a, b) == op[a, b]

...

42| X == ... DoubleDo([ x \in TypeA ,  y \in TypeA |-> Op(x,y)], z)

Is there a disadvantage to using TLA+ functions and the trick above? Specifically, could that hurt performance in case `TypeA` is a complex set?

Where can I learn more about the tradeoffs between using TLA+-operators to encode lambda-calc-functions or TLA+-functions to encode lambda-calc-functions?

Thanks,

Victor

[Markus Kuppe]

On 8/10/21 1:02 AM, Victor Miraldo wrote:
> @Markus, thanks for the link. I couldn't figure out whether the issue
> you linked meant to say the support will disappear or whether there is
> more interest in supporting it. It surely doesn't help that the
> `SetReduce` appears on the https://learntla.com/tla/operators/ page.

[...]

> Is there a disadvantage to using TLA+ functions and the trick above? Specifically, could that hurt performance in case `TypeA` is a complex set?
> Where can I learn more about the tradeoffs between using TLA+-operators to encode lambda-calc-functions or TLA+-functions to encode lambda-calc-functions?

Hi Viktor,

the existing bug #57 is about aligning TLC with the TLA+ language spec,
i.e., fix TLC to no longer accept higher-order recursive operators.

If you believe that TLA+ should support higher-order recursive operators
and have the capacity to design and implement it, please open an RFC at
https://github.com/tlaplus/rfcs.

As for LearnTLA: https://github.com/hwayne/learntla/issues/98

You will have to create a benchmark to determine if performance differs
significantly between recursive operators and recursive functions.

Markus

[Victor Miraldo]

Hello Markus,

> You will have to create a benchmark to determine if performance differs
> significantly between recursive operators and recursive functions.

From this I infer that there is no obvious reason stopping us from using the trick I suggested.

That's good news. Thanks.

> the existing bug #57 is about aligning TLC with the TLA+ language spec,
> i.e., fix TLC to no longer accept higher-order recursive operators.

Another reason for us to switch to using functions ASAP.

> If you believe that TLA+ should support higher-order recursive operators
> and have the capacity to design and implement it, please open an RFC at
> https://github.com/tlaplus/rfcs.

Thanks! I certainly think TLA+ should support HO recursive operators and would

love to pick something like that up if I ever get enough free time or my employer

is happy with that. :)

Cheers,

Victor