Maude-help mailing list

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

The semantics of module importation/composition/parametrization/instantiation 
are subtle. There are formal semantics but you would need to ask Jose or 
Narciso where they are published. I'm guessing the relevant papers are >20 
years old and couched in Category Theory.

Steven

On Tuesday, August 07, 2018 12:04:01 AM PATRICK BROWNE wrote:
>  Thanks, that clarifies the position.
> 
> I see that a theory cannot be imported into a module. Theories can only be
> used as parameters of modules. So the code below is not legal Maude.
> What is the rational here?  Are there any references the cover the
> importation of theories into modules?
> 
> Pat
> 
> fth COUNTRY is
>   sort Country .
>   op EnglishSpeakingCountry : -> Country .
> endfth
> 
> fmod  PLANETS is
> including COUNTRY .
> sort Planet .
>   op Earth : -> Planet .
>   op onEarth : Country Planet -> Bool .
>   eq onEarth(EnglishSpeakingCountry,Earth) = true .
> endfm
> 
> On 6 August 2018 at 08:26, PATRICK BROWNE 
> <patrick.browne AT dit.ie>
>  wrote:
> > I am trying represent the fact that exactly one named object exists
> > (uniqueness quantifier) and some object exists (existential quantifier).
> > To do this, I am using constants within Maude's function modules (tight
> > denotation) and theories (loose denotation).
> > Does the Maude code below capture the meaning of the following senetences?
> > 
> > There is one and only one Earth. On Earth there exists at least one
> > country where people speak English.
> > 
> > fmod  PLANETS is
> > *** Uniqueness quantifier, there is one and only one Earth
> > sort Planet .
> > 
> >   op Earth : -> Planet .
> > 
> > endfm
> > 
> > fth COUNTRY is
> > 
> >   pr PLANETS .
> >   sort Country .
> >   ***  Existential quantifier, there is at least one English speaking
> > 
> > country
> > 
> >   op EnglishSpeakingCountry : -> Country .
> >   op onEarth : Country Planet -> Bool .
> >   eq onEarth(EnglishSpeakingCountry,Earth) = true .
> > 
> > endfth
> > 
> > 
> > Thanks,
> > Pat