Binary representation of numbers in finite structures

The binary encoding: a number carried by an instance is given by a set of bit positions, the positions being linearly ordered elements of the structure. This is the honest encoding for problems whose numbers must be exponential in the instance size (SubsetSum, Partition, Knapsack…), where the unary representation of DescriptiveComplexity.Numbers.Unary would change the complexity.

• DescriptiveComplexity.posRank: the rank of a position in the increasing enumeration (via monoEquivOfFin, so positions need not literally be Fin m);
• DescriptiveComplexity.binValue b: the number ∑ 2 ^ rank p over set bits – the decoding function;
• DescriptiveComplexity.binEncode k: the canonical encoding, via Nat.testBit;
• round-trips DescriptiveComplexity.binValue_binEncode (for k < 2 ^ #positions) and DescriptiveComplexity.testBit_binValue;
• range bound DescriptiveComplexity.binValue_lt_two_pow;
• invariance under order-isomorphisms (DescriptiveComplexity.binValue_orderIso), for the DecisionProblem.iso_invariant proof of a problem carrying binary numbers;
• the most-significant-differing-bit comparison DescriptiveComplexity.binValue_lt_binValue_iff – the Lean counterpart of the FO(≤) formula comparing two binary numbers.

The problems of the catalog reach this layer through DescriptiveComplexity.Numbers.BinRel, which decodes the same bits when the order on positions is a relation symbol of the vocabulary rather than a LinearOrder instance: Knapsack, Partition, Job Sequencing and 0-1 Integer Programming. The choice between this encoding and the unary one is argued in DescriptiveComplexity.Numbers.

Sums of powers of two over a bit predicate

Positions, decoding and encoding

noncomputable def DescriptiveComplexity.posRank (P : Type) [Fintype P] [LinearOrder P] (p : P) : ℕ

The rank of a bit position: its index in the increasing enumeration of the positions.

Equations

• DescriptiveComplexity.posRank P p = ↑((monoEquivOfFin P ⋯).symm p)

theorem DescriptiveComplexity.posRank_lt (P : Type) [Fintype P] [LinearOrder P] (p : P) : posRank P p < Fintype.card P

theorem DescriptiveComplexity.posRank_lt_posRank_iff (P : Type) [Fintype P] [LinearOrder P] {p q : P} : posRank P p < posRank P q ↔ p < q

theorem DescriptiveComplexity.posRank_injective (P : Type) [Fintype P] [LinearOrder P] : Function.Injective (posRank P)

noncomputable def DescriptiveComplexity.binValue (P : Type) [Fintype P] [LinearOrder P] (b : P → Prop) : ℕ

The number represented in binary by a set of positions: the sum of 2 ^ rank over the set bits. This is the decoding function of the binary representation.

Equations

• DescriptiveComplexity.binValue P b = ∑ p : P, if b p then 2 ^ DescriptiveComplexity.posRank P p else 0

def DescriptiveComplexity.binEncode (P : Type) [Fintype P] [LinearOrder P] (k : ℕ) : P → Prop

The canonical binary encoding of a number as a set of positions.

Equations

• DescriptiveComplexity.binEncode P k p = (k.testBit (DescriptiveComplexity.posRank P p) = true)

noncomputable def DescriptiveComplexity.posBits (P : Type) [Fintype P] [LinearOrder P] (b : P → Prop) : ℕ → Bool

The bits of a set of positions, as a function of the rank.

Equations

• DescriptiveComplexity.posBits P b i = decide (∃ (p : P), DescriptiveComplexity.posRank P p = i ∧ b p)

theorem DescriptiveComplexity.posBits_posRank {P : Type} [Fintype P] [LinearOrder P] (b : P → Prop) (p : P) : posBits P b (posRank P p) = true ↔ b p

theorem DescriptiveComplexity.binValue_eq_sum_range {P : Type} [Fintype P] [LinearOrder P] (b : P → Prop) : binValue P b = ∑ i ∈ Finset.range (Fintype.card P), if posBits P b i = true then 2 ^ i else 0

theorem DescriptiveComplexity.binValue_lt_two_pow {P : Type} [Fintype P] [LinearOrder P] (b : P → Prop) : binValue P b < 2 ^ Fintype.card P

The decoded number is smaller than 2 ^ #positions.

theorem DescriptiveComplexity.binValue_binEncode {P : Type} [Fintype P] [LinearOrder P] {k : ℕ} (h : k < 2 ^ Fintype.card P) : binValue P (binEncode P k) = k

Decoding after encoding is the identity, for numbers within range.

theorem DescriptiveComplexity.testBit_binValue {P : Type} [Fintype P] [LinearOrder P] (b : P → Prop) (p : P) : (binValue P b).testBit (posRank P p) = true ↔ b p

The bits of the decoded number are the original set of positions.

theorem DescriptiveComplexity.binValue_orderIso {P : Type} [Fintype P] [LinearOrder P] {Q : Type} [Fintype Q] [LinearOrder Q] (e : P ≃o Q) (b : Q → Prop) : (binValue P fun (p : P) => b (e p)) = binValue Q b

The decoded number is invariant under order-isomorphisms of the positions.

theorem DescriptiveComplexity.binValue_congr {P : Type} [Fintype P] [LinearOrder P] {b b' : P → Prop} (h : ∀ (p : P), b p ↔ b' p) : binValue P b = binValue P b'

binValue only depends on the extension of the bit predicate.

theorem DescriptiveComplexity.binValue_lt_binValue_iff {P : Type} [Fintype P] [LinearOrder P] (b b' : P → Prop) : binValue P b < binValue P b' ↔ ∃ (p : P), ¬b p ∧ b' p ∧ ∀ (q : P), p < q → (b q ↔ b' q)

Most-significant-bit comparison: one binary number is smaller than another iff at some position the first has bit 0 and the second bit 1, all higher positions agreeing. This is the Lean counterpart of the FO(≤) formula comparing binary numbers.