Canonical binary addition — definitions

This module defines binary addition from the reusable canonical count-up loop. The source tape is the preserved loop limit, the destination is incremented once per source value, and a distinct scratch counter records loop progress. After the loop, the scratch tape is cleared back to canonical zero.

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

Add the preserved canonical binary source into the destination, leaving the scratch counter equal to the source at loop exit.

Equations

• Complexity.TM.binaryAddLoopTM srcIdx dstIdx counterIdx = (Complexity.TM.binarySuccTM dstIdx).binaryForTM counterIdx srcIdx

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

Add the preserved canonical binary source into the destination, then restore the scratch counter to canonical zero.

Equations

• Complexity.TM.binaryAddIntoTM srcIdx dstIdx counterIdx = (Complexity.TM.binaryAddLoopTM srcIdx dstIdx counterIdx).seqTM (Complexity.TM.clearWorkTM counterIdx)

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

Exact running time of the count-up loop used for binary addition.

Equations

• Complexity.TM.binaryAddLoopTime srcValue dstValue = Complexity.TM.binaryForLoopTime (fun (value : ℕ) => Complexity.TM.binarySuccTime (dstValue + value)) srcValue 0 srcValue

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

Time bound for binary addition, including the composition seam and scratch clearing.

Equations

• Complexity.TM.binaryAddTime srcValue dstValue = Complexity.TM.binaryAddLoopTime srcValue dstValue + 1 + Complexity.TM.clearWorkTimeBound srcValue.size

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

Honest all-prefix space bound for the addition loop. It depends on the binary widths of the source and largest destination value, not on total loop runtime.

Equations

• Complexity.TM.binaryAddLoopSpace initialSpace srcValue dstValue = initialSpace + 2 * srcValue.size + 2 * (dstValue + srcValue).size + 5

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

All-prefix space bound for addition followed by scratch clearing.

Equations

• Complexity.TM.binaryAddSpace initialSpace srcValue dstValue = Complexity.TM.binaryAddLoopSpace initialSpace srcValue dstValue + Complexity.TM.clearWorkTimeBound srcValue.size