[tlaplus] Question about : symbol in subexpressions of recursive operators

• From: Andrew Helwer <andrew.helwer@xxxxxxxxx>
• Date: Tue, 11 May 2021 06:49:04 -0700 (PDT)
• Ironport-hdrordr: A9a23:KiY5jKCNBzL78C/lHej8sceALOsnbusQ8zAXPhhKOGFomszxrbHNoByCvSWE+wr5K0tQ5exoX5PwM080lKQFkbX5Uo3SJTUO1FHJEGgm1/qZ/9SCIVyKygc+79YZT0EWMrSZZzcVsS+52njCLz9K+qjjzEncv5a5854bd3APV0gP1XYbNu7qeHcceOFpb6BJc6Z10qB81nCdkQp8VLXOOpEiMtKz0eEi5/jdDCIuNloN4BKUhTm15ba/KDO8mioETylTzbpn3m7fjQTj66m52svWqyM1oAXont9rcKqN8KoNOCQP4PJlZwkFCWyTFchcs8zphkFDnAncgmxa2eUk6C1QQPibo0mhAF1dfiGdkzUI/gxemkPf9Q==

Trying to wrap my head around how exactly this subexpression works. From page 14 of the TLA+ 2 language guide we have:

We usually don’t need to name the entire _expression_ to the right of a == because the operator being defined names it. However, as observed in Section 2, this is not true for recursively defined operators. If Op is recursively defined by Op(p1, ..., pk) == exp then Op(P1, ..., Pk)!: names exp with Pi substituted for pi , for each i
in 1 . . k.

Perhaps this is just a case of TLC semantics not matching TLA+ semantics, but I can't seem to find the use of : when referring to a recursive operator like:

RECURSIVE Factorial(_)
Factorial(n) == IF n = 0 THEN 1 ELSE n * Factorial(n - 1)

If I plug in Factorial(3)!3 to the TLC constant _expression_ evaluator, it gives me 6 as you'd expect. If I plug in Factorial(3)!:!3, I get the error:

!: can be used only after a name and either at the end after an operator name or before an operator name.

So what sort of otherwise-inaccessible subexpressions can I address with the : symbol? Thanks!

Andrew

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