[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Mutually Recursive Higher Order Terms Syntax Error
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
--
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/af4f5d40-1c2a-e105-18f3-bffa12cceeb5%40lemmster.de.