One of the most interesting sections in
Specifying Systems is 6.4,
Functions versus Operators. I keep coming back to it. Here's a quote:
"The distinction between functions and operators seems to confuse some people. One reason is that, although this distinction exists in ordinary math, it usually goes unnoticed by mathematicians. If you ask a mathematician whether subset is a function, she's likely to say yes. But if you point out to her that subset can't be a function because its domain can't be a set, she will probably realize for the first time that mathematicians use operators like subset and \in without noticing that they form a class of objects different from functions. Logicians will observe that the distinction between operators and values, including functions, arises because TLA+ is a first-order logic rather than a higher-order logic."
Where can I find out more about this? Internet sources on functions vs operators are very muddled and seem to reflect unclear thinking (
example). Also, the last sentence in the above quote about the distinction not being present in higher-order logics - why is that? Thanks!
Andrew