Faithful encodings, for counting problems

DescriptiveComplexity.Encoding bundles a concrete instance type with its encoding as a structure and the two size bounds that keep the encoding honest. Its semantic obligation, DescriptiveComplexity.Encoding.Faithful, is stated for decision problems. This file states it for counting problems: DescriptiveComplexity.Encoding.CountFaithful asks the abstract counting problem to return, on every encoded instance, the number the concrete definition returns. The encoding itself, with its size bounds and its computability, is the same object. The converse direction has its counting form too: DescriptiveComplexity.CountDecoding, a computable decoder whose decoded instances have the count of the structure they come from.

def DescriptiveComplexity.Encoding.CountFaithful {L : FirstOrder.Language} {ι : Type u_1} [L.IsRelational] (e : Encoding L ι) (conc : ι → ℕ) (C : CountingProblem L) : Prop

Semantic equivalence for a counting problem: the abstract problem C computes the concrete count conc on every encoded instance.

Equations

• e.CountFaithful conc C = ∀ (i : ι), conc i = C.Count (e.Univ i)

theorem DescriptiveComplexity.Encoding.CountFaithful.support {L : FirstOrder.Language} {ι : Type u_1} [L.IsRelational] {e : Encoding L ι} {conc : ι → ℕ} {C : CountingProblem L} (h : e.CountFaithful conc C) : e.Faithful (fun (i : ι) => 0 < conc i) C.support

A faithful encoding for a counting problem is faithful for its support: the concrete count is positive exactly on the yes-instances.

structure DescriptiveComplexity.CountDecoding (L : FirstOrder.Language) [L.IsRelational] {ι : Type u_1} (W : DecisionProblem L) (conc : ι → ℕ) (C : CountingProblem L) : Type u_1

A computable decoding, for a counting problem: the counterpart of DescriptiveComplexity.Decoding. dec is a computation from presented structures to concrete instances, none on junk; sound says the concrete count of a decoded instance is the abstract count of the structure it came from; total says well-formed nonempty presentations always decode.

• dec : FinPresentation L → Option ι

  The decoder.

• sound (S : FinPresentation L) (i : ι) : i ∈ self.dec S → conc i = C.Count (Fin S.card)

  A decoded instance has the count of the presented structure.

• total (S : FinPresentation L) : 0 < S.card → W.Holds (Fin S.card) → (self.dec S).isSome = true

  Well-formed nonempty presentations always decode.