Maude-help mailing list

[Steven Eker <steveneker AT gmail.com>]

Hi Marko,

There's a couple of problems with your example:

(1) Membership axioms only move a term to a lower sort. Here 0
has sort Zero and 10 has sort NzNat and Tick is not below either
of them.

(2) Even if you fixed this issue, your membership axiom
  cmb N : Tick if N < 100 .
has a bare variable as its pattern, which trivially leads to
nontermination, because the sort of N has to be computed before
matching a pattern for N < 100

Membership axioms are nice theoretically but are tricky to
use and don't have an efficient implementation. Also they
don't play nice with associativity because of extension issues.
In general, I recommend avoiding them unless you really know
what you are doing.

Steven

On Thu, Jun 24, 2021 at 10:18 AM Marko Schuetz-Schmuck <MarkoSchuetz AT web.de> wrote:

Dear All,

if I define

(fth TICK-SIZE is protecting FLOAT . op ticksize : -> Float . endfth)
(fmod X-AXIS-TICK-SIZE is protecting FLOAT . op ticksize : -> Float . eq ticksize = 0.01 . endfm)
(view X-AXIS-TICK-SIZE from TICK-SIZE to X-AXIS-TICK-SIZE is op ticksize to ticksize . endv)
(fmod TICK{X :: TICK-SIZE} is
    protecting CONVERSION .
    op toFloat : Nat -> Float .
    var T : Nat .
    eq toFloat(T) = float(T) * ticksize .
endfm)

then I can

Maude> (red in TICK{X-AXIS-TICK-SIZE} : toFloat(10) .)
reduce in TICK{X-AXIS-TICK-SIZE}:
  toFloat(10)
result FiniteFloat :
  1.0000000000000001e-1

But maybe I want to constrain the ticks, say to less than 100:

(fmod TICK{X :: TICK-SIZE} is
    protecting CONVERSION .
    sort Tick .
    subsort Tick < Nat .
    var N : Nat .
    cmb N : Tick if N < 100 .
    op toFloat : Tick -> Float .
    var T : Tick .
    eq toFloat(T) = float(T) * ticksize .
endfm)

then I get

Maude> (red in TICK{X-AXIS-TICK-SIZE} : toFloat(10) .)
<warnings removed>
reduce in TICK{X-AXIS-TICK-SIZE}:
  toFloat(10)
result [Float] :
  toFloat(10)

I do not see why the reduction stops there and why

(red in TICK{X-AXIS-TICK-SIZE} : 0 :: Tick .)

is false. Is this related to the warnings about membership axioms in the
presence of associative and/or iterated symbols with declarations not at
the kind level?

Best regards,

Marko
--
Prof. Dr. Marko Schütz-Schmuck
Department of Computer Science and Engineering
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681