[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Functions and Operators


as Leslie implies, most working mathematicians apply the distinction intuitively, and it is only when you try to make things precise or look at foundations that you realize that you have to be careful in order to avoid the paradoxes of naive set theory. Also, the terminology is not universally accepted. Operators are often called "class functions" in standard expositions of formal set theory. Functions are objects that exist within the universe of set theory, i.e. they are themselves sets. In standard constructions of set theory they are sets of pairs (argument, result) – although TLA+ does not commit to any specific representation for functions but has dedicated syntax for functions. An operator such as \in is "too big" to be a set: its domain would have to include the collection of all sets, which is not a set itself.

A classic introduction to the subject is Halmos' "Naive Set Theory" (http://www.amazon.com/Naive-Set-Theory-Paul-Halmos/dp/1614271313); it is more accessible than real formal presentations such as those by Suppes (http://www.amazon.com/Axiomatic-Theory-Dover-Books-Mathematics/dp/0486616304) or Shoenfield's chapter in the Handbook of Mathematical Logic (http://www.amazon.com/Handbook-Mathematical-Studies-Foundations-Mathematics/dp/0444863885) that go into more detail on the axiomatic systems.

I find Paulson's Formath paper available at http://www.cl.cam.ac.uk/~lp15/papers/Formath/set-I.pdf a very well written, careful introduction: see e.g., the distinction between \lambda for defining operators and Lambda(_,_) for defining functions in section 2.2. However, it insists a lot on how things are encoded in the Isabelle logical framework and then describes techniques for automatic reasoning that are not relevant for understanding the basics, so your mileage may vary.

In higher-order logic (aka Church's Simple Theory of Types), there is not one universe of values, but the latter are classified by types, and in particular a function does not live in the same type as its arguments or results. In this way, the paradoxes of naive set theory are avoided, and operators are just (polymorphic) functions. For example, \in has type "'a set => bool", which can be read as saying that there is a collection of functions (one per type 'a) from sets over 'a to Booleans. Similarly, the SUBSET (powerset) operator of TLA+ has type "'a set => 'a set set".


On 21 Mar 2015, at 07:24, Andrew Helwer <andrew...@xxxxxxxxx> wrote:

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!