[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.


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.