Documentation

Complexitylib.Models.TuringMachine.Subroutines.PairSplit.Defs

Pair-splitting machine — definitions #

This file defines the deterministic machine that decodes the library's self-delimiting binary pair from the input tape onto two work tapes. Proofs and the public compositional specification live in the adjacent internal and surface modules.

source
inductive Complexity.TM.PairSplitPhase :
Type

Control states of pairSplitCoreTM: .init steps off ▷; .scanX, .afterFalse, and .writeTrue decode the doubled-bit prefix (with 01 as separator); .copyY copies the suffix; .done is the halting state.

Instances For
    source
    @[implicit_reducible]
    instance Complexity.TM.instDecidableEqPairSplitPhase :
    DecidableEq PairSplitPhase
    Equations
    source
    @[implicit_reducible]
    instance Complexity.TM.instFintypePairSplitPhase :
    Fintype PairSplitPhase
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Complexity.TM.pairSplitIdle {k : ℕ} (newState : PairSplitPhase) (iHead : Γ) (wHeads : Fin k → Γ) (oHead : Γ) :
    PairSplitPhase × (Fin k → Γw) × Γw × Dir3 × (Fin k → Dir3) × Dir3

    Idle pair-split transition. It preserves every work and output tape away from the left-end marker; a tape on ▷ takes the structurally required right move. Unlike the generic allIdle, it writes back the symbols under the heads instead of blanking them.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.TM.rightOfStart_pairSplitIdle {k : ℕ} (iHead : Γ) (wHeads : Fin k → Γ) (oHead : Γ) :
      (iHead = Γ.start → idleDir iHead = Dir3.right) ∧ (∀ (i : Fin k), wHeads i = Γ.start → idleDir (wHeads i) = Dir3.right) ∧ (oHead = Γ.start → idleDir oHead = Dir3.right)

      pairSplitIdle satisfies the mandatory right move at every left-end marker.

      source
      def Complexity.TM.pairSplitCoreTM {k : ℕ} (xIdx yIdx : Fin k) :
      TM k

      Core pair-splitting machine. On well-formed inputs pair x y, it decodes the doubled-bit prefix onto work tape xIdx and copies the remaining suffix to work tape yIdx. Invalid inputs halt early; clients that need total malformed input semantics must use a parser with a distinct failure result, since this machine's halting state does not distinguish success from early failure.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.TM.pairSplitCoreTime (xLen yLen : ℕ) :
        ℕ

        Exact running time of the core split phase on canonical pair x y inputs, including its initial controller step.

        Equations
        Instances For