Maude-help mailing list

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

I notice in the OBJ manual using, subsorts  Int < List, they say  that
single integers such as 5 are valid lists. This could be logically
consistent if we consider 5 has a most specific type Int and most
general type List.


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


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