Documentation

DescriptiveComplexity.Numbers.Binary

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)

Instances For

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)

@[simp]

theorem DescriptiveComplexity.posRank_fin {m : ℕ} (p : Fin m) :

posRank (Fin m) p = ↑p

On Fin m, which is already the increasing enumeration of itself, the rank of a position is its index. This is what lets a concrete encoder lay its bit positions out as Fin m and read the place values off directly.

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

Instances For

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)

Instances For

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

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)

Instances For

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.