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.