Little-endian binary successor — definitions

This module defines the canonical tape representation and finite controller for ripple-carry successor. Natural numbers use Nat.bits, whose least significant bit comes first and whose representation of zero is empty. Overflow therefore appends one new high bit at the first blank cell.

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

Ripple one carry through a little-endian bit string.

Equations

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

def Complexity.BinarySucc.steps : List Bool → ℕ

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

Equations

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

def Complexity.Tape.HasBinaryNat (t : Tape) (value : ℕ) : Prop

A rewound tape containing the canonical little-endian representation of one natural number, including its immutable left-end marker.

Equations

• t.HasBinaryNat value = (t.cells 0 = Complexity.Γ.start ∧ t.HasBinaryString value.bits)

inductive Complexity.TM.BinarySuccPhase : Type

Finite phases of ripple-carry successor.

• carry : BinarySuccPhase
• rewind : BinarySuccPhase
• done : BinarySuccPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqBinarySuccPhase : DecidableEq BinarySuccPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeBinarySuccPhase : Fintype BinarySuccPhase

BinarySuccPhase has exactly three states.

Equations

• Complexity.TM.instFintypeBinarySuccPhase = { elems := {Complexity.TM.BinarySuccPhase.carry, Complexity.TM.BinarySuccPhase.rewind, Complexity.TM.BinarySuccPhase.done}, complete := ⋯ }

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

Exact running time of canonical successor on value.bits.

Equations

• Complexity.TM.binarySuccTime value = Complexity.BinarySucc.steps value.bits

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

Increment the canonical little-endian natural on work tape idx.

The carry phase turns initial one bits into zero bits. The first zero becomes one; if the carry reaches the terminating blank, one is appended there. 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.