Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

There are a number of ways of defining sets in Maude. The common trick of 
putting Element < Set gives a convenient data structure for recursing over 
but 
identifies singleton sets with their elements, contrary to the standard 
notion 
of mathematical sets. This is the approach used by the Maude SET{} 
parameterized module.

You could have a strict separation between elements and sets, but then the 
singleton set becomes another basis case for programming.

You can also take the view that Set < Element which is somewhat closer in 
spirit to ZF set theory. This allows nesting of sets and is the approach 
taken 
in the alternative Set*{} parameterized module.

The syntactic subsort relation between sorts corresponds the subset relation 
on the carrier sets. In the first way of defining sets, there are no 
syntactic 
set braces, so the carrier for NatSet contains elements such as
 
empty
0
1
0, 1
2,
0, 2
1, 2
0, 1, 2
...

As pointed out above, these don't correspond to conventional mathematical 
sets 
in that there is no distinction between say 1 and the set containing 1.

Steven

On Saturday 24 July 2010 06:05:36 am Patrick Browne wrote:
> Hi,
> I am trying to understand the semantics of subsorts in Maude.
> In the literature I see sub-sort declarations of the type
> subsort Element < Collection
> 
> More specifically say we have:
> subsort Nat < NatSet .
> 
> Then the sorts and their instances could be described as follows:
> 1) The sort Nat can be interpreted as *the set* of natural numbers (i.e.
> {1,2,3..}).
> 2) Instances of sort Nat can be any natural number (i.e. 1, 2, 3..).
> 3) The sort NatSet represents the set of finite sets of natural numbers
> (e.g. {{1},{5,1,4}{3,1}} is this really a power set?).
> 4) Instances of sort NatSet are finite sets of natural numbers (e.g.
> {1},{5,1,4}{3,1}). I assume this does not include *the set* of natural
> numbers.
> 
> So typical elements of the carrier set of Nat are 1,2  as distinct from
> typical elements of the carrier set of NatSet  {1}, {1,2}. My
> interpretation of point 3) may be wrong. It could be interpreted as just
> finite sets (e.g. {1}, {1,2},{1,2,3}), not the *set of finite sets*. But
> we will leave that aside for the moment.
> 
> Is the  interpretation of < is based on a sub-set inclusion or a more
> general embedding?
> If we interpret < as sub-set inclusion  then I cannot make sense of  1
> isSubsetOf {1}.
> If we interpret < as an embedding  then there is a obvious mapping of
> elements to their singleton set 1 -> {1}. But I cannot make sense of
> general Nat elements in relation to general NatSet elements ??? ->
> {1,2,3,4}.  Perhaps I do not have a good understanding of embedding.
> 
> Any help would be appreciated.
> Apologies if I am missing something extremely simple and obvious.
> 
> Pat
> 
> 
> This message has been scanned for content and viruses by the DIT
>  Information Services E-Mail Scanning Service, and is believed to be clean.
>  http://www.dit.ie _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>