Maude-help mailing list

[Patrick Browne <patrick.browne AT dit.ie>]

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