Maude-help mailing list

[Matthias Radestock <matthias AT sorted.org>]

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.