[Haskell-cafe] towards a new foundation for set theory with atoms

[Greg Meredith]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20070810/1a3a4b7f/attachment.htm