[tlaplus] Mutually Recursive Higher Order Terms Syntax Error

[Victor Miraldo <victor.miraldo@xxxxxxxx>]

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

-- 
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/d7978eb0-7d00-4d0d-9341-217c3eda91f8n%40googlegroups.com.