A concrete probabilistic database

Lax794877.ExampleDatabase · concepts/Lax794877/ExampleDatabase.lean · lax-794877

definition

Loading review…

Natural Language Statement

Definition

A probabilistic database over the schema $R$ , $S$ , $T$ has $n$ constants and, for every possible fact, a status: absent, certain, or uncertain with a weight of presence and a weight of absence, both below $2^n$ . A world gives every fact a truth value admitted by its status, and has the product of the weights of its uncertain facts as its weight. The count of the database is the sum of the weights of the worlds in which $h_0$ holds, and its total the sum of the weights of all worlds; both are computed by enumerating the worlds. The database is encoded as a weighted instance on its constants, which serve as bit positions in their own order.

Concept map

14 concepts; 7 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Tactic.FinCases
2	import Mathlib.Data.Fintype.BigOperators
3	import Mathlib.Order.Lattice.Nat
4	import Mathlib.Data.Set.Card
5	import Mathlib.ModelTheory.Order
6	import Mathlib.ModelTheory.Semantics
7	import Mathlib.ModelTheory.Complexity
8	import Mathlib.Order.PiLex
9	import Mathlib.Data.Prod.Lex
10	import Mathlib.Data.Fintype.EquivFin
11	import Mathlib.Logic.Equiv.Fin.Basic
12	import Mathlib.Data.Finite.Sigma
13	import Mathlib.Data.Fintype.Lattice
14	import Mathlib.Data.Fintype.Pigeonhole
15	import Mathlib.Dynamics.FixedPoints.Basic
16	import Mathlib.Algebra.BigOperators.Finprod
17	import Mathlib.Algebra.Order.BigOperators.Group.Finset
18	import Mathlib.ModelTheory.Syntax
19	import Mathlib.Data.Fintype.Card
20	import Mathlib.SetTheory.Cardinal.Finite
21	import Mathlib.Data.Finset.Max
22	import Mathlib.Logic.Equiv.Prod
23	import Mathlib.Algebra.BigOperators.Group.Finset.Basic
24	import Mathlib.Algebra.BigOperators.Pi
25	import Mathlib.Algebra.BigOperators.Ring.Finset
26	import Mathlib.Algebra.BigOperators.Field
27	import Mathlib.Algebra.Order.BigOperators.Ring.Finset
28	import Mathlib.Algebra.Order.Ring.Rat
29	import Mathlib.Algebra.Order.Field.Basic
30	import Mathlib.Data.Fintype.Pi
31	import Mathlib.Tactic.Linarith
32	import Mathlib.Tactic.FieldSimp
33	import Mathlib.Tactic.Ring
34	import Mathlib.Data.Set.Finite.Lemmas
35	import Mathlib.Algebra.Group.Action.Defs
36	import Mathlib.ModelTheory.Graph
37	import Mathlib.Data.Fintype.Sort
38	import Mathlib.Order.Hom.Set
39	import Mathlib.Algebra.BigOperators.Fin
40	import Mathlib.Data.Nat.Bitwise
41	import Lax794877.WeightedWorlds
42	import Lax794877.Queries
43
44	/-!
45	---
46	title: A concrete probabilistic database
47	type: definition
48	---
49	A probabilistic database over the schema $R$ , $S$ , $T$ has $n$ constants
50	and, for every possible fact, a status: absent, certain, or uncertain with a
51	weight of presence and a weight of absence, both below $2^n$ . A world gives
52	every fact a truth value admitted by its status, and has the product of the
53	weights of its uncertain facts as its weight. The count of the database is
54	the sum of the weights of the worlds in which $h_0$ holds, and its total the
55	sum of the weights of all worlds; both are computed by enumerating the
56	worlds. The database is encoded as a weighted instance on its constants,
57	which serve as bit positions in their own order.
58	-/
59
60	namespace Lax794877.ExampleDatabase
61
62	open FirstOrder
63
64	open Language Structure
65
66	/-- What a database says of a fact: it is absent, it is certain, or it is
67	uncertain with weights `a` and `c`, i.e., present with probability
68	`a / (a + c)`. -/
69	inductive FactStatus : Type
70	/-- The fact is not in the database. -/
71	\| absent : FactStatus
72	/-- The fact is in the database for sure. -/
73	\| certain : FactStatus
74	/-- The fact is present with weight `a` and absent with weight `c`. -/
75	\| uncertain (a c : ℕ) : FactStatus
76	deriving DecidableEq
77
78	namespace FactStatus
79
80	/-- The fact is certain. -/
81	def isCert : FactStatus → Bool
82	\| certain => true
83	\| _ => false
84
85	/-- The fact is uncertain. -/
86	def isUnc : FactStatus → Bool
87	\| uncertain _ _ => true
88	\| _ => false
89
90	/-- The weight of presence of an uncertain fact (and `0` otherwise). -/
91	def presW : FactStatus → ℕ
92	\| uncertain a _ => a
93	\| _ => 0
94
95	/-- The weight of absence of an uncertain fact (and `0` otherwise). -/
96	def absW : FactStatus → ℕ
97	\| uncertain _ c => c
98	\| _ => 0
99
100	end FactStatus
101
102	/-- A probabilistic database over the schema `R`, `S`, `T`, with `n`
103	constants: the status of every possible fact. The weights are written in
104	binary on `n` bits, so they are below `2 ^ n`. -/
105	structure ProbDb where
106	/-- The number of constants. -/
107	n : ℕ
108	/-- The status of the fact `R(x)`. -/
109	r : Fin n → FactStatus
110	/-- The status of the fact `S(x, y)`. -/
111	s : Fin n → Fin n → FactStatus
112	/-- The status of the fact `T(y)`. -/
113	t : Fin n → FactStatus
114	/-- The weights of the `R`-facts fit in `n` bits. -/
115	fits_r : ∀ x, (r x).presW < 2 ^ n ∧ (r x).absW < 2 ^ n
116	/-- The weights of the `S`-facts fit in `n` bits. -/
117	fits_s : ∀ x y, (s x y).presW < 2 ^ n ∧ (s x y).absW < 2 ^ n
118	/-- The weights of the `T`-facts fit in `n` bits. -/
119	fits_t : ∀ y, (t y).presW < 2 ^ n ∧ (t y).absW < 2 ^ n
120
121	namespace FactStatus
122
123	/-- A world may give the fact the truth value `b`: an absent fact is false, a
124	certain fact is true, an uncertain fact is either. -/
125	def admits : FactStatus → Bool → Bool
126	\| absent, b => !b
127	\| certain, b => b
128	\| uncertain _ _, _ => true
129
130	/-- The weight the fact contributes to a world giving it the truth value `b`:
131	its weight of presence or of absence if it is uncertain, and `1` otherwise. -/
132	def weight : FactStatus → Bool → ℕ
133	\| uncertain a c, b => if b then a else c
134	\| _, _ => 1
135
136	end FactStatus
137
138	/-- A world over `n` constants: the truth value of every possible fact. -/
139	abbrev World (n : ℕ) : Type := (Fin n → Bool) × (Fin n → Fin n → Bool) × (Fin n → Bool)
140
141	namespace ProbDb
142
143	variable (i : ProbDb)
144
145	/-- The world is a possible world of the database. -/
146	def Valid (W : World i.n) : Prop :=
147	(∀ x, (i.r x).admits (W.1 x) = true) ∧ (∀ x y, (i.s x y).admits (W.2.1 x y) = true) ∧
148	∀ y, (i.t y).admits (W.2.2 y) = true
149
150	instance instDecidableValid (W : World i.n) : Decidable (i.Valid W) := by
151	unfold Valid
152	infer_instance
153
154	/-- The weight of a world: the product of the weights of the facts. -/
155	def weight (W : World i.n) : ℕ :=
156	(∏ x, (i.r x).weight (W.1 x)) * ((∏ x, ∏ y, (i.s x y).weight (W.2.1 x y)) *
157	∏ y, (i.t y).weight (W.2.2 y))
158
159	end ProbDb
160
161	/-- The query `h₀` holds in a world. -/
162	def HoldsH0 {n : ℕ} (W : World n) : Prop :=
163	∃ x y, W.1 x = true ∧ W.2.1 x y = true ∧ W.2.2 y = true
164
165	instance {n : ℕ} (W : World n) : Decidable (HoldsH0 W) := by
166	unfold HoldsH0
167	infer_instance
168
169	/-- The concrete weighted count of `h₀`: the sum of the weights of the
170	possible worlds of the database in which the query holds. -/
171	def ProbDb.count (i : ProbDb) : ℕ :=
172	∑ W : World i.n, if i.Valid W ∧ HoldsH0 W then i.weight W else 0
173
174	/-- The weighted count of all the possible worlds: the denominator of the
175	probability. -/
176	def ProbDb.total (i : ProbDb) : ℕ :=
177	∑ W : World i.n, if i.Valid W then i.weight W else 0
178
179	open Lax794877.WeightedWorlds Lax794877.Queries
180
181	/-- The relations of the encoded database: the status of each fact, the binary
182	digits of its weights, and the order of the constants. -/
183	def probDbRel (i : ProbDb) : ∀ {n}, (weightedLang rst).Relations n → (Fin n → Fin i.n) → Bool :=
184	fun {n} R =>
185	match n, R with
186	\| _, .cert .r => fun x => (i.r (x 0)).isCert
187	\| _, .cert .s => fun x => (i.s (x 0) (x 1)).isCert
188	\| _, .cert .t => fun x => (i.t (x 0)).isCert
189	\| _, .unc .r => fun x => (i.r (x 0)).isUnc
190	\| _, .unc .s => fun x => (i.s (x 0) (x 1)).isUnc
191	\| _, .unc .t => fun x => (i.t (x 0)).isUnc
192	\| _, .pres .r => fun x => (i.r (x 0)).presW.testBit (x 1).1
193	\| _, .pres .s => fun x => (i.s (x 0) (x 1)).presW.testBit (x 2).1
194	\| _, .pres .t => fun x => (i.t (x 0)).presW.testBit (x 1).1
195	\| _, .abs .r => fun x => (i.r (x 0)).absW.testBit (x 1).1
196	\| _, .abs .s => fun x => (i.s (x 0) (x 1)).absW.testBit (x 2).1
197	\| _, .abs .t => fun x => (i.t (x 0)).absW.testBit (x 1).1
198	\| _, .le => fun x => decide (x 0 ≤ x 1)
199
200	/-- The encoded database: the weighted instance on the constants. -/
201	def probDbStructure (i : ProbDb) : (weightedLang rst).Structure (Fin i.n) where
202	funMap f := isEmptyElim f
203	RelMap R x := probDbRel i R x = true
204
205	end Lax794877.ExampleDatabase
206

Builds on

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

A concrete probabilistic database

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments