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

[Greg Meredith]

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 <lgreg.meredith at biosimilarity.com> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20070810/8e42d658/attachment-0001.htm