Little-endian binary predecessor — definitions

This module defines the finite controller for in-place predecessor on a positive canonical binary natural. Borrow turns initial low-order zero bits into ones. The first one becomes zero; when it was the unique high bit, a one-cell lookahead detects the terminating blank and erases that now-redundant zero before rewinding.

The controller is total on zero, where it simply rewinds the unchanged empty representation. Public correctness theorems intentionally start from value + 1, so no underflow behavior is claimed.

def Complexity.BinaryPred.ripple : List Bool → List Bool

Ripple one borrow through a little-endian bit string, dropping a vacated unique high bit. The empty case defines underflow as unchanged zero.

Equations

• Complexity.BinaryPred.ripple [] = []
• Complexity.BinaryPred.ripple (false :: rest) = true :: Complexity.BinaryPred.ripple rest
• Complexity.BinaryPred.ripple [true] = []
• Complexity.BinaryPred.ripple (true :: bit :: rest) = false :: bit :: rest

def Complexity.BinaryPred.steps : List Bool → ℕ

Exact transition count used by binaryPredTM on a canonical bit string.

Equations

• Complexity.BinaryPred.steps [] = 2
• Complexity.BinaryPred.steps (false :: rest) = Complexity.BinaryPred.steps rest + 2
• Complexity.BinaryPred.steps (true :: tail) = 4

inductive Complexity.TM.BinaryPredPhase : Type

Finite phases of ripple-borrow predecessor.

• borrow : BinaryPredPhase
• check : BinaryPredPhase
• erase : BinaryPredPhase
• rewind : BinaryPredPhase
• done : BinaryPredPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqBinaryPredPhase : DecidableEq BinaryPredPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeBinaryPredPhase : Fintype BinaryPredPhase

BinaryPredPhase has exactly five states.

Equations

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

def Complexity.TM.binaryPredTime (value : ℕ) : ℕ

Exact running time for decrementing canonical value + 1 to value.

Equations

• Complexity.TM.binaryPredTime value = Complexity.BinaryPred.steps (value + 1).bits

def Complexity.TM.binaryPredSpace (initialSpace value : ℕ) : ℕ

Explicit width-based all-prefix space budget for predecessor.

Equations

• Complexity.TM.binaryPredSpace initialSpace value = initialSpace + 2 * (value + 1).size + 2

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

Decrement a positive canonical little-endian natural on work tape idx.

The borrow phase flips initial zeros to ones and replaces the first one by zero. A lookahead distinguishes an internal bit from the terminating blank; the latter case erases the vacated high zero. The machine finally rewinds to cell one. On canonical zero it takes the blank branch and leaves zero intact.

Equations

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