metaNormalize

The (partial) operation metaNormalize takes as arguments the metarepresentation of a module $\mathcal{R}$ and the metarepresentation of a term $t$.

  op metaNormalize : Module Term ~> ResultPair [special (...)] .

When $t$ is a term in $\mathcal{R}$, $\texttt{metaNormalize(}\overline{\mathcal{R}}\texttt{,}\overline{t}\texttt{)}$ returns the metarepresentation of the normal form of $t$ with respect to the equational theory consisting of the equational attributes of the operators in $t$, without doing any simplification or rewriting with respect to equations or rules in $\mathcal{R}$, together with the metarepresentation of its corresponding sort or kind. For example, from the declarations in the predefined NAT module

  op s_ : Nat -> NzNat  [ctor iter  special (...)] .
  op _+_ : NzNat Nat -> NzNat [assoc comm prec 33 special (...)] .
  op _+_ : Nat Nat -> Nat [ditto] .

we know that the successor operator satisfies the iter theory (see Section 4.4.2) and that the addition operator is associative and commutative (see Section 4.4.1). With this information it is easy to make sense of the following results:

  Maude> red in META-LEVEL : 
           metaNormalize(upModule('NAT, false), 's_['s_['0.Zero]]) .
  result ResultPair: {'s_^2['0.Zero],'NzNat}

  Maude> red in META-LEVEL : 
           metaNormalize(upModule('NAT, false), 
             '_+_['s_['s_['0.Zero]],'0.Zero]) .
  result ResultPair: {'_+_['0.Zero,'s_^2['0.Zero]],'NzNat}

  Maude> red in META-LEVEL : 
           metaNormalize(upModule('NAT, false),
             '_+_['0.Zero,'_+_['s_['s_['0.Zero]],'0.Zero]]) .
  result ResultPair: {'_+_['0.Zero,'0.Zero,'s_^2['0.Zero]],'NzNat}

Notice that associative terms are flattened and, if they are also commutative, the subterms are sorted with respect to an internal order. Notice also that in the last two examples the subterm '0.Zero does not disappear. This is because 0 is not declared as an identity element for _+_.