Fresh-input entry for proof-carrying binary routines -- definitions

This module connects the initial Turing-machine configuration to the canonical binary work-vector discipline. It first counts the unary input length into one designated work tape, then runs a proof-carrying binary routine.

def Complexity.BinaryRoutine.inputLengthValues {n : ℕ} (lengthIdx : Fin n) (length : ℕ) : BinaryValues n

The canonical all-zero work vector with one designated value set to the input length.

Equations

• Complexity.BinaryRoutine.inputLengthValues lengthIdx length = Function.update (fun (x : Fin n) => 0) lengthIdx length

def Complexity.BinaryRoutine.afterInputLength {n : ℕ} (lengthIdx : Fin n) (routine : BinaryRoutine n) : TM n

Count the input length in binary, then enter a proof-carrying routine.

Equations

• Complexity.BinaryRoutine.afterInputLength lengthIdx routine = (Complexity.TM.binaryLengthTM lengthIdx).seqTM routine.machine

def Complexity.BinaryRoutine.afterInputLengthTime {n : ℕ} (lengthIdx : Fin n) (routine : BinaryRoutine n) (length : ℕ) : ℕ

Compositional runtime bound for fresh-input routine entry.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BinaryRoutine.afterInputLengthSpace {n : ℕ} (lengthIdx : Fin n) (routine : BinaryRoutine n) (length : ℕ) : ℕ

All-prefix auxiliary-space bound for fresh-input routine entry.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BinaryRoutine.afterInputLengthFunction {n : ℕ} (lengthIdx : Fin n) (routine : BinaryRoutine n) : List Bool → List Bool

Function emitted by a fresh-input routine. Only the unary input length is observable after entry into the binary routine layer.

Equations

• Complexity.BinaryRoutine.afterInputLengthFunction lengthIdx routine input = routine.emitted (Complexity.BinaryRoutine.inputLengthValues lengthIdx input.length)