Maude-help mailing list

[Matthias Radestock <matthias AT sorted.org>]

Francisco,

thanks for your quick response.

Francisco Duran 
<duran AT lcc.uma.es>
 writes:

> Please, take a look to Section 2.5 on Kinds in the Maude Manual.

Section 3.5, actually. I had read that, but obviously not carefully
enough.

> Given your module, you have a single kind [Zero,3*Nat,Nat], which can
> be referred to as [Zero], [3*Nat], [Nat], ... they are all the same
> one.
>
> The idea is that if a term doesn't have a sort, then it is in the
> corresponding kind, that is, you can think of a kind as a sort at the
> top of the hierarchy containing all the error terms.
>
> The term s3 s Zero doesn't have a sort, it is an error term in the
> kind [Nat], or [3*Nat] if you wish to call it that way.

Understood. This is all reasonably clear from section 3.5, now that I've
re-read it.

Is there any way to get Maude to tell me, perhaps via some analysis
tools, when my program contains terms without a sort?

> The operator declaration
>    op s3_ : 3*Nat -> 3*Nat .
> is semantically interpreted as
>    op s3_ : [3*Nat] -> [3*Nat] .
>    mb s3 V:3*Nat : 3*Nat .

That certainly explains the results I was getting. However, I cannot
find this in the manual, except perhaps for the sentence "The Maude
system also lifts automatically to kinds all the operators involving
sorts of the corresponding connected components to form error
expressions.". Perhaps the above should be included as an example.

Regards,

Matthias.