Functions defined by their binary digits

A function from ordered structures to numbers is digit-definable (DescriptiveComplexity.DigitDefinable) when its binary digits are relations of a least fixed point: there are rules (DescriptiveComplexity.DigitLFPDef) and finitely many of their relation variables, bit 0, …, bit (c - 1), all of the same arity ℓ, such that the value is ∑ 2 ^ rank(τ, x̄) over the pairs of a τ < c and a tuple x̄ in the relation bit τ. The pairs are the positions of the digits, ranked by τ first and then lexicographically (DescriptiveComplexity.orank): the digit of weight 2 ^ r is 1 exactly when the position of rank r is in its relation.

Several relations are needed, and not only tuples of one: a structure with one element has a single tuple of each length, and a function may take any value on it.

This is the normal form through which QFO(LFP) is shown to capture FP (Arenas, Muñoz, Riveros 2020, proof of Theorem 4.4): a function computable in polynomial time has polynomially many digits, each computable in polynomial time, hence, by the Immerman–Vardi theorem, definable by a least fixed point over the ordered structure.

Both directions hold for the library's FP (DescriptiveComplexity.Problems.CircuitNumber): digit-definable problems are in FP (DescriptiveComplexity.DigitDefinable.mem_FP), and every problem of FP is digit-definable (DescriptiveComplexity.FPDefinable.digitDefinable, in DescriptiveComplexity.Counting.Digits.NormalForm).

theorem DescriptiveComplexity.finsum_digits_eq {X P : Type} [LinearOrder P] [Finite P] (Out Bit : X → Prop) (Below : X → X → Prop) (φ : P → X) (hφ : Function.Injective φ) (hout : ∀ (x : X), Out x ↔ ∃ (q : P), x = φ q) (hbelow : ∀ (q' q : P), Below (φ q') (φ q) ↔ q' ≤ q) : (∑ᶠ (x : X), if Out x ∧ Bit x then 2 ^ Nat.card { y : X // Out y ∧ y ≠ x ∧ Below y x } else 0) = ∑ᶠ (q : P), if Bit (φ q) then 2 ^ orank q else 0

A sum of place values, read along an enumeration of the digits. Marked elements Out, compared by Below, each contributing two to the number of marked elements strictly below it when it carries a digit Bit: if the marked elements are enumerated by a finite linear order, in order, the sum is the one over that order, with ranks as exponents.

structure DescriptiveComplexity.DigitLFPDef (L : FirstOrder.Language) : Type 1

A definition of a number by its binary digits: a least fixed point, as for DescriptiveComplexity.LFPDef, and the relation variables holding the digits.

• B : SOBlock

  The relation variables computed by the fixed point.

• k : ℕ

  The number of first-order variables shared by the rules.

• rules : List (HornClause (L.sum FirstOrder.Language.order) self.B self.k)

  The rules defining the variables.

• c : ℕ

  The number of relation variables holding digits.

• c_pos : 0 < self.c

  There is at least one.

• ℓ : ℕ

  Their common arity.

• bit : Fin self.c → self.B.ι

  The relation variables holding the digits, the least significant first.

• bit_injective : Function.Injective self.bit

  They are distinct.

• arity_bit (τ : Fin self.c) : self.B.arity (self.bit τ) = self.ℓ

  They have the same arity.

def DescriptiveComplexity.DigitLFPDef.Holds {L : FirstOrder.Language} (d : DigitLFPDef L) (A : Type) [L.Structure A] [LinearOrder A] (q : Lex (Fin d.c × Lex (Fin d.ℓ → A))) : Prop

The digit at a position is 1: the tuple is in the relation of its group.

Equations

• d.Holds A q = DescriptiveComplexity.lfpAssign d.rules (d.bit (ofLex q).1) fun (k : Fin (d.B.arity (d.bit (ofLex q).1))) => ofLex (ofLex q).2 (Fin.cast ⋯ k)

noncomputable def DescriptiveComplexity.DigitLFPDef.value {L : FirstOrder.Language} (d : DigitLFPDef L) (A : Type) [L.Structure A] [LinearOrder A] : ℕ

The value of a definition on an ordered structure: the number whose digit of weight 2 ^ r is 1 exactly when the position of rank r is in its relation of the least fixed point.

Equations

• d.value A = ∑ᶠ (q : Lex (Fin d.c × Lex (Fin d.ℓ → A))), if d.Holds A q then 2 ^ DescriptiveComplexity.orank q else 0

def DescriptiveComplexity.DigitDefinable {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : Prop

A counting problem is digit-definable when, on nonempty finite structures, its binary digits are relations of a least fixed point, whatever the linear order.

Equations

• DescriptiveComplexity.DigitDefinable C = ∃ (d : DescriptiveComplexity.DigitLFPDef L), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], C.Count A = d.value A