Addition of a fixed natural to a canonical binary tape — definitions

A fixed constant is compiled into finitely many sequential applications of canonical binary successor. No work tape is needed for the hardwired value, so the construction preserves every tape except its destination.

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

Add a hardwired natural to one canonical binary work tape.

Equations

• Complexity.TM.binaryAddConstTM idx 0 = Complexity.TM.skipTM
• Complexity.TM.binaryAddConstTM idx constant.succ = (Complexity.TM.binaryAddConstTM idx constant).seqTM (Complexity.TM.binarySuccTM idx)

def Complexity.TM.binaryAddConstTime (constant dstValue : ℕ) : ℕ

Exact runtime of fixed-constant binary addition.

Equations

• Complexity.TM.binaryAddConstTime 0 dstValue = 1
• Complexity.TM.binaryAddConstTime constant_1.succ dstValue = Complexity.TM.binaryAddConstTime constant_1 dstValue + 1 + Complexity.TM.binarySuccTime (dstValue + constant_1)

def Complexity.TM.binaryAddConstSpace (initialSpace constant dstValue : ℕ) : ℕ

All-prefix width-based space bound for fixed-constant addition.

Equations

• Complexity.TM.binaryAddConstSpace initialSpace constant dstValue = initialSpace + 2 * (dstValue + constant).size + 3