Copying canonical binary naturals

This definitions layer composes work-tape clearing with width-linear canonical binary addition. The source and zero scratch tapes are preserved, while the destination is replaced by an exact copy of the source.

def Complexity.TM.binaryCopyIntoTM {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) : TM n

Clear dstIdx, then copy the canonical binary natural on srcIdx into it. The distinct counterIdx supplies the preserved zero operand to ripple addition, and dstIdx is its fresh result tape.

Equations

• Complexity.TM.binaryCopyIntoTM srcIdx dstIdx counterIdx = (Complexity.TM.clearWorkTM dstIdx).seqTM (Complexity.TM.binaryRippleAddTM srcIdx counterIdx dstIdx)

def Complexity.TM.binaryCopyTime (srcValue dstValue : ℕ) : ℕ

Compositional running-time bound for canonical binary copying.

Equations

• Complexity.TM.binaryCopyTime srcValue dstValue = Complexity.TM.clearWorkTimeBound dstValue.size + 1 + Complexity.TM.binaryRippleAddTime srcValue 0

def Complexity.TM.binaryCopySpace (initialSpace srcValue dstValue : ℕ) : ℕ

All-prefix auxiliary-space bound for canonical binary copying.

Equations

• Complexity.TM.binaryCopySpace initialSpace srcValue dstValue = max (initialSpace + Complexity.TM.clearWorkTimeBound dstValue.size) (initialSpace + Complexity.TM.binaryRippleAddTime srcValue 0)