Maude-help mailing list

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

On Sunday 20 November 2005 18:27, Craig Ugoretz wrote:
> "constructs". Right now I am trying to understand how subsorts work, and to
> do this, I have been trying to develop an "integers greater than three"
> sort using the "mb" construct. I have tried many ideas, but have not found
> success. Subsorts seem to be a crucial concept to learn in order to program
> in Maude, so I would appreciate a small sample program to successfully
> demonstrate my first experiemental objective.

Membership axioms aren't guarenteed to work correctly with the number 
hierarchy because of the special internal representation for iterated towers 
of s_ symbols; Maude will print a advisory about this if you try it. Also 
membership axioms where the lhs is a bare variable apply everywhere, 
including places you didn't expect; conditional membership axioms with a bare 
variable lhs are usually nonterminating (which causes a stack overflow and is 
reported as a segmentation fault under most operating systems).

Even when they do work, membership axioms are inefficient, and so should only 
be used as a last resort. You don't really need them for you example - I 
would do it by giving  a sort structure below the standard one and 
redeclaring the constructors (only s_ in this case) on it.

fmod INT-GT-3 is
  inc INT .
  sorts One Two Three IntGt3 .
  subsorts One Two Three IntGt3 < NzNat .
  op s_ : Zero -> One [ctor ditto] .
  op s_ : One -> Two [ctor ditto] .
  op s_ : Two -> Three [ctor ditto] .
  op s_ : Three -> IntGt3 [ctor ditto] .
  op s_ : IntGt3 -> IntGt3 [ctor ditto] .
endfm

red -1 .
red 0 .
red 1 .
red 3 .
red 4 .
red 12345678901234567890 .

Steven