Well-formed instances and computable decodings

The decoding direction of an encoding (DescriptiveComplexity.Encoding): membership results transfer to the concrete problem along a faithful encoding for free, but reading a hardness theorem back to concrete data needs a converse – the abstract problem must not be hard only on junk structures the encoding never produces. This file makes that converse checkable, in two independent, composable pieces designed to keep the user-facing work minimal.

Well-formedness is a decision problem. The junk-free structures are cut out by an isomorphism-invariant property W – typically a plain first-order sentence, bundled by DescriptiveComplexity.DecisionProblem.ofSentence so that invariance comes for free. Hardness on well-formed instances then needs no new framework at all: it is ordinary hardness of the conjunction W ⊓ P (pointwise ∧, the Min instance below), and the library's existing machinery applies to it unchanged. A user upgrades an existing completeness proof with two one-liners:

• hardness: a reduction into P whose images are all well-formed is a reduction into W ⊓ P – DescriptiveComplexity.FOReduction.withInvariant / DescriptiveComplexity.OrderedFOReduction.withInvariant turn the existing reduction plus an image lemma into the strengthened one;
• membership: DescriptiveComplexity.SigmaSODefinable.inf_ofSentence conjoins the sentence W into the existing Σ₁ kernel.

The choice of W is self-policing: chosen too narrow, the hardness reduction cannot land in it; chosen too wide, the decoding below cannot handle it. Both failure modes are proofs that do not close, never silent unsoundness.

Decodings are computations. The lesson of DescriptiveComplexity.Encoding.CoversUpTo's removal is that an existential decoding statement (∀ A, ∃ i, Conc i ↔ P A) is classically near-vacuous: casing on P A discharges it with no decoding whatsoever, whenever the concrete type has one yes- and one no-instance. The honest content is a function, so DescriptiveComplexity.Decoding bundles one, with the same computability hygiene as encoders: a plain def

• dec : FinPresentation L → Option ι – from concretely presented finite structures (DescriptiveComplexity.FinPresentation: a size and a Bool-valued relation table) to concrete instances, none being the junk case, so no proof-carrying arguments and no partiality tricks;
• sound – whatever dec returns is decided by Conc exactly as the presented structure is by P;
• total – on well-formed (nonempty) presentations, dec returns something.

Because dec is Option-valued and computable, it can be run: #guards can test a decoder on small presentations exactly as they test encoders, and the compiler rejects a decoder whose data decides an undecidable predicate. The residual gap is also the same as for encoders: computability is enforced, a complexity bound is not (a decoder may brute-force the answer); that would need the machine bridge (ROADMAP.md §7).

The Prop-level consequence – every well-formed finite structure is semantically a concrete instance – is DescriptiveComplexity.Decoding.exists_conc_iff; unlike its removed predecessor it cannot be established by classical casing, because it is derived from the bundled function.

Worked decoders are in the two tutorials (DescriptiveComplexity.Examples.ConjunctiveQueries, DescriptiveComplexity.Examples.GraphCrawling); the crawling one exists only thanks to well-formedness – on structures marking several roots no honest decoder can choose without computing reachability, and W (“exactly one root”) is what removes them.

Main declarations

• DescriptiveComplexity.DecisionProblem.ofSentence: a first-order sentence as a decision problem, the usual shape of a well-formedness condition;
• the Min instance on DescriptiveComplexity.DecisionProblem, giving the restriction W ⊓ P;
• DescriptiveComplexity.FOReduction.withInvariant and DescriptiveComplexity.OrderedFOReduction.withInvariant: strengthen a reduction's target by an invariant its images satisfy;
• DescriptiveComplexity.SigmaSODefinable.inf_ofSentence: conjoin a first-order sentence into a Σₖ definition;
• DescriptiveComplexity.Encoding.Faithful.inf: encoded instances that are well-formed are faithful for the restricted problem;
• DescriptiveComplexity.FinPresentation and DescriptiveComplexity.Decoding: concretely presented structures and computable decodings, with DescriptiveComplexity.Decoding.exists_conc_iff as the Prop-level consequence.

Well-formedness as a decision problem

def DescriptiveComplexity.DecisionProblem.and {L : FirstOrder.Language} (W P : DecisionProblem L) : DecisionProblem L

The conjunction of two decision problems: a structure is a yes-instance when it is one of both. Written W ⊓ P (through the Min instance below); with W a well-formedness condition, W ⊓ P is “P, on well-formed instances”.

Equations

• W.and P = { Holds := fun (A : Type) (inst : L.Structure A) => W.Holds A ∧ P.Holds A, iso_invariant := ⋯ }

@[instance_reducible]

instance DescriptiveComplexity.instMinDecisionProblem {L : FirstOrder.Language} : Min (DecisionProblem L)

Equations

• DescriptiveComplexity.instMinDecisionProblem = { min := DescriptiveComplexity.DecisionProblem.and }

@[simp]

theorem DescriptiveComplexity.DecisionProblem.min_holds {L : FirstOrder.Language} (W P : DecisionProblem L) (A : Type) [L.Structure A] : (W ⊓ P).Holds A ↔ W.Holds A ∧ P.Holds A

def DescriptiveComplexity.DecisionProblem.ofSentence {L : FirstOrder.Language} (ψ : L.Sentence) : DecisionProblem L

A first-order sentence, read as a decision problem: the structures satisfying it. Isomorphism-invariance is automatic, which makes this the cheapest way to state a well-formedness condition W.

Equations

• DescriptiveComplexity.DecisionProblem.ofSentence ψ = { Holds := fun (A : Type) (inst : L.Structure A) => A ⊨ ψ, iso_invariant := ⋯ }

@[simp]

theorem DescriptiveComplexity.DecisionProblem.ofSentence_holds {L : FirstOrder.Language} (ψ : L.Sentence) (A : Type) [L.Structure A] : (DecisionProblem.ofSentence ψ).Holds A ↔ A ⊨ ψ

Reductions with an image invariant

A reduction into P whose images all satisfy W is a reduction into W ⊓ P – so hardness of the restricted problem costs one image lemma on top of the reduction already at hand. Only the last hop of a reduction chain needs the lemma: composing any further reduction in front leaves the images unchanged.

def DescriptiveComplexity.FOReduction.withInvariant {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : FOReduction P Q) (W : DecisionProblem L') (h : ∀ (A : Type) [inst : L.Structure A] [Nonempty A], W.Holds (f.toInterpretation.Map A)) : FOReduction P (W ⊓ Q)

Strengthen the target of a reduction by an invariant its images satisfy.

Equations

• f.withInvariant W h = { Tag := f.Tag, tagFinite := ⋯, tagNonempty := ⋯, dim := f.dim, toInterpretation := f.toInterpretation, correct := ⋯ }

def DescriptiveComplexity.OrderedFOReduction.withInvariant {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : OrderedFOReduction P Q) (W : DecisionProblem L') (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], W.Holds (f.toInterpretation.Map A)) : OrderedFOReduction P (W ⊓ Q)

Strengthen the target of an ordered reduction by an invariant its images satisfy.

Equations

• f.withInvariant W h = { Tag := f.Tag, tagFinite := ⋯, tagNonempty := ⋯, dim := f.dim, toInterpretation := f.toInterpretation, correct := ⋯ }

Conjoining a sentence into a second-order definition

instance DescriptiveComplexity.instNonemptyAssignment (B : SOBlock) (A : Type) : Nonempty (B.Assignment A)

def DescriptiveComplexity.soLift {L : FirstOrder.Language} (Bs : List SOBlock) : L.Sentence → (soLang L Bs).Sentence

A sentence of the base language, lifted to the language of a kernel: the symbols are unchanged, only their address in the iterated sum grows.

Equations

• DescriptiveComplexity.soLift [] x✝ = x✝
• DescriptiveComplexity.soLift (head :: Bs) x✝ = DescriptiveComplexity.soLift Bs (FirstOrder.Language.LHom.sumInl.onSentence x✝)

theorem DescriptiveComplexity.SigmaSODefinable.inf_ofSentence {L : FirstOrder.Language} {k : ℕ} {P : DecisionProblem L} (h : SigmaSODefinable k P) (ψ : L.Sentence) : SigmaSODefinable k (DecisionProblem.ofSentence ψ ⊓ P)

Conjoining a first-order sentence preserves Σₖ-definability: the sentence joins the kernel, lifted along the block languages. This is the membership half of restricting a problem to its well-formed instances.

Faithfulness for the restricted problem

theorem DescriptiveComplexity.Encoding.Faithful.inf {L : FirstOrder.Language} [L.IsRelational] {ι : Type u_1} {e : Encoding L ι} {Conc : ι → Prop} {P : DecisionProblem L} (hf : e.Faithful Conc P) (W : DecisionProblem L) (hW : ∀ (i : ι), W.Holds (e.Univ i)) : e.Faithful Conc (W ⊓ P)

A faithful encoding whose images are all well-formed is faithful for the restricted problem: the completeness theorem for W ⊓ P reads back to the same concrete predicate.

Concretely presented structures and computable decodings

structure DescriptiveComplexity.FinPresentation (L : FirstOrder.Language) : Type

A concretely presented finite L-structure: a size and a computable relation table. This is the input type of decoders – the “raw bytes” a decoding computation reads.

• card : ℕ

  The number of elements.

• relBool {n : ℕ} : L.Relations n → (Fin n → Fin self.card) → Bool

  The relations, as computations on Fin card.

@[instance_reducible]

instance DescriptiveComplexity.FinPresentation.str {L : FirstOrder.Language} [L.IsRelational] (S : FinPresentation L) : L.Structure (Fin S.card)

The L-structure a presentation presents.

Equations

• S.str = { funMap := fun {n : ℕ} (f : L.Functions n) => isEmptyElim f, RelMap := fun {n : ℕ} (R : L.Relations n) (x : Fin n → Fin S.card) => S.relBool R x = true }

@[simp]

theorem DescriptiveComplexity.FinPresentation.relMap_iff {L : FirstOrder.Language} [L.IsRelational] (S : FinPresentation L) {n : ℕ} (R : L.Relations n) (x : Fin n → Fin S.card) : FirstOrder.Language.Structure.RelMap R x ↔ S.relBool R x = true

noncomputable def DescriptiveComplexity.FinPresentation.ofStructure {L : FirstOrder.Language} (A : Type) [L.Structure A] [Fintype A] : FinPresentation L

Any nonempty finite structure, presented concretely (classically: the presentation decides the relations by choice, which is fine for the Prop-level transport below – actual decoders never see it).

Equations

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

noncomputable def DescriptiveComplexity.FinPresentation.equivOfStructure {L : FirstOrder.Language} [L.IsRelational] (A : Type) [L.Structure A] [Fintype A] : L.Equiv A (Fin (ofStructure A).card)

The presented structure is isomorphic to the original one.

Equations

• DescriptiveComplexity.FinPresentation.equivOfStructure A = { toEquiv := Fintype.equivFin A, map_fun' := ⋯, map_rel' := ⋯ }

structure DescriptiveComplexity.Decoding (L : FirstOrder.Language) [L.IsRelational] {ι : Type u_1} (W : DecisionProblem L) (Conc : ι → Prop) (P : DecisionProblem L) : Type u_1

A computable decoding of well-formed structures into concrete instances: the converse of an encoding, with the same hygiene. dec is a plain computation from presented structures to Option ι – returning none is the junk case, so there are no proof-carrying arguments and the decoder can be run and #guard-tested; sound says decoded instances are equidecided with the structure they came from; total says well-formed nonempty presentations always decode. See the module docstring for why the bundled function, and not a ∀∃ statement, is the meaningful notion.

• dec : FinPresentation L → Option ι

  The decoder: a computation from presented structures to concrete instances, none on junk. Keep it a plain def-legible field, as for Encoding.relBool.

• sound (S : FinPresentation L) (i : ι) : i ∈ self.dec S → (Conc i ↔ P.Holds (Fin S.card))

  Decoded instances are decided by the concrete semantics exactly as the presented structure is by the abstract problem.

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

  Well-formed nonempty presentations always decode.

theorem DescriptiveComplexity.Decoding.exists_conc_iff {L : FirstOrder.Language} [L.IsRelational] {ι : Type u_1} {W : DecisionProblem L} {Conc : ι → Prop} {P : DecisionProblem L} (d : Decoding L W Conc P) (A : Type) [L.Structure A] [Finite A] [Nonempty A] (hW : W.Holds A) : ∃ (i : ι), Conc i ↔ P.Holds A

Well-formed structures are semantically concrete: along a decoding, every well-formed nonempty finite structure is decided by the abstract problem exactly as some concrete instance is by the concrete semantics. This is the honest form of the removed Encoding.CoversUpTo – honest because it is derived from the bundled computation, not established by casing on P A.