Maude-help mailing list

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

Hi,

There are a couple of problems with your spec. Firstly it is
nonterminating since your cmb introduces the constant 0 in its
condition which matches the lhs of the cmb. Secondly, a membership
axiom cannot be used to move a term between incomparable sorts
such as NzMachineInt and MachineNat. One way of doing what you want is
to introduce the intersection of NzMachineInt and MachineNat, and make
sure the cmb does match 0. You then also need an mb to bring 0 into
MachineNat, so you end up with this:

fmod MACHINE-NAT is
  protecting MACHINE-INT .
  sorts NzMachineNat MachineNat .
  subsorts NzMachineNat < MachineNat NzMachineInt < MachineInt .

  mb 0 : MachineNat .
  var N : NzMachineInt .
  cmb N : NzMachineNat if N >= 0 .
endfm

red 0 >= 0 .
red 0 .
red -1 .
red 1 .

BTW the Maude 1 system is essentially dead code - we haven't
maintained it about 3 years. If you would like to be an alpha tester
for Maude 2, let me know and I will send you the details of how to
access it. Maude 2 replaces MACHINE-INT with a proper algebraically
defined number hierarchy starting from 0 and sucessor and building up
to the rationals. It also has strings, floats and an LTL model checker
as built-ins.

Steven


On Tuesday 27 May 2003 05:52 am, Geert Janssen wrote:
> Dear Maude help mailing list,
>
> I wondered whether it is possible to "subsort" the MachineInts.
> I wanted to have a sort MachineNat that represents the natural numbers.
> However, I tried using conditional membership statements to no avail.
> What I did was this (in Core Maude):
>
>     fmod MACHINE-NAT is
>       protecting MACHINE-INT .
>       sort MachineNat .
>       subsort MachineNat < MachineInt .
>
>       var N : MachineInt .
>       cmb N : MachineNat if N >= 0 .
>     endfm
>
> Try reducing "0 >= 0" in this module ...
> Anyway I am hoping that a guru can help me out here.
> I have the feeling that it is simply impossible.
>
> Geert Janssen
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/mailman/listinfo/maude-help