Every digit-definable function reduces to the number written by unit propagation

DescriptiveComplexity.DigitLFPDef.orderedParsimoniousHorn: a function whose binary digits are relations of a least fixed point (DescriptiveComplexity.DigitDefinable) reduces to DescriptiveComplexity.HornNumber by an ordered parsimonious reduction.

The Horn formula is the one of the Horn discharge (DescriptiveComplexity.hornInterp): a variable per atom, a clause per instance of a rule whose guard holds. Its least model is the least fixed point of the rules (DescriptiveComplexity.HornNum.forced_var_iff), so the output variables are the atoms of the relations holding the digits. The rules without a head derive nothing and are dropped first: they would be goal clauses, and could make the formula unsatisfiable.

Dropping the rules without a head

def DescriptiveComplexity.HornNum.headed {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) : HornProgram (L.sum FirstOrder.Language.order) B k

The rules with a head.

Equations

• DescriptiveComplexity.HornNum.headed prog = List.filter (fun (c : DescriptiveComplexity.HornClause (L.sum FirstOrder.Language.order) B k) => c.head.isSome) prog

theorem DescriptiveComplexity.HornNum.derives_headed {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (prog : HornProgram (L.sum FirstOrder.Language.order) B k) (q : (i : B.ι) × (Fin (B.arity i) → A)) : Derives (headed prog) q ↔ Derives prog q

The least model of the Horn formula is the least fixed point

theorem DescriptiveComplexity.HornNum.forced_var_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {a₀ : A} (h₀ : IsBot a₀) (i : B.ι) (w : Fin (clauseDim B k) → A) : Forced (varTag i, w) ↔ Canon (B.arity i) w ∧ Derives prog ⟨i, pref ⋯ w⟩

The least model of the Horn formula is the least fixed point of the rules.

The interpretation, with its outputs

noncomputable def DescriptiveComplexity.HornNum.hornNumInterp {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) {c : ℕ} (bit : Fin c → B.ι) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.satOut (HornTag prog) (clauseDim B k)

The Horn formula of a system of rules, with the atoms of the relation variables bit τ as output variables.

Equations

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

def DescriptiveComplexity.HornNum.satEquiv {L : FirstOrder.Language} {B : SOBlock} {k c : ℕ} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) (bit : Fin c → B.ι) (A : Type) [L.Structure A] [LinearOrder A] : FirstOrder.Language.sat.Equiv ((hornNumInterp prog bit).Map A) ((hornInterp prog).Map A)

The CNF part of the interpreted structure is the Horn discharge's.

Equations

• DescriptiveComplexity.HornNum.satEquiv prog bit A = { toEquiv := Equiv.refl ((DescriptiveComplexity.HornNum.hornNumInterp prog bit).Map A), map_fun' := ⋯, map_rel' := ⋯ }

noncomputable def DescriptiveComplexity.HornNum.varPt {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) {c : ℕ} (bit : Fin c → B.ι) {ℓ : ℕ} (hℓ : ∀ (τ : Fin c), B.arity (bit τ) = ℓ) (a₀ : A) (q : Lex (Fin c × Lex (Fin ℓ → A))) : (hornNumInterp prog bit).Map A

The output variable of a position.

Equations

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

theorem DescriptiveComplexity.HornNum.varPt_injective {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} {ℓ : ℕ} (hinj : Function.Injective bit) (hℓ : ∀ (τ : Fin c), B.arity (bit τ) = ℓ) (a₀ : A) : Function.Injective (varPt prog bit hℓ a₀)

theorem DescriptiveComplexity.HornNum.below_varPt {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} {ℓ : ℕ} {a₀ : A} (hinj : Function.Injective bit) (hℓ : ∀ (τ : Fin c), B.arity (bit τ) = ℓ) (q' q : Lex (Fin c × Lex (Fin ℓ → A))) : FirstOrder.Language.Structure.RelMap hnBelow ![varPt prog bit hℓ a₀ q', varPt prog bit hℓ a₀ q] ↔ q' ≤ q

theorem DescriptiveComplexity.HornNum.hornNumber_hornNumInterp {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} {ℓ : ℕ} {a₀ : A} (hinj : Function.Injective bit) (hℓ : ∀ (τ : Fin c), B.arity (bit τ) = ℓ) [Finite A] [Nonempty A] (hhead : ∀ c ∈ prog, c.head.isSome = true) (h₀ : IsBot a₀) : hornNumber ((hornNumInterp prog bit).Map A) = ∑ᶠ (q : Lex (Fin c × Lex (Fin ℓ → A))), if lfpAssign prog (bit (ofLex q).1) fun (n : Fin (B.arity (bit (ofLex q).1))) => ofLex (ofLex q).2 (Fin.cast ⋯ n) then 2 ^ orank q else 0

The Horn formula writes the number whose digits are the relations bit τ of the least fixed point, the rules having heads.

The reduction

noncomputable def DescriptiveComplexity.DigitLFPDef.orderedParsimoniousHorn {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (d : DigitLFPDef L) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], C.Count A = d.value A) : OrderedParsimoniousReduction C HornNumber

A function whose binary digits are relations of a least fixed point reduces to the number written by unit propagation.

Equations

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

theorem DescriptiveComplexity.DigitDefinable.nonempty_orderedParsimoniousHorn {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : DigitDefinable C) : Nonempty (OrderedParsimoniousReduction C HornNumber)

Every digit-definable problem parsimoniously reduces to the number written by unit propagation.