Maude-help mailing list

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

I was a bit too focused on a mathematical interpretation and missed the
programming perspective.

Thanks.
Pat


Steven Eker wrote:
> 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
>>


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