Website graphs
Lax117614.WebsiteGraphs · concepts/Lax117614/WebsiteGraphs.lean · lax-117614
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A website graph is a finite structure with a binary relation, the hyperlinks between pages, and three unary relations: the root pages, the target pages, and a marked set of pages whose cardinality is the crawling budget, in unary representation. This is the website of Gauquier, Manolescu and Senellart (EDBT 2026) at unit page costs, the budget being then a number of pages.
Concept map
In the paper
- page 2 of this submission's paper
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Mathlib.ModelTheory.Syntax |
| 3 | import Mathlib.Data.Fintype.Lattice |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Website graphs |
| 8 | type: definition |
| 9 | --- |
| 10 | A website graph is a finite structure with a binary relation, the |
| 11 | hyperlinks between pages, and three unary relations: the root pages, the |
| 12 | target pages, and a marked set of pages whose cardinality is the crawling |
| 13 | budget, in unary representation. This is the website of Gauquier, Manolescu |
| 14 | and Senellart (EDBT 2026) at unit page costs, the budget being then a |
| 15 | number of pages. |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax117614.WebsiteGraphs |
| 19 | |
| 20 | open FirstOrder |
| 21 | |
| 22 | open FirstOrder.Language Structure |
| 23 | |
| 24 | /-- The relation symbols of the language. -/ |
| 25 | inductive siteGraphRel : ℕ → Type where |
| 26 | /-- `edge a b`: a hyperlink from page `a` to page `b`. -/ |
| 27 | | edge : siteGraphRel 2 |
| 28 | /-- `root a`: the page `a` is the crawl's starting point. -/ |
| 29 | | root : siteGraphRel 1 |
| 30 | /-- `target a`: the page `a` must be crawled. -/ |
| 31 | | target : siteGraphRel 1 |
| 32 | /-- `marked a`: the page `a` belongs to the marked set carrying the |
| 33 | budget. -/ |
| 34 | | marked : siteGraphRel 1 |
| 35 | deriving DecidableEq |
| 36 | |
| 37 | /-- The relational language of website graphs: directed links, a root, a set |
| 38 | of target pages, and a marked set whose cardinality is the crawling budget. -/ |
| 39 | def siteGraph : FirstOrder.Language := |
| 40 | ⟨fun _ => Empty, siteGraphRel⟩ |
| 41 | |
| 42 | instance instIsRelationalSiteGraph : FirstOrder.Language.IsRelational siteGraph := fun _ => |
| 43 | (inferInstance : IsEmpty Empty) |
| 44 | |
| 45 | /-- `edge a b`: a hyperlink from page `a` to page `b`. -/ |
| 46 | abbrev wsEdge : siteGraph.Relations 2 := |
| 47 | .edge |
| 48 | |
| 49 | /-- `root a`: the page `a` is the crawl's starting point. -/ |
| 50 | abbrev wsRoot : siteGraph.Relations 1 := |
| 51 | .root |
| 52 | |
| 53 | /-- `target a`: the page `a` must be crawled. -/ |
| 54 | abbrev wsTarget : siteGraph.Relations 1 := |
| 55 | .target |
| 56 | |
| 57 | /-- `marked a`: the page `a` belongs to the marked set carrying the |
| 58 | budget. -/ |
| 59 | abbrev wsMarked : siteGraph.Relations 1 := |
| 60 | .marked |
| 61 | |
| 62 | section Shorthands |
| 63 | |
| 64 | variable {A : Type} [siteGraph.Structure A] |
| 65 | |
| 66 | /-- A hyperlink in a website graph. -/ |
| 67 | def WSEdge (a b : A) : Prop := RelMap wsEdge ![a, b] |
| 68 | |
| 69 | /-- Being the root of a website graph. -/ |
| 70 | def WSRoot (a : A) : Prop := RelMap wsRoot ![a] |
| 71 | |
| 72 | /-- Being a target page. -/ |
| 73 | def WSTarget (a : A) : Prop := RelMap wsTarget ![a] |
| 74 | |
| 75 | /-- Belonging to the marked set carrying the budget. -/ |
| 76 | def WSMarked (a : A) : Prop := RelMap wsMarked ![a] |
| 77 | |
| 78 | end Shorthands |
| 79 | |
| 80 | end Lax117614.WebsiteGraphs |
| 81 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments