Handling infinite objects is a typical feature of lazy (functional) languages. Although reductions in Maude are basically innermost (or eager), Maude is able to exhibit a similar behavior by using strategy annotations. 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. In fact, Maude gives a strategy annotation (1 2 ··· k 0) to each symbol f without an explicit strategy annotation.

Consider the following modules LAZY-NAT and LIST-NAT defining sorts Nat and LNat, and symbols 0 and s for defining natural numbers, and symbols nil (the empty list) and _._ for the construction of lists.

  fmod LAZY-NAT is
    sort Nat .
    op 0 : -> Nat .
    op s : Nat -> Nat [strat (0)] .
    op _+_ : Nat Nat -> Nat .
    vars M N : Nat .
    eq 0 + N = N .
    eq s(M) + N = s(M + N) .
  endfm

  fmod LIST-NAT is
    pr LAZY-NAT .
    sorts LNat .
    subsort Nat < LNat .
    op _._ : Nat LNat -> LNat [strat (1 0)] .
    op nil : -> LNat .
    op nats : -> LNat .
    op incr : LNat -> LNat .
    op length : LNat -> Nat .
    vars X Y : Nat .
    vars XS YS : LNat .
    eq incr(X . XS) = s(X) . incr(XS) .
    eq nats = 0 . incr(nats) .
    eq length(nil) = 0 .
    eq length(X . XS) = s(length(XS)) .
  endfm

Nevertheless, the absence of some indices in the local strategies can also jeopardize the ability of such strategies to compute normal forms. For instance, the evaluation of the expression s(0) + s(0) using the Maude 2.0 [CDELMMT03] yields the following:

  Maude> (red s(0) + s(0) .)
  result Nat: s(0 + s(0))

Due to the annotation (0) for the symbol s, the contraction of the redex 0 + s(0) is not possible and the evaluation stops here.

The handicaps, regarding correctness and completeness of computations, of using (only) positive annotations are discussed in, e.g., [AEGL02,WRLA02,Lucas01, NO01,OF00], and a number of solutions have been proposed:

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) [WRLA02].
3. Use on-demand strategy annotations where the presence of negative indices allows for some extra evaluation [AEGL02,NO01,OF00].

In [DEL04], we have introduced two new commands (norm and eval) to make techniques 1 and 2 available for the execution of Maude programs, follow this link for the implementation of both commands. In this piece of work we show how to bring on-demand strategies into Maude. Before entering into details, we show how negative indices can improve Maude strategy annotations.

The following NATS-TO-BIN module uses previous modules LAZY-NAT and LIST-NAT and implements the binary encoding of natural numbers as lists of 0 and 1 (starting from the least significative bit).

  fmod NATS-TO-BIN is
    ex LAZY-NAT .
    pr LIST-NAT .
    op 1 : -> Nat .
    op natToBin : Nat -> LNat .
    op natToBin2 : Nat Nat -> LNat .
    vars M N X : Nat .
    vars XS YS : LNat .
    eq natToBin2(0, 0) = 0 .
    eq natToBin2(0, M) = 0 . natToBin(M) .
    eq natToBin2(s(0), 0) = 1 .
    eq natToBin2(s(0), M) = 1 . natToBin(M) .
    eq natToBin2(s(s(N)), M) = natToBin2(N, s(M)) .
    eq natToBin(N) = natToBin2(N, 0) .
  endfm

The evaluation of the expression natToBin(s(0) + s(0)) should yield the binary representation of 2. However, we get:

  Maude> (red natToBin(s(0) + s(0)) .)
  result LNat: natToBin2(s(0 + s(0)), 0)

The problem is that the current strategy annotations disallow the evaluation of subexpression 0 + s(0) in natToBin2(s(0 + s(0)), 0), thus disabling the application of the last equation for natToBin2. The use of the command norm introduced in [DEL04] does not solve this problem, since it just normalizes non-reduced subexpressions:

  Maude> (norm natToBin(s(0) + s(0)) .)
  result LNat: natToBin2(s(s(0)), 0)

On-demand strategy annotations can solve this problem. In fact, the use of the strategy (-1 0) for symbol s, declaring its first argument as evaluable only on-demand, permits to recover the desired behavior while keeps termination of the program. The on-demand evaluation obtains a head-normal form:

  Maude> (red natToBin(s(0) + s(0)) .)
  result LNat : 0 . natToBin(s(0))

  Maude> (norm natToBin(s(0) + s(0)) .)
  result LNat : 0 . 1

First, the original Full Maude file full-maude.maude contains a small bug that avoids proper execution of local strategies with negative annotations. Thus, the fixed Full Maude file full-maude-fixOct102004.maude should be downloaded and included in the distribution directory or in the local directory with the Maude file redOnDemand.maude (shown below).

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

Third, download the appropriate Maude files:

1. On-demand evaluation (command red): Download the Maude file redOnDemand.maude and the UNIX shell file fmaude-redOnDemand in order to make available on-demand reduction in Full Maude. Note that the previous fixed Full Maude version full-maude-fixOct102004.maude will be loaded.
   
   
2. Normalization by layered evaluation: Download the Maude file normOnDemand.maude and the UNIX shell file fmaude-normOnDemand in order to make available on-demand reduction and on-demand normalization in Full Maude. Note that the previous on-demand red command redOnDemand.maude will be loaded.