The reduce, match, trace, and show commands

Here we assemble the whole module for the NUMBERS running example to illustrate some of the basic commands for interacting with Maude. See Chapter 16 for full details about these and other Maude commands.

Notice that, since the result of the _in_ predicate is a Boolean value, we import the predefined module BOOL (see Section 7.1) by means of a protecting declaration (described in Section 6.1.1).

  fmod NUMBERS is
    protecting BOOL .

    sort Zero .
    sorts Nat NzNat .
    subsort Zero NzNat < Nat .
    op zero : -> Zero [ctor] .
    op s_ : Nat -> NzNat [ctor] .
    op sd : Nat Nat -> Nat .
    ops _+_ _*_ : Nat Nat -> Nat [assoc comm] .
    op _+_ : NzNat Nat -> NzNat [ditto] .
    op _*_ : NzNat NzNat -> NzNat [ditto] .
    op p : NzNat -> Nat .

    vars I N M : Nat .
    eq N + zero = N .
    eq N + s M = s (N + M) .
    eq sd(N, N) = zero .
    eq sd(N, zero) = N .
    eq sd(zero, N) = N .
    eq sd(s N, s M) = sd(N, M) .
    eq N * zero = zero .
    eq N * s M = (N * M) + N .
    eq p(s N) = N [label partial-predecessor] .

    eq (N + M) * I = (N * I) + (M * I)
      [nonexec metadata "distributive law"] .

    sort Nat3 .
    ops 0 1 2 : -> Nat3 [ctor] .
    op _+_ : Nat3 Nat3 -> Nat3 [comm] .
    vars N3 : Nat3 .
    eq N3 + 0 = N3  .
    eq 1 + 1 = 2 .
    eq 1 + 2 = 0 .
    eq 2 + 2 = 1 .

    sort NatSeq .
    subsort Nat < NatSeq .
    op nil : -> NatSeq .
    op __ : NatSeq NatSeq -> NatSeq [assoc id: nil] .

    sort NatSet .
    subsort Nat < NatSet .
    op empty : -> NatSet .
    op _;_ : NatSet NatSet -> NatSet [assoc comm id: empty] .
    eq N ; N = N [label natset-idem] .

    op _in_ : Nat NatSet -> Bool .
    var NS : NatSet .
    eq N in N ; NS = true .
    eq N in NS = false [owise] .
  endfm

First, we evaluate some expressions using the reduce command. Maude repeats the command filling in any omitted optional information. Then statistics about the execution are printed.^4.16Finally, the result is printed, prefaced by its least sort.

The first two examples evaluate the sum of three ones in Nat and in Nat3.

  Maude> red s zero + s zero + s zero .
  reduce in NUMBERS : s zero + s zero + s zero .
  rewrites: 4 in 0ms cpu (0ms real) (~ rews/sec)
  result NzNat: s s s zero

  Maude> red 1 + (1 + 1) .
  reduce in NUMBERS : 1 + (1 + 1) .
  rewrites: 2 in 0ms cpu (0ms real) (~ rews/sec)
  result Nat3: 0

The next example illustrates the effect of the idempotency equation for sets of natural numbers.

  Maude> red zero ; s zero ; zero ; s zero .
  reduce in NUMBERS : zero ; s zero ; zero ; s zero .
  rewrites: 2 in 0ms cpu (0ms real) (~ rews/sec)
  result NatSet: zero ; s zero

Finally we convince ourselves that the owise attribute works.

  Maude> red zero in s zero ; zero ; s s zero .
  reduce in NUMBERS : zero in s zero ; zero ; s s zero .
  rewrites: 1 in 0ms cpu (0ms real) (~ rews/sec)
  result Bool: true

  Maude> red zero in s zero ; s s zero .
  reduce in NUMBERS : zero in s zero ; s s zero .
  rewrites: 1 in 0ms cpu (0ms real) (~ rews/sec)
  result Bool: false

The commands xmatch and match operate in the same way, unless the subject term has an operator that needs extension on top, in which case it can match proper subterms in the same theory layer, as required for rewriting modulo that theory. The xmatch command was illustrated in Section 4.8. Here we compare match and xmatch on a pattern that splits a sequence of natural numbers into two parts. To be safe, we ask for at most five matches, but in fact there are only four.

  Maude> match [5] NS0:NatSeq NS1:NatSeq <=? zero zero zero .
  match [5] in NUMBERS : NS0:NatSeq NS1:NatSeq <=? zero zero zero .
  Decision time: 0ms cpu (0ms real)

  Solution 1
  NS0:NatSeq --> nil
  NS1:NatSeq --> zero zero zero

  Solution 2
  NS0:NatSeq --> zero
  NS1:NatSeq --> zero zero

  Solution 3
  NS0:NatSeq --> zero zero
  NS1:NatSeq --> zero

  Solution 4
  NS0:NatSeq --> zero zero zero
  NS1:NatSeq --> nil

Using the xmatch command for the same pattern and term, we see that in addition to the whole term matches, Maude also reports matches within the subterm zero zero. In fact, there are two occurrences of this subterm. We only show five of the matches.

  Maude> xmatch [5] NS0:NatSeq NS1:NatSeq <=? zero zero zero .
  xmatch [5] in NUMBERS : NS0:NatSeq NS1:NatSeq <=? zero zero zero .
  Decision time: 0ms cpu (7ms real)

  Solution 1
  Matched portion = zero zero
  NS0:NatSeq --> nil
  NS1:NatSeq --> zero zero

  Solution 2
  Matched portion = zero zero
  NS0:NatSeq --> zero
  NS1:NatSeq --> zero

  Solution 3
  Matched portion = zero zero
  NS0:NatSeq --> zero zero
  NS1:NatSeq --> nil

  Solution 4
  Matched portion = (whole)
  NS0:NatSeq --> nil
  NS1:NatSeq --> zero zero zero

  Solution 5
  Matched portion = (whole)
  NS0:NatSeq --> zero
  NS1:NatSeq --> zero zero

Let us consider now a small example using the trace command. We turn on selective tracing and choose to trace only uses of the equation labeled partial-predecessor.

  Maude> set trace on .
  Maude> set trace select on .
  Maude> trace select partial-predecessor .

  Maude> red s s p(s zero) + s p(s zero) .
  reduce in NUMBERS : s s p(s zero) + s p(s zero) .
  *********** equation
  eq p(s N) = N [label partial-predecessor] .
  N --> zero
  p(s zero)
  --->
  zero
  rewrites: 3 in 0ms cpu (0ms real) (~ rews/sec)
  result NzNat: s s s zero

Note that Maude only reports one use of this equation, despite the fact that there are two occurrences in the term. This is because, when performing equational simplification, occurrences of the same subterm are internally shared^4.17and hence there is only one occurrence of the subterm p(s zero) in the internal representation.

We can ask Maude to show the module FIBONACCI (assuming it has been loaded).

  Maude> show module FIBONACCI .
  fmod FIBONACCI is
    protecting NAT .
    op fibo : Nat -> Nat [memo] .
    var N : Nat .
    eq fibo(0) = 0 .
    eq fibo(1) = 1 .
    eq fibo(s s N) = fibo(N) + fibo(s N) .
  endfm

The show sorts command shows all the sorts declared and for each sort its sub- and super-sorts.

  Maude> show sorts NUMBERS .
  sort Bool .
  sort Zero . subsorts Zero < Nat NatSet NatSeq .
  sort Nat . subsorts NzNat Zero < Nat < NatSet NatSeq .
  sort NzNat . subsorts NzNat < Nat NatSet NatSeq .
  sort Nat3 .
  sort NatSeq . subsorts NzNat Zero Nat < NatSeq .
  sort NatSet . subsorts NzNat Zero Nat < NatSet .

The show components command shows the connected components (kinds) in the sort partial order.

  Maude> show components NUMBERS .
  [Bool]:
          1       Bool

  [NatSeq, NatSet]:
          1       NatSeq
          2       NatSet
          3       Nat
          4       Zero
          5       NzNat

  [Nat3] (error free):
          1       Nat3

Note that the name of the kind corresponding to the connected component containing the natural numbers contains the names of two sorts. These are the maximal sorts in the component. The (error free) comment about the sort Nat3 means that all terms of kind [Nat3] are in fact of sort Nat3.