Completeness without a class: the degree of a problem

Every completeness result of this library measures a problem against a class defined by a logic. The same machinery supports a second, orthogonal notion, at almost no cost: completeness for the degree of a fixed problem, with no logic anywhere. “GI-complete” – complete for the degree of Graph Isomorphism (DescriptiveComplexity.DigraphIso) – is the standard example, and the reason this file exists.

DescriptiveComplexity.ComplexityClass.below Q₀ is the downward closure of a fixed relational problem Q₀ under ordered first-order reductions, as a bona fide DescriptiveComplexity.ComplexityClass: membership is “reduces to Q₀”, closed under reductions by transitivity, and hardness is the same cofinal hardness (DescriptiveComplexity.CofinalHard) every other class of the library uses – it is parameterized by an arbitrary membership predicate, so nothing has to be reproved. (below Q₀).Complete P then unfolds to “P is Q₀-complete”, and DescriptiveComplexity.ComplexityClass.complete_below_iff states it in the form one uses: P reduces to Q₀ and Q₀ reduces back to P.

Two sanity checks come with the construction:

• the class only depends on the degree of Q₀, not on Q₀ itself (DescriptiveComplexity.ComplexityClass.below_congr);
• a class with a complete problem is the degree of that problem (DescriptiveComplexity.ComplexityClass.eq_below_of_complete), so “Q₀-hardness is 𝒞-hardness” stops being folklore. The statement takes the class's own hardness-is-cofinal-hardness equation as a hypothesis, which is Iff.rfl for every class built by DescriptiveComplexity.ComplexityClass.ofMem, and the non-relativized reduction as its other hypothesis: a class's own hardness discharge delivers one, while DescriptiveComplexity.cofinalHard_iff on its own yields only the relativized ≤ʳᶠᵒ[≤].

Cofinal hardness only depends on the membership predicate

theorem DescriptiveComplexity.CofinalHard.congr_mem {Mem₁ Mem₂ : {L₀ : FirstOrder.Language} → [inst : L₀.IsRelational] → DecisionProblem L₀ → Prop} (h : ∀ {L₀ : FirstOrder.Language} [inst : L₀.IsRelational] (Q : DecisionProblem L₀), Mem₁ Q ↔ Mem₂ Q) {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : CofinalHard (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => Mem₁) P ↔ CofinalHard (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => Mem₂) P

Cofinal hardness is congruent in its membership predicate: two collections with the same problems have the same hard problems. This is what makes the degree construction below independent of the presentation of a class.

The degree of a problem

noncomputable def DescriptiveComplexity.ComplexityClass.below {L₀ : FirstOrder.Language} [L₀.IsRelational] (Q₀ : DecisionProblem L₀) : ComplexityClass

The degree of a problem: the problems that (ordered) first-order reduce to Q₀, as a complexity class. Membership is closed under reductions by transitivity of reductions, and hardness is cofinal hardness for that membership, exactly as in the logically defined classes.

(below Q₀).Complete P is then literally “P is Q₀-complete”; see DescriptiveComplexity.ComplexityClass.complete_below_iff.

Equations

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

@[simp]

theorem DescriptiveComplexity.ComplexityClass.mem_below_iff {L₀ : FirstOrder.Language} [L₀.IsRelational] {L : FirstOrder.Language} [L.IsRelational] {Q₀ : DecisionProblem L₀} (P : DecisionProblem L) : (below Q₀).Mem P ↔ Nonempty (OrderedFOReduction P Q₀)

theorem DescriptiveComplexity.ComplexityClass.hard_below_iff {L₀ : FirstOrder.Language} [L₀.IsRelational] {L : FirstOrder.Language} [L.IsRelational] {Q₀ : DecisionProblem L₀} (P : DecisionProblem L) : (below Q₀).Hard P ↔ ∀ {L' : FirstOrder.Language} [inst : L'.IsRelational] (Q : DecisionProblem L'), Nonempty (OrderedFOReduction Q Q₀) → Nonempty (RelOrderedFOReduction Q P)

Hardness for a degree, spelled out: everything reducing to Q₀ reduces to P. (An instance of DescriptiveComplexity.cofinalHard_iff, whose relativized conclusion ≤ʳᶠᵒ[≤] is what cofinal hardness yields in general.)

theorem DescriptiveComplexity.ComplexityClass.mem_below_self {L₀ : FirstOrder.Language} [L₀.IsRelational] (Q₀ : DecisionProblem L₀) : (below Q₀).Mem Q₀

A problem belongs to its own degree.

theorem DescriptiveComplexity.ComplexityClass.hard_below_self {L₀ : FirstOrder.Language} [L₀.IsRelational] (Q₀ : DecisionProblem L₀) : (below Q₀).Hard Q₀

A problem is hard for its own degree: everything reducing to it reduces to it.

theorem DescriptiveComplexity.ComplexityClass.below_complete_self {L₀ : FirstOrder.Language} [L₀.IsRelational] (Q₀ : DecisionProblem L₀) : (below Q₀).Complete Q₀

A problem is complete for its own degree – the statement that makes below the right construction.

theorem DescriptiveComplexity.ComplexityClass.complete_below_iff {L₀ : FirstOrder.Language} [L₀.IsRelational] {L : FirstOrder.Language} [L.IsRelational] {Q₀ : DecisionProblem L₀} (P : DecisionProblem L) : (below Q₀).Complete P ↔ Nonempty (OrderedFOReduction P Q₀) ∧ Nonempty (RelOrderedFOReduction Q₀ P)

Q₀-completeness is mutual reducibility: P is complete for the degree of Q₀ exactly when P reduces to Q₀ and Q₀ reduces back to P. The backward reduction is the relativized ≤ʳᶠᵒ[≤], which is what hardness delivers and what a spanning problem needs.

theorem DescriptiveComplexity.ComplexityClass.below_congr {L₀ : FirstOrder.Language} [L₀.IsRelational] {Q₀ : DecisionProblem L₀} {L₁ : FirstOrder.Language} [L₁.IsRelational] {Q₁ : DecisionProblem L₁} (h₀ : Nonempty (OrderedFOReduction Q₀ Q₁)) (h₁ : Nonempty (OrderedFOReduction Q₁ Q₀)) : below Q₀ = below Q₁

The degree only depends on the degree: mutually reducible problems have the same downward closure.

theorem DescriptiveComplexity.ComplexityClass.eq_below_of_complete {L₀ : FirstOrder.Language} [L₀.IsRelational] {C : ComplexityClass} (Q₀ : DecisionProblem L₀) (hmem : C.Mem Q₀) (hred : ∀ {L' : FirstOrder.Language} [inst : L'.IsRelational] (P : DecisionProblem L'), C.Mem P → Nonempty (OrderedFOReduction P Q₀)) (hhard : ∀ {L' : FirstOrder.Language} [inst : L'.IsRelational] (P : DecisionProblem L'), C.Hard P ↔ CofinalHard (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => C.Mem) P) : C = below Q₀

A class with a complete problem is that problem's degree: 𝒞 = below Q₀ whenever Q₀ is 𝒞-complete in the strong sense that every member of 𝒞 reduces to it by a non-relativized ordered reduction – which is what a class's own hardness discharge (DescriptiveComplexity.sat_hard_of_sigmaSODefinable and its siblings) produces.

The last hypothesis says that 𝒞 reads hardness as cofinal hardness for its own members; it is fun _ => Iff.rfl for every class built by DescriptiveComplexity.ComplexityClass.ofMem, hence for every logically defined class of this library.