Binary input-length counter — definitions

This module instantiates the read-only-input loop with little-endian successor. The input region supplies unary loop fuel without being copied into auxiliary space; the designated work tape holds the growing canonical Nat.bits counter.

def Complexity.TM.binaryLengthLoopTime (value count : ℕ) : ℕ

Exact remaining driver time: run successor on value once for each of count remaining input symbols, then take the final blank-exit step.

Equations

• Complexity.TM.binaryLengthLoopTime value count = Complexity.TM.forInputLoopTime Complexity.TM.binarySuccTime value count

def Complexity.TM.binaryLengthTime (length : ℕ) : ℕ

Exact fresh-start running time of the binary input-length counter. The leading one is the initial left-marker setup step.

Equations

• Complexity.TM.binaryLengthTime length = 1 + Complexity.TM.binaryLengthLoopTime 0 length

def Complexity.TM.binaryLengthSpace (length : ℕ) : ℕ

Honest all-reachable auxiliary-space budget for binary length counting.

Equations

• Complexity.TM.binaryLengthSpace length = 2 * length.size + 3

def Complexity.TM.Experimental.binaryLengthRoutine {n : ℕ} (counterIdx : Fin n) : Routine n

First-order routine program for binary input-length counting.

Equations

• Complexity.TM.Experimental.binaryLengthRoutine counterIdx = (Complexity.TM.Experimental.Routine.call (Complexity.TM.binarySuccTM counterIdx)).forInput

def Complexity.TM.binaryLengthTM {n : ℕ} (counterIdx : Fin n) : TM n

Count the Boolean input length in canonical little-endian binary on work tape counterIdx. The executable machine is obtained by structural routine lowering.

Equations

• Complexity.TM.binaryLengthTM counterIdx = (Complexity.TM.Experimental.binaryLengthRoutine counterIdx).lower