Maude-help mailing list

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

Hi Matthias,

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

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.

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 is, a term of the form s3 T has sort 3*Nat if T has sort 3*Nat; 
otherwise it is in the kind [3*Nat].

Best regards,

Paco Durán



Matthias Radestock escribió:
> I am trying to get a better understanding of the static checks Maude
> performs. In the process I stumbled across some unexpected behaviour,
> illustrated by the following example:
>
> fmod 3*NAT is
>     sort Zero Nat .
>     subsort Zero < Nat .
>     op zero : -> Zero [ctor] .
>     op s_ : Nat -> Nat [ctor] .
>     sort 3*Nat .
>     subsorts Zero < 3*Nat < Nat .
>     var M3 : 3*Nat .
>     mb (s s s M3) : 3*Nat .
>     op s3 _ : 3*Nat -> 3*Nat .
>     eq s3 M3 = s s s M3 .
> endfm
>
> This module definition is taken from the manual, with an added operation
> s3 that is defined for 3*Nats only. Running some tests, I get:
>
> Maude> red s3 zero .
> reduce in 3*NAT : s3 zero .
> rewrites: 2
> result 3*Nat: s s s zero
> Maude> red s3 s zero .
> reduce in 3*NAT : s3 s zero .
> rewrites: 0
> result [Nat]: s3 s zero
>
> The first result is expected. The second isn't. Since s3 is only defined
> on 3*Nat and I apply it to a term that isn't in 3*Nat, shouldn't I be
> getting an error? I am also puzzled by the result type - shouldn't it be
> [3*Nat]?
>
>
> Regards,
>
>
> Matthias.
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help