Skip to content

Chase (algorithm)

Rule-saturation procedure for reasoning about relational data dependencies.

Version
v1 · 2026-09-28 · History
Domain-specific #
8421
Domain group
Applied Sciences & Engineering
Origin domain
Computer Science & Software Engineering
Subdomains
Relational Databases, Database Theory → Computer Science & Software Engineering
Aliases
Database chase, Chase procedure

Core Idea

The chase is database dependency reasoning by repeated rule application. From a relational instance or tableau, it finds an unsatisfied dependency premise, adds the tuple or equality that the rule requires, and continues until a fixed point, contradiction or appropriately qualified stopping state. The result can test dependency implication or lossless decomposition and can construct data-exchange or cleaning outcomes.

The canonical tableau calculation demonstrates why an equality dependency can turn a projection row into an all-distinguished row. LLUNATIC demonstrates a published implemented chase engine for tgds and egds. Neither case licenses a claim that every dependency set terminates or every database product uses the same variant.

How would you explain it like I'm…

Keep Fixing Until Happy

Imagine a notebook of facts and a list of rules like 'if someone is in a class, they must have a teacher'. You look for a rule that isn't being followed, add whatever it says is missing, and look again. You keep going until every rule is happy, or you find two facts that can't both be true. That repeated fixing is called the chase.

Rule-Fixing Loop

Databases store facts in tables and often have rules the data should follow, called dependencies. The chase is a method that keeps checking the rules: when it finds a rule that isn't satisfied, it adds the new row or makes two values equal, exactly as the rule demands. It repeats until nothing changes, until it hits a contradiction, or until some agreed stopping point. People use it to test whether one rule follows from others, whether splitting a table loses information, and to build or clean up data.

Dependency Chase Procedure

The chase is a procedure for reasoning with database dependencies by repeated rule application. Starting from a relational instance or a tableau (a table with variables), it finds a dependency whose premise is matched but whose conclusion isn't satisfied, then adds the required tuple (for tuple-generating dependencies) or equates the required values (for equality-generating dependencies). It continues until a fixed point, a contradiction, or a qualified stopping condition. Applications include testing whether a set of dependencies implies another, checking lossless-join decomposition, and computing results for data exchange or data cleaning. It doesn't always terminate for every set of dependencies, and there are several variants.

 

The chase applies dependencies to a relational instance or tableau as rewrite rules: each step selects a dependency whose body is satisfied by a homomorphism but whose head is not, then either adds tuples (tgds, possibly with fresh labeled nulls) or unifies values (egds), failing if an egd forces two distinct constants equal. Iteration proceeds to a fixed point, a contradiction, or a suitably qualified stopping state. For dependency implication, one chases a tableau for the premise and checks whether the conclusion holds in the result. For lossless decomposition, the classic tableau test succeeds when equality dependencies turn some row into an all-distinguished row. The same machinery constructs solutions in data exchange and repairs in cleaning, and implemented engines such as LLUNATIC chase tgds and egds. Termination is not guaranteed for arbitrary dependency sets, and chase variants differ, so claims about termination or behavior must name the variant and the dependency class.

Structural Signature

Sig role-phrases:

  • Relational instance or tableau — A structured starting state records tuples, symbols or schema projections. It is constitutive. Counterfactual: An unconstrained prose claim is not a chase state.
  • Dependency rules — Functional or generating/equality dependencies state when a pattern demands an update. It is constitutive. Counterfactual: Repeated scanning with no logical rules is not a chase.
  • Violation match — A homomorphism or tableau match identifies a currently unsatisfied rule premise. It is constitutive. Counterfactual: A rule not triggered by current data causes no chase step.
  • Repair or witness step — Equate symbols or add required facts/witnesses according to the chosen chase variant. It is constitutive. Counterfactual: An arbitrary edit unrelated to a dependency is not a chase step.
  • Stopping and inference — A fixed point, contradiction or qualified cutoff supports a query, implication or consistency conclusion. It is constitutive. Counterfactual: Nontermination without bounded claims does not prove a desired implication.

What It Is Not

  • Not any database iteration. Steps must enforce stated dependencies.
  • Not a universal termination theorem. Guarantees depend on rule classes and variant.
  • Not only lossless-join testing. Data exchange and cleaning also use chase mechanisms.
  • Not arbitrary data repair. Updates follow formal rule triggers.
  • Closest near-miss. A recursive SQL computation reaching a fixed point resembles saturation but is not a chase unless its steps enforce dependencies on a tableau or instance.

Scope of Application

  • Schema design. Test lossless decompositions under dependencies.
  • Dependency implication. Determine whether constraints force another constraint.
  • Data exchange. Populate targets from source-to-target rules.
  • Data cleaning. Find and repair constraint violations under a chosen semantics.

Clarity

The chase repeatedly applies database dependencies to a tableau or relational instance. It may equate symbols, create required tuples or stop at a fixed point. A small functional-dependency tableau can prove a lossless join; LLUNATIC implements chase variants for exchange and cleaning. Termination is not universal.

Manages Complexity

Rule saturation turns many interacting dependencies into a trace of justified local updates. The trace can certify a structural property when the variant's conditions hold; unrestricted cases can generate new witnesses indefinitely or several repair alternatives, so stopping and result semantics must be stated.

Abstract Reasoning

  1. Choose a tableau or database instance and a dependency set.
  2. Find a premise match not yet satisfied.
  3. Apply the required equality or tuple-generating step.
  4. Repeat under a named chase variant.
  5. Test fixed point, failure or bounded termination condition.
  6. State exactly which implication or repair conclusion follows.

Knowledge Transfer

Rule-saturation algorithms recur in logic and verification, but the database chase specifically operates over relational instances/tableaux and dependencies. A generic fixed-point iteration transfers the skeleton without becoming this algorithm.

Examples

Canonical

A precise lossless-join tableau construction uses R(A,B,C), F={A→B}, and projections AB and AC. Begin with rows (a,b,c₁) and (a,b₂,c); A→B equates b₂ with b, producing the all-distinguished row (a,b,c), so the decomposition is lossless under F. This is a worked instance of the original 1979 tableau method, not a quotation of that exact toy schema from the papers.

Mapped back: Relational instance or tableau → two projection rows with distinguished and indexed symbols; Dependency rules → the functional dependency A→B; Violation match → same A symbol a with differing B symbols; Repair or witness step → equate b₂ to b under A→B; Stopping and inference → all-distinguished row certifies lossless reconstruction.

Applied / In Practice

The LLUNATIC research software implements a chase engine that executes tuple-generating and equality-generating dependencies for published data-exchange and data-cleaning scenarios. Its project page lists released software and research publications. This is an attested research implementation, not evidence that all commercial database systems run LLUNATIC or that every dependency class terminates.

Mapped back: Relational instance or tableau → source/target database instances in LLUNATIC scenarios; Dependency rules → source-to-target tgds, target tgds and egds; Violation match → engine finds mappings or constraints needing enforcement; Repair or witness step → engine generates target facts or repairs equalities under selected scenario; Stopping and inference → computed scenario solution or qualified repair result.

Structural Tensions

T1 — Expressive Rules versus Termination Guarantee. Richer dependencies handle more cases but can make chase runs diverge or require guarded variants.

Diagnostic: Which dependency class and chase variant apply?

T2 — Complete Repair versus Combinatorial Cost. Exploring possible solutions can improve coverage but expand runtime and result space.

Diagnostic: Is one witness sufficient?

T3 — Symbolic Equivalence versus Data Provenance. Equating symbols can establish implication while practical cleaning needs explanation of changed values.

Diagnostic: What result must be audited?

Structural–Framed Character

The database chase is mixed-structural. Its repeated rule application has a sharply formal shape, but the rules and inference claims belong to relational-database semantics. Evaluative weight: reaching a fixed point is a formal result under chosen dependencies, not a verdict that repaired data are factually correct. Human-practice dependence: the procedure executes automatically after a designer supplies schemas, rules and variant; those choices shape which outputs count as solutions. Institutional origin: database theory named and developed the chase; the logical update relation is not an arbitrary convention, but its algorithmic variants are scholarly designs. Vocabulary travel: match, apply, repeat and stop travel to many algorithms; tuples, tgds, egds and tableaux do not travel without translation. Import versus recognition: a new relational dependency engine using these steps is a chase instance; a generic iterative optimizer is only analogous.

The portable skeleton resembles the verified Algorithm prime in its specified inputs and rule-ordered updates, but the current prime additionally requires guaranteed termination for every admissible input. The unrestricted chase need not meet that condition. Its character: a formal domain procedure whose conclusion and termination guarantee depend on rule class and execution variant.

Structural Core vs. Domain Accent

This section decides why the Chase is domain-specific rather than a prime.

What is skeletal (could lift toward a cross-domain prime). A state is inspected for a rule trigger, transformed by an authorized local step and inspected again. That resembles part of Algorithm's input–procedure–result structure, but unrestricted chase may never reach the result or stopping condition that the present prime requires on all admissible inputs. Saturation to a fixed point remains broadly recognizable in the terminating cases. The worked tableau shows why a local equality can establish a global lossless-join property when the relevant database theorem applies; it does not turn every repeated loop into the same theorem.

What is domain-bound. The state is a relational tableau or database instance, and the triggers are functional, tuple-generating or equality-generating dependencies. Aho, Beeri and Ullman's join setting uses distinguished tableau symbols; LLUNATIC uses tgds and egds for data exchange and cleaning. Changing the dependency class or chase variant can change termination, branching and what conclusion the result licenses. Strip away relational patterns and dependency-enforced tuple/equality steps and a fixed-point process remains, but the database chase does not.

Why this does not clear the prime bar. Across database applications, the same named procedure is recognizable when its formal roles are preserved. Outside that setting, logic engines may share rule saturation but require their own inference semantics; simply importing “chase” because a process iterates is analogy. The current Algorithm prime captures terminating procedural work but cannot strictly parent the broader chase identity, because some admissible chase runs diverge. The entry stays domain-specific because its triggers and conditional guarantees are stated in the vocabulary of relations, dependencies and tableaux.

  • Related prime: Algorithm, not an asserted parent. A terminating chase run is algorithmic, but unrestricted chase can continue indefinitely on admissible dependencies, while the current Algorithm prime makes guaranteed termination constitutive. The broader chase procedure therefore cannot be strictly subsumed by that node.

  • Conceptual relation: data dependency. The chase reasons over database constraints, not the current catalog's program-read/write dependency node, so that homonymous node is not a parent.

Neighborhood in Abstraction Space

Chase (algorithm) sits in a crowded region of the domain-specific corpus (39th percentile for distinctiveness): several abstractions share nearly its structure, so a description that fits it tends to fit its neighbors too.

Family — Formal Systems & Discrete Structures (18 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With

  • Recursive SQL query. Tell: May iterate without enforcing dependencies.
  • Constraint satisfaction in general. Tell: Broader family, without the chase's tableau/instance update discipline.
  • Arbitrary data cleaning. Tell: A manual correction need not be a chase step.
  • Program data dependency. Tell: Concerns read/write ordering, a different catalog sense.

References