Documentation

Complexity.Computability.Machines.Turing.MultiTape.Encodings.StepMachineComp

Composing step-machine resource certificates #

The composition g.comp f retains resource certificates: its halting test and its step take the time of those of f and g plus a polynomial in the size of the state, and the space of those of f and g plus the size of the state.

Main definitions #

Main results #

Encodings #

source
def Turing.StepMachine.encPhase :
CompPhase ↪ List Bool

The phases, as words.

Instances For
    source
    instance Turing.StepMachine.instFiniteCompPhase :
    Finite CompPhase
    source
    def Turing.StepMachine.Countdown.equivProd :
    Countdown ≃ ℕ × Bool × ℕ

    Countdowns, as triples.

    Instances For
      source
      def Turing.StepMachine.encCountdown :
      Countdown ↪ List Bool

      Countdowns, as words.

      Instances For
        source
        def Turing.StepMachine.CompState.equivProd {σf σg : Type} :
        CompState σf σg ≃ (σg × ℕ) × CompPhase × σf × Countdown

        The states of g.comp f, as tuples.

        Instances For
          source
          def Turing.StepMachine.encCompState {σf σg : Type} (encF : σf ↪ List Bool) (encG : σg ↪ List Bool) :
          CompState σf σg ↪ List Bool

          The states of g.comp f, as words.

          Instances For
            source
            theorem Turing.StepMachine.length_encCompState {σf σg : Type} {encF : σf ↪ List Bool} {encG : σg ↪ List Bool} (s : CompState σf σg) :
            ((encCompState encF encG) s).length = 2 * (2 * (encG s.g.1).length + 1 + (MultiTapeTM.encNat s.g.2).length) + 1 + (2 * (encPhase s.phase).length + 1 + (2 * (encF s.f).length + 1 + (2 * (MultiTapeTM.encNat s.cd.k).length + 1 + (2 * 1 + 1 + (MultiTapeTM.encNat s.cd.len).length))))

            Projections #

            Countdowns #

            source
            theorem Turing.StepMachine.Countdown.length_encCountdown (c : Countdown) :
            (encCountdown c).length = 2 * (MultiTapeTM.encNat c.k).length + 4 + (MultiTapeTM.encNat c.len).length

            Counting down an emitted word #

            The step of the composition #

            source
            def Turing.StepMachine.compTime {σf σg : Type} (encF : σf ↪ List Bool) (encG : σg ↪ List Bool) (Tf Sf : σf → ℕ) (Tg : σg → ℕ) (s : CompState σf σg) :
            ℕ

            The time of a step of g.comp f.

            Instances For
              source
              def Turing.StepMachine.compSpace {σf σg : Type} (encF : σf ↪ List Bool) (encG : σg ↪ List Bool) (Sf : σf → ℕ) (Sg : σg → ℕ) (s : CompState σf σg) :
              ℕ

              The space of a step of g.comp f.

              Instances For

                The parts of a step, against the size L of the state and the bounds of the step.

                source
                theorem Turing.StepMachine.ResourceCertificate.comp {σf σg : Type} {encF : σf ↪ List Bool} {encG : σg ↪ List Bool} {f : StepMachine σf Bool Bool} {g : StepMachine σg Bool Bool} {Tf Sf : σf → ℕ} {Tg Sg : σg → ℕ} (hf : f.ResourceCertificate encF Tf Sf) (hg : g.ResourceCertificate encG Tg Sg) :
                (g.comp f).ResourceCertificate (encCompState encF encG) (compTime encF encG Tf Sf Tg) (compSpace encF encG Sf Sg)

                Composition preserves step-machine resource certificates.