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