🚀 go-pugleaf

The following (longish) message describes what I believe is a novel use 
of memoization --- I haven't seen it in this generality in any functional 
or logic language.  

There appear to be two separate motivations for memoization: (1) efficiency 
reasons, and (2) semantic reasons.  Examples of (1) are well-known.
As an example of the second kind, as David Warren and others have noted,
an SLD interpreter that uses memoization terminates more often.  To 
motivate a related but perhaps more general use of memoization,  consider 
the following natural program for the set of reachable nodes of a graph,
represented as a set of ordered pairs edge(a,b): 

reach(V, G)    = {V}  U  {Y : X in adjacent(V, G),  Y in reach(X, G)}

adjacent(V, G) = {A : edge(V,A) in G}	  

This program would loop if graph G is cyclic, but wouldn't under memoization.
However, memoization alone is not enough to compute the desired answer!  
In general, it must be coupled with a "re-do" mechanism for iterating to 
the least fixed-point.   The re-do mechanism is derived from the underlying
partial ordering on interpretations, which states that I1 <= I1 iff
[f(x)=s1 in I1  implies  (f(x) = s2 in I2,  and s1 is a subset of s2)].
So, the initial look-up value for a memoized call becomes the empty set (the 
least element of the partial ordering), and we keep iterating (or re-doing),
forming larger sets for each memoized call until the lfp is reached.  
Naturally, there are some monotonicity and continuity requirements 
in order that the lfp can be found in this manner, but these are not 
hard to state, and the above program possess these properties.

The above example actually does not make full use of re-do.  The need 
for re-do is pervasive in graph algorithms, as well as in many problems 
involving sets, e.g. solving dataflow equations during compiler optimization.
To keep this message short, I won't get into them here.

% Now, a plug for our work ... but please do read it!

There is a family of functional-cum-relational languages (SEL, SRL, and 
SuRE), developed by David Plaisted, myself, and our students, based upon the 
subset assertion (see references at end), wherein the above semantics is 
achieved.   The exact syntax for the "reach" program in the language SEL 
(Subset-Equational Language) is as follows.  
	
	closure reach/2, allreach/2.	% closure indicates need for re-do;
					% other functions are not memoized. 
	reach(V, G) contains {V}.
	reach(V, G) contains allreach(adjacent(V,G), G).

	allreach({W \ _}, G) contains reach(W, G).

	adjacent(V,  {edge(V,W) \ _})  contains {W}.

Notes: {X \ T} matches set S such that (X in S) and T = S-{X}. 
When a function f is defined with a "contains" (or subset) assertion, 
the result of f(t) is the union of the sets resulting from all applicable 
r.h.s., taking every possible match from every l.h.s.  

For more details on these languages, please see the references below.

References:

1.Functional Programming with Sets, B.Jayaraman & D.A. Plaisted, FPCA, 1987.
2.Programming with Equations, Subsets and Relations, "  ", NACLP 89.
3.Subset-logic Programming, B.Jayaraman & A. Nair, Jt SLP/ICLP, 1988.
4.The SuRE Programming Framework, B. Jayaraman, SUNY-Buffalo, TR 91-11.
5.Impln. of Subset-Equational Programs, ", JLP, 1992 (to appear)
6.Set Constructors, Finite Sets & Logical Semantics, D.Jana & B.Jayaraman
	(Refs. 2 and 4 discuss closure functions to some extent.)

Implementation Notes: Version 2 of the SEL compiler is written (by Ph.D.
student K. Moon) in Quintus Prolog, and it generates WAM-like code, differing 
from standard WAM in the provision of set matching, memoization, and re-do.