Packaged crawling instances
Lax117614.CrawlInstances · concepts/Lax117614/CrawlInstances.lean · lax-117614
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A packaged crawling instance is the website as a user handles it: a page count, a finite set of hyperlinks, a root page, a finite set of target pages and a budget, clamped to the page count since a crawl never has more pages than the site. Its size is the textbook one, pages, links, targets and the budget in unary, and its semantics the textbook one, some set of pages containing the root and the targets, reachable from the root inside itself, within budget. The encoder computes the website graph of an instance, on its pages as universe. A presentation is a raw relation table on a finite universe; a presented website is well-formed when it has exactly one root page, which a first-order sentence states, and the decoder reads a packaged instance off a well-formed presented website. Well-formed graph crawling is the graph crawling problem restricted to well-formed website graphs.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Mathlib.ModelTheory.Syntax |
| 3 | import Mathlib.Data.Fintype.Lattice |
| 4 | import Mathlib.Data.Fintype.EquivFin |
| 5 | import Mathlib.Logic.Equiv.Fin.Basic |
| 6 | import Mathlib.Tactic.FinCases |
| 7 | import Lax117614.WebsiteGraphs |
| 8 | import Lax117614.GraphCrawlingProblem |
| 9 | |
| 10 | /-! |
| 11 | --- |
| 12 | title: Packaged crawling instances |
| 13 | type: definition |
| 14 | --- |
| 15 | A packaged crawling instance is the website as a user handles it: a page |
| 16 | count, a finite set of hyperlinks, a root page, a finite set of target pages |
| 17 | and a budget, clamped to the page count since a crawl never has more pages |
| 18 | than the site. Its size is the textbook one, pages, links, targets and the |
| 19 | budget in unary, and its semantics the textbook one, some set of pages |
| 20 | containing the root and the targets, reachable from the root inside itself, |
| 21 | within budget. The encoder computes the website graph of an instance, on its |
| 22 | pages as universe. A presentation is a raw relation table on a finite |
| 23 | universe; a presented website is well-formed when it has exactly one root |
| 24 | page, which a first-order sentence states, and the decoder reads a packaged |
| 25 | instance off a well-formed presented website. Well-formed graph crawling is |
| 26 | the graph crawling problem restricted to well-formed website graphs. |
| 27 | -/ |
| 28 | |
| 29 | namespace Lax117614.CrawlInstances |
| 30 | |
| 31 | open FirstOrder |
| 32 | |
| 33 | open FirstOrder.Language Structure |
| 34 | |
| 35 | open Lax904597.Problems Lax904597.Classes Lax799700.Problems |
| 36 | open Lax117614.WebsiteGraphs Lax117614.GraphCrawlingProblem |
| 37 | |
| 38 | /-- A concretely presented finite `L`-structure: a size and a computable |
| 39 | relation table. This is the input type of decoders – the “raw bytes” a |
| 40 | decoding computation reads. -/ |
| 41 | structure FinPresentation (L : Language.{0, 0}) where |
| 42 | /-- The number of elements. -/ |
| 43 | card : ℕ |
| 44 | /-- The relations, as computations on `Fin card`. -/ |
| 45 | relBool : ∀ {n}, L.Relations n → (Fin n → Fin card) → Bool |
| 46 | |
| 47 | /-- The `L`-structure a presentation presents. -/ |
| 48 | instance FinPresentation.str {L : Language.{0, 0}} [L.IsRelational] (S : FinPresentation L) : |
| 49 | L.Structure (Fin S.card) where |
| 50 | funMap f := isEmptyElim f |
| 51 | RelMap R x := S.relBool R x = true |
| 52 | |
| 53 | /-- A packaged concrete crawling instance: `n + 1` pages, the hyperlinks, the |
| 54 | root page, the target pages, and the budget (clamped to `n + 1` by its type: |
| 55 | a crawl never has more pages than the site). -/ |
| 56 | structure CrawlInstance where |
| 57 | /-- The page count, minus one: pages are `Fin (n + 1)`, so a website is |
| 58 | never empty. -/ |
| 59 | n : ℕ |
| 60 | /-- The hyperlinks. -/ |
| 61 | edges : Finset (Fin (n + 1) × Fin (n + 1)) |
| 62 | /-- The root page, where crawls start. -/ |
| 63 | root : Fin (n + 1) |
| 64 | /-- The target pages. -/ |
| 65 | targets : Finset (Fin (n + 1)) |
| 66 | /-- The budget, clamped by its type: a crawl never has more pages than the |
| 67 | site. -/ |
| 68 | budget : Fin (n + 2) |
| 69 | deriving DecidableEq |
| 70 | |
| 71 | /-- The textbook size of a packaged instance: pages, links, targets, and the |
| 72 | budget in unary. The one audited line of the encoding. -/ |
| 73 | def crawlSize : CrawlInstance → ℕ |
| 74 | | ⟨n, E, _, T, B⟩ => (n + 1) + E.card + T.card + B.1 |
| 75 | |
| 76 | /-- The textbook semantics of a packaged instance: some set of pages |
| 77 | containing the root and every target, each of its pages reachable from the |
| 78 | root by links inside it, within budget. -/ |
| 79 | def ConcreteCrawlHolds : CrawlInstance → Prop |
| 80 | | ⟨n, E, r, T, B⟩ => ∃ S : Finset (Fin (n + 1)), r ∈ S ∧ T ⊆ S ∧ |
| 81 | (∀ v ∈ S, Relation.ReflTransGen (fun a b => a ∈ S ∧ b ∈ S ∧ (a, b) ∈ E) r v) ∧ |
| 82 | S.card ≤ B.1 |
| 83 | |
| 84 | /-- The encoder, standalone and auditable: a plain `def`, so the compiler |
| 85 | vouches that it computes. -/ |
| 86 | def crawlRelBool (i : CrawlInstance) {n : ℕ} (R : siteGraph.Relations n) : |
| 87 | (Fin n → Fin (i.n + 1)) → Bool := |
| 88 | match n, R with |
| 89 | | _, .edge => fun x => decide ((x 0, x 1) ∈ i.edges) |
| 90 | | _, .root => fun x => decide (x 0 = i.root) |
| 91 | | _, .target => fun x => decide (x 0 ∈ i.targets) |
| 92 | | _, .marked => fun x => decide ((x 0).1 < i.budget.1) |
| 93 | |
| 94 | /-- The website graph a packaged instance encodes: the pages themselves as |
| 95 | universe, the relations the encoder's computations read as propositions. -/ |
| 96 | instance crawlStructure (i : CrawlInstance) : siteGraph.Structure (Fin (i.n + 1)) where |
| 97 | funMap f := isEmptyElim f |
| 98 | RelMap R x := crawlRelBool i R x = true |
| 99 | |
| 100 | /-- Well-formedness of a website graph: exactly one root page. What makes an |
| 101 | honest decoder possible. -/ |
| 102 | noncomputable def crawlWFSentence : siteGraph.Sentence := |
| 103 | FirstOrder.Language.Formula.iExs (Fin 1) |
| 104 | (FirstOrder.Language.Relations.formula₁ wsRoot (FirstOrder.Language.Term.var (Sum.inr 0)) ⊓ |
| 105 | FirstOrder.Language.Formula.iAlls (Fin 1) |
| 106 | ((FirstOrder.Language.Relations.formula₁ wsRoot |
| 107 | (FirstOrder.Language.Term.var (Sum.inr 0))).imp |
| 108 | (FirstOrder.Language.Term.equal (FirstOrder.Language.Term.var (Sum.inr 0)) |
| 109 | (FirstOrder.Language.Term.var (Sum.inl (Sum.inr 0)))))) |
| 110 | |
| 111 | section Decoder |
| 112 | |
| 113 | variable (S : FinPresentation siteGraph) |
| 114 | |
| 115 | /-- The root pages of a presented website. -/ |
| 116 | def crawlRoots : Finset (Fin S.card) := |
| 117 | Finset.univ.filter fun x => S.relBool wsRoot ![x] |
| 118 | |
| 119 | /-- Decode a presented website whose unique root has been found: read the |
| 120 | links, targets and budget off the tables, the budget clamped to the page |
| 121 | count as the packaging requires. (The root's existence is what makes the |
| 122 | page count positive.) -/ |
| 123 | def crawlDecodeAt (r : Fin S.card) : CrawlInstance := |
| 124 | ⟨S.card - 1, |
| 125 | Finset.univ.filter fun p : Fin (S.card - 1 + 1) × Fin (S.card - 1 + 1) => |
| 126 | S.relBool wsEdge ![Fin.cast (Nat.succ_pred_eq_of_pos r.pos) p.1, |
| 127 | Fin.cast (Nat.succ_pred_eq_of_pos r.pos) p.2], |
| 128 | Fin.cast (Nat.succ_pred_eq_of_pos r.pos).symm r, |
| 129 | Finset.univ.filter fun x : Fin (S.card - 1 + 1) => |
| 130 | S.relBool wsTarget ![Fin.cast (Nat.succ_pred_eq_of_pos r.pos) x], |
| 131 | ⟨min ((Finset.univ.filter fun x : Fin (S.card - 1 + 1) => |
| 132 | S.relBool wsMarked ![Fin.cast (Nat.succ_pred_eq_of_pos r.pos) x]).card) |
| 133 | (S.card - 1 + 1), by omega⟩⟩ |
| 134 | |
| 135 | /-- The decoder: `none` unless the site has exactly one root. -/ |
| 136 | def crawlDecode : Option CrawlInstance := |
| 137 | match (crawlRoots S).sort (· ≤ ·) with |
| 138 | | [] => none |
| 139 | | [r] => some (crawlDecodeAt S r) |
| 140 | | _ :: _ :: _ => none |
| 141 | |
| 142 | end Decoder |
| 143 | |
| 144 | /-- Graph crawling on well-formed websites: those with exactly one root, the |
| 145 | ones the decoder handles. -/ |
| 146 | def WFGraphCrawling : DecisionProblem siteGraph := |
| 147 | DecisionProblem.ofPred fun (A : Type) [siteGraph.Structure A] => |
| 148 | A ⊨ crawlWFSentence ∧ HasCheapCrawl A |
| 149 | |
| 150 | end Lax117614.CrawlInstances |
| 151 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments