Counting possible worlds

The counting problem behind query evaluation over an incomplete or probabilistic database, for an arbitrary finite relational schema L.

An instance is a structure over two copies of the schema, L.sum L: the left copy holds the certain facts and the right copy the uncertain ones. A possible world keeps every certain fact and some of the uncertain ones (DescriptiveComplexity.IsWorld); it is a structure over the schema itself (DescriptiveComplexity.worldStructure). For a sentence φ of the schema, DescriptiveComplexity.PossibleWorlds φ is the number of possible worlds in which φ holds.

A world is one relation per symbol of the schema, i.e., an assignment of the block DescriptiveComplexity.worldBlock, and both “this is a world” and “φ holds in it” are first-order in the instance expanded by that block. So the problem is the witness count of a kernel, and is in #P for every sentence whatever (DescriptiveComplexity.possibleWorlds_mem_sharpP): the data complexity of counting the worlds of a first-order query never exceeds #P.

The reading in probabilities: a fact that is uncertain and not certain is open, and an instance with k open facts has 2 ^ k worlds (DescriptiveComplexity.card_isWorld). With each open fact present with probability 1/2, independently, the probability of φ is PossibleWorlds φ / 2 ^ k: the model is a tuple-independent database whose probabilities are 1/2 and 1. Hardness depends on the query, and is the business of DescriptiveComplexity.Examples.ProbabilisticQueries.

Worlds

def DescriptiveComplexity.worldBlock (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] : SOBlock

The block guessing a world: one relation variable per relation symbol of the schema, of the same arity.

Equations

• DescriptiveComplexity.worldBlock L = { ι := (n : ℕ) × L.Relations n, ιFinite := inst✝, arity := fun (p : (n : ℕ) × L.Relations n) => p.fst }

@[instance_reducible]

def DescriptiveComplexity.worldStructure {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [L.IsRelational] (ρ : (worldBlock L).Assignment A) : L.Structure A

The structure over the schema that a family of relations is.

Equations

• DescriptiveComplexity.worldStructure ρ = { funMap := fun {n : ℕ} (f : L.Functions n) => isEmptyElim f, RelMap := fun {n : ℕ} (R : L.Relations n) (x : Fin n → A) => ρ ⟨n, R⟩ x }

def DescriptiveComplexity.IsWorld {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(L.sum L).Structure A] (ρ : (worldBlock L).Assignment A) : Prop

The family of relations ρ is a possible world of the instance: it contains every certain fact, and only certain or uncertain facts.

Equations

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

def DescriptiveComplexity.IsOpenFact {L : FirstOrder.Language} {A : Type} [(L.sum L).Structure A] (q : (p : (n : ℕ) × L.Relations n) × (Fin p.fst → A)) : Prop

A fact that is uncertain and not certain: the facts a world is free to keep or to drop.

Equations

• DescriptiveComplexity.IsOpenFact q = (FirstOrder.Language.Structure.RelMap (Sum.inr q.fst.snd) q.snd ∧ ¬FirstOrder.Language.Structure.RelMap (Sum.inl q.fst.snd) q.snd)

theorem DescriptiveComplexity.card_isWorld {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] {A : Type} [(L.sum L).Structure A] [Finite A] : Nat.card { ρ : (worldBlock L).Assignment A // IsWorld ρ } = 2 ^ Nat.card { q : (p : (n : ℕ) × L.Relations n) × (Fin p.fst → A) // IsOpenFact q }

An instance with k open facts has 2 ^ k possible worlds: a world is a choice among them. So, each open fact being present with probability 1/2 independently of the others, the probability of a sentence is the number of worlds in which it holds, divided by 2 ^ k. Registered in the Lax archive as Lax794877.WorldCount.card_isWorld.

The kernel

@[reducible, inline]

abbrev DescriptiveComplexity.worldLang (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] : FirstOrder.Language

The vocabulary of the kernel: the instance, and the guessed world.

Equations

• DescriptiveComplexity.worldLang L = (L.sum L).sum (DescriptiveComplexity.worldBlock L).lang

@[reducible, inline]

abbrev DescriptiveComplexity.worldSym {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] (p : (n : ℕ) × L.Relations n) : (worldLang L).Relations p.fst

The symbol of the guessed world for a relation symbol of the schema.

Equations

• DescriptiveComplexity.worldSym p = Sum.inr ⟨p, ⋯⟩

def DescriptiveComplexity.toWorld (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] : L →ᴸ worldLang L

Reading a sentence of the schema in the guessed world.

Equations

• DescriptiveComplexity.toWorld L = { onFunction := fun {x : ℕ} (f : L.Functions x) => isEmptyElim f, onRelation := fun {n : ℕ} (R : L.Relations n) => DescriptiveComplexity.worldSym ⟨n, R⟩ }

noncomputable def DescriptiveComplexity.worldSentence (L : FirstOrder.Language) [Finite ((n : ℕ) × L.Relations n)] : (worldLang L).Sentence

The sentence saying that the guessed relations form a possible world.

Equations

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

noncomputable def DescriptiveComplexity.worldKernel {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] (φ : L.Sentence) : (worldLang L).Sentence

The kernel of the problem: the guessed relations form a possible world, in which the sentence holds.

Equations

• DescriptiveComplexity.worldKernel φ = DescriptiveComplexity.worldSentence L ⊓ (DescriptiveComplexity.toWorld L).onSentence φ

The counting problem

noncomputable def DescriptiveComplexity.PossibleWorlds {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] (φ : L.Sentence) : CountingProblem (L.sum L)

Counting possible worlds: the number of possible worlds of the instance in which the sentence φ of the schema holds.

Equations

• DescriptiveComplexity.PossibleWorlds φ = DescriptiveComplexity.CountingProblem.ofKernel (DescriptiveComplexity.worldBlock L) (DescriptiveComplexity.worldKernel φ)

theorem DescriptiveComplexity.possibleWorlds_apply {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] (φ : L.Sentence) (A : Type) [(L.sum L).Structure A] : (PossibleWorlds φ).Count A = Nat.card { ρ : (worldBlock L).Assignment A // IsWorld ρ ∧ A ⊨ φ }

theorem DescriptiveComplexity.possibleWorlds_mem_sharpP {L : FirstOrder.Language} [Finite ((n : ℕ) × L.Relations n)] [L.IsRelational] (φ : L.Sentence) : SharpP.Mem (PossibleWorlds φ)

Counting the possible worlds of a first-order sentence is in #P, whatever the sentence. Registered in the Lax archive as Lax794877.WorldsInSharpP.possibleWorlds_mem_sharpP.