Hacker News Reader

Comment by karpierz | Hacker News Reader

Let's see if I can clear this up:

An equivalent way to phrase the Axiom of Choice is: there exists a function that takes in any non-empty set, and returns an element of that set.

IE, this exists: choose a :: NonEmptySet a -> a

That's it. All of this stuff about "take a choice from a countable number (IE, list) of sets" is fluff; once you have choose, you can make a function that takes in an Iterator (NonEmptySet a) and produces (NonEmptySet a), such that the output will contain every element.

oneFromEachSet :: Iterator (NonEmptySet a) -> NonEmptySet a

oneFromEachSet iter = NonEmptySet (choose (first iter)) <> (oneFromEachSet (rest iter))

Where '<>' is set union.

Does that fix your issue with an "infinite" number of choices? Or do you take issue with assuming 'choose' exists, now that it's a single function?

View on HN

From a programmatic viewpoint that would be describing the axiom of countable choice, since such recursion can only occur countably infinite number of times.

Even if we ignore that by allowing for syntax where we fanout uncountably many times with each recursion, the construction as shown requires the collection of sets to be orderable, to be able to do have a "first", unless we are implementing first in terms of choose itself. (Alternatively one could also argue in terms of Axiom of Choice implying the well-ordering theorem, allowing up to pick a minimum via some such ordering (although you may need to use the choice function to pick one such ordering), but this won't fully help here anyway).

But even if you do that (implement iterator's first in terms of choose) it is not immediately obvious that you really have covered everything some full statements of the axiom of choice does. The axiom of choice is generally phased in terms of collections or families of sets, not sets of sets, but obviously the choose function takes in a set, not a more general family or collection.

It is easy enough to dismiss away certainly non-set collections of sets, like multisets of sets, since "choose" being a function will return the same value every time from a repeated input, and in the above formulation we are returning a set of results, so such duplicates won't matter. We could even handwave away a version where we return a multiset without too much trouble.

But the more expansive versions of the axiom of choice allow us to do something like "choose one element from each set in the class of non-empty sets." This is a real problem, as the "class of non-empty sets" is pretty well known to not be a set, and thus trying to implement iterator first in terms of it would not even be possible for that scenario.

"First" in this case was just getting the first element of the iterator, it wasn't related to choosing a value from the set.

The Axiom of Choice is equivalent to the following:

1) "For any set A, there exists a function from non-empty elements of the power set of A to elements of A."

Which is equivalent to:

2) "There exists a function that takes a non-empty set as input, and returns an element of that set"

2 -> 1, since we can take the function 2 defines, and use it to define the function from 1.

1 -> 2 since we can define 2 as such:

For a set A, take the power set of A. Then take the function that 1 claims exists. Use that function to get an element of A, since A is an element of its power set.

But back to your core point:

But I agree that Iterator is a bad fit for the axiom of choice, since we have an (uncountable) number of sets to pick from.

Here's a way to phrase it programmatically that allows for uncountable sets-of-sets:

The axiom of choice claims that given a set of non-empty sets, you can construct a new set which contains an element from each of the sets.

pickOneFromEach :: Set (NonEmptySet a) -> NonEmptySet a

If you have a function:

choose :: NonEmptySet a -> a

And a function:

map :: (a -> b) -> Set a -> Set b

then you can define pickOneFromEach as follows:

pickOneFromEach setOfSets = map choose setOfSets

Reply on news.ycombinator.com