Direct work-symbol branch combinator -- definitions

TM.branchWorkBlankTM idx onBlank onNonblank inspects work tape idx once. A blank selects onBlank; every other symbol selects onNonblank. The dispatcher uses the ordinary read-back action on every tape and never uses the output tape as control storage.

inductive Complexity.TM.WorkBranchPhase : Type

Finite driver states for direct work-symbol branching.

• dispatch : WorkBranchPhase
• done : WorkBranchPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqWorkBranchPhase : DecidableEq WorkBranchPhase

Equations

• Complexity.TM.instDecidableEqWorkBranchPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeWorkBranchPhase : Fintype WorkBranchPhase

WorkBranchPhase has exactly two states.

Equations

• Complexity.TM.instFintypeWorkBranchPhase = { elems := {Complexity.TM.WorkBranchPhase.dispatch, Complexity.TM.WorkBranchPhase.done}, complete := ⋯ }

@[reducible, inline]

abbrev Complexity.TM.WorkBranchQ (QBlank QNonblank : Type) : Type

State space of a direct work-symbol branch.

Equations

• Complexity.TM.WorkBranchQ QBlank QNonblank = (Complexity.TM.WorkBranchPhase ⊕ QBlank ⊕ QNonblank)

def Complexity.TM.workBranchBlankState {n : ℕ} (onBlank onNonblank : TM n) (q : onBlank.Q) : WorkBranchQ onBlank.Q onNonblank.Q

Embed a blank-branch state, collapsing its halt state to the shared halt.

Equations

• onBlank.workBranchBlankState onNonblank q = if q = onBlank.qhalt then Sum.inl Complexity.TM.WorkBranchPhase.done else Sum.inr (Sum.inl q)

def Complexity.TM.workBranchNonblankState {n : ℕ} (onBlank onNonblank : TM n) (q : onNonblank.Q) : WorkBranchQ onBlank.Q onNonblank.Q

Embed a nonblank-branch state, collapsing its halt state to the shared halt.

Equations

• onBlank.workBranchNonblankState onNonblank q = if q = onNonblank.qhalt then Sum.inl Complexity.TM.WorkBranchPhase.done else Sum.inr (Sum.inr q)

def Complexity.TM.branchWorkBlankTime (blankTime nonblankTime : ℕ) : ℕ

Uniform time bound for a one-step dispatch followed by either branch.

Equations

• Complexity.TM.branchWorkBlankTime blankTime nonblankTime = 1 + max blankTime nonblankTime

def Complexity.TM.branchWorkBlankTM {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) : TM n

Inspect one work symbol and run the selected branch on the same tapes.

The dispatcher selects onBlank exactly when wHeads idx = Γ.blank and otherwise selects onNonblank. Branch halt states are collapsed into the shared halt state on the same simulated transition, so there is no trailing seam step and no extra tape action after a branch halts.

Equations

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