21.5 Membership Checking

< Free Open Study >

We now turn our attention to the central question of the chapter: how to decide, given a generating function F on some universe U and an element x Î U, whether or not x falls in the greatest fixed point of F. Membership checking for least fixed points is addressed more briefly (in Exercise 21.5.13).

A given element x Î U can, in general, be generated by F in many ways. That is, there can be more than one set X ⊆ U such that x Î F(X). Call any such set X a generating set for x. Because of the monotonicity of F, any superset of a generating set for x is also a generating set for x, so it makes sense to restrict our attention to minimal generating sets. Going one step further, we can focus on the class of "invertible" generating functions, where each x has at most one minimal generating set.

21.5.1 Definition

A generating function F is said to be invertible if, for all x Î U, the collection of sets

G_x = {X ⊆ U | x Î F(X)}

either is empty or contains a unique member that is a subset of all the others. When F is invertible, the partial function support_F Î U ⇀ P(U) is defined as follows:

The support function is lifted to sets as follows:

When F is clear from context, we will often omit the subscript in support_F (and similar functions based on F that we define later).

21.5.2 Exercise [⋆⋆]

Verify that S_f and S, the generating functions for the subtyping relations from Definitions 21.3.1 and 21.3.2, are invertible, and give their support functions.

Our goal is to develop algorithms for checking membership in the least and greatest fixed points of a generating function F. The basic steps in these algorithms will involve "running F backwards": to check membership for an element x, we need to ask how x could have been generated by F. The advantage of an invertible F is that there is at most one way to generate a given x. For a non-invertible F, elements can be generated in multiple ways, leading to a combinatorial explosion in the number of paths that the algorithm must explore. From now on, we restrict our attention to invertible generating functions.

21.5.3 Definition

An element x is F-supported if support_F(x)↓; otherwise, x is F-unsupported. An F-supported element is called F-ground if support_F(x) = ø.

Note that an unsupported element x does not appear in F(X) for any X, while a ground x is in F(X) for every X.

An invertible function can be visualized as a support graph. For example, Figure 21-2 defines a function E on the universe {a, b, c, d, e, f, g, h, i} by showing which elements are needed to support a given element of the universe: for a given x, the set support_E(x) contains every y for which there is an arrow from x to y. An unsupported element is denoted by a slashed circle. In this example, i is the only unsupported element and g is the only ground element. (Note that, according to our definition, h is supported, even though its support set includes an unsupported element.)

Figure 21-2: A Sample Support Function

21.5.4 Exercise [⋆]

Give inference rules corresponding to this function, as we did in Example 21.1.3. Check that E({b,c}) = {g,a,d}, that E({a,i}) = {g,h}, and that the sets of elements marked in the figure as μE and vE are indeed the least and the greatest fixed points of E.

Thinking about the graph in Figure 21-2 suggests the idea that an element x is in the greatest fixed point iff no unsupported element is reachable from x in the support graph. This suggests an algorithmic strategy for checking whether x is in vF: enumerate all elements reachable from x via the support function; return failure if an unsupported element occurs in the enumeration; otherwise, succeed. Observe, however, that there can be cycles of reachability between the elements, and the enumeration procedure must take some precautions against falling into an infinite loop. We will pursue this idea for the remainder of this section.

21.5.5 Definition

Suppose F is an invertible generating function. Define the boolean-valued function gfp_F (or just gfp) as follows:

gfp(X)

=

if support(X) ↑, then false

else if support(X) ⊆ X, then true

else gfp(support(X) È X).

Intuitively, gfp starts from X and keeps enriching it using support until either it becomes consistent or else an unsupported element is found. We extend gfp to individual elements by taking gfp(x) = gfp({x}).

21.5.6 Exercise [⋆]

Another observation that can be made from Figure 21-2 is that an element x of vF is not a member of μF if x participates in a cycle in the support graph (or if there is a path from x to an element that participates in a cycle). Is the converse also true—that is, if x is a member of vF but not μF, is it necessarily the case that x leads to a cycle?

The remainder of the section is devoted to proving the correctness and termination of gfp. (First-time readers may want to skip this material and jump to the next section.) We start by observing a couple of properties of the support function.

21.5.7 Lemma

X ⊆ F(Y) iff support_F(X)↓ and support_F(X) ⊆ Y.

Proof: It suffices to show that x Î F(Y) iff support(x)↓ and support(x) ⊆ Y. Suppose first that x Î F(Y). Then Y Î G_x = {X ⊆ U | x Î F(X)}—that is, G_x ≠ . Therefore, since F is invertible, support(x), the smallest set in G_x, exists and support(x) ⊆ Y. Conversely, if support(x) ⊆ Y, then F(support(x)) ⊆ F(Y) by monotonicity. But x Î F(support(x)) by the definition of support, so x Î F(Y).

21.5.8 Lemma

Suppose P is a fixed point of F. Then X ⊆ P iff support_F(X)↓ and support_F(X) ⊆ P.

Proof: Recall that P = F(P) and apply Lemma 21.5.7.

Now we can prove partial correctness of gfp. (We are not concerned with total correctness yet, because some generating functions will make gfp diverge. We prove termination for a restricted class of generating functions later in the section.)

21.5.9 Theorem

If gfp_F(X) = true, then X ⊆ vF.
If gfp_F(X) = false, then X ⊈ vF.

Proof: The proof of each clause proceeds by induction on the recursive structure of a run of the algorithm.

From the definition of gfp, it is easy to see that there are two cases where gfp(X) can return true. If gfp(X) = true because support(X) ⊆ X, then, by Lemma 21.5.7, we have X ⊆ F(X), i.e., X is F-consistent; thus, X ⊆ vF by the coinduction principle. On the other hand, if gfp(X) = true because gfp(support(X) È X) = true, then, by the induction hypothesis, support(X) È X ⊆ vF, and so X ⊆ vF.
Again, there are two ways to get gfp(X) = false. Suppose first that gfp(X) = false because support(X) ↑. Then X ⊈ vF by Lemma 21.5.8. On the other hand, suppose gfp(X) = false because gfp(support(X) È X) = false. By the induction hypothesis, support(X) È X ⊈ vF. Equivalently, X ⊈ vF or support(X) ⊈ vF. Either way, X ⊈ vF (using Lemma 21.5.8 in the second case).

Next, we identify a sufficient termination condition for gfp, giving a class of generating functions for which the algorithm is guaranteed to terminate. To describe the class, we need some additional terminology.

21.5.10 Definition

Given an invertible generating function F and an element x Î U, the set pred_F(x) (or just pred(x)) of immediate predecessors of x is

and its extension to sets X ⊆ U is

The set reachable_F(X) (or just reachable(X)) of all elements reachable from a set X via support is defined as

and its extension to single elements x Î U is

reachable(x) = reachable({x}).

An element y Î U is reachable from an element x if y Î reachable(x).

21.5.11 Definition

An invertible generating function F is said to be finite state if reachable(x) is finite for each x Î U.

For a finite-state generating function, the search space explored by gfp is finite and gfp always terminates:

21.5.12 Theorem

If reachable_F(X) is finite, then gfp_F(X) is defined. Consequently, if F is finite state, then gfp_F(X) terminates for any finite X ⊆ U.

Proof: For each recursive call gfp(Y) in the call graph generated by the original invocation gfp(X), we have Y ⊆ reachable(X). Moreover, Y strictly increases on each call. Since reachable(X) is finite, m(Y) = |reachable(X)| - |Y| serves as a termination measure for gfp.

21.5.13 Exercise [⋆⋆⋆]

Suppose F is an invertible generating function. Define the function lfp_F (or just lfp) as follows:

lfp(X)

=

if support(X) ↑, then false

else if X = ø, then true

else lfp(support(X)).

Intuitively, lfp works by starting with a set X and using the support relation to reduce it until it becomes empty. Prove that this algorithm is partially correct, in the sense that

If lfp_F(X) = true, then X ⊆ μF.
If lfp_F(X) = false, then X ⊈ μF.

Can you find a class of generating functions for which lfp_F is guaranteed to terminate on all finite inputs?

< Free Open Study >