search

Apress / practical-tla-plus

Source Code for 'Practical TLA+' by Hillel Wayne
Other
287 stars 67 forks source link

Chapter 3 - page 54 #13

Closed heidihoward closed 3 years ago

heidihoward commented 3 years ago

The sentence "Functions ... have no restrictions on recursion" implied to me that operations could not be recursive. However, they can be and here is what SumUpTo(n) might look like as a recursive operator:

RECURSIVE SumUpTo(_)
SumUpTo(n) == IF n=0 THEN 0 ELSE n + SumUpTo(n-1)
heidihoward commented 3 years ago

This comes up again in PT: https://github.com/Apress/practical-tla-plus/blob/1afed6f8c95bf921adc948d23d4260d9cd300724/PT/PT.tla#L21

hwayne commented 3 years ago

TLA+ operators can be recursive or higher-order, but not both. This matters because PT!ReduceSet is higher-order, so needs to use a function in its implementation to get recursion.

hwayne commented 3 years ago

Clarified errata.