Documentation

Complexitylib.Models.TuringMachine.Repetition.Defs

Fixed-time repetition of probabilistic Turing machines #

This file defines the machine underlying bounded-error amplification. For a machine tm : NTM n, a repetition count k, and a fixed per-run time T, NTM.repeatAtTime tm k T performs k sequential T-step runs and returns their strict-majority verdict.

Every run gets a fresh bank of n + 1 work tapes: n tapes simulate tm's work tapes and the last tape simulates its output tape. The real input tape is rewound between runs, while the real output tape is reserved for the final majority bit. Each run occupies exactly 2 * T + 2 transitions: T simulated steps, T + 1 fixed rewind steps, and one finish step. In particular, early halting does not shift the random-bit slots used by later runs.

The two leading transitions park every tape at cell one and then position the first simulated configuration at cell zero. Thus the complete fixed schedule has length 2 + k * (2 * T + 2), and simulated choice (j, t) is consumed at global position 2 + j * (2 * T + 2) + t.

The degenerate cases are intentional: zero repetitions output 0, and a zero-step run votes according to the initial configuration of tm.

Main definitions #

Tape-bank layout and fixed schedule #

source
def Complexity.NTM.repeatTapeIdx {n k : ℕ} (j : Fin k) (i : Fin (n + 1)) :
Fin (k * (n + 1))

Index a local tape in repetition j's fresh bank. The local bank has n + 1 tapes: the first n simulate work tapes and the last simulates the output tape.

Equations
Instances For
    source
    def Complexity.NTM.repeatWorkIdx {n k : ℕ} (j : Fin k) (i : Fin n) :
    Fin (k * (n + 1))

    Physical work-tape index simulating work tape i in repetition j.

    Equations
    Instances For
      source
      def Complexity.NTM.repeatOutputIdx {n k : ℕ} (j : Fin k) :
      Fin (k * (n + 1))

      Physical work-tape index simulating the output tape in repetition j.

      Equations
      Instances For
        source
        def Complexity.NTM.repeatTapeCoord {n k : ℕ} (i : Fin (k * (n + 1))) :
        Fin k × Fin (n + 1)

        The bank and local index represented by a physical repetition tape.

        Equations
        Instances For
          source
          @[simp]
          theorem Complexity.NTM.repeatTapeCoord_repeatTapeIdx {n k : ℕ} (j : Fin k) (i : Fin (n + 1)) :
          repeatTapeCoord (repeatTapeIdx j i) = (j, i)

          Decoding a freshly constructed bank index recovers its two coordinates.

          source
          theorem Complexity.NTM.repeatTapeIdx_injective {n k : ℕ} :
          Function.Injective fun (p : Fin k × Fin (n + 1)) => repeatTapeIdx p.1 p.2

          Fresh-bank indexing is injective in the pair of coordinates.

          source
          def Complexity.NTM.repeatAtTimeStride (T : ℕ) :
          ℕ

          Number of transitions from the beginning of one simulated run to the next.

          Equations
          Instances For
            source
            def Complexity.NTM.repeatAtTimeSteps (k T : ℕ) :
            ℕ

            Exact number of transitions used by repeatAtTime tm k T.

            Equations
            Instances For
              source
              def Complexity.NTM.repeatChoiceIdx {k : ℕ} (T : ℕ) (j : Fin k) (t : Fin T) :
              Fin (repeatAtTimeSteps k T)

              Global choice position used for simulated step t of repetition j.

              Equations
              Instances For
                source
                def Complexity.NTM.repeatAcceptEvent {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) :
                Finset (Fin T → Bool)

                The single-run accepting event on T source-machine choices.

                Equations
                Instances For

                  Control state and transition helpers #

                  source
                  inductive Complexity.NTM.RepeatQ {n : ℕ} (tm : NTM n) (k T : ℕ) :
                  Type

                  Finite control for repeatAtTime. votes records completed-run verdicts. During rewind, the Boolean flags say which heads have already bounced off cell zero and are parked at cell one.

                  Instances For
                    source
                    def Complexity.NTM.instDecidableEqRepeatQ.decEq {n✝ : ℕ} {tm✝ : NTM n✝} {k✝ T✝ : ℕ} (x✝ x✝¹ : tm✝.RepeatQ k✝ T✝) :
                    Decidable (x✝ = x✝¹)
                    Equations
                    Instances For
                      source
                      @[implicit_reducible]
                      instance Complexity.NTM.instDecidableEqRepeatQ {n✝ : ℕ} {tm✝ : NTM n✝} {k✝ T✝ : ℕ} :
                      DecidableEq (tm✝.RepeatQ k✝ T✝)
                      Equations
                      source
                      @[implicit_reducible]
                      instance Complexity.NTM.instFintypeRepeatQ {n : ℕ} (tm : NTM n) (k T : ℕ) :
                      Fintype (tm.RepeatQ k T)

                      The repetition control is finite because every phase datum is finite.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      source
                      def Complexity.NTM.repeatAfterRunState {n k T : ℕ} (tm : NTM n) (j : Fin k) (t : Fin T) (q : tm.Q) (votes : Fin k → Bool) :
                      tm.RepeatQ k T

                      Advance the fixed simulation counter after one source-machine transition, entering the rewind phase after the last of the T simulation slots.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Complexity.NTM.repeatAfterRewindState {n k T : ℕ} (tm : NTM n) (j : Fin k) (r : Fin (T + 1)) (q : tm.Q) (votes : Fin k → Bool) (inputDone : Bool) (bankDone : Fin (n + 1) → Bool) :
                        tm.RepeatQ k T

                        Advance the fixed rewind counter using the completion flags computed by the current rewind transition, entering finish after the last rewind slot.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Complexity.NTM.repeatRewindDone (done : Bool) (head : Γ) :
                          Bool

                          Update a rewind-completion flag after observing a tape head.

                          Equations
                          Instances For
                            source
                            def Complexity.NTM.repeatRewindDir (done : Bool) (head : Γ) :
                            Dir3

                            Rewind an unfinished tape toward cell zero, bounce to cell one on ▷, and park a finished tape. The ▷ case always moves right, including on malformed control states, so the machine satisfies δ_right_of_start globally.

                            Equations
                            Instances For
                              source
                              def Complexity.NTM.repeatSafeDir (head : Γ) (dir : Dir3) :
                              Dir3

                              Guard an arbitrary proposed direction with the machine model's mandatory rightward move on the left-end marker.

                              Equations
                              Instances For
                                source
                                def Complexity.NTM.repeatGuardTransition {Q : Type} {m : ℕ} (iHead : Γ) (wHeads : Fin m → Γ) (oHead : Γ) (r : Q × (Fin m → Γw) × Γw × Dir3 × (Fin m → Dir3) × Dir3) :
                                Q × (Fin m → Γw) × Γw × Dir3 × (Fin m → Dir3) × Dir3

                                Apply repeatSafeDir to every direction in a transition result.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  theorem Complexity.NTM.repeatGuardTransition_right_of_start {Q : Type} {m : ℕ} (iHead : Γ) (wHeads : Fin m → Γ) (oHead : Γ) (r : Q × (Fin m → Γw) × Γw × Dir3 × (Fin m → Dir3) × Dir3) :
                                  match repeatGuardTransition iHead wHeads oHead r with | (fst, fst_1, fst_2, inputDir, workDirs, outputDir) => (iHead = Γ.start → inputDir = Dir3.right) ∧ (∀ (i : Fin m), wHeads i = Γ.start → workDirs i = Dir3.right) ∧ (oHead = Γ.start → outputDir = Dir3.right)

                                  Guarded transitions satisfy the left-end direction condition independently of the unguarded transition.

                                  source
                                  def Complexity.NTM.repeatWorkReads {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) (i : Fin n) :
                                  Γ

                                  Read the simulated work heads in repetition j's bank.

                                  Equations
                                  Instances For
                                    source
                                    def Complexity.NTM.repeatBankWrites {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) (workWrites : Fin n → Γw) (outputWrite : Γw) :
                                    Fin (k * (n + 1)) → Γw

                                    Apply an action to every tape in bank j, preserving every other bank.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      def Complexity.NTM.repeatBankDirs {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) (workDirs : Fin n → Dir3) (outputDir : Dir3) :
                                      Fin (k * (n + 1)) → Dir3

                                      Apply directions to every tape in bank j, idling every other bank.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        @[simp]
                                        theorem Complexity.NTM.repeatBankWrites_work {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) (workWrites : Fin n → Γw) (outputWrite : Γw) (i : Fin n) :
                                        repeatBankWrites wHeads j workWrites outputWrite (repeatWorkIdx j i) = workWrites i

                                        Bank writes reproduce the simulated action on an active work tape.

                                        source
                                        @[simp]
                                        theorem Complexity.NTM.repeatBankWrites_output {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) (workWrites : Fin n → Γw) (outputWrite : Γw) :
                                        repeatBankWrites wHeads j workWrites outputWrite (repeatOutputIdx j) = outputWrite

                                        Bank writes reproduce the simulated action on the redirected output tape.

                                        source
                                        @[simp]
                                        theorem Complexity.NTM.repeatBankDirs_work {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) (workDirs : Fin n → Dir3) (outputDir : Dir3) (i : Fin n) :
                                        repeatBankDirs wHeads j workDirs outputDir (repeatWorkIdx j i) = workDirs i

                                        Bank directions reproduce the simulated action on an active work tape.

                                        source
                                        @[simp]
                                        theorem Complexity.NTM.repeatBankDirs_output {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) (workDirs : Fin n → Dir3) (outputDir : Dir3) :
                                        repeatBankDirs wHeads j workDirs outputDir (repeatOutputIdx j) = outputDir

                                        Bank directions reproduce the simulated action on the redirected output tape.

                                        source
                                        def Complexity.NTM.repeatPositionBankDirs {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) :
                                        Fin (k * (n + 1)) → Dir3

                                        Position every tape of bank j at cell zero; all other banks idle.

                                        Equations
                                        Instances For
                                          source
                                          def Complexity.NTM.repeatRewindBankDirs {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) (done : Fin (n + 1) → Bool) :
                                          Fin (k * (n + 1)) → Dir3

                                          Fixed-time rewind directions for the active bank.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            def Complexity.NTM.repeatRewindBankDone {n k : ℕ} (wHeads : Fin (k * (n + 1)) → Γ) (j : Fin k) (done : Fin (n + 1) → Bool) :
                                            Fin (n + 1) → Bool

                                            Updated rewind-completion flags for the active bank.

                                            Equations
                                            Instances For
                                              source
                                              def Complexity.NTM.repeatPaddingDirs {n k : ℕ} (iHead : Γ) (wHeads : Fin (k * (n + 1)) → Γ) (oHead : Γ) :
                                              Dir3 × (Fin (k * (n + 1)) → Dir3) × Dir3

                                              Choices are ignored after the simulated machine halts, but cells are preserved and any head on ▷ bounces right. This consumes the rest of the run's fixed T-bit slot without shifting later blocks.

                                              Equations
                                              Instances For

                                                Repetition machine #

                                                source
                                                def Complexity.NTM.repeatAtTime {n : ℕ} (tm : NTM n) (k T : ℕ) :
                                                NTM (k * (n + 1))

                                                Repeat tm exactly k times for T simulated transitions per run and write the strict-majority verdict to the real output tape.

                                                The machine has k * (n + 1) work tapes, split into fresh banks. Its exact fixed running time is repeatAtTimeSteps k T; only the positions specified by repeatChoiceIdx affect simulated runs.

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