Haskellians, 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.
Best wishes, --greg On 8/10/07, Greg Meredith <[EMAIL PROTECTED]> wrote: > > 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 -- L.G. Meredith Managing Partner Biosimilarity LLC 505 N 72nd St Seattle, WA 98103 +1 206.650.3740 http://biosimilarity.blogspot.com
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe