[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Mon, 9 Aug 2021 09:49:03 -0700*References*: <d7978eb0-7d00-4d0d-9341-217c3eda91f8n@googlegroups.com>

On 8/9/21 6:22 AM, Victor Miraldo wrote:

Hello TLA+,I'm currently developing a tool that generates TLA+ from SystemF. Thismorning I came across some interesting generated code, which wasrejected 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". Thisbehavior is surprising to me because I cannot say "RECURSIVE Do(_(_,_),_, _)", which means I can't declare "Do" with the correct type beforeits usage.Sure, in the snippet above I could always swap the definitions of Do andDoubleDo, but in general, this happens with mutually recursive functiondefinitions that actually use each other in their bodies, so regardlessof 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 mutuallyrecursive definitions?On a similar note, we thought of representing all higher-order'nessthrough 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 tofunctions or could we simply use functions everywhere? It's worthmentioning we generate thousands of lines of TLA+, so performance is amust. 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/2871f5c9-e81c-6800-e8a8-07f85bdd50b0%40lemmster.de.

**Follow-Ups**:**Re: [tlaplus] Mutually Recursive Higher Order Terms Syntax Error***From:*Victor Miraldo

**References**:**[tlaplus] Mutually Recursive Higher Order Terms Syntax Error***From:*Victor Miraldo

- Prev by Date:
**Re: [tlaplus] More Sophisticated Forms of Model Checking** - Next by Date:
**Re: [tlaplus] More Sophisticated Forms of Model Checking** - Previous by thread:
**[tlaplus] Mutually Recursive Higher Order Terms Syntax Error** - Next by thread:
**Re: [tlaplus] Mutually Recursive Higher Order Terms Syntax Error** - Index(es):