Functions and Operators

[Andrew Helwer]

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

[Stephan Merz]

Hello,

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

Regards,

Stephan

[Stephan Merz]

> For example, \in has type "'a set => bool"

That should (of course) have been "'a => ('a set => bool)". Incidentally, you can define "'a set" simply as an abbreviation for "'a => bool" in HOL, identifying sets and their characteristic predicate (and \in is just [reverse] function application). Then, you can define the set of all values of type 'a as

UNIV :: "'a set" == \lambda x::'a. true

Note that there is a separate such set for every type, in particular

(UNIV :: "'a set") and (UNIV :: "'a set set")

are different for any type 'a, and this helps avoiding paradoxes.

Stephan

[Andrew Helwer]

Thanks for the book recommendations! The Handbook of Mathematical Logic is peculiarly expensive, but it looks like the University of Washington Library has a copy. I'll check out the Halmos text first.

[Leslie Lamport]

Unless you are interested in linguistics, I think it's a waste of time
to worry about this.  I expect that everyone has her own idea of what
the two words mean--an idea that usually approximates some dictionary
definition.  My own observation is that 40-50 years ago, most
mathematicians used the words more or less interchangeably most of the
time.  However, when they were trying to be very rigorous (generally
in teaching introductory courses), they defined a function to be a set
of ordered pairs.