Maudeの練習

test02.maude

***(
  > load test02.maude
)

fmod NAT is
  sorts Zero NzNat Nat .
  subsort Zero NzNat < Nat .

  op o   :         -> Zero  [ctor] .
  op s_  : Nat     -> NzNat [ctor] .
  op _+_ : Nat Nat -> Nat .
  op _-_ : Nat Nat -> Nat .

  vars N M : Nat .
  eq o   + M = M .
  eq s N + M = s (N + M) .

  eq o   - M   = o .
  eq s N - o   = s N .
  eq s N - s M = N - M .

endfm

mod MODULO is
  protecting NAT .

  vars N M : Nat .

  op _<=_ : Nat Nat   -> Bool .
  eq o   <= M   = true .
  eq s N <= o   = false .
  eq s N <= s M = N <= M .

  op _%_  : Nat NzNat -> Nat .
***  op ss   : NzNat       -> Nat [ctor] .
  crl [mod1] : N % M => (N - M) % M if      M <= N  .
  crl [mod2] : N % M => N           if not (M <= N) .
endm


***(
E:\me\Maude>maude
                     \||||||||||||||||||/
                   --- Welcome to Maude ---
                     /||||||||||||||||||\
           Maude 2.7.1 built: Mar 20 2017 11:23:54
            Copyright 1997-2016 SRI International
                   Sun Nov 17 14:46:26 2019
Maude> load test02.maude
Advisory: redefining module NAT.
Maude> reduce s s s s s o + s s s o .
reduce in MODULO : s s s s s o + s s s o .
rewrites: 6 in -21466385033510ms cpu (0ms real) (~ rewrites/second)
result NzNat: s s s s s s s s o
Maude> reduce s s s s s o - s s s o .
reduce in MODULO : s s s s s o - s s s o .
rewrites: 4 in -21466363560153ms cpu (0ms real) (~ rewrites/second)
result NzNat: s s o
Maude> reduce s s s s s o - s s s s s s s s o .
reduce in MODULO : s s s s s o - s s s s s s s s o .
rewrites: 6 in -21461025496153ms cpu (0ms real) (~ rewrites/second)
result Zero: o
★　0除算すると固まります。
★　NzNatにしているのに弾いてくれない...
Maude> rewrite s s s s s o % s s s o .
rewrite in MODULO : s s s s s o % s s s o .
rewrites: 15 in -21466957343666ms cpu (0ms real) (~ rewrites/second)
result NzNat: s s o
Maude> quit
Bye.
)