Maude-help mailing list

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

----------  Forwarded Message  ----------

Subject: Re: [[Maude-help] ] Existentials in Maude
Date: Monday, August 06, 2018, 12:30:40 PM
From: Steven Eker 
<eker AT csl.sri.com>
To: 
maude-help AT lists.cs.illinois.edu,
 
patrick.browne AT dit.ie
CC: 
maude-help AT lists.illinois.edu

So that's a question about semantics. The answer is on page 118 of the Maude 
Manual or page 200 of the Maude Book. When a module is imported into a theory 
using protecting or extending it retains it initial (i.e. tight) semantics.

Of course this is purely theoretical. In practice term rewriting is valid 
with 
both semantics. It is other proof techniques that the user might implement on 
top of Maude, most notably, structural induction, where this distinction 
matters.

Steven

On Monday, August 06, 2018 08:26:09 AM PATRICK BROWNE 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
-----------------------------------------