Haskellians,<br><br>A quick follow up. If you look at the code that i have written there is a great deal of repeated structure. Each of these different kinds of sets and atoms are isomorphic copies of each other. Because, however, of the alternation discipline, i could see no way to abstract the structure and simplify the code. Perhaps someone better versed in the Haskellian mysteries could enlighten me.
<br><br>Best wishes,<br><br>--greg<br><br><div><span class="gmail_quote">On 8/10/07, <b class="gmail_sendername">Greg Meredith</b> <<a href="mailto:lgreg.meredith@biosimilarity.com">lgreg.meredith@biosimilarity.com</a>
> wrote:</span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Haskellians,<br><br>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?
<br><br>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
<br><br>Set ::= { Set* }<br><br>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
<br><br>RSet ::= { Ref* }<br>Ref ::= `Set*'<br><br>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.
<br><br>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
<br><br>Set(i) ::= {i Set(0 <= j < n : j <> i)* i}<br><br>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:
<a href="http://svn.biosimilarity.com/src/open/mirrororrim/rsets/trunk/MPSet.hs" target="_blank" onclick="return top.js.OpenExtLink(window,event,this)">http://svn.biosimilarity.com/src/open/mirrororrim/rsets/trunk/MPSet.hs
</a><br><br>Best wishes,<br><br>--greg<br clear="all"><br>-- <br>L.G. Meredith
<br>Managing Partner<br>Biosimilarity LLC<br>505 N 72nd St<br>Seattle, WA 98103<br><br>+1 206.650.3740<br><br><a href="http://biosimilarity.blogspot.com" target="_blank" onclick="return top.js.OpenExtLink(window,event,this)">
http://biosimilarity.blogspot.com</a>
</blockquote></div><br><br clear="all"><br>-- <br>L.G. Meredith<br>Managing Partner<br>Biosimilarity LLC<br>505 N 72nd St<br>Seattle, WA 98103<br><br>+1 206.650.3740<br><br><a href="http://biosimilarity.blogspot.com">http://biosimilarity.blogspot.com
</a>