Memo

If an operator is given the memo attribute, this instructs Maude to memoize the results of equational simplification (that is, the canonical forms) for those subterms having that operator at the top. This means that when the canonical form of a subterm having that operator at the top is obtained, an entry associating to that subterm its canonical form is stored in the memoization table for this operator. Whenever the Maude interpreter encounters a subterm whose top operator has the memo attribute, it looks to see if its canonical form is already stored. If so, that result is used; otherwise, equational simplification proceeds according to the operator's strategy. Giving to some operators the memo attribute allows trading off space for time in equational simplifications: more space is needed, but if subcomputations involving memoized operators have to be repeated many times, then a computation may be substantially sped up, provided that the machine's main memory limits are not exceeded.

An operator's memo attribute and its user's specified or default evaluation strategy (see Section 4.4.7) may interact with each other, impacting the size of the memoization table. The issue is how many entries for different subterms, all having the same canonical form, may be possibly stored in the memoization table. If the operator has the default, bottom-up strategy, the answer is: only one such entry is possible. For other strategies, different terms having the same canonical form may be stored, making the memoization table bigger. For example, using the default strategy (1 2 0) for a memoized operator f, only subterms of the form f(v, v') with v and v' fully reduced to canonical form (up to the strategies given for all operators) will be mapped to their corresponding canonical forms. This is because, with the default strategy, equational simplification at the top of f can only happen after all its arguments are in canonical form. For other operator strategies this uniqueness may be lost, even when evaluating just one subterm involving f. For example, if f's strategy is (0 1 2 0), then both the starting term f(t, t') and the term f(v, v') (where v and v' are, respectively, the canonical forms of t and t') will be mapped to the final result, since the strategy specifies rewriting at the top twice. That is, each time the operator's strategy calls for rewriting at the top, Maude will add the current version of the term to the set of terms that will be mapped to the final result. Furthermore, other terms of the form f(u, u'), with u and u' having also v and v' as their canonical forms may appear in other subcomputations, and will then also be stored in the memoization table.

In general, whenever an application will perform an operation many times, it may be useful to give that operator the memo attribute. This may be due to the high frequency with which the operator is called by other operators in a given application, or to the highly recursive nature of the equations defining that operator. For example, the recursive definition of the Fibonacci function is given as follows, where NAT denotes the predefined module of natural numbers and arithmetic operations on them (as described in Section 7.2), which is imported by means of a protecting declaration (see Section 6.1.1).

  fmod FIBONACCI is
    protecting NAT .
    op fibo : Nat -> Nat .

    var N : Nat .
    eq fibo(0) = 0 .
    eq fibo(1) = 1 .
    eq fibo(s s N) = fibo(N) + fibo(s N) .
  endfm

Due to the highly recursive nature of this definition of fibo, the evaluation of an expression like fibo(50) will compute many calls to the same instances of the function again and again, and will expand the original term into a whole binary tree of additions before collapsing it to a number. The exponential number of repeated function calls makes the evaluation of fibo with the above equations very inefficient, requiring over 61 billion rewrite steps for fibo(50):

  Maude> red fibo(50) .
  reduce in FIBONACCI : fibo(50) .
  rewrites: 61095033220 in 132081000ms cpu (145961720ms real)
    (462557 rews/sec)
  result NzNat: 12586269025

If we instead give the Fibonacci function the memo attribute,

    op fibo : Nat -> Nat [memo] .

the change in performance is quite dramatic:

  Maude> red fibo(50) .
  reduce in FIBONACCI : fibo(50) .
  rewrites: 148 in 0ms cpu (0ms real) (~ rews/sec)
  result NzNat: 12586269025

  Maude> red fibo(100) .
  reduce in FIBONACCI : fibo(100) .
  rewrites: 151 in 0ms cpu (1ms real) (~ rews/sec)
  result NzNat: 354224848179261915075

  Maude> red fibo(1000) .
  reduce in FIBONACCI : fibo(1000) .
  rewrites: 2701 in 0ms cpu (11ms real) (~ rews/sec)
  result NzNat: 434665576869374564356885276750406258025646605173717804
    024817290895365554179490518904038798400792551692959225930803226347
    752096896232398733224711616429964409065331879382989696499285160037
    04476137795166849228875

In some cases we may introduce a constant operator as an abbreviation for a possibly complex expression that may require a substantial number of equational simplification steps to be reduced to canonical form; furthermore, the operator may be used repeatedly in different subcomputations. In such cases one can declare a constant operator, give it the memo attribute, and give an equation defining it to be equal to the expression of interest. For example, suppose we have defined a search space with initial state myState and a function findAnswer to search the space for a state satisfying some property. Then we can name the search result and use it again without redoing an expensive computation as follows:

  op myAns : -> Answer [memo] .
  eq myAns = findAnswer(myState) .

Maude will then remember the result of rewriting the constant in the memoization table for that operator and will not repeat the work until the memoization tables are cleared. Memoization tables can be cleared explicitly by the command

  do clear memo .

Automatic clearing before each top level rewriting command can be turned on and off with

  set clear memo on .
  set clear memo off .

By default, set clear memo is off.