Maude-help mailing list

[Francisco Duran <duran AT lcc.uma.es>]

Hi Matthias,

You are right, there is no much information on this in the manual, and 
additional examples would be very wellcome. I believe that error 
handling should be explained and illustrated somewhere.

Note however that in Section 3.5 we say

"For example, suppose we add a partial predecessor function to our
NUMBERS module,
  op p : NzNat -> Nat .
Then Maude will parse the term p(zero) and assign it the kind [Nat],
or equivalently [NatSeq] or also [Nat, NatSeq], since the sorts Nat and
NatSeq belong to the same connected component."

Which is exactly the same case.

Regarding a way of checking whether a program contains a term without a 
sort, the answer I'm afraid is no. But note that you may want to write 
equations on terms at the kind level for e.g. error recovery. Having 
such error terms doesn't necessarely mean an error in your spec.

Best regards,

Paco Durán


Matthias Radestock escribió:
> 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.