Worked example: web crawling – data acquisition as graph crawling

This file is the library's second tutorial, a companion to DescriptiveComplexity.Examples.ConjunctiveQueries: it walks, step by step, through the addition of a new problem domain, ending in an NP-completeness theorem and a machine-checked concrete encoding. The domain is Web data acquisition: graph crawling, the optimization problem underlying focused crawling of structured documents, formalized by Gauquier–Manolescu–Senellart 2026. A website is a rooted directed graph of pages and hyperlinks; a crawl is an r-rooted subtree; the decision problem asks for a crawl containing every target page within a cost budget. The paper proves this NP-complete (its Prop. 4) already for unit page costs, by reduction from Set Cover; that unit-cost variant is what this file formalizes, following the paper's proof.

The file follows the user-first arc of the conjunctive-query tutorial: start from the concrete problem in the user's own formalism (step 1), construct the encoding with the machinery of DescriptiveComplexity.Encoding – size bounds discharged at construction (step 3) – prove the encoded problem equivalent to the concrete one (step 6), and only then establish the NP-completeness of the encoded variant (steps 7–9), which faithfulness reads back to the concrete instances. Every step exercises machinery the CQ file does not, which is why this example is worth reading second:

• the budget is a cardinality threshold – a number in the unary representation of DescriptiveComplexity.Numbers.Unary, honest here because crawl costs are bounded by the page count – checked by a guessed injection (DescriptiveComplexity.nonempty_embedding_iff_ncard_le);
• the semantics contains a reachability condition, which is not first-order; the membership proof replaces it by a certificate (an order in which every crawled page has a crawled in-neighbor strictly below it), the directed, single-root sibling of the Steiner-tree certificate;
• the hardness reduction is an ordered FO reduction (≤ᶠᵒ[≤]): the paper's budget |U| + B + 1 needs a marked set with exactly one extra element, and a canonical singleton is definable only from an order – the same triage point as for Chromatic Number;
• the concrete instance type is single-sorted with a clamped budget, a second worked instance of DescriptiveComplexity.Encoding after the two-sorted CQ one.

Main results:

• DescriptiveComplexity.GraphCrawling: the bundled decision problem;
• DescriptiveComplexity.graphCrawling_sigmaSODefinable: membership in NP;
• DescriptiveComplexity.setCover_ordered_fo_reduction_graphCrawling : SetCover ≤ᶠᵒ[≤] GraphCrawling: the paper's reduction;
• DescriptiveComplexity.graphCrawling_NP_complete;
• DescriptiveComplexity.crawlEncoding with DescriptiveComplexity.crawlEncoding_faithful: the size-honest concrete encoding and its semantic faithfulness;
• DescriptiveComplexity.crawlDecoding and DescriptiveComplexity.crawlWF_NP_complete: the computable decoding of well-formed (single-root) websites, and completeness restricted to them;
• DescriptiveComplexity.crawlShallow_NP_complete: completeness already on websites of depth 2 whose targets have no out-links, the shape of the paper's hard instances;
• DescriptiveComplexity.quotaCrawling_NP_complete: the variant asking for a crawl of at most B pages containing at least K targets, the quota K carried by a second marked set (step 10).

Step 1: the concrete problem, in the user's own formalism

A user does not start from finite structures: they start from the data of their own development. Here that is a packaged crawling instance – a page count, a set of links, a root, a set of targets, a budget – with the textbook semantics as a plain Lean predicate. Nothing in this step mentions model theory; it is the problem as the paper states it, and it is what the final completeness theorem will be about, through the faithfulness theorem of step 5.

structure DescriptiveComplexity.CrawlInstance : Type

A packaged concrete crawling instance: n + 1 pages, the hyperlinks, the root page, the target pages, and the budget (clamped to n + 1 by its type: a crawl never has more pages than the site).

• n : ℕ

  The page count, minus one: pages are Fin (n + 1), so a website is never empty.

• edges : Finset (Fin (self.n + 1) × Fin (self.n + 1))

  The hyperlinks.

• root : Fin (self.n + 1)

  The root page, where crawls start.

• targets : Finset (Fin (self.n + 1))

  The target pages.

• budget : Fin (self.n + 2)

  The budget, clamped by its type: a crawl never has more pages than the site.

def DescriptiveComplexity.instDecidableEqCrawlInstance.decEq (x✝ x✝¹ : CrawlInstance) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCrawlInstance : DecidableEq CrawlInstance

Equations

• DescriptiveComplexity.instDecidableEqCrawlInstance = DescriptiveComplexity.instDecidableEqCrawlInstance.decEq

def DescriptiveComplexity.crawlSize : CrawlInstance → ℕ

The textbook size of a packaged instance: pages, links, targets, and the budget in unary. The one audited line of the encoding.

Equations

• DescriptiveComplexity.crawlSize { n := n, edges := E, root := root, targets := T, budget := B } = n + 1 + E.card + T.card + ↑B

def DescriptiveComplexity.ConcreteCrawlHolds : CrawlInstance → Prop

The textbook semantics of a packaged instance: some set of pages containing the root and every target, each of its pages reachable from the root by links inside it, within budget.

Equations

• One or more equations did not get rendered due to their size.

Step 2: the vocabulary of website graphs

An instance is a single finite structure: the pages, the directed links, a mark for the root, a mark for the targets, and a marked set whose cardinality is the budget – the unary representation of numbers, as used by Set Cover, Steiner Tree and the other threshold problems of the catalog.

instance FirstOrder.Language.instIsRelationalSiteGraph : Language.siteGraph.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.wsTarget : Language.siteGraph.Relations 1

target a: the page a must be crawled.

Equations

• FirstOrder.Language.wsTarget = FirstOrder.Language.siteGraphRel.target

def FirstOrder.Language.instDecidableEqSiteGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : siteGraphRel a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev FirstOrder.Language.wsEdge : Language.siteGraph.Relations 2

edge a b: a hyperlink from page a to page b.

Equations

• FirstOrder.Language.wsEdge = FirstOrder.Language.siteGraphRel.edge

@[reducible, inline]

abbrev FirstOrder.Language.wsMarked : Language.siteGraph.Relations 1

marked a: the page a belongs to the marked set carrying the budget.

Equations

• FirstOrder.Language.wsMarked = FirstOrder.Language.siteGraphRel.marked

inductive FirstOrder.Language.siteGraphRel : ℕ → Type

The relation symbols of the language.

• edge : siteGraphRel 2

  edge a b: a hyperlink from page a to page b.

• root : siteGraphRel 1

  root a: the page a is the crawl's starting point.

• target : siteGraphRel 1

  target a: the page a must be crawled.

• marked : siteGraphRel 1

  marked a: the page a belongs to the marked set carrying the budget.

@[reducible, inline]

abbrev FirstOrder.Language.wsRoot : Language.siteGraph.Relations 1

root a: the page a is the crawl's starting point.

Equations

• FirstOrder.Language.wsRoot = FirstOrder.Language.siteGraphRel.root

def FirstOrder.Language.siteGraph : Language

The relational language of website graphs: directed links, a root, a set of target pages, and a marked set whose cardinality is the crawling budget.

Equations

• FirstOrder.Language.siteGraph = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.siteGraphRel }

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqSiteGraphRel {a✝ : ℕ} : DecidableEq (siteGraphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqSiteGraphRel = FirstOrder.Language.instDecidableEqSiteGraphRel.decEq

Step 3: the encoding, size bounds discharged at construction

With the vocabulary fixed, the concrete instances are encoded as finite structures using DescriptiveComplexity.Encoding: a computable encoder (crawlRelBool, standalone so it can be audited in isolation) and the bundle whose card_le/le_card fields force the encoding to be size-honest – no padding, no compression – before anything is proved about its meaning.

Two packaging choices are dictated by the machinery:

• the budget is clamped by the type (Fin (n + 2)): a crawl never has more than n + 1 pages, so any larger budget is equivalent to n + 1 – and an unclamped ℕ budget, counted in unary in the size, would break le_card exactly as List-repetition would for CQ atoms. The WLOG is baked into the packaging;
• the budget is counted in unary in crawlSize. This is the unary representation of DescriptiveComplexity.Numbers.Unary, and it is honest here because the clamp keeps the budget below the page count – contrast the weighted problems of DescriptiveComplexity/Encoding/UnaryBlowup.lean, where unary weights are exactly what the size bounds reject.

def DescriptiveComplexity.crawlRelBool (i : CrawlInstance) {n : ℕ} (R : FirstOrder.Language.siteGraph.Relations n) : (Fin n → Fin (i.n + 1)) → Bool

The encoder, standalone and auditable (cf. cqRelBool): a plain def, so the compiler vouches that it computes, and the #guards below run it.

Equations

• DescriptiveComplexity.crawlRelBool i FirstOrder.Language.siteGraphRel.edge = fun (x : Fin 2 → Fin (i.n + 1)) => decide ((x 0, x 1) ∈ i.edges)
• DescriptiveComplexity.crawlRelBool i FirstOrder.Language.siteGraphRel.root = fun (x : Fin 1 → Fin (i.n + 1)) => decide (x 0 = i.root)
• DescriptiveComplexity.crawlRelBool i FirstOrder.Language.siteGraphRel.target = fun (x : Fin 1 → Fin (i.n + 1)) => decide (x 0 ∈ i.targets)
• DescriptiveComplexity.crawlRelBool i FirstOrder.Language.siteGraphRel.marked = fun (x : Fin 1 → Fin (i.n + 1)) => decide (↑(x 0) < ↑i.budget)

def DescriptiveComplexity.crawlEncoding : Encoding FirstOrder.Language.siteGraph CrawlInstance

The encoding of packaged crawling instances by Language.siteGraph-structures: the pages themselves as universe, the budget decoded as the marked initial segment DescriptiveComplexity.initSeg. Both size bounds are discharged at construction.

Equations

• One or more equations did not get rendered due to their size.

Step 4: abstract semantics – rooted reachability, crawls, and their certificates

The paper defines a crawl as an r-rooted subtree of the website; the semantics below phrases “some r-rooted subtree with node set S” as “every node of S is reachable from r by edges inside S” – equivalent, since the parent pointers of a breadth-first traversal assemble any such reachable set into a tree, and it is precisely those parent pointers that the first-order certificate recovers (each non-root node has an in-neighbor strictly closer to the root). Reachability itself is a transitive-closure condition, not first-order; as for connectivity in the Steiner-tree problem, the certificate is what makes the membership proof possible, and it reuses the DescriptiveComplexity.reachIn staging for the distance that Relation.ReflTransGen does not carry.

def DescriptiveComplexity.DiLink {A : Type} (Adjp : A → A → Prop) (S : A → Prop) (a b : A) : Prop

The directed step available inside a chosen set: an edge whose two endpoints are both chosen.

Equations

• DescriptiveComplexity.DiLink Adjp S a b = (S a ∧ S b ∧ Adjp a b)

def DescriptiveComplexity.ReachesAllOn {A : Type} (Adjp : A → A → Prop) (r : A) (S : A → Prop) : Prop

Every member of S is reachable from r by directed steps inside S – the shape of an r-rooted subtree with node set S, reachability being all a breadth-first traversal needs to assemble the tree.

Equations

• DescriptiveComplexity.ReachesAllOn Adjp r S = ∀ (x : A), S x → Relation.ReflTransGen (DescriptiveComplexity.DiLink Adjp S) r x

The crawling property

def DescriptiveComplexity.CrawlOn {A : Type} (Adjp : A → A → Prop) (Rp Tp Kp : A → Prop) : Prop

Some marked root admits a crawl: a set of pages containing the root and every target, entirely reachable from the root inside itself, of size (the paper's total cost, at unit page costs) at most the number encoded by the marked set.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.crawlOn_iff_certificate {A : Type} [Finite A] (Adjp : A → A → Prop) (Rp Tp Kp : A → Prop) : CrawlOn Adjp Rp Tp Kp ↔ ∃ (S : A → Prop), (∀ (x : A), Tp x → S x) ∧ (∃ (Rt : A → Prop), (∃ (x : A), Rt x) ∧ (∀ (x : A), Rt x → Rp x ∧ S x) ∧ (∀ (x y : A), Rt x → Rt y → x = y) ∧ ∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (x : A), S x → ¬Rt x → ∃ (y : A), S y ∧ Adjp y x ∧ Lt y x) ∧ Nonempty ({ x : A // S x } ↪ { x : A // Kp x })

The certified form, with reachability witnessed by an order on the chosen set and the budget by an injection into the marked set: the shape the second-order definition guesses. The root is guessed as a relation constrained to hold of exactly one element, which the object language can express.

theorem DescriptiveComplexity.CrawlOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {RB TB KB : B → Prop} {AdjA : A → A → Prop} {RA TA KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hR : ∀ (b : B), RB b ↔ RA (u b)) (hT : ∀ (b : B), TB b ↔ TA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) (h : CrawlOn AdjB RB TB KB) : CrawlOn AdjA RA TA KA

CrawlOn transports along an equivalence commuting with the four predicates.

theorem DescriptiveComplexity.CrawlOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {RB TB KB : B → Prop} {AdjA : A → A → Prop} {RA TA KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hR : ∀ (b : B), RB b ↔ RA (u b)) (hT : ∀ (b : B), TB b ↔ TA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) : CrawlOn AdjB RB TB KB ↔ CrawlOn AdjA RA TA KA

CrawlOn transports along an equivalence, iff version.

Step 5: isomorphism-invariance and the bundled problem

As always, the invariance proof is a transport of the RelMap shorthands along the isomorphism via the shared relMap_equiv₁/₂ lemmas; the junk conventions were stated with the semantics (a structure marking no root is a no-instance, one marking several is read disjunctively).

def DescriptiveComplexity.WSEdge {A : Type} [FirstOrder.Language.siteGraph.Structure A] (a b : A) : Prop

A hyperlink in a website graph.

Equations

• DescriptiveComplexity.WSEdge a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wsEdge ![a, b]

def DescriptiveComplexity.WSRoot {A : Type} [FirstOrder.Language.siteGraph.Structure A] (a : A) : Prop

Being the root of a website graph.

Equations

• DescriptiveComplexity.WSRoot a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wsRoot ![a]

def DescriptiveComplexity.WSTarget {A : Type} [FirstOrder.Language.siteGraph.Structure A] (a : A) : Prop

Being a target page.

Equations

• DescriptiveComplexity.WSTarget a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wsTarget ![a]

def DescriptiveComplexity.WSMarked {A : Type} [FirstOrder.Language.siteGraph.Structure A] (a : A) : Prop

Belonging to the marked set carrying the budget.

Equations

• DescriptiveComplexity.WSMarked a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wsMarked ![a]

def DescriptiveComplexity.HasCheapCrawl (A : Type) [FirstOrder.Language.siteGraph.Structure A] : Prop

A website graph admits a crawl within budget: a set of pages containing the marked root and every target, reachable from the root inside itself, with at most as many pages as the marked set has elements. (Finiteness of the universe is part of the property: cardinality thresholds are only meaningful on finite structures.)

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.hasCheapCrawl_iso {A B : Type} [FirstOrder.Language.siteGraph.Structure A] [FirstOrder.Language.siteGraph.Structure B] (e : FirstOrder.Language.siteGraph.Equiv A B) : HasCheapCrawl A ↔ HasCheapCrawl B

The crawling property is isomorphism-invariant.

def DescriptiveComplexity.GraphCrawling : DecisionProblem FirstOrder.Language.siteGraph

GRAPH CRAWLING (Gauquier–Manolescu–Senellart 2026, decision variant, unit page costs), as a problem on website graphs: is there a crawl – a set of pages containing the marked root and every target, reachable from the root inside itself – of at most as many pages as the marked set has elements?

Equations

• DescriptiveComplexity.GraphCrawling = { Holds := fun (A : Type) (inst : FirstOrder.Language.siteGraph.Structure A) => DescriptiveComplexity.HasCheapCrawl A, iso_invariant := ⋯ }

Step 6: faithfulness – the encoded problem is the concrete one

The bridge between steps 1 and 5: the abstract problem computes the textbook semantics on every encoded instance (Encoding.Faithful). With the size bounds already discharged by the bundle of step 3, this equivalence is the whole of the encoding obligation – from here on, every theorem about GraphCrawling reads back to the concrete instances. The worked instance and the #guards then run the encoder against a hand computation.

The decoding direction is what well-formedness is for. An abstract structure may mark several roots (read disjunctively by the semantics), and no packaged instance – carrying a single root – transcribes such a structure without deciding which root works, a computation a decoder should not contain. The well-formedness sentence crawlWFSentence (“exactly one root”) removes these, and on well-formed structures a computable decoder crawlDecode exists: find the root, read the links, targets and clamped budget off the tables. It assembles into DescriptiveComplexity.crawlDecoding, runs (#guards below), and step 9 restricts the completeness theorem to well-formed instances accordingly (crawlWF_NP_complete). See DescriptiveComplexity/Decoding.lean for why the bundled computation – and not an ∃-only covering statement – is the meaningful notion.

theorem DescriptiveComplexity.crawlEncoding_faithful : crawlEncoding.Faithful ConcreteCrawlHolds GraphCrawling

The packaged encoding is faithful: the abstract problem GraphCrawling computes the textbook semantics on every encoded instance – obligation (1), with obligation (2) already discharged by the bundle.

As in the CQ tutorial, the encoder can be run: the #guards evaluate the encoded relations of the worked instance against the hand computation.

The well-formedness sentence, its meaning, and the decoder.

noncomputable def DescriptiveComplexity.crawlWFSentence : FirstOrder.Language.siteGraph.Sentence

Well-formedness of a website graph: exactly one root page. What makes an honest decoder possible.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.crawlRoots (S : FinPresentation FirstOrder.Language.siteGraph) : Finset (Fin S.card)

The root pages of a presented website.

Equations

• DescriptiveComplexity.crawlRoots S = {x : Fin S.card | S.relBool FirstOrder.Language.wsRoot ![x] = true}

def DescriptiveComplexity.crawlDecodeAt (S : FinPresentation FirstOrder.Language.siteGraph) (r : Fin S.card) : CrawlInstance

Decode a presented website whose unique root has been found: read the links, targets and budget off the tables, the budget clamped to the page count as the packaging requires. (The root's existence is what makes the page count positive.)

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.crawlDecode (S : FinPresentation FirstOrder.Language.siteGraph) : Option CrawlInstance

The decoder: none unless the site has exactly one root.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.crawlDecode_sound (S : FinPresentation FirstOrder.Language.siteGraph) (i : CrawlInstance) (hi : i ∈ crawlDecode S) : ConcreteCrawlHolds i ↔ GraphCrawling.Holds (Fin S.card)

theorem DescriptiveComplexity.crawlDecode_total (S : FinPresentation FirstOrder.Language.siteGraph) (_hpos : 0 < S.card) (hW : (DecisionProblem.ofSentence crawlWFSentence).Holds (Fin S.card)) : (crawlDecode S).isSome = true

def DescriptiveComplexity.crawlDecoding : Decoding FirstOrder.Language.siteGraph (DecisionProblem.ofSentence crawlWFSentence) ConcreteCrawlHolds GraphCrawling

The computable decoding of well-formed website graphs. Together with crawlEncoding_faithful it closes the loop between the concrete and the abstract problem – a decoder that exists only because well-formedness removed the multi-root structures.

Equations

• DescriptiveComplexity.crawlDecoding = { dec := DescriptiveComplexity.crawlDecode, sound := DescriptiveComplexity.crawlDecode_sound, total := DescriptiveComplexity.crawlDecode_total }

def DescriptiveComplexity.crawlPres : FinPresentation FirstOrder.Language.siteGraph

The worked instance of step 1, presented as raw tables.

Equations

• One or more equations did not get rendered due to their size.

Step 7: membership in NP

NP is defined as Σ₁ second-order definability, so membership means exhibiting a second-order sentence: guess an object-level certificate, check it with a first-order kernel. The certificate is the one of DescriptiveComplexity.crawlOn_iff_certificate: the crawled set, its root, the order witnessing reachability, and the injection witnessing the budget – four relation variables, nine first-order clauses. The construction mirrors the Steiner-tree kernel (DescriptiveComplexity.Problems.Steiner.Membership), with three differences worth spotting: the step clause walks into each crawled page along a directed edge, the guessed root must exist and carry the vocabulary's root mark, and the budget injection is total on the whole crawled set, since the paper's cost counts every crawled page.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCrawlGuessBlockIx : DecidableEq CrawlGuessBlockIx

Equations

• DescriptiveComplexity.instDecidableEqCrawlGuessBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DescriptiveComplexity.kCrSetRel : crawlGuessBlock.lang.Relations 1

The set relation variable.

Equations

• DescriptiveComplexity.kCrSetRel = ⟨DescriptiveComplexity.CrawlGuessBlockIx.set, DescriptiveComplexity.kCrSetRel._proof_1⟩

def DescriptiveComplexity.crawlGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Graph Crawling: the four relation variables it guesses.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.kCrStartRel : crawlGuessBlock.lang.Relations 1

The start relation variable.

Equations

• DescriptiveComplexity.kCrStartRel = ⟨DescriptiveComplexity.CrawlGuessBlockIx.start, DescriptiveComplexity.kCrStartRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.kCrTargetSym : crawlSOLang.Relations 1

The target symbol over the sum.

Equations

• DescriptiveComplexity.kCrTargetSym = Sum.inl FirstOrder.Language.wsTarget

def DescriptiveComplexity.kCrOrderRel : crawlGuessBlock.lang.Relations 2

The order relation variable.

Equations

• DescriptiveComplexity.kCrOrderRel = ⟨DescriptiveComplexity.CrawlGuessBlockIx.order, DescriptiveComplexity.kCrOrderRel._proof_1⟩

def DescriptiveComplexity.kCrInjRel : crawlGuessBlock.lang.Relations 2

The inj relation variable.

Equations

• DescriptiveComplexity.kCrInjRel = ⟨DescriptiveComplexity.CrawlGuessBlockIx.inj, DescriptiveComplexity.kCrInjRel._proof_1⟩

@[instance_reducible]

instance DescriptiveComplexity.instFintypeCrawlGuessBlockIx : Fintype CrawlGuessBlockIx

Equations

• One or more equations did not get rendered due to their size.

inductive DescriptiveComplexity.CrawlGuessBlockIx : Type

The relation variables of the block.

• set : CrawlGuessBlockIx

  The crawled set of pages.

• start : CrawlGuessBlockIx

  The start page of the crawl.

• order : CrawlGuessBlockIx

  The order certifying reachability from the start page.

• inj : CrawlGuessBlockIx

  The injection witnessing the budget.

@[reducible, inline]

abbrev DescriptiveComplexity.kCrInjSym : crawlSOLang.Relations 2

The inj symbol over the sum.

Equations

• DescriptiveComplexity.kCrInjSym = Sum.inr DescriptiveComplexity.kCrInjRel

@[reducible, inline]

abbrev DescriptiveComplexity.kCrEdgeSym : crawlSOLang.Relations 2

The edge symbol over the sum.

Equations

• DescriptiveComplexity.kCrEdgeSym = Sum.inl FirstOrder.Language.wsEdge

@[reducible, inline]

abbrev DescriptiveComplexity.crawlSOLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.crawlSOLang = FirstOrder.Language.siteGraph.sum DescriptiveComplexity.crawlGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kCrMarkedSym : crawlSOLang.Relations 1

The marked symbol over the sum.

Equations

• DescriptiveComplexity.kCrMarkedSym = Sum.inl FirstOrder.Language.wsMarked

@[reducible, inline]

abbrev DescriptiveComplexity.kCrStartSym : crawlSOLang.Relations 1

The start symbol over the sum.

Equations

• DescriptiveComplexity.kCrStartSym = Sum.inr DescriptiveComplexity.kCrStartRel

@[reducible, inline]

abbrev DescriptiveComplexity.kCrOrderSym : crawlSOLang.Relations 2

The order symbol over the sum.

Equations

• DescriptiveComplexity.kCrOrderSym = Sum.inr DescriptiveComplexity.kCrOrderRel

@[reducible, inline]

abbrev DescriptiveComplexity.kCrSetSym : crawlSOLang.Relations 1

The set symbol over the sum.

Equations

• DescriptiveComplexity.kCrSetSym = Sum.inr DescriptiveComplexity.kCrSetRel

@[reducible, inline]

abbrev DescriptiveComplexity.kCrRootSym : crawlSOLang.Relations 1

The root symbol over the sum.

Equations

• DescriptiveComplexity.kCrRootSym = Sum.inl FirstOrder.Language.wsRoot

The clauses

Realization

@[reducible, inline]

abbrev DescriptiveComplexity.CRealize {A : Type} [FirstOrder.Language.siteGraph.Structure A] (ρ : crawlGuessBlock.Assignment A) (φ : crawlSOLang.Sentence) : Prop

Realization at a structure expanded by an assignment of the block.

Equations

• DescriptiveComplexity.CRealize ρ φ = A ⊨ φ

theorem DescriptiveComplexity.graphCrawling_sigmaSODefinable : SigmaSODefinable 1 GraphCrawling

Graph Crawling is Σ₁-definable: guess the crawled set, its root, an order certifying that everything crawled is reachable from the root, and an injection of the crawled set into the marked set, then check the nine conditions first-order.

Step 8: NP-hardness, by reduction from Set Cover

The hardness half follows the paper's proof: a set-cover instance becomes a depth-2 website – a root linking to one page per set of the family, each set page linking to the elements it contains – whose targets are the elements, and a cover of at most B sets is exactly a crawl of at most |U| + B + 1 pages (the root, the chosen sets, and all the elements).

The budget |U| + B + 1 is assembled per tag: the marked set of the produced instance is the elements (on the element tag, |U|), the marked elements of the source (on the set tag, B), and one copy of the minimum of the input's order (on the root tag, 1). The + 1 is why this is an ordered reduction: a marked set with exactly one more element needs a canonical singleton, which only an order provides. The root mark and the root's out-edges are guarded by minimality too, so the junk copies of the root tag are unmarked and edgeless.

Cardinality bookkeeping is by tag slices: a set of interpreted elements that is a per-tag family of subsets of the input has as cardinality the sum of the slices (DescriptiveComplexity.ncard_tagged_eq_sum), and both the crawl produced from a cover and the marked set decompose this way, so both directions of the correctness proof reduce to arithmetic on three slice sizes.

inductive DescriptiveComplexity.CrawlTag : Type

Tags for the interpretation of website graphs in set systems.

• root : CrawlTag

  (root, a): a copy of the crawl root (only the copy of the minimum is marked as root, linked, and counted).

• fam : CrawlTag

  (fam, a): the page of the set a of the family.

• elem : CrawlTag

  (elem, a): the page of the ground element a – a target.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCrawlTag : DecidableEq CrawlTag

Equations

• DescriptiveComplexity.instDecidableEqCrawlTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.instNonemptyCrawlTag : Nonempty CrawlTag

@[instance_reducible]

instance DescriptiveComplexity.instFintypeCrawlTag : Fintype CrawlTag

Equations

• DescriptiveComplexity.instFintypeCrawlTag = { elems := {DescriptiveComplexity.CrawlTag.root, DescriptiveComplexity.CrawlTag.fam, DescriptiveComplexity.CrawlTag.elem}, complete := ⋯ }

@[reducible, inline]

abbrev DescriptiveComplexity.oSSElem : (FirstOrder.Language.setSystem.sum FirstOrder.Language.order).Relations 1

The ground-element symbol over the ordered expansion of set systems.

Equations

• DescriptiveComplexity.oSSElem = Sum.inl FirstOrder.Language.ssElem

@[reducible, inline]

abbrev DescriptiveComplexity.oSSFam : (FirstOrder.Language.setSystem.sum FirstOrder.Language.order).Relations 1

The family symbol over the ordered expansion of set systems.

Equations

• DescriptiveComplexity.oSSFam = Sum.inl FirstOrder.Language.ssFam

@[reducible, inline]

abbrev DescriptiveComplexity.oSSMem : (FirstOrder.Language.setSystem.sum FirstOrder.Language.order).Relations 2

The incidence symbol over the ordered expansion of set systems.

Equations

• DescriptiveComplexity.oSSMem = Sum.inl FirstOrder.Language.ssMem

@[reducible, inline]

abbrev DescriptiveComplexity.oSSMarked : (FirstOrder.Language.setSystem.sum FirstOrder.Language.order).Relations 1

The mark symbol over the ordered expansion of set systems.

Equations

• DescriptiveComplexity.oSSMarked = Sum.inl FirstOrder.Language.ssMarked

noncomputable def DescriptiveComplexity.crawlInterp : FOInterpretation (FirstOrder.Language.setSystem.sum FirstOrder.Language.order) FirstOrder.Language.siteGraph CrawlTag 1

The interpretation producing, from a set system, the depth-2 website of the paper's reduction: the minimum's root copy links to every set of the family, each set links to its elements, the elements are the targets, and the marked set carries |U| + B + 1.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DescriptiveComplexity.crawl_edge_iff {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (t t' : CrawlTag) (w w' : Fin 1 → A) : WSEdge (t, w) (t', w') ↔ t = CrawlTag.root ∧ t' = CrawlTag.fam ∧ (∀ (a : A), w 0 ≤ a) ∧ SSFam (w' 0) ∨ t = CrawlTag.fam ∧ t' = CrawlTag.elem ∧ (SSMem (w' 0) (w 0) ∧ SSFam (w 0)) ∧ SSElem (w' 0)

@[simp]

theorem DescriptiveComplexity.crawl_root_iff {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (t : CrawlTag) (w : Fin 1 → A) : WSRoot (t, w) ↔ t = CrawlTag.root ∧ ∀ (a : A), w 0 ≤ a

@[simp]

theorem DescriptiveComplexity.crawl_target_iff {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (t : CrawlTag) (w : Fin 1 → A) : WSTarget (t, w) ↔ t = CrawlTag.elem ∧ SSElem (w 0)

@[simp]

theorem DescriptiveComplexity.crawl_marked_iff {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (t : CrawlTag) (w : Fin 1 → A) : WSMarked (t, w) ↔ match t with | CrawlTag.root => ∀ (a : A), w 0 ≤ a | CrawlTag.fam => SSMarked (w 0) | CrawlTag.elem => SSElem (w 0)

Counting by tag slices

Correctness

Step 9: completeness

Membership and hardness combine into the completeness theorem – the formalized counterpart of Prop. 4 of Gauquier–Manolescu–Senellart 2026. Through the faithfulness theorem of step 6, it is a statement about the packaged concrete instances of step 1: ConcreteCrawlHolds is decided by a problem that is NP-complete, over an encoding that provably neither pads nor compresses.

theorem DescriptiveComplexity.graphCrawling_mem_NP : NP.Mem GraphCrawling

Graph Crawling is in NP.

theorem DescriptiveComplexity.graphCrawling_NP_hard : NP.Hard GraphCrawling

Graph Crawling is NP-hard: Set Cover, which is NP-hard, reduces to it by an ordered FO reduction.

theorem DescriptiveComplexity.graphCrawling_NP_complete : NP.Complete GraphCrawling

The graph crawling problem is NP-complete (Gauquier–Manolescu–Senellart 2026, Prop. 4). Registered in the Lax archive as Lax117614.GraphCrawlingNPComplete.graphCrawling_NP_complete.

theorem DescriptiveComplexity.crawlWF_NP_complete : NP.Complete (DecisionProblem.ofSentence crawlWFSentence ⊓ GraphCrawling)

Well-formed graph crawling is NP-complete: crawling restricted to websites with exactly one root – the instances the decoder of step 6 handles. Both halves are one-line upgrades of the plain completeness proof (OrderedFOReduction.withInvariant, SigmaSODefinable.inf_ofSentence). Registered in the Lax archive as Lax117614.CrawlDecoding.wfGraphCrawling_NP_complete.

The paper's hard instances are more special than the statement above records: the website produced from a set system has depth 2, and its targets are its leaves. The restriction is again one sentence, invariant on the image of the reduction, so the same two upgrades give NP-completeness on that class.

noncomputable def DescriptiveComplexity.crawlShallowSentence : FirstOrder.Language.siteGraph.Sentence

Shallowness of a website graph: target pages have no out-links, and no path follows three links (every page lies within two links of wherever a path starts). The shape of the instances produced from set systems.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.crawlShallow_NP_complete : NP.Complete (DecisionProblem.ofSentence crawlShallowSentence ⊓ (DecisionProblem.ofSentence crawlWFSentence ⊓ GraphCrawling))

Graph crawling is NP-complete already on shallow websites: depth 2, targets without out-links, a single root – the shape of the hard instances of Gauquier–Manolescu–Senellart 2026, Prop. 4.

Step 10: a variant – reaching a quota of targets

Crawling every target is the problem the reduction of step 8 is about; a focused crawler is more often judged by how many targets a crawl of a given size reaches. The decision variant asks for a crawl of at most B pages containing at least K targets, the quota K being the cardinality of a second marked set: the vocabulary grows by one unary symbol, and the arc of steps 5–9 runs again, compressed. Membership guesses one more injection, from the quota into the crawled targets. Hardness needs no new gadget: marking the targets themselves as the quota turns Graph Crawling into the variant, since a crawl contains as many targets as there are exactly when it contains them all – an order-free reduction, the identity on everything else.

@[reducible, inline]

abbrev FirstOrder.Language.qwEdge : Language.quotaSiteGraph.Relations 2

edge a b: a hyperlink from page a to page b.

Equations

• FirstOrder.Language.qwEdge = FirstOrder.Language.quotaSiteGraphRel.edge

@[reducible, inline]

abbrev FirstOrder.Language.qwRoot : Language.quotaSiteGraph.Relations 1

root a: the page a is the crawl's starting point.

Equations

• FirstOrder.Language.qwRoot = FirstOrder.Language.quotaSiteGraphRel.root

@[reducible, inline]

abbrev FirstOrder.Language.qwTarget : Language.quotaSiteGraph.Relations 1

target a: the page a is a target.

Equations

• FirstOrder.Language.qwTarget = FirstOrder.Language.quotaSiteGraphRel.target

inductive FirstOrder.Language.quotaSiteGraphRel : ℕ → Type

The relation symbols of the language.

• edge : quotaSiteGraphRel 2

  edge a b: a hyperlink from page a to page b.

• root : quotaSiteGraphRel 1

  root a: the page a is the crawl's starting point.

• target : quotaSiteGraphRel 1

  target a: the page a is a target.

• marked : quotaSiteGraphRel 1

  marked a: the page a belongs to the marked set carrying the budget.

• quota : quotaSiteGraphRel 1

  quota a: the page a belongs to the marked set carrying the number of targets to reach.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqQuotaSiteGraphRel {a✝ : ℕ} : DecidableEq (quotaSiteGraphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqQuotaSiteGraphRel = FirstOrder.Language.instDecidableEqQuotaSiteGraphRel.decEq

def FirstOrder.Language.instDecidableEqQuotaSiteGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : quotaSiteGraphRel a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance FirstOrder.Language.instIsRelationalQuotaSiteGraph : Language.quotaSiteGraph.IsRelational

def FirstOrder.Language.quotaSiteGraph : Language

The relational language of website graphs with a quota: the symbols of Language.siteGraph, and a second marked set whose cardinality is the number of targets to reach.

Equations

• FirstOrder.Language.quotaSiteGraph = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.quotaSiteGraphRel }

@[reducible, inline]

abbrev FirstOrder.Language.qwMarked : Language.quotaSiteGraph.Relations 1

marked a: the page a belongs to the marked set carrying the budget.

Equations

• FirstOrder.Language.qwMarked = FirstOrder.Language.quotaSiteGraphRel.marked

@[reducible, inline]

abbrev FirstOrder.Language.qwQuota : Language.quotaSiteGraph.Relations 1

quota a: the page a belongs to the marked set carrying the number of targets to reach.

Equations

• FirstOrder.Language.qwQuota = FirstOrder.Language.quotaSiteGraphRel.quota

The quota semantics and its certificate

def DescriptiveComplexity.QuotaCrawlOn {A : Type} (Adjp : A → A → Prop) (Rp Tp Kp Qp : A → Prop) : Prop

Some marked root admits a crawl reaching the quota: a set of pages containing the root, entirely reachable from it inside itself, of at most as many pages as Kp has elements, and containing at least as many targets as Qp has elements.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.quotaCrawlOn_iff_certificate {A : Type} [Finite A] (Adjp : A → A → Prop) (Rp Tp Kp Qp : A → Prop) : QuotaCrawlOn Adjp Rp Tp Kp Qp ↔ ∃ (S : A → Prop), (∃ (Rt : A → Prop), (∃ (x : A), Rt x) ∧ (∀ (x : A), Rt x → Rp x ∧ S x) ∧ (∀ (x y : A), Rt x → Rt y → x = y) ∧ ∃ (Lt : A → A → Prop), (∀ (x y z : A), Lt x y → Lt y z → Lt x z) ∧ (∀ (x : A), ¬Lt x x) ∧ ∀ (x : A), S x → ¬Rt x → ∃ (y : A), S y ∧ Adjp y x ∧ Lt y x) ∧ Nonempty ({ x : A // S x } ↪ { x : A // Kp x }) ∧ Nonempty ({ x : A // Qp x } ↪ { x : A // S x ∧ Tp x })

The certified form: the certificate of crawlOn_iff_certificate, with the targets no longer required to be crawled, and a second injection, of the quota into the crawled targets.

theorem DescriptiveComplexity.QuotaCrawlOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {RB TB KB QB : B → Prop} {AdjA : A → A → Prop} {RA TA KA QA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hR : ∀ (b : B), RB b ↔ RA (u b)) (hT : ∀ (b : B), TB b ↔ TA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) (hQ : ∀ (b : B), QB b ↔ QA (u b)) (h : QuotaCrawlOn AdjB RB TB KB QB) : QuotaCrawlOn AdjA RA TA KA QA

QuotaCrawlOn transports along an equivalence commuting with the five predicates.

theorem DescriptiveComplexity.QuotaCrawlOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {RB TB KB QB : B → Prop} {AdjA : A → A → Prop} {RA TA KA QA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hR : ∀ (b : B), RB b ↔ RA (u b)) (hT : ∀ (b : B), TB b ↔ TA (u b)) (hK : ∀ (b : B), KB b ↔ KA (u b)) (hQ : ∀ (b : B), QB b ↔ QA (u b)) : QuotaCrawlOn AdjB RB TB KB QB ↔ QuotaCrawlOn AdjA RA TA KA QA

QuotaCrawlOn transports along an equivalence, iff version.

The bundled problem

def DescriptiveComplexity.QWRoot {A : Type} [FirstOrder.Language.quotaSiteGraph.Structure A] (a0 : A) : Prop

root a: the page a is the crawl's starting point.

Equations

• DescriptiveComplexity.QWRoot a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qwRoot ![a0]

def DescriptiveComplexity.QWQuota {A : Type} [FirstOrder.Language.quotaSiteGraph.Structure A] (a0 : A) : Prop

quota a: the page a belongs to the marked set carrying the number of targets to reach.

Equations

• DescriptiveComplexity.QWQuota a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qwQuota ![a0]

def DescriptiveComplexity.QWMarked {A : Type} [FirstOrder.Language.quotaSiteGraph.Structure A] (a0 : A) : Prop

marked a: the page a belongs to the marked set carrying the budget.

Equations

• DescriptiveComplexity.QWMarked a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qwMarked ![a0]

def DescriptiveComplexity.QWTarget {A : Type} [FirstOrder.Language.quotaSiteGraph.Structure A] (a0 : A) : Prop

target a: the page a is a target.

Equations

• DescriptiveComplexity.QWTarget a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qwTarget ![a0]

def DescriptiveComplexity.QWEdge {A : Type} [FirstOrder.Language.quotaSiteGraph.Structure A] (a0 a1 : A) : Prop

edge a b: a hyperlink from page a to page b.

Equations

• DescriptiveComplexity.QWEdge a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qwEdge ![a0, a1]

def DescriptiveComplexity.HasQuotaCrawl (A : Type) [FirstOrder.Language.quotaSiteGraph.Structure A] : Prop

A website graph with a quota admits a crawl within budget reaching the quota.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.hasQuotaCrawl_iso {A B : Type} [FirstOrder.Language.quotaSiteGraph.Structure A] [FirstOrder.Language.quotaSiteGraph.Structure B] (e : FirstOrder.Language.quotaSiteGraph.Equiv A B) : HasQuotaCrawl A ↔ HasQuotaCrawl B

The quota-crawling property is isomorphism-invariant.

def DescriptiveComplexity.QuotaCrawling : DecisionProblem FirstOrder.Language.quotaSiteGraph

GRAPH CRAWLING WITH A QUOTA (unit page costs): is there a crawl – a set of pages containing the marked root, reachable from it inside itself – of at most as many pages as the marked set has elements, containing at least as many targets as the quota set has elements?

Equations

• DescriptiveComplexity.QuotaCrawling = { Holds := fun (A : Type) (inst : FirstOrder.Language.quotaSiteGraph.Structure A) => DescriptiveComplexity.HasQuotaCrawl A, iso_invariant := ⋯ }

Membership in NP

@[reducible, inline]

abbrev DescriptiveComplexity.kQcOrderSym : quotaSOLang.Relations 2

The order symbol over the sum.

Equations

• DescriptiveComplexity.kQcOrderSym = Sum.inr DescriptiveComplexity.kQcOrderRel

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqQuotaGuessBlockIx : DecidableEq QuotaGuessBlockIx

Equations

• DescriptiveComplexity.instDecidableEqQuotaGuessBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev DescriptiveComplexity.kQcQuotaSym : quotaSOLang.Relations 1

The quota symbol over the sum.

Equations

• DescriptiveComplexity.kQcQuotaSym = Sum.inl FirstOrder.Language.qwQuota

def DescriptiveComplexity.kQcPickRel : quotaGuessBlock.lang.Relations 2

The pick relation variable.

Equations

• DescriptiveComplexity.kQcPickRel = ⟨DescriptiveComplexity.QuotaGuessBlockIx.pick, DescriptiveComplexity.kQcPickRel._proof_1⟩

def DescriptiveComplexity.quotaGuessBlock : SOBlock

The existential block of the Σ₁ definition of quota crawling: the four relation variables of crawlGuessBlock, and the injection of the quota into the crawled targets.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev DescriptiveComplexity.kQcPickSym : quotaSOLang.Relations 2

The pick symbol over the sum.

Equations

• DescriptiveComplexity.kQcPickSym = Sum.inr DescriptiveComplexity.kQcPickRel

@[instance_reducible]

instance DescriptiveComplexity.instFintypeQuotaGuessBlockIx : Fintype QuotaGuessBlockIx

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev DescriptiveComplexity.kQcInjSym : quotaSOLang.Relations 2

The inj symbol over the sum.

Equations

• DescriptiveComplexity.kQcInjSym = Sum.inr DescriptiveComplexity.kQcInjRel

inductive DescriptiveComplexity.QuotaGuessBlockIx : Type

The relation variables of the block.

• set : QuotaGuessBlockIx

  The crawled set of pages.

• start : QuotaGuessBlockIx

  The start page of the crawl.

• order : QuotaGuessBlockIx

  The order certifying reachability from the start page.

• inj : QuotaGuessBlockIx

  The injection witnessing the budget.

• pick : QuotaGuessBlockIx

  The injection witnessing the quota.

@[reducible, inline]

abbrev DescriptiveComplexity.kQcRootSym : quotaSOLang.Relations 1

The root symbol over the sum.

Equations

• DescriptiveComplexity.kQcRootSym = Sum.inl FirstOrder.Language.qwRoot

@[reducible, inline]

abbrev DescriptiveComplexity.kQcStartSym : quotaSOLang.Relations 1

The start symbol over the sum.

Equations

• DescriptiveComplexity.kQcStartSym = Sum.inr DescriptiveComplexity.kQcStartRel

@[reducible, inline]

abbrev DescriptiveComplexity.kQcMarkedSym : quotaSOLang.Relations 1

The marked symbol over the sum.

Equations

• DescriptiveComplexity.kQcMarkedSym = Sum.inl FirstOrder.Language.qwMarked

@[reducible, inline]

abbrev DescriptiveComplexity.quotaSOLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.quotaSOLang = FirstOrder.Language.quotaSiteGraph.sum DescriptiveComplexity.quotaGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.kQcTargetSym : quotaSOLang.Relations 1

The target symbol over the sum.

Equations

• DescriptiveComplexity.kQcTargetSym = Sum.inl FirstOrder.Language.qwTarget

def DescriptiveComplexity.kQcOrderRel : quotaGuessBlock.lang.Relations 2

The order relation variable.

Equations

• DescriptiveComplexity.kQcOrderRel = ⟨DescriptiveComplexity.QuotaGuessBlockIx.order, DescriptiveComplexity.kQcOrderRel._proof_1⟩

def DescriptiveComplexity.kQcStartRel : quotaGuessBlock.lang.Relations 1

The start relation variable.

Equations

• DescriptiveComplexity.kQcStartRel = ⟨DescriptiveComplexity.QuotaGuessBlockIx.start, DescriptiveComplexity.kQcStartRel._proof_1⟩

def DescriptiveComplexity.kQcSetRel : quotaGuessBlock.lang.Relations 1

The set relation variable.

Equations

• DescriptiveComplexity.kQcSetRel = ⟨DescriptiveComplexity.QuotaGuessBlockIx.set, DescriptiveComplexity.kQcSetRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.kQcSetSym : quotaSOLang.Relations 1

The set symbol over the sum.

Equations

• DescriptiveComplexity.kQcSetSym = Sum.inr DescriptiveComplexity.kQcSetRel

@[reducible, inline]

abbrev DescriptiveComplexity.kQcEdgeSym : quotaSOLang.Relations 2

The edge symbol over the sum.

Equations

• DescriptiveComplexity.kQcEdgeSym = Sum.inl FirstOrder.Language.qwEdge

def DescriptiveComplexity.kQcInjRel : quotaGuessBlock.lang.Relations 2

The inj relation variable.

Equations

• DescriptiveComplexity.kQcInjRel = ⟨DescriptiveComplexity.QuotaGuessBlockIx.inj, DescriptiveComplexity.kQcInjRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.QRealize {A : Type} [FirstOrder.Language.quotaSiteGraph.Structure A] (ρ : quotaGuessBlock.Assignment A) (φ : quotaSOLang.Sentence) : Prop

Realization at a structure expanded by an assignment of the block.

Equations

• DescriptiveComplexity.QRealize ρ φ = A ⊨ φ

theorem DescriptiveComplexity.quotaCrawling_sigmaSODefinable : SigmaSODefinable 1 QuotaCrawling

Quota crawling is Σ₁-definable: the certificate of Graph Crawling, without the requirement that every target be crawled, and with a second injection, of the quota into the crawled targets.

NP-hardness, by reduction from Graph Crawling

def DescriptiveComplexity.quotaInterp : FOInterpretation FirstOrder.Language.siteGraph FirstOrder.Language.quotaSiteGraph Unit 1

The interpretation marking the targets as the quota, and copying everything else.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.quotaCrawling_mem_NP : NP.Mem QuotaCrawling

Quota crawling is in NP.

theorem DescriptiveComplexity.quotaCrawling_NP_hard : NP.Hard QuotaCrawling

Quota crawling is NP-hard: Graph Crawling reduces to it.

theorem DescriptiveComplexity.quotaCrawling_NP_complete : NP.Complete QuotaCrawling

Graph crawling with a quota is NP-complete: deciding whether some crawl of at most B pages contains at least K targets.