[Maude-help] Integers greater than three sort (need help ...)
eker at csl.sri.com
Mon Nov 21 13:28:14 CST 2005
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] .
red -1 .
red 0 .
red 1 .
red 3 .
red 4 .
red 12345678901234567890 .
More information about the Maude-help