Haskellians, i have a particular interest in FM-set theory in that it simplifies a host of otherwise non-trivial aspects of programming language semantics, especially, fresh names. You can provide semantics without sets with atoms, but the functor category machinery is more than a little on the heavy side. The down side of FM-set theory is that it posits an infinite collection of atomic entities -- atomic in the sense that they have no observable internal structure. This poses a real problem for computational accounts. No where do we have an infinite supply of atomic entities. All our infinite collections need some finite presentation -- some basic starting structure and then a finite set of rules that say how to generate the rest. This is particularly important since the atoms have to come with a equality predicate. If the predicate cannot inspect internal structure, then the equality predicate is too big to hold in any finitely presentable computation. Thus, there's a little conundrum: how do you get all the conveniences of a set theory with atoms and still have a finite presentation? Here's one approach. The issue is that atoms cannot have internal structure observable by the set-theoretic operators, \in : Set -> Atom + Set -> Bool, and { - } : [Atom + Set] -> Set. That doesn't mean they can't have structure. Where would this structure come from? Well, it's related to another observation about sets: they're really collections of pointers. More specifically, the axiom of extensionality says that two sets are equal iff they have exactly the same members. Thus, wherever we see the set { } it's the same. Therefore, in { { }, { { } } } we see the very same set occurring in two locations. This is not very physical. These notions of location or identity must be more logical notions. And, one obvious way to resolve this is that what's "inside" the braces are references or pointers. We can start to formalize this naively using a simple grammar-nee type formulation. Ordinary sets can be specified like this Set ::= { Set* } for some appropriately infinite version of Kleene-star. (Note, this grammar is really sugar for a domain equation.) Now, if we want sets over references, we could modify the grammar, like this RSet ::= { Ref* } Ref ::= `Set*' R-sets only contain references and references point to (collections of) sets. Then, you can add a dereference operation to you theory to get back the sets being referenced. But, while under the quotes, the internal structure is not observable by the element-of and brace operators. Thus, from the point of view of these operators, they look like atoms. Note that as written, the quotes are serving a role isomorphic to the role of the braces. They are essentially two different collection operators that have been intertwined in an alternating manner. This alternation is in perfect correspondence with games semantics. We interpret { as opponent question, } as opponent answer, ` as player question, ' as player answer. This means that winning strategies for opponent yield sets while winning strategies for player yield references. The observation leads to a further generalization. Nothing restricts us to two kinds of collection operators. We could posit n different "colored" braces and element-of operators, written {i - i}, \in_i, for color i. Then we have the following specification for these sets Set(i) ::= {i Set(0 <= j < n : j <> i)* i} i have coded up (in my pidgin Haskell) a version for 3 colors and then shown how to do the von Neumann encoding of the naturals in this setting. The code can be found here: http://svn.biosimilarity.com/src/open/mirrororrim/rsets/trunk/MPSet.hs Best wishes, --greg -- L.G. Meredith Managing Partner Biosimilarity LLC 505 N 72nd St Seattle, WA 98103 +1 206.650.3740 http://biosimilarity.blogspot.com