The ability of dealing with infinite objects is typical of lazy (functional) languages. Although the reductions in Maude are basically innermost (or eager), Maude is able to exhibit a similar behavior by using strategy annotations (see [Lucas03a]).

Maude strategy annotations are lists of non-negative integers associated to function symbols which specify the ordering in which the arguments are (eventually) evaluated in function calls: when considering a function call f(t₁,...,t_k), only the arguments whose indices are present as positive integers in the local strategy (i₁ ··· i_n) for f are evaluated (following the specified ordering). If 0 is found, a reduction step on the whole term f(t₁,...,t_k) is attempted. The introduction of "true" replacement restrictions (i.e., that forbid reductions on some arguments) is often sufficient to ensure (and even prove) a terminating behavior of a Maude program even though some expressions that denote an infinite object are involved (see [Lucas03b] for an overview of methods to formally prove termination in these cases).

Full Maude is a language extension of Maude written in Maude itself, that endows Maude with notation for object-oriented programming and with a powerful and extensible module algebra in which Maude modules can be combined together to build more complex modules [DM98,Duran99,CDELMMQ02]. Every Maude module can be loaded in Full Maude by just enclosing it into parentheses. Then, the usual evaluation commands of Maude (e.g., reduce, rewrite, etc.) are available in Full Maude by also enclosing them into parentheses.

As a first example, let us consider the following parameterized modules LAZY-LIST and LIST-OF-NATS. Module LAZY-LIST provides a "polymorphic" sort List(X), and symbols nil (the empty list) and _._ for the construction of polymorphic lists. And module LIST-OF-NATS provides a a function natsFrom, which is able to generate the infinite list of natural numbers.

   (fth TRIV is
     sort Elt .
    endfth)

   (fmod LAZY-LIST(X :: TRIV) is
     protecting INT .
     sort List(X) .
     subsort X@Elt < List(X) .
     op nil : -> List(X) [ctor] .
     op _._ : X@Elt List(X) -> List(X) [ctor strat (1 0)] .
     op take : Int List(X) -> List(X) .
     var N : Int .  var X : X@Elt .  var Z : List(X) .
     eq take(0, Z) = nil .
     eq take(N, X . Z) = X . take(N - 1, Z) .
    endfm)

   (view Nat from TRIV to NAT is
     sort Elt to Nat .
    endv)

    (fmod LIST-OF-NATS is
     protecting LAZY-LIST(Nat) .
     op natsFrom : Nat -> List(Nat) .
     var N : Nat .
     eq natsFrom(N) = N . natsFrom(N + 1) .
    endfm)

Note the strategy (1 0) associated to the constructor symbol _._, which forbids replacements on its second argument. Given a term of the form X . L, the strategy indicates that its first argument, the subterm X, will first be reduced, and then a reduction step on the whole term would be attempted. The LAZY-LIST module also includes a typical polymorphic operator take which selects the first n components of a list. Even though take has no explicit strategy annotation, Maude internally assigns a by default one (1 2 0). In fact, Maude gives a strategy annotation (1 2 ··· k 0) to each symbol f without an explicit strategy annotation.

Thanks to the strategy annotation (1 0) for the list constructor, after entering these modules into Full Maude, we can evaluate, e.g., the expression take(4, natsFrom(0)) without entering into a non-terminating computation.

    Maude> (red take(4, natsFrom(0)) .)
    reduce in LIST-OF-NATS : take(4, natsFrom(0))
    result List`(Nat`) :
      0 . take(4 - 1, natsFrom(0 + 1))

1. Performing a layered normalization: when the evaluation stops due to the replacement restrictions introduced by the strategy annotations, it is resumed over concrete inner parts of the resulting expression until the normal form is reached (if any) [Lucas02a,Lucas02b].
2. Transform the program to obtain a different one which is able to obtain sufficiently interesting outputs (e.g., constructor terms) [AEL02].
3. Use on-demand strategy annotations where the presence of negative indices allows for some extra evaluation [AEGL02].

In this piece of work, we introduce new commands to make normalization via layered normalization and program transformation available for the execution of Maude programs. Both commands are made available in Full Maude 2.0 as Core Maude 2.0 programs which extend some Full Maude modules. See [DEL04] for details. Note that on-demand strategy annotations has also been directly available in Maude at this other link.

We have implemented the normalization via layered evaluation procedure as a new command norm which uses the outcome of usual Maude command red to perform the layered evaluation of the initial expressions. The new command permits to obtain the intended value of the previous expression take(4, natsFrom(0)).

    Maude> (norm take(4, natsFrom(0)) .)
    reduce in LIST-OF-NATS :
      take(4, natsFrom(0))
    result List`(Int`) :
      0 . 1 . 2 . 3 . nil

And we have implemented the normalization via program transformation procedure as a new command eval which transforms the original program into another one where the command red is able to obtain the intended normal form associated to the term given to eval (see [AEL02] for further information).

  Maude> (eval take(4, natsFrom(0)) .)
  transforming module LIST-OF-NATS for symbol take
  transformed module QLIST-OF-NATS is complete for defined symbols: take

  reduce in QLIST-OF-NATS :
    unquote(quote(take(4, natsFrom(0))))
  result List`(Nat`) :
    0 . 1 . 2 . 3 . nil

First, download the Full Maude file full-maude.maude if it is not already present in the local installation of Maude.

Second, download the following Maude file with auxiliary functions utils.maude.

Third, download the appropriate Maude files:

1. Normalization by layered evaluation: Download the Maude file norm.maude and the UNIX shell command fmaude-norm in order to make available the command norm in Full Maude.
   
   
2. Normalization by program transformation: Download the Maude file eval.maude and the UNIX shell command fmaude-eval in order to make available the command eval in Full Maude.

To make both commands available at the same time, download the Maude file norm-eval.maude, the UNIX shell command fmaude-norm-eval norm-eval.maude and the two previous files norm.maude anD eval.maude.