Enumerating the witnesses of a bounded existential

⚠️ Unreviewed by Bolton

polyExistsLang quantifies over witnesses w with |w| ≤ p |x|. A machine cannot quantify; it counts. This file replaces the quantifier over strings by a quantifier over a length and a value — the two numbers a loop actually iterates — by exhibiting the round trip between a bitstring and its length-plus-binary-value.

Nothing here is about machines: it is the arithmetic that makes an enumeration faithful.

Main definitions

• binVal — the big-endian value of a bitstring
• bitsOfLen — the bitstring of a given length and value

Main results

• bitsOfLen_binVal, binVal_bitsOfLen — the round trip, both ways: a bijection between bitstrings and length-plus-value pairs
• exists_bounded_iff, exists_bounded_iff_le — the bounded existential over strings is one over two numbers, in either bit order
• choicesOfNat, natOfChoices — choice sequences as counter values, for the path-counting machine
• bitsOfLenLE_getElem, choicesOfNat_apply — each bit of the enumeration is a bit of the counter, in the form a tape encoding produces
• binValLE_bits, bits_injective — the canonical counter representation determines its value
• getD_eq_bit — reading a bitstring past its end agrees with reading the number's bits
• dropTop, topPlus, exists_bounded_iff_count — the same existential as a single count, over the counter values below 2 ^ (m + 1)
• bumpLE, dropTop_succ — the witness advances in step with the counter, so a machine can carry it on a tape instead of computing it

def Complexity.binVal : List Bool → ℕ

The big-endian value of a bitstring.

Equations

• Complexity.binVal [] = 0
• Complexity.binVal (b :: w) = (if b = true then 2 ^ w.length else 0) + Complexity.binVal w

def Complexity.bitsOfLen : ℕ → ℕ → List Bool

The bitstring of a given length and value, big-endian.

Equations

• Complexity.bitsOfLen 0 x✝ = []
• Complexity.bitsOfLen ℓ.succ x✝ = decide (x✝ / 2 ^ ℓ % 2 = 1) :: Complexity.bitsOfLen ℓ (x✝ % 2 ^ ℓ)

@[simp]

theorem Complexity.bitsOfLen_length (ℓ v : ℕ) : (bitsOfLen ℓ v).length = ℓ

theorem Complexity.binVal_lt (w : List Bool) : binVal w < 2 ^ w.length

A bitstring's value fits in its length.

theorem Complexity.bitsOfLen_binVal (w : List Bool) : bitsOfLen w.length (binVal w) = w

The round trip. A bitstring is recovered from its length together with its value, so iterating over lengths and values enumerates every bitstring exactly once.

theorem Complexity.binVal_bitsOfLen (ℓ v : ℕ) : v < 2 ^ ℓ → binVal (bitsOfLen ℓ v) = v

The other half of the round trip. The value of the bitstring of length ℓ and value v is v again, provided v fits. Together with bitsOfLen_binVal this makes the correspondence a bijection, which is what lets a loop's counter be the witness: incrementing the counter advances the witness by exactly one place in the enumeration.

theorem Complexity.exists_bounded_iff (m : ℕ) (P : List Bool → Prop) : (∃ (w : List Bool), w.length ≤ m ∧ P w) ↔ ∃ ℓ ≤ m, ∃ v < 2 ^ ℓ, P (bitsOfLen ℓ v)

A bounded existential over strings is a bounded existential over two numbers. This is the form a counting loop can implement: iterate the length, then the value.

The little-endian enumeration

Every binary subroutine in the library — TM.binarySuccTM and the rest — uses canonical little-endian bit lists. Since the order in which witnesses are enumerated is immaterial, only that the enumeration is a bijection, the machine should use the convention its counter already speaks. These are the little-endian counterparts of the definitions above.

def Complexity.binValLE : List Bool → ℕ

The little-endian value of a bitstring.

Equations

• Complexity.binValLE [] = 0
• Complexity.binValLE (b :: w) = (if b = true then 1 else 0) + 2 * Complexity.binValLE w

def Complexity.bitsOfLenLE : ℕ → ℕ → List Bool

The little-endian bitstring of a given length and value.

Equations

• Complexity.bitsOfLenLE 0 x✝ = []
• Complexity.bitsOfLenLE ℓ.succ x✝ = decide (x✝ % 2 = 1) :: Complexity.bitsOfLenLE ℓ (x✝ / 2)

@[simp]

theorem Complexity.bitsOfLenLE_length (ℓ v : ℕ) : (bitsOfLenLE ℓ v).length = ℓ

theorem Complexity.binValLE_lt (w : List Bool) : binValLE w < 2 ^ w.length

theorem Complexity.bitsOfLenLE_binValLE (w : List Bool) : bitsOfLenLE w.length (binValLE w) = w

The round trip, one way.

theorem Complexity.binValLE_bitsOfLenLE (ℓ v : ℕ) : v < 2 ^ ℓ → binValLE (bitsOfLenLE ℓ v) = v

The round trip, the other way.

theorem Complexity.exists_bounded_iff_le (m : ℕ) (P : List Bool → Prop) : (∃ (w : List Bool), w.length ≤ m ∧ P w) ↔ ∃ ℓ ≤ m, ∃ v < 2 ^ ℓ, P (bitsOfLenLE ℓ v)

The little-endian form of the enumeration.

Choice sequences as counter values

The counting machine iterates a binary counter, but NTM.acceptCount ranges over functions Fin T → Bool. These convert between the two, reusing the bitstring enumeration.

def Complexity.choicesOfNat (T v : ℕ) : Fin T → Bool

The choice sequence of length T with counter value v.

Equations

• Complexity.choicesOfNat T v j = (Complexity.bitsOfLenLE T v)[↑j]

def Complexity.natOfChoices (T : ℕ) (ch : Fin T → Bool) : ℕ

The counter value of a choice sequence.

Equations

• Complexity.natOfChoices T ch = Complexity.binValLE (List.ofFn ch)

theorem Complexity.natOfChoices_lt (T : ℕ) (ch : Fin T → Bool) : natOfChoices T ch < 2 ^ T

theorem Complexity.choicesOfNat_natOfChoices (T : ℕ) (ch : Fin T → Bool) : choicesOfNat T (natOfChoices T ch) = ch

theorem Complexity.natOfChoices_choicesOfNat (T v : ℕ) (hv : v < 2 ^ T) : natOfChoices T (choicesOfNat T v) = v

theorem Complexity.bitsOfLenLE_getElem (ℓ v j : ℕ) (h : j < ℓ) : (bitsOfLenLE ℓ v)[j] = decide (v / 2 ^ j % 2 = 1)

Each bit of the enumeration is a bit of the counter. The j-th entry of the length-ℓ little-endian string for v is bit j of v. This is the form in which the correspondence meets a tape: whatever encoding a counter tape uses, its j-th cell holds this bit — and cells beyond the counter's own digits read as false, which is bit j of v too.

theorem Complexity.choicesOfNat_apply (T v : ℕ) (j : Fin T) : choicesOfNat T v j = decide (v / 2 ^ ↑j % 2 = 1)

The j-th choice bit of counter value v is bit j of v.

Canonical bits and their value

The library's counter subroutines represent a number by Nat.bits. Reading that representation back as a value is binValLE, and the two are mutually inverse — which is what makes a counter tape determine the number it holds.

theorem Complexity.binValLE_bits (n : ℕ) : binValLE n.bits = n

The canonical representation reads back as its value.

theorem Complexity.bits_injective : Function.Injective Nat.bits

The canonical representation determines the number.

theorem Complexity.getD_eq_bit (w : List Bool) (j : ℕ) : w.getD j false = decide (binValLE w / 2 ^ j % 2 = 1)

Reading a bitstring past its end agrees with reading the number's bits. Entry j of a little-endian string, taken as false beyond the end, is bit j of the number it denotes — the high bits of that number being zero. This is what lets a counter tape be read as a choice sequence with no padding step.

The single-counter enumeration

A nested loop over a length and then a value is two loops; a machine that enumerates witnesses would rather run one. Appending a marker bit turns the enumeration into a plain count: the numbers in [1, 2 ^ (m + 1)) are in bijection with the bitstrings of length at most m, a number denoting its canonical bits with the leading one removed.

def Complexity.dropTop (v : ℕ) : List Bool

The witness a counter value denotes: the value's canonical bits, less the leading one.

Equations

• Complexity.dropTop v = v.bits.dropLast

def Complexity.topPlus (w : List Bool) : ℕ

The counter value at which a witness is enumerated: its value with a marker bit above it.

Equations

• Complexity.topPlus w = Complexity.binValLE w + 2 ^ w.length

theorem Complexity.one_le_topPlus (w : List Bool) : 1 ≤ topPlus w

theorem Complexity.bits_topPlus (w : List Bool) : (topPlus w).bits = w ++ [true]

The marker bit is the leading one.

theorem Complexity.dropTop_topPlus (w : List Bool) : dropTop (topPlus w) = w

The round trip.

theorem Complexity.topPlus_lt {m : ℕ} {w : List Bool} (h : w.length ≤ m) : topPlus w < 2 ^ (m + 1)

theorem Complexity.length_dropTop_le {m v : ℕ} (hv : v < 2 ^ (m + 1)) : (dropTop v).length ≤ m

A counter value below 2 ^ (m + 1) denotes a witness of length at most m.

theorem Complexity.exists_bounded_iff_count (m : ℕ) (P : List Bool → Prop) : (∃ (w : List Bool), w.length ≤ m ∧ P w) ↔ ∃ v < 2 ^ (m + 1), P (dropTop v)

The bounded existential is a count. A witness of length at most m exists exactly when some counter value below 2 ^ (m + 1) denotes one — a single loop over a single register, with the same shape the path-counting machine of PP ⊆ PSPACE already runs.

The enumeration is not injective at the bottom — 0 and 1 both denote the empty witness — but it does not have to be: only that every witness is denoted, and that every value denotes one.

Enumerating the witness alongside the counter

The machine will not compute dropTop from the counter; it will carry the witness on a tape of its own and advance it in step with the counter. bumpLE is that advance — the counter's increment seen through dropTop. It is the ordinary little-endian increment except at the end of the string, where the carry extends the witness by a zero instead of writing a one: the bit it would have written is the counter's leading one, which dropTop discards.

def Complexity.bumpLE : List Bool → List Bool

One step of the witness enumeration: increment the string, extending it on overflow.

Equations

• Complexity.bumpLE [] = [false]
• Complexity.bumpLE (false :: w) = true :: w
• Complexity.bumpLE (true :: w) = false :: Complexity.bumpLE w

@[simp]

theorem Complexity.topPlus_nil : topPlus [] = 1

theorem Complexity.topPlus_bumpLE (w : List Bool) : topPlus (bumpLE w) = topPlus w + 1

The advance is the counter's increment.

theorem Complexity.bits_eq_dropTop (v : ℕ) : 1 ≤ v → v.bits = dropTop v ++ [true]

A positive number's canonical bits end in one, so they are its witness and that one.

theorem Complexity.topPlus_dropTop {v : ℕ} (h : 1 ≤ v) : topPlus (dropTop v) = v

The counter is recovered from its witness.

theorem Complexity.dropTop_succ {v : ℕ} (h : 1 ≤ v) : dropTop (v + 1) = bumpLE (dropTop v)

The witness advances with the counter. This is the loop invariant the enumerating machine carries: one tape holds the counter, another holds the witness it denotes, and each iteration advances both.

theorem Complexity.exists_bounded_iff_count_pos (m : ℕ) (P : List Bool → Prop) : (∃ (w : List Bool), w.length ≤ m ∧ P w) ↔ ∃ (v : ℕ), 1 ≤ v ∧ v < 2 ^ (m + 1) ∧ P (dropTop v)

Every witness of the admitted lengths is still reached, with the counter starting at one: the value 0, which the count above admits, denotes the same empty witness as 1.