Re: [tlaplus] Mutually Recursive Higher Order Terms Syntax Error

[Victor Miraldo <victor.miraldo@xxxxxxxx>]

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

On Monday, August 9, 2021 at 6:49:12 PM UTC+2 Markus Alexander Kuppe wrote:

On 8/9/21 6:22 AM, Victor Miraldo wrote:
> 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

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

M.

-- 
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/875df3b8-49ec-46c7-8e15-00e25cbcd7bcn%40googlegroups.com.