21.6 More Efficient Algorithms

---

21.6 More Efficient Algorithms

Although the gfp algorithm is correct, it is not very efficient, since it has to recompute the support of the whole set X every time it makes a recursive call. For example, in the following trace of gfp on the function E from Figure 21-2,

•  

  	gfp({a})
  =	gfp({a,b,c})
  =	gfp({a,b,c,e,f,g})
  =	gfp({a,b,c,e,f,g,d})
  =	true.

Note that support(a) is recomputed four times. We can refine the algorithm to eliminate this redundant recomputation by maintaining a set A of assumptions whose support sets have already been considered and a set X of goals whose support has not yet been considered.

21.6.1 Definition

Suppose F is an invertible generating function. Define the function (or just gfp^a) as follows (the superscript "a" is for "assumptions"):

•  

  gfp^a(A, X)

  =

  if support(X) ↑, then false

  else if X = ø, then true

  else gfp^a(A È X, support(X) \ (A È X)).

In order to check x Î vF, compute gfp^a(ø, {x}).

This algorithm (like the two following algorithms in this section) computes the support of each element at most once. A trace for the above example looks like this:

•  

  	gfpa(ø, {a})
  =	gfpa({a}, {b,c})
  =	gfpa({a,b,c}, {e,f,g})
  =	gfpa({a,b,c,e,f,g}, {d})
  =	gfpa({a,b,c,e,f,g,d}, ø)
  =	true.

Naturally, the correctness statement for this algorithm is slightly more elaborate than the one we saw in the previous section.

21.6.2 Theorem

1. If support_F(A) ⊆ A È X and , then A È X ⊆ vF.

2. If , then X ⊈ vF.

Proof: Similar to 21.5.9.

The remainder of this section examines two more variations on the gfp algorithm that correspond more closely to well-known subtyping algorithms for recursive types. First-time readers may want to skip to the beginning of the next section.

21.6.3 Definition

A small variation on gfp^a has the algorithm pick just one element at a time from X and expand its support. The new algorithm is called (or just gfp^s, s" being for "single").

•  

  gfp^s (A, X)

  =

  if X = , then true

  else let x be some element of X in

  • if x Î A then gfp^s (A, X \ {x})

  • else if support(x) ↑ then false

  • else gfp^s (A È {x}, (X È support(x)) \ (A È {x})).

The correctness statement (i.e., the invariant of the recursive "loop") for this algorithm is exactly the same as Theorem 21.6.2.

Unlike the above algorithm, many existing algorithms for recursive subtyping take just one candidate element, rather than a set, as an argument. Another small modification to our algorithm makes it more similar to these. The modified algorithm is no longer tail recursive,^[3] since it uses the call stack to remember subgoals that have not yet been checked. Another change is that the algorithm both takes a set of assumptions A as an argument and returns a new set of assumptions as a result. This allows it to record the subtyping assumptions that have been generated during completed recursive calls and reuse them in later calls. In effect, the set of assumptions is "threaded" through the recursive call graph-whence the name of the algorithm, gfp^t.

21.6.4 Definition

Given an invertible generating function F, define the function (or just gfp^t) as follows:

•  

  gfp^t (A,x)

  =

  if x Î A, then A

  else if support(x) ↑, then fail

  else

  • let {x₁,...,x_n} = support(x) in

  • let A₀ = A È {x} in

  • let A₁ = gfp^t (A₀,x₁) in

  • ...

  • let A_n = gfp^t (A_n-1,x_n) in

  • A_n.

To check x Î vF, compute gfp^t (,x). If this call succeeds, then x Î vF; if it fails, then x ∉ vF. We use the following convention for failure: if an expression B fails, then "let A = B in C" also fails. This avoids writing explicit "exception handling" clauses for every recursive invocation of gfp^t.

The correctness statement for this algorithm must again be refined from what we had above, taking into account the non-tail-recursive nature of this formulation by positing an extra "stack" X of elements whose supports remain to be checked.

21.6.5 Lemma

1. If , then A È {x} ⊆ A′.

2. For all X, if support_F(A) ⊆ AÈXÈ{x} and , then support_F(A′) ⊆ A′ È X.

Proof: Part (1) is a routine induction on the recursive structure of a run of the algorithm.

Part (2) also goes by induction on the recursive structure of a run of the algorithm. If x Î A, then A′ = A and the desired conclusion follows immediately from the assumption. On the other hand, suppose A′ ≠ A, and consider the special case where support(x) contains two elements x₁ and x₂-the general case (not shown here) is proved similarly, using an inner induction on the size of support(x). The algorithm calculates A₀, A₁, and A₂ and returns A₂. We want to show, for an arbitrary X₀, that if support(A) ⊆ A È {x} È X₀, then support(A₂) ⊆ A₂ È X₀. Let X₁ = X₀ È {x₂}. Since we can apply the induction hypothesis to the first recursive call by instantiating the universally quantified X with X₁. This yields support(A₁) ⊆ A₁ È X₁ = A₁ È {x₂} È X₀. Now, we can apply the induction hypothesis to the second recursive call by instantiating the universally quantified X with X₀ to obtain the desired result: support(A₂) ⊆ A₂ È X₀.

•  

  support(A0)	=	support(A) È support(x)
  	=	support(A) È {x1,x2}
  	⊆	A È {x} È X0 È {x1,x2}
  	=	A0 È X0 È {x1,x2}
  	=	A0 È X1 È {x1},

21.6.6 Theorem

1. If , then x Î vF.

2. If , then x ∉ vF.

Proof: For part (1), observe that, by Lemma 21.6.5(1), x Î A′. Instantiating part (2) of the lemma with X = , we obtain support(A′) ⊆ A′-that is, A′ is F-consistent by Lemma 21.5.7, and so A′ ⊆ vF by coinduction. For part (2), we argue (by an easy induction on the depth of a run of the algorithm, using Lemma 21.5.8) that if, for some A, we have , then x ∉ vF.

Since all of the algorithms in this section examine the reachable set, a sufficient termination condition for all of them is the same as that of the original gfp algorithm: they terminate on all inputs when F is finite state.

^[3]A tail-recursive call (or tail call) is a recursive call that is the last action of the calling function-i.e., such that the result returned from the recursive call will also be caller's result. Tail calls are interesting because most compilers for functional languages will implement a tail call as a simple branch, re-using the stack space of the caller instead of allocating a new stack frame for the recursive call. This means that a loop implemented as a tail-recursive function compiles into the same machine code as an equivalent while loop.

---