Lambda the Ultimate

I'm assuming you mean finite sets, so the axiom of choice doesn't come into play.

Are you concerned that "iterating" over a set imposes an ordering (whether non-determinstic, determined by some "secret sauce" such as a hash index or an ordering function like Erlang imposes), etc?

Here's a way to soothe your mind. Map and filter can easily be viewed as parallel operators when going from set-to-set, with traversal order an unimportant implementation detail when implementing on machines incapable of processing every element in parallel.

With fold[l|r], it depends on the communativity and associativity of the operator in question. If the operator is both communative and associative, the results of the fold are order-independent. Otherwise, the results of the fold *are* order-dependent, and traversing a set with fold without specifying an ordering produces non-determinstic results. So indeed, you shouldn't do that. :)

Some languages, of course, feature sorted sets in which you can specify an ordering. Of course, if the order is partial, you may still have trouble.

Your sense that using a choice operator and something like sri are equivalent is basically correct -- the two are interderivable. However, sri-style operators are somewhat easier to use if you need to do automated reasoning. Here's why:

A finite set is isomorphic to a list type quotiented by the equivalence relation generated by the congruent closure of associativity and idempotence of cons. That is, you take the congruent closure of the following two equations:

   x :: y :: rest == y :: x :: rest
   x :: y :: rest == x :: rest       when x = y

This means that any function on lists is also uniquely determines a function on sets, if the function is invariant under modifying the list argument by associativity or idempotence. Now, it's easy an easy inductive argument to show that a fold function fold f initis invariant under this relation if the functional argument f is also associative and indempotent, since fold just replaces calls to cons with calls to f.

So the bulk of the proof burden lies in showing that f(x, f(x, a)) == f(x, a) and that f(x, f(y, a)) == f(y, f(x, a)). Note that the variables x and y are universally quantified here. This makes automatic or semi-automatic checking easier, because computers are generally quite bad at instantiating existentially quantified variables at types which have an interesting equality structure.

If you give a choice operator, it will have a signature and specification like:

   mem    : (elt * set) -> bool
   choose : set -> (elt * set) option 

   forall xs:set. 
      forall x: elt. not (mem(x, xs)) and choose(xs) == None 
      or
      exists x:elt, ys:set. choose(xs) == Some(x, ys) and 
                            not(mem(x, ys) and 
                            add(x, ys) == xs

Basically, the specification of choose is that either you get None when its argument is empty, or you get an arbitrary element of the argument and the set that's the result of taking that element out. Note that this specification has an existential quantifier in it. Automatically proving things about programs that use choose directly is harder, because the specification of choose choose existentially quantifies over its return value, and involves the membership function to boot.

Now, observe that you can define sri in terms of choose, and vice-versa.

  let rec sri f e set = 
    match choose set with
    | None -> e
    | Some(x, xs) -> f(x, sri f e xs)

   let choose set = 
     sri (fun x acc ->
            match acc with
            | None          -> Some(x, Set.emptyset)
            | Some(y, rest) -> Some(y, Set.add(x, rest)))
         None
         set

For a set API in a general purpose language, you probably want to expose choose. However, if what you're interested in is in letting programmers define some new group functions in a database query language, you may prefer to use sri in order to simplify checking that what they've defined actually is a good group function.