The graph crawling problem
Lax117614.GraphCrawlingProblem · concepts/Lax117614/GraphCrawlingProblem.lean · lax-117614
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A crawl of a website graph is a set of pages containing a root page and every target page, each of its pages reachable from the root by hyperlinks inside the set; this is the node set of a rooted subtree, the crawl of Gauquier, Manolescu and Senellart (EDBT 2026). A website graph has a cheap crawl when it is finite and some crawl has at most as many pages as the marked set has elements, the budget. The graph crawling problem is the decision problem on website graphs whose yes-instances are the website graphs isomorphic to one with a cheap crawl.
Concept map
In the paper
- page 2 of this submission's paper
Lean source view on GitHub
| 1 | import Mathlib.SetTheory.Cardinal.Finite |
| 2 | import Mathlib.ModelTheory.Semantics |
| 3 | import Mathlib.Data.Set.Card |
| 4 | import Mathlib.Data.Set.Finite.Lemmas |
| 5 | import Lax904597.Classes |
| 6 | import Lax799700.Problems |
| 7 | import Lax117614.WebsiteGraphs |
| 8 | |
| 9 | /-! |
| 10 | --- |
| 11 | title: The graph crawling problem |
| 12 | type: definition |
| 13 | --- |
| 14 | A crawl of a website graph is a set of pages containing a root page and |
| 15 | every target page, each of its pages reachable from the root by hyperlinks |
| 16 | inside the set; this is the node set of a rooted subtree, the crawl of |
| 17 | Gauquier, Manolescu and Senellart (EDBT 2026). A website graph has a cheap |
| 18 | crawl when it is finite and some crawl has at most as many pages as the |
| 19 | marked set has elements, the budget. The graph crawling problem is the |
| 20 | decision problem on website graphs whose yes-instances are the website |
| 21 | graphs isomorphic to one with a cheap crawl. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax117614.GraphCrawlingProblem |
| 25 | |
| 26 | open FirstOrder |
| 27 | |
| 28 | open FirstOrder.Language Structure |
| 29 | |
| 30 | open Lax904597.Problems Lax904597.Classes Lax799700.Problems Lax117614.WebsiteGraphs |
| 31 | |
| 32 | section Reachability |
| 33 | |
| 34 | variable {A : Type} |
| 35 | |
| 36 | /-- The directed step available inside a chosen set: an edge whose two |
| 37 | endpoints are both chosen. -/ |
| 38 | def DiLink (Adjp : A → A → Prop) (S : A → Prop) (a b : A) : Prop := |
| 39 | S a ∧ S b ∧ Adjp a b |
| 40 | |
| 41 | /-- Every member of `S` is reachable from `r` by directed steps inside `S` – |
| 42 | the shape of an `r`-rooted subtree with node set `S`, reachability being all a |
| 43 | breadth-first traversal needs to assemble the tree. -/ |
| 44 | def ReachesAllOn (Adjp : A → A → Prop) (r : A) (S : A → Prop) : Prop := |
| 45 | ∀ x, S x → Relation.ReflTransGen (DiLink Adjp S) r x |
| 46 | |
| 47 | end Reachability |
| 48 | |
| 49 | section Generic |
| 50 | |
| 51 | variable {A : Type} |
| 52 | |
| 53 | /-- Some marked root admits a crawl: a set of pages containing the root and |
| 54 | every target, entirely reachable from the root inside itself, of size (the |
| 55 | paper's total cost, at unit page costs) at most the number encoded by the |
| 56 | marked set. -/ |
| 57 | def CrawlOn (Adjp : A → A → Prop) (Rp Tp Kp : A → Prop) : Prop := |
| 58 | ∃ r, Rp r ∧ ∃ S : A → Prop, S r ∧ (∀ x, Tp x → S x) ∧ ReachesAllOn Adjp r S ∧ |
| 59 | {x | S x}.ncard ≤ {x | Kp x}.ncard |
| 60 | |
| 61 | end Generic |
| 62 | |
| 63 | section Problem |
| 64 | |
| 65 | variable (A : Type) [siteGraph.Structure A] |
| 66 | |
| 67 | /-- A website graph admits a crawl within budget: a set of pages containing |
| 68 | the marked root and every target, reachable from the root inside itself, with |
| 69 | at most as many pages as the marked set has elements. (Finiteness of the |
| 70 | universe is part of the property: cardinality thresholds are only meaningful |
| 71 | on finite structures.) -/ |
| 72 | def HasCheapCrawl : Prop := |
| 73 | Finite A ∧ CrawlOn (WSEdge (A := A)) WSRoot WSTarget WSMarked |
| 74 | |
| 75 | end Problem |
| 76 | |
| 77 | /-- GRAPH CRAWLING, decision variant at unit page costs: does the website |
| 78 | graph satisfy `HasCheapCrawl`? -/ |
| 79 | def GraphCrawling : DecisionProblem siteGraph := |
| 80 | DecisionProblem.ofPred HasCheapCrawl |
| 81 | |
| 82 | end Lax117614.GraphCrawlingProblem |
| 83 |
Used by
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments