PaperlayerView exact revision on arXiv

Source-linked AI summary

Property Testing for Recursive Query Languages

Isolde Adler, Carsten Lutz, Quentin Manière, Marcin Przybyłko, Lukas Schulze

arXiv:2609.03908v1cs.DBcs.LO

TL;DR

Property testing asks whether query answers can be tested with few database probes, extending a framework previously characterized for conjunctive queries. This paper studies recursive query languages through 2RPQs and monadic Datalog, proving positive results for several classes and a conditional lower bound for others.

  • Problem

    Property testing had been characterized for conjunctive queries, but its reach to recursive query languages remained to be investigated.

    Source: §1 · p. 2

  • Method

    The paper studies 2RPQs and monadic Datalog using property-testing reductions, including reductions to unreachability, 2RPQs, and α-acyclic UCQs.

    Source: §1 · pp. 2–3

  • Results

    Every 2RPQ and simple branching program has constant-query one-sided testing for falsity, while non-α-acyclic-equivalent Boolean MDLog is not testable under self-join freeness.

    Source: §1 · pp. 2–3

  • Takeaways & Limitations

    Positive one-sided testability extends to some recursive branching MDLog programs, though the broader class remains unresolved.

    Source: §1 · p. 3

    The SBP result does not settle broader acyclic MDLog; even constant-length edge paths and repeated relation symbols remain unresolved extensions.

    Source: §4.2 · p. 12, §4.3 · p. 14

Abstract

from arXiv · show

In the context of database querying, property testing provides a framework for testing query answers with high confidence while inspecting only a sublinear part of the database, through completion queries and size queries. A fundamental result of Chen and Yoshida (2019) states that non-satisfaction of a Boolean conjunctive query $q$ is testable with a constant number of such queries and one-sided error if and only if $q$ is equivalent to an $\alpha$-acyclic query. In this article, we initiate the study of property testing for recursive query languages, focusing on two-way regular path queries (2RPQs) and monadic Datalog. One of our main results is positive: non-answers to any 2RPQ are constant query testable with one-sided error. We extend this slightly to a certain class of monadic Datalog programs in which recursion is restricted to be linear and rule bodies must be $\alpha$-acyclic. Turning towards unrestricted monadic Datalog, we next show that if a monadic Datalog program $\Pi$ is not equivalent to an $\alpha$-acyclic program, then falsity of $\Pi$ is not constant query testable with one-sided error. This is under the assumption that all rule-bodies are self-join free. We leave open the case of monadic Datalog programs with $\alpha$-acyclic rule bodies that are not restricted to linear recursion, but observe as a first step that there exist $\alpha$-acyclic programs that are mildly non-linear and constant query testable with one-sided error.

1 Introduction

Property testing asks which queries can be tested with few database probes, an important question as data scales make exhaustive computation increasingly impractical. The paper extends this inquiry from conjunctive queries to recursive query languages, establishing positive results for 2RPQs and some monadic Datalog programs alongside a conditional lower bound.

1 Introduction

  • Property testing aims to distinguish objects satisfying a property from objects far from satisfying it using only sublinear, ideally constant, probes.The motivation is that large modern datasets can make even a sequential scan a substantial computational task.Source: §1 · pp. 1–2
  • Chen and Yoshida’s result characterizes one-sided constant-query testability for Boolean UCQs through α-acyclic homomorphism cores after removing strictly contained CQs.Their database model uses completion and size queries; the result applies to bag databases, where multiplicities affect the number of fact deletions needed to falsify a query.Source: §1 · p. 2
  • Non-answers to every 2RPQ are constant query testable with one-sided error, by reduction to testing unreachability in directed multigraphs.The unreachability property is known to have the same testability guarantee.Source: §1 · p. 2
  • Strongly linear programs are constant query testable with one-sided error by reduction to the 2RPQ case.Their rule bodies have exactly two variables and no IDB atom contains the head variable; informally, satisfaction is witnessed by a linear database part without single-edge branching, though multi-edges and reflexive loops may occur.Source: §1 · p. 3
  • Simple branching programs are a recursive, branching MDLog class whose falsity is constant query testable with one-sided error.The approach reduces reflexive loops and multi-edges, decomposes programs into simple linear programs, and uses a Menger-style argument to obtain many constant-length paths and reduce to α-acyclic UCQs.Source: §1 · p. 3
  • Falsity of a Boolean MDLog program not equivalent to one with α-acyclic rule bodies is not constant query testable with one-sided error when its rule bodies are self-join free.The proof identifies a chordless cycle or tetra that every derivation must use non-trivially, then reduces from testing falsity of these hard CQs.Source: §1 · p. 3
  • The testability status of many recursive and branching MDLog programs remains open beyond the modest SBP class with a positive result.The authors point to a need for removal lemmas for branching subgraphs of varying size, which they say are not known for directed graphs.Source: §1 · p. 3

2 Preliminaries

The preliminaries establish the database, query, and Datalog terminology used throughout, then formalize property testing through completion and size queries. They also define property-testing reductions, which transfer one-sided constant-query testability between problems.

2 Preliminaries

  • Databases are finite multisets of facts over a schema, and query equivalence means mutual containment over every database.An α-acyclic database has a join tree; an MDLog program is α-acyclic when every rule body is an α-acyclic CQ.Source: §2 · pp. 4–5
  • A 2RPQ is an NFA over relation symbols and their inverses, and it answers pairs connected by a path whose label the automaton accepts.Fact multiplicities do not affect which pairs are answers.Source: §2 · p. 4
  • A CQ is a conjunction of relational atoms, while a Datalog program consists of rules with conjunctive-query bodies; MDLog restricts IDB relations to be monadic, except possibly the goal.Linear programs have at most one IDB atom per rule body, and self-join-free bodies use each EDB relation at most once.Source: §2 · pp. 4–5
  • A database is ε-far from a property when more than ε|D| fact additions or removals are needed to reach it.For the properties studied, adding facts is not helpful, so only removals need consideration.Source: §2 · p. 5
  • Property testing treats non-answers as the property of interest and tests pointed databases using completion and size queries.A completion query samples a matching fact tuple; a size query returns the number of matching completions. One-sided error means the tester always accepts instances in the property.Source: §2 · pp. 5–6
  • A property-testing reduction preserves membership, maps far instances to far instances, and lets target queries be simulated with constantly many source queries.If testing the target property is constant query testable with one-sided error, then so is the source property.Source: §2 · pp. 6–7

3 Two-Way Regular Path Queries

Every 2RPQ’s non-answers are constant query testable with one-sided error. The proof reduces this problem to testing unreachability in a multi-digraph.

3 Two-Way Regular Path Queries

  • The unreachability tester handles an unrestricted target set by identifying its vertices, while extension to multiple sources remains conjectural.The paper does not work out the multiple-source (and target) generalization.Source: §3 · pp. 7–8
  • Multi-digraph unreachability is constant query testable with one-sided error using only completion queries of the form (a, *), and no size queries.The underlying random-walk tester can be implemented with these completion queries.Source: §3 · p. 7
  • The product multi-digraph has vertices adom(D) × Q and edges derived from database facts and automaton transitions, with reverse transitions reversing endpoints.Bag multiplicities produce multiple edges, each attributable to a unique database fact.Source: §3 · p. 8
  • If (D, a1a2) is ε-far from being a non-answer, its product graph is ε|Δ|-far from the target set being unreachable from the source.The source is ⟨a1,s0⟩ and the target set is {a2} × F.Source: §3 · p. 8
  • Non-answers to every 2RPQ are constant query testable with one-sided error.The result follows by reduction to multi-digraph unreachability.Source: §3 · pp. 7–8
  • Product-graph completion queries can be simulated with constantly many database queries by sampling a relation symbol and compatible automaton state to obtain a uniform successor.The symbol distribution reflects successor counts; a completion query to D supplies the database neighbor.Source: §3 · pp. 8–9

4 Monadic Datalog: Upper Bounds

This section establishes one-sided constant-query testability for restricted recursive monadic Datalog classes and examines limits on extending those results. It illustrates these limits with examples involving linear q1, q2, and a tree-packing approach, while noting that q1 and q2 do not capture the full richness of acyclic monadic Datalog.

4 Monadic Datalog: Upper Bounds

  • For non-recursive monadic Datalog, falsity is testable iff the program is equivalent to an α-acyclic non-recursive monadic Datalog program; this fails for non-monadic Datalog.The cited non-monadic example is α-acyclic but equivalent to a conjunctive query whose falsity is not constant query testable with one-sided error.Source: §4 · p. 9

4.1 Strongly Linear Programs

  • Falsity of every strongly linear MDLog program over a binary schema is constant query testable with one-sided error.Strongly linear rule bodies have exactly two variables and no IDB atom uses the head variable; the proof reduces to 2RPQs after eliminating reflexive loops and parallel edges.Source: §4.1 · pp. 10–11

4.2 Simple Branching Programs

  • Falsity of every simple branching program is constant query testable with one-sided error.The proof builds a UCQ from fixed-length S-path queries: ε-farness yields more than (ε/6)|D| fact-disjoint realizations, and the UCQ tester is run with ε′ = ε/12.Source: §4.2 · pp. 12–13, C Proofs for Section 4.2 · p. 32
  • Theorem 4.9’s simple branching class does not settle extensions with constant-length paths or non-distinct relation symbols, which remain difficult to handle.The authors conjecture the result extends to simple branching programs with reflexive loops and multi-edges, but report not knowing how to handle these other extensions.Source: §4.2 · p. 12

4.3 Acyclic Non-Linear Programs Beyond Simple Branching

  • Beyond simple branching programs, testability appears to require removal lemmas for branching subgraphs of varying size; a corresponding directed Steiner-tree packing result remains open.The known 5ℓ + 4 edge-cut condition yields ℓ edge-disjoint Steiner trees in undirected graphs, but the analogous directed packing question is a long-standing open problem.Source: §4.3 · p. 13
  • Because q1 is linear, its falsity is constant query testable using methods similar to those in Section 4.1.The query asks for a path that follows R^- to a and then R to b, so the proposed tree-packing result is unnecessary.Source: §4.3 · p. 14
  • Problem 4.13 asks whether a linear edge-removal threshold for q2 can guarantee many pairwise edge-disjoint trees meeting specified neighborhood sets.A positive answer would allow the authors to show that falsity of q2 is constant query testable; the sets ensure connecting paths have length at least 1.Source: §4.3 · p. 14
  • Lemma 4.14 rules out the proposed packing condition for any threshold function f satisfying f(ℓ) < 2ℓ.This differs from the corresponding form of Menger’s theorem, where the threshold is f(ℓ) = ℓ.Source: §4.3 · p. 14
  • The queries q1 and q2 do not nest branching inside recursion, are expressible as CRPQs, and use only one binary relation symbol.The authors note that acyclic monadic Datalog programs are a richer class than these two queries.Source: §4.3 · p. 14

5 Monadic Datalog: Lower Bounds

For self-join-free Boolean monadic Datalog programs, the section establishes a lower bound: when a program is not equivalent to an α-acyclic program, its falsity is not constant query testable with one-sided error. The proof identifies a chordless cycle or tetra that every derivation must use.

5 Monadic Datalog: Lower Bounds

  • Falsity of a self-join-free Boolean MDLog program not equivalent to an α-acyclic program is not constant query testable with one-sided error.The lower bound permits relations of unrestricted arity.Source: §5 · p. 14
  • The α-acyclic approximation Π* derives only answers of Π, agrees with Π on α-acyclic databases, and is equivalent to Π exactly when Π has an α-acyclic equivalent.Source: §5 · p. 16
  • A rule application uses a pattern when its induced CQ contains a matching cycle or tetra that maps bijectively to that pattern.A crucial set intersects the patterns used by every derivation.Source: §5 · p. 17
  • For such a program, some database and satisfying tuple have a chordless cycle or tetra used by every derivation.Theorem 5.11 makes this pattern crucial for the tuple.Source: §5 · p. 17
  • The proof builds tree-like homomorphic preimages to obtain isomorphic crucial patterns, separates them, then safely identifies them into one crucial pattern.The separation addresses new rule matches that naive identification could create.Source: §5 · pp. 17–18
  • The reduction from falsity testing for a cycle or tetra CQ transfers its instances to Π while preserving farness up to a constant factor.The constructed database has size |D||E|, giving factor 1/|D|.Source: §5 · p. 18

6 Conclusion

The paper establishes constant query testability for non-answers to every 2RPQ and a lower bound for certain recursive MDLog programs. It leaves a large class of recursive, branching MDLog programs open.

6 Conclusion

  • Non-answers to every 2RPQ are constant query testable with one-sided error.Source: §6 · p. 18
  • For self-join-free Boolean MDLog programs not equivalent to an α-acyclic program, falsity is not constant query testable with one-sided error.Source: §6 · p. 18
  • The status of many recursive, branching MDLog programs remains open, and the paper also raises questions about bag versus set semantics.It asks whether lower bounds extend to set semantics and whether set semantics permits testability absent under bag semantics.Source: §6 · p. 18

A Proofs for Section 3

The proof shows that if the database-answer pair is ε-far from falsity of a 2RPQ, then the associated product graph remains reachable after a limited edge deletion. It converts those deletions into database fact deletions to establish the reachability claim.

A Proofs for Section 3

  • If (D,a1a2) is ε-far from non-answerhood, the product graph is ε|Δ|-far from the target set being unreachable from the source set.Source: A Proofs for Section 3 · p. 21
  • The proof orders deleted parallel edges by index and translates each deletion into removing copies of its unique originating database fact.For each fact, it removes at most the number of deleted derived edges or the fact's multiplicity, whichever is smaller.Source: A Proofs for Section 3 · p. 21
  • At most ε|D| facts are removed, so the remaining database still has a query-answer witness, whose product graph lies within the reduced graph and preserves reachability.Source: A Proofs for Section 3 · p. 21

B Proofs for Section 4.1

The proofs develop testability methods for recursive programs across distinct structural cases: gadget reductions encode removed loops or parallel edges, while strongly linear programs whose rule bodies contain neither receive direct one-sided tests. They also specify how completion and size queries on the constructed U support domain-membership testing and degree recovery.

B Proofs for Section 4.1

  • If falsity of Π′ is constant query testable with one-sided error, then falsity of Π is too, via a reduction replacing reflexive loops with an N1-N2 gadget.The gadget returns to the original element exactly when the removed loops hold, and the constructed database has size 3|D|.Source: B Proofs for Section 4.1 · pp. 21–23
  • The same testability transfer holds when Π′ replaces parallel edges in a strongly linear rule with an N1-N2-N3 gadget.The N1 and N3 edges isolate N2 edges per fact, while dummy edges preserve the size-query behavior when the parallel edges are absent.Source: B Proofs for Section 4.1 · pp. 23–25
  • Falsity of a strongly linear MDLog program with no reflexive loops or multi-edges is constant query testable with one-sided error.The proof encodes derivations as accepting walks of a query automaton; strong linearity supplies a simple path through every inner derivation node.Source: B Proofs for Section 4.1 · pp. 26–27
  • For U, completion queries return u or ⊥ based on domain membership, while size queries return 2|D|, deg_D(c), or 0 according to their arguments.U(*,c) returns u exactly when c∈adom(D); U(c,*) returns 2|D| when c=u, and U(*,c) has size deg_D(c) for c∈adom(D).Source: B Proofs for Section 4.1 · pp. 27–28
  • The test for c∈adom(D) uses size queries S(c,*) and S(*,c) for each S∈S, and degree information is obtained in the same way.The size query U(*,*) returns 2|D|.Source: B Proofs for Section 4.1 · p. 28

C Proofs for Section 4.2

These proofs show how to obtain many fact-disjoint realizations of Π, using a set-database 2RPQ argument with product-graph cuts and overlap control, and by ensuring a sufficient supply of required incident facts. They also state a factor-six guarantee for simple branching programs.

Main part

  • If a database is ε-far from falsifying a simple linear program, the proof obtains more than ε|D|/6 fact-disjoint realizations.The argument’s greedy selection loses a factor of 6: a factor of 2 from restricting to paths with limited overlap and a factor of 3 from discarding overlapping partners.Source: C Proofs for Section 4.2 · pp. 30–32

From SLP to 2RPQs

  • The simple linear-program proof replaces Π with a Boolean 2RPQ whose minimal realizations correspond to Π’s realizations, preserving the relevant distance and disjointness properties.This lets the proof transfer the problem to path realizations of the query.Source: C Proofs for Section 4.2 · pp. 28–29

From bag to set

  • The proof encodes each fact multiplicity as indexed relation symbols, producing a multiplicity-one database of the same size and translating fact-disjoint realizations in both directions.Source: C Proofs for Section 4.2 · p. 29

Main part

  • In the product graph, a small edge cut would contradict ε-farness; Menger’s theorem [Men27] then yields many edge-disjoint paths, which overlap control converts into fact-disjoint realizations.Overlaps can arise only through S-facts: each such fact gives one initial and one recurrent S-edge, enabling the proof to retain a large non-overlapping subset.Source: C Proofs for Section 4.2 · pp. 30–31

Lemma 4.11

  • For a simple branching program, if D is ε-far from making Π false, there are more than ε|D|/6 fact-disjoint realizations of Π in D.Source: C Proofs for Section 4.2 · p. 32

C Proofs for Section 4.2

  • An SLP Π′ yields more than m/6 fact-disjoint R1S+T1 paths, which the proof completes into fact-disjoint realizations of Π.For each path, the completion adds incoming Ri-edges and outgoing Tj-edges while preserving fact-disjointness.Source: C Proofs for Section 4.2 · p. 32
  • For each second element c used by n paths, the proof needs at least n facts Ri(*,c) for every 1 < i ≤ k to complete them distinctly.It argues by contradiction: assuming fewer than n such facts, it deletes one R1(b,c) fact and obtains an m-element witness F to non-satisfaction.Source: C Proofs for Section 4.2 · pp. 32–33
  • The witness F must contain every remaining R1(*,c) fact; otherwise D′ minus F would still fail Π, contradicting D′’s minimality.A realization avoiding the deleted fact remains valid, while one using it can replace it with another R1(*,c) fact.Source: C Proofs for Section 4.2 · p. 33
  • Replacing those R1(*,c) facts in F with the assumed fewer Ri(*,c) facts yields an m-sized F′ whose removal still leaves Π satisfied, a contradiction.Any derivation after removing F′ cannot use an R1(*,c) fact, so its homomorphism also gives a derivation after removing F from D′′.Source: C Proofs for Section 4.2 · p. 33

D Proofs for Section 4.3

Lemma 4.14 establishes a lower bound for Problem 4.13: no threshold function below 2ℓ can resolve it. The proof scales a graph whose edge-disjoint tree packing is smaller than the number of removals needed to falsify q2.

D Proofs for Section 4.3

  • Lemma 4.14 rules out resolving the problem with any function f satisfying f(ℓ) < 2ℓ for any ℓ.The constructed graph requires at least 2ℓ edge removals to make q2 false, while its maximum qualifying tree packing has size ℓ.Source: D Proofs for Section 4.3 · p. 33
  • In G1, at least two edge removals are needed to make q2 false, but the graph cannot contain two qualifying trees with pairwise edge-disjoint edges and disjoint specified vertices.The proof uses the directed graph G1 shown in Figure 5.Source: D Proofs for Section 4.3 · p. 33, Figure 5 · p. 34
  • The proof forms Gℓ by replacing each G1 edge with 2ℓ edges through fresh vertices, preserving the obstruction at arbitrary ℓ.In Gℓ, at least 2ℓ edges must be removed to make q2 false.Source: D Proofs for Section 4.3 · p. 33
  • In Gℓ, at most ℓ qualifying trees can be pairwise edge-disjoint and avoid sharing vertices in the specified successor sets.This packing bound yields f(ℓ) ≥ 2ℓ.Source: D Proofs for Section 4.3 · p. 33

E Proof of Theorem 5.4

The proof characterizes the α-acyclic approximation Π*: it is sound on every database, agrees with Π on α-acyclic databases, and captures when Π is equivalent to an α-acyclic program.

E Proof of Theorem 5.4

  • Π is equivalent to an α-acyclic MDLog program exactly when Π is equivalent to Π*.Π*(D) ⊆ Π(D) for every database, while Π(D) ⊆ Π*(D) for α-acyclic databases.Source: E Proof of Theorem 5.4 · p. 34
  • Every derivation from Π* can be converted into one from Π by reversing each rule-body contraction and composing its variable identification with the homomorphism.This establishes Π*(D) ⊆ Π(D) without requiring D to be α-acyclic.Source: E Proof of Theorem 5.4 · p. 34
  • On α-acyclic databases, each derivation is converted by contracting rule bodies and repairing any remaining chordless cycle or tetra.When such a pattern remains, the proof adds an atom supported by a fact in the database that supplies a chord or covers the tetra.Source: E Proof of Theorem 5.4 · pp. 34–35

F Proof of Theorem 5.11

The proof establishes a hard-pattern characterization for self-join-free MDLog programs that are not equivalent to an acyclic program. It also distinguishes the set semantics used for the constructed database from the bag databases relevant to property testing.

F Proof of Theorem 5.11

  • A self-join-free MDLog program not equivalent to an acyclic program has a database, an answer tuple, and a chordless cycle or tetra crucial to that answer.The constructed database needs only fact multiplicities 0 or 1, even though the property-testing proof uses bag databases.Source: F Proof of Theorem 5.11 · p. 35
  • The proof starts from a tree-like database D₀ with an answer in Π(D₀) but not Π*(D₀).D₀-compatibility requires the answer tuple in the root bag and in Π(D), together with a homomorphism from D to D₀ fixing the tuple.Source: F Proof of Theorem 5.11 · pp. 35–36
  • A D₀-compatible database cannot be α-acyclic, since Π and Π* coincide on α-acyclic databases.Otherwise a derivation through Π* would contradict the choice of D₀.Source: F Proof of Theorem 5.11 · p. 36

Obtaining a set of hard patterns

The construction repeatedly unravels a maximal bag type containing a hard pattern, replacing it with smaller types while preserving the proof's invariants. Finiteness of the available types ensures that the process reaches a type whose hard patterns are crucial to the answer.

Obtaining a set of hard patterns

  • The construction replaces each occurrence of the selected maximal type using copies of existing bags or smaller abstract types.Fresh copies are attached along shared elements, and their types are recorded by the typing function.Source: Obtaining a set of hard patterns · pp. 37–38
  • A newly realized hard-pattern type is no greater than a previously realized type containing a hard pattern.This bounds how the set of hard-pattern types changes during unraveling.Source: Obtaining a set of hard patterns · p. 38
  • Each unraveling preserves D₀-compatibility and good typing, while carrying the chosen derivation of the answer into the new database.The new derivation is finite because its branches are no longer than those in the original derivation.Source: Obtaining a set of hard patterns · pp. 38–40
  • The unraveling process terminates at a database and typing function where some hard-pattern type is crucial for the answer.Each step replaces a maximal realized type containing a hard pattern with smaller types; because there are finitely many types, this can happen only finitely often.Source: Obtaining a set of hard patterns · pp. 37, 40

Increasing distance between hard patterns

The procedure reduces the set of crucial hard-pattern types until one remains, then increases the separation between its occurrences. It ends with either a single crucial pattern or patterns at least the chosen distance apart, which are interchangeable by automorphisms.

Increasing distance between hard patterns

  • The procedure yields either one crucial hard pattern or multiple crucial patterns at pairwise distance at least N.The latter patterns also have the same database-scale behavior, with automorphisms mapping any one to any other.Source: Increasing distance between hard… · pp. 41–42
  • The surviving type is concrete, so its crucial bags are fresh copies of one fixed bag in D₀.Strong automorphisms can map any crucial bag to another while preserving the typing and the homomorphism back to D₀.Source: Increasing distance between hard… · pp. 43, 45
  • The inner loop preserves cruciality while removing types that some derivation can avoid, or retaining only a type used by every derivation.Unraveling preserves cruciality for the remaining types; the restart case changes type assignments without changing the database.Source: Increasing distance between hard… · pp. 43–44
  • Each outer-loop iteration at least doubles the minimum distance between distinct surviving-type bags and adds one: d_next ≥ 2d + 1.Thus the procedure reaches the chosen distance N after finitely many restarts, unless only one bag remains first.Source: Increasing distance between hard… · p. 44

Merging hard patterns

The final proof step merges distant crucial patterns into one and preserves its cruciality for the derived answer. Compactness then yields a finite database retaining that answer.

Merging hard patterns

  • Separating crucial bags by at least d + 1 ensures new cycles are too long for rule bodies, so their usable patterns come from D.Here d is the maximum Gaifman diameter of a rule body.Source: Merging hard patterns · pp. 45–46
  • The construction collapses each crucial bag onto B1 using automorphisms, leaving X as the unique surviving hard pattern.The resulting map is a surjective homomorphism, although the merged database is no longer tree-like.Source: Merging hard patterns · p. 46
  • A rule-body homomorphism that leaves B1 can return only through the same element, because its diameter is at most d.Distinct elements of B1 are separated by at least d + 1 in D.Source: Merging hard patterns · p. 46
  • Origins and strong automorphisms lift any derivation in D′ to D, then transfer cruciality to X in D′.The one-bag localization and the absence of new usable patterns ensure the lifted hard-pattern witness maps to X.Source: Merging hard patterns · pp. 46–48
  • The merged database and pattern satisfy Theorem 5.11, and compactness gives a finite subdatabase that still derives the answer.The pattern remains crucial in the merged database.Source: Merging hard patterns · p. 48

G Proof of Lemma 5.12.

This section proves Lemma 5.12 by giving separate reductions for databases with a crucial chordless cycle or tetra. The reductions transfer satisfaction and completion queries between the constructed instances and show that deleting a bounded fraction of facts preserves satisfaction under the stated condition.

Lemma 5.12

  • A crucial chordless cycle or tetra in a satisfying database suffices to make falsity of the Boolean MDLog program not constant query testable with one-sided error.This is the condition and conclusion of Lemma 5.12.Source: G Proof of Lemma 5.12 · p. 48

Chordless-cycle case

  • For a crucial chordless cycle, the proof reduces testing triangle-freeness to testing program falsity, transferring the lower bound for a self-join-free triangle query.The construction encodes triangle edges along the first four cycle constants and closes the remaining cycle using identity links.Source: G Proof of Lemma 5.12 · pp. 49–50

Tetra case

  • For the tetra case, the proof maps database facts to fresh relation symbols, producing a self-join-free Boolean CQ in which the constants of the crucial tetra form a tetra.The map pads images of lower arity with constants so the resulting query has the required form.Source: G Proof of Lemma 5.12 · p. 52
  • The tetra proof reduces testing that constructed query to program falsity by encoding its facts in a new database and preserving the reduction’s testing conditions.Facts using exactly k constants encode input tuples; other facts support a program derivation, and multiplicities are adjusted to |G| per original fact.Source: G Proof of Lemma 5.12 · pp. 52–53

G Proof of Lemma 5.12.

  • A bounded number of size queries suffices to compute the database size and the number of facts added during construction.The count of relevant occurrences is bounded, so the procedure also uses boundedly many queries overall.Source: G Proof of Lemma 5.12 · p. 53
  • For a completion query, the procedure weights each occurrence by its size-query count and selects an occurrence or multiplicity-correction fact accordingly.If the total count is zero it fails; otherwise it constructs a completion, using at most a single call to the oracle for G when needed.Source: G Proof of Lemma 5.12 · pp. 53–54
  • Removing m facts from f(G) corresponds to removing no more than m facts from G, allowing satisfaction to transfer to the resulting structure H.The proof uses homomorphisms between the projected structures and the derivation to establish H |= Π.Source: G Proof of Lemma 5.12 · p. 54
  • G |= q_K if and only if f(G) |= Π, completing the proof of property (i).The forward direction lifts a derivation to f(G); for the reverse, the crucial set K yields a homomorphism from q_K to G.Source: G Proof of Lemma 5.12 · pp. 54–55
  • The crucial tetra in the derivation ensures the constructed map preserves relations, making it a homomorphism from q_K to G.The atom corresponding to each relation in q_K comes from a fact added to f(G), which in turn was generated from a fact in G.Source: G Proof of Lemma 5.12 · p. 54
Loading 2609.03908v1…