The zero-extending increment — definitions

⚠️ Unreviewed by Bolton

TM.binarySuccTM increments the number a tape holds: a carry that runs off the end appends a new high 1. This module defines the same scan with one write changed — the carry appends a 0 — which increments the string a tape holds, one place wider each time it overflows.

That is the enumeration of all bitstrings in order of length: [], 0, 1, 00, 10, …. It is the increment of a fixed-width counter that widens instead of wrapping, and it is what a machine enumerating the witnesses of a bounded existential advances each iteration.

def Complexity.BinaryBump.bump : List Bool → List Bool

Ripple one carry through a little-endian bit string, widening the string when the carry runs off its end.

Equations

• Complexity.BinaryBump.bump [] = [false]
• Complexity.BinaryBump.bump (false :: rest) = true :: rest
• Complexity.BinaryBump.bump (true :: rest) = false :: Complexity.BinaryBump.bump rest

def Complexity.BinaryBump.steps : List Bool → ℕ

Exact number of transitions used by binaryBumpTM on a bit string. It is twice the successor of the number of initial low-order one bits.

Equations

• Complexity.BinaryBump.steps [] = 2
• Complexity.BinaryBump.steps (false :: rest) = 2
• Complexity.BinaryBump.steps (true :: rest) = Complexity.BinaryBump.steps rest + 2

inductive Complexity.TM.BinaryBumpPhase : Type

Finite phases of the zero-extending increment.

• carry : BinaryBumpPhase
• rewind : BinaryBumpPhase
• done : BinaryBumpPhase

@[instance_reducible]

instance Complexity.TM.instDecidableEqBinaryBumpPhase : DecidableEq BinaryBumpPhase

Equations

• Complexity.TM.instDecidableEqBinaryBumpPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.TM.instFintypeBinaryBumpPhase : Fintype BinaryBumpPhase

BinaryBumpPhase has exactly three states.

Equations

• Complexity.TM.instFintypeBinaryBumpPhase = { elems := {Complexity.TM.BinaryBumpPhase.carry, Complexity.TM.BinaryBumpPhase.rewind, Complexity.TM.BinaryBumpPhase.done}, complete := ⋯ }

def Complexity.TM.binaryBumpTime (bits : List Bool) : ℕ

Exact running time of the zero-extending increment on a bit string.

Equations

• Complexity.TM.binaryBumpTime bits = Complexity.BinaryBump.steps bits

def Complexity.TM.binaryBumpTM {n : ℕ} (idx : Fin n) : TM n

Advance the little-endian bit string on work tape idx to the next one.

The carry phase turns initial one bits into zero bits. The first zero becomes one; if the carry reaches the terminating blank, a zero is appended there — one place wider, all zeros — which is the only difference from TM.binarySuccTM. The machine then rewinds to cell one. Input, output, and unrelated work tapes use the structurally safe read-back/idle action.

Equations

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