Documentation

Complexitylib.Models.TuringMachine.Subroutines.PairEmit.Defs

Pair emission from the input and a work tape #

This file defines a small deterministic transducer that emits pair first second. The first component is scanned on a designated work tape and doubled on the output; the second component is then copied verbatim from the real input tape. Both sources are consumed only through their first blank delimiter.

Main definitions #

source
inductive Complexity.TM.PairInputWorkPhase :
Type

Control phases for pairInputWorkTM. firstAgain bit remembers the first component bit while emitting its second copy.

Instances For
    source
    def Complexity.TM.instDecidableEqPairInputWorkPhase.decEq (x✝ x✝¹ : PairInputWorkPhase) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Complexity.TM.instDecidableEqPairInputWorkPhase :
      DecidableEq PairInputWorkPhase
      Equations
      source
      @[implicit_reducible]
      instance Complexity.TM.instFintypePairInputWorkPhase :
      Fintype PairInputWorkPhase

      PairInputWorkPhase is finite, as required for a Turing-machine state space.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Complexity.TM.pairInputWorkTM {n : ℕ} (firstIdx : Fin n) :
      TM n

      Emit pair first second, reading first from work tape firstIdx and second from the real input. Sources begin at cell one and advance to their first blank delimiters. The output is the fresh empty tape parked at cell one and is left immediately after the emitted pair, without a rewind.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.TM.pairInputWorkTime (first second : List Bool) :
        ℕ

        Exact running time of pairInputWorkTM on components first and second: two steps per first-component bit, two separator steps, one step per second-component bit, and one final blank-detection step.

        Equations
        Instances For