Maude-help mailing list

[Marko Schuetz-Schmuck <MarkoSchuetz AT web.de>]

Dear Steven,

thanks, that really helped.

I have now:
(fmod TICK{X :: TICK-SIZE} is
    protecting CONVERSION .
    sort Tick NzTick .
    subsort NzTick < NzNat .
    subsorts Zero NzTick < Tick .
    mb 99 : NzTick .
    var N : NzNat .
    cmb N : NzTick if N <= 99 .
    op toFloat : Tick -> Float .
    var T : Tick .
    eq toFloat(T) = float(T) * ticksize .
endfm)

There is still the warning concerning membership axioms and iterated
symbols, but apart from that it reduces as I expected.

Best regards,

Marko

Steven Eker 
<steveneker AT gmail.com>
 writes:

> 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
>>

Attachment: signature.asc
Description: PGP signature