[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[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:
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!
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/2a659530-59ad-4451-bb20-c2bde444083en%40googlegroups.com.