Link Search Menu Expand Document

Unstable-Funcons-beta : Memos.cbs | PRETTY | PDF


Memos

A memo is like a mutable variable, except that the memo is updated and accessed by a specified key, rather than by an allocated location. The collection of memos is represented by a mutable entity that maps keys to values.

Entity 
  < _ , memo-map(_:maps(ground-values, values)) > --->
  < _ , memo-map(_:maps(ground-values, values)) >
Funcon
  initialise-memos(_:=>values) : =>values
Rule
  < initialise-memos(X) , memo-map(_) > ---> < X , memo-map(map( )) >

When key K is associated with value V, the funcon memo-value(K, X) simply gives V, without evaluating X. When K is not currently associated with any value, it associates K with the value computed by X.

The initialisation could fail due to memoisation of a (potentially different) value for K during the computation X. In that case, the value computed by X is simply discarded; a resource-safe funcon would take an extra argument to roll back the effects of X.

Funcon
  initialise-memo-value(_:ground-values, _:values) : =>null-type
Rule
  map-unite(M, {K |-> V}) ~> M′
  -----------------------------------------------------------------
  < initialise-memo-value(K:ground-values, V:values), memo-map(M) >
    ---> < null-value , memo-map(M′) >
Rule
  map-unite(M, {K |-> V}) ~> ( )
  -----------------------------------------------------------------
  < initialise-memo-value(K:ground-values, V:values), memo-map(M) >
    ---> < fail , memo-map(M) >
Funcon
  memo-value-recall(_:ground-values) : =>values
Rule
  lookup(M, K) ~> V
  ----------------------------------------------------------------------------
  < memo-value-recall(K:ground-values), memo-map(M) > ---> < V , memo-map(M) >
Rule
  lookup(M, K) ~> ( )
  -------------------------------------------------------------------------------
  < memo-value-recall(K:ground-values), memo-map(M) > ---> < fail , memo-map(M) >