The Chase as a General Test for Dependency Implication

Attribute closure decides implication for functional dependencies in polynomial time, but it does not generalize. Multivalued dependencies, join dependencies, and inclusion dependencies all need a different decision procedure, and the one that works for the first two is the chase: a tableau-based algorithm that repeatedly applies dependencies to a hypothetical pair of rows until either the tableau collapses to a single row or no further application is possible. The chase is the standard tool for two questions that come up in every serious schema design — is this decomposition lossless, and does this dependency set imply that one — and its complexity profile explains why normalization tools stop at fourth normal form.

The tableau, and why a hypothetical instance is enough

Implication is a statement about all instances: F implies f when every instance satisfying F also satisfies f. To refute implication it suffices to exhibit one instance satisfying F and violating f. The chase constructs that instance, or proves that none exists.

The construction starts from the violation of the target dependency. For an FD X → Y, a violation is a pair of tuples agreeing on X and disagreeing on some attribute of Y. The chase therefore begins with two rows that agree on X, differ on the attributes of Y, and hold distinct symbolic variables elsewhere. The variables are not values; they are placeholders that stand for arbitrary distinct domain elements.

Then dependencies from F are applied to the tableau. Each application either forces two variables to become equal — a symbol merge, written by replacing every occurrence of one variable with another — or, for a dependency that generates tuples, adds a row. The chase succeeds (the dependency is implied) when the two original rows become identical on the attributes of Y, because that contradicts the assumption that a violation exists. The chase fails when no dependency applies and the rows still differ, because the resulting tableau is a concrete counterexample: instantiate each variable with a distinct value and the instance satisfies F while violating f.

The key point is that variables can be equated but never distinguished. The chase only adds information; it never invents a distinction that the dependencies do not force. This monotonicity is what makes the procedure sound: any equality it derives holds in every instance satisfying F.

The FD case, worked

Take R(A, B, C) with F = {A → B, B → C} and test whether F implies A → C.

Start with two rows agreeing on A:

	A	B	C
t1	a	b1	c1
t2	a	b2	c2

Lowercase letters are variables; a is shared because the rows must agree on A for the violation. The target is A → C, so success means c1 and c2 become the same variable.

Apply A → B: both rows have A = a, so both must have the same B. Merge b2 into b1:

	A	B	C
t1	a	b1	c1
t2	a	b1	c2

Apply B → C: both rows now have B = b1, so their C values must be equal. Merge c2 into c1, and the rows are identical on C. The chase succeeds, so A → C is implied. This is the tableau-level version of the transitivity argument, and it is mechanical in a way that transitivity is not when several dependencies interact.

Now test F implies C → A with the same F. Start with two rows agreeing on C and differing on A. No dependency has C on its left, so nothing applies. The tableau stays split, and the chase fails — correctly, since {A → B, B → C} does not imply C → A.

The MVD case and the row-generating rule

Multivalued dependencies need a different application rule, because they assert the existence of a tuple rather than an equality. For X →→ Y, if the tableau contains two rows t1 and t2 with t1[X] = t2[X], the chase adds a row t3 with t3[X] = t1[X], t3[Y] = t1[Y], and t3[R − X − Y] = t2[R − X − Y]. If such a row already exists, the rule adds nothing.

The generated row is the formal counterpart of the independence condition: it is the combination of one row’s Y values with the other row’s remaining values. Applying the rule repeatedly generates the full cross product of the independent groups, which is exactly the redundancy the MVD permits.

For R(A, B, C) with A →→ B, testing whether A →→ C is implied: start with two rows agreeing on A, and apply the rule. The generated row has B from t1 and C from t2, which is the tuple asserting that t1’s B combines with t2’s C. The complement rule A →→ C is equivalent to A →→ B by the definition, so the chase succeeds by symmetry. This is the formal statement of the complementarity noted in multivalued dependencies and the redundancy BCNF cannot see.

The interesting case is a schema where MVDs interact with FDs. A B → C alongside A →→ B can force additional equalities that neither dependency forces alone, and the chase finds them by interleaving the two rule types. This is why the implication problem for mixed FD/MVD sets cannot be reduced to attribute closure on either class separately.

Lossless join as a chase question

The most common use of the chase is testing a decomposition. Given R decomposed into R1, …, Rk, construct a tableau with one row per Ri. Row i carries the distinguished symbol for attribute A in every attribute A ∈ Ri, and a nondistinguished variable unique to the pair (i, A) in every other attribute. Distinguished symbols are indexed by attribute alone, so two rows that both contain A hold the same symbol there — that shared symbol is what encodes agreement. In the tables below, c, s, and z stand for the distinguished symbols of city, street, and zip, and b1, b2 are nondistinguished variables. Then chase with F. The decomposition is lossless if and only if the chase produces a row that is entirely distinguished — every attribute holds its own distinguished symbol, with no nondistinguished variable surviving anywhere.

The intuition: the tableau is the universal instance that the join of the projections can produce, with variables marking the parts that the dependencies have not forced. If the chase can eliminate every variable in some row, no spurious tuple can survive the join. If it cannot, the surviving variables can be instantiated with distinct values, and the join then produces tuples that were not in R.

For the (city, street, zip) example from Boyce-Codd normal form and the cost of losing a dependency, decomposed into R1(zip, city) and R2(street, zip):

	city	street	zip
R1	c	b1	z
R2	b2	s	z

Row 1 is distinguished on city and zip; row 2 is distinguished on street and zip. The symbol z in the zip column is shared, because a distinguished symbol is indexed by attribute, not by row, so any two rows containing the same attribute agree on it by construction. Apply zip → city: the rows agree on zip, so they must agree on city, and b2 merges into c. Row 2 becomes (c, s, z) — every column holds its own distinguished symbol, so the chase succeeds. The decomposition is lossless, matching the two-way rule that R1 ∩ R2 → R1 holds because zip → city.

A decomposition that fails the test is visible by the same mechanism. Split R(city, street, zip) into R1(city, street) and R2(city, zip) instead, keeping both dependencies:

	city	street	zip
R1	c	s	b1
R2	c	b2	z

The intersection is {city}, and city alone determines neither street nor zip, so no dependency applies to merge b1 with b2. The shared c in city is already equal in both rows, and the surviving variables cannot be eliminated. Neither row becomes entirely distinguished, and the decomposition is lossy: joining the projections pairs every street in a city with every zip in that city, including combinations the original relation did not contain. That is precisely the {city, street} → zip violation the split made unenforceable.

def lossless(attrs, fds, rels):
    # The distinguished symbol for attribute a is the string a; every other
    # cell holds the nondistinguished variable (row_index, attribute).
    rows = [{a: a if a in rels[i] else (i, a) for a in attrs}
            for i in range(len(rels))]

    def merge(old, new):
        for r in rows:
            for k, v in r.items():
                if v == old:
                    r[k] = new

    changed = True
    while changed:
        changed = False
        for lhs, rhs in fds:
            groups = {}
            for r in rows:
                groups.setdefault(tuple(r[a] for a in lhs), []).append(r)
            for group in groups.values():
                for a in rhs:
                    # Prefer a distinguished symbol; it always wins a merge.
                    values = [r[a] for r in group]
                    target = next((v for v in values if isinstance(v, str)), values[0])
                    for v in values:
                        if v != target:
                            merge(v, target)
                            changed = True

    # Lossless iff some row holds its own distinguished symbol in every column.
    return any(all(r[a] == a for a in attrs) for r in rows)

The variable representation is the fiddly part in any implementation: merging must rewrite every occurrence, and the distinguished/variable distinction must survive the rewrite. A union-find over variable identifiers handles both cleanly, with distinguished variables marked as their own roots.

Termination and the cost of generality

The chase terminates for FD and MVD sets. The argument is a measure: the number of distinct variables is non-increasing under merges, and while MVD application can add rows, the set of possible rows is bounded by the product of the variable domains, which is finite. In practice the tableau for a k-relation decomposition with n attributes has k rows and at most n variables per row, and MVD application generates rows from existing ones, so the closure is bounded by k · 2^n rows in the worst case.

That bound is why the chase is not a practical algorithm for large schemas. It is exponential in the number of attributes in the worst case. The implication problem for FDs and MVDs together is decidable in polynomial time, but the decision procedure that achieves that bound is a specialized algorithm over dependency sets rather than the chase, which pays for its generality in tableau size. For the sizes that arise in schema design — ten to forty attributes — the exponential is irrelevant, and the chase is the clearest correct procedure.

For join dependencies the picture changes. A join dependency *(R1, …, Rk) asserts that R equals the join of its projections onto the Ri, which is a stronger condition than any MVD. The implication problem for join dependencies is NP-complete, and the chase inherits that: no polynomial procedure exists unless P = NP. This is the boundary that makes fifth normal form impractical to verify mechanically at scale, examined in join dependencies and fifth normal form.

Inclusion dependencies push further: the implication problem for inclusion dependencies alone is decidable but requires reasoning about infinite chains of values, and the chase must be modified to track them. The combined problem for FDs and inclusion dependencies is undecidable, which is the sharpest limit in the area — see inclusion dependencies and the limits of implication.

What the chase is used for

Three uses recur.

Verifying a decomposition before committing to it. A schema migration that splits a table is lossless if and only if the chase says so. Running the chase on the proposed split, with the actual declared dependencies, is a five-minute check that prevents the most expensive class of schema error — one that silently duplicates or drops rows on the join.

Deriving the dependencies of a decomposed schema. After splitting, the dependencies that hold in each Ri are the projections of F+ onto Ri. The chase computes them: for each candidate dependency in Ri, test implication against the original F restricted to Ri’s attributes. This is how a normalization tool reports what constraints the new schema can enforce.

Finding a minimal cover. Redundancy in a dependency set is an implication question, and the chase answers it for MVDs where attribute closure cannot. The chase-based test is slower than closure but applies to a strictly larger class.

The chase does not tell whether a decomposition is in a normal form — that requires enumerating dependencies, which the chase can help with but does not automate. And it does not tell whether the declared dependencies are true of the domain, which remains a designer’s judgement.