From oleg-at-okmij.org Thu Dec 23 21:54:56 2004 Subject: The Axiom of Choice Message-ID: <20041224055456.52EA2A975@Adric.metnet.navy.mil> Date: Thu, 23 Dec 2004 21:54:56 -0800 (PST) Status: RO I was reading yesterday a wonderfully written Interlude in the book "Alfred Tarski, Life and Logic" (Anita Burdman Feferman, Solomon Feferman). I think I have finally understood the Axiom of Choice. It is a black-box API for a set. Suppose we have a set S -- and we know it is definitely a set, rather than a large class. The typical set API includes a membership predicate. Some say that the membership predicate is the whole representation of a set (if the domain of that predicate is a set as well). But that representation is wanting: all it gives us is the ability to test if a particular element of the domain is in our set, or not. We can't even find any element of our set, unless we correctly `guess' it. We can't even tell, in general, if our set is empty (if the membership predicate is `const False' and the domain is infinite, we will never find out for sure that our set is truly empty). One approach to that dilemma is white-box. We should be able to see how our set S has been constructed, via primitive operations (union, product, sum, selection, powerset) applied to the empty set or to the set of all natural numbers. We can then find an element of our set, or determine if the set is empty. Another approach is black-box. We can't see how our set is constructed. However, we are given a method that returns an element of the set. So, the Axiom of Choice is the extension of the set API with an extra function: Set e -> Maybe e. The Axiom of Choice lets us deal with sets extensionally. In that sense, the Axiom of Choice is quite natural (I never had any problem with it). In Datalog terms: a set Foo is represented by an unary predicate foo(X). Without the axiom of choice, this predicate is assumed unsafe -- that is, X must be fully instantiated by the time the predicate is called. So, we must use foo/1 only in the context domain(X), foo(X) where domain/1 enumerates the domain, e.g. domain(zero). domain(succ(N)) :- domain(N). The axiom of choice lets us assume that the predicate foo/1 is safe, so foo(X) can be used in any mode, whether X is bound or not. Come to think of it, the `msplit'* contraption can also be considered the manifestation of the Axiom of Choice. [*] Backtracking, Interleaving, and Terminating Monad Transformers (Functional Pearl), with Chung-chieh Shan, Daniel P. Friedman and Amr Sabry. ICFP'05. Addendum. Recently Neelakantan Krishnaswami in a message ``Re: FP-style map over set'' posted on a newsgroup comp.lang.functional on Mon, 28 Nov 2005 23:45:27 +0000 (UTC) introduced a choose function as an indispensable part of a set API. The function enables equational, algebraic reasoning about sets. The following is an extended excerpt from his message
So, the difference between a list and a finite set is that a list is a free algebra, and sets aren't. You can construct a list of elements of type t using the following signature: nil : set add : t * set -> set There are no equations between the lists you build up using nil and add, aside from reflexivity. A finite set is also generated by these two function symbols, but it satisfies the two additional equations forall x, y, rest. add x (add y rest) == (add y (add x rest)) and forall x, rest. add x (add x rest) == add x rest The first equation says that changing the order of insertion doesn't change the value, and the second says that adding the same element multiple times won't change the value. (The second equation is why sets require equality.) Assuming that you have a function choose : set -> (t * set) option which satisfies the equations choose nil == None and forall x, rest. there exist x', rest'. (add x rest) == (add x' rest') and (x' not in rest') and choose (add x rest) == Some(x', rest') then you can define a perfectly good map function in the obvious way: fun map f list = case choose list of None => nil | Some(x', rest') => add x' (map f rest') Now, you can show the correctness of map with a simple inductive argument based on the number of distinct elements of a finite set. There are other ways of specifying sets algebraically, but this works fine -- you can define map, union, and so on, and relatively easily prove that they have the desired properties. ... Here, we very carefully DON'T say that choose (add x rest) == Some(x, rest) Instead, we use an existential quantifier to say that choose returns some distinct element of the set, not necessarily the "most recently inserted" one. Indeed, upon reflection it should be clear that because of the property that the order of insertion doesn't matter, we /can't/ promise any such behavior.