Documentation

Complexitylib.Models.TuringMachine.UTM.Internal.TermCheck

termCheckTM: deciding TerminatedRegion by a single input scan #

The body machine's per-iteration theorem (bodyIteration) carries the side condition TerminatedRegion α on the encoded description. The time-hierarchy diagonalizer must decide this property of its own input by machine, so it can route the (malformed) inputs violating it around the universal simulation.

Contents:

  1. terminatedRegionB — a Boolean version of TerminatedRegion, with the bridge terminatedRegionB_iff.
  2. scanStep/ctrlVerdict — a six-state symbol-level automaton whose left-fold over groupPairs α computes terminatedRegionB α (scanVerdict_eq): track the two □ separators of the takeField decomposition, then inspect the first two symbols of the entry region.
  3. termCheckTM : TM 8 — the machine: a single left-to-right scan of the input decoding bit pairs into symbols (symOfPair) and driving the automaton, then an input rewind to cell 1 and a verdict write at output cell 1. All 8 work tapes idle throughout.
  4. termCheckTM_hoareTime — the Hoare specification: 2·|x| + 8 steps, input head returned to cell 1, work tapes preserved exactly, verdict Γ.one/Γ.zero at output cell 1 (output head parked back at 1).
source
def Complexity.TM.UTMBody.terminatedRegionB (α : List Bool) :
Bool

Boolean version of TerminatedRegion: the entry region (after the two takeField splits) fails the check exactly when it starts with a □ followed by a non-□ symbol.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.TM.UTMBody.terminatedRegionB_iff (α : List Bool) :
    terminatedRegionB α = true ↔ TerminatedRegion α

    terminatedRegionB decides TerminatedRegion.

    source
    inductive Complexity.TM.UTMBody.TermCtrl :
    Type

    Control of the symbol-level scan deciding terminatedRegionB:

    • seek1/seek2 — before the first/second □ separator;
    • look1/look2 — examining the first/second symbol of the entry region;
    • good/bad — verdict absorbed (region terminated / not terminated).
    Instances For
      source
      @[implicit_reducible]
      instance Complexity.TM.UTMBody.instDecidableEqTermCtrl :
      DecidableEq TermCtrl
      Equations
      source
      @[implicit_reducible]
      instance Complexity.TM.UTMBody.instFintypeTermCtrl :
      Fintype TermCtrl
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Complexity.TM.UTMBody.scanStep :
      TermCtrl → Γw → TermCtrl

      One decoded desc symbol updates the scan control: □s advance through the takeField structure, the first two region symbols decide the verdict, and verdicts are absorbing.

      Equations
      Instances For
        source
        def Complexity.TM.UTMBody.ctrlVerdict :
        TermCtrl → Bool

        End-of-stream verdict: only bad rejects (a truncated region is fine — TerminatedRegion needs two symbols after the second □ to fire).

        Equations
        Instances For
          source
          theorem Complexity.TM.UTMBody.scanVerdict_eq (α : List Bool) :
          ctrlVerdict (List.foldl scanStep TermCtrl.seek1 (groupPairs α)) = terminatedRegionB α

          The scan computes the region check: folding the automaton over the decoded symbol stream of α and taking the end-of-stream verdict is exactly terminatedRegionB α.

          source
          inductive Complexity.TM.UTMBody.TermCheckQ :
          Type

          Control states of termCheckTM:

          • readFst ctrl — scanning, at the first bit of the current pair;
          • readSnd ctrl b — scanning, at the second bit of a pair whose first bit was b;
          • rewind v — walking the input head back to ▷, verdict v in hand;
          • emit v — input head at cell 1: write the verdict at output cell 1;
          • done — halt.
          Instances For
            source
            def Complexity.TM.UTMBody.instDecidableEqTermCheckQ.decEq (x✝ x✝¹ : TermCheckQ) :
            Decidable (x✝ = x✝¹)
            Equations
            Instances For
              source
              @[implicit_reducible]
              instance Complexity.TM.UTMBody.instDecidableEqTermCheckQ :
              DecidableEq TermCheckQ
              Equations
              source
              @[implicit_reducible]
              instance Complexity.TM.UTMBody.instFintypeTermCheckQ :
              Fintype TermCheckQ
              Equations
              • One or more equations did not get rendered due to their size.
              source
              def Complexity.TM.UTMBody.termCheckTM :
              TM 8

              Terminated-region check: scan the input left to right decoding bit pairs into desc symbols (symOfPair) and driving scanStep; at the input's first blank (end of x, or a dropped trailing odd bit) take ctrlVerdict, rewind the input head to cell 1, and write the verdict (1 = terminated, 0 = not) at output cell 1. All 8 work tapes idle throughout.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Complexity.TM.UTMBody.termCheckTM_hoareTime (x : List Bool) (work₀ : Fin 8 → Tape) (out₀ : Tape) (hw : ∀ (i : Fin 8), 1 ≤ (work₀ i).head ∧ (work₀ i).read ≠ Γ.start) (hout0 : out₀.cells 0 = Γ.start) (houtns : ∀ (j : ℕ), 1 ≤ j → out₀.cells j ≠ Γ.start) (houth : out₀.head = 1) :
                termCheckTM.HoareTime (fun (inp : Tape) (work : Fin 8 → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ inp.head = 1 ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin 8 → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ inp.head = 1 ∧ work = work₀ ∧ out.cells = Function.update out₀.cells 1 (if terminatedRegionB x = true then Γ.one else Γ.zero) ∧ out.head = 1) (2 * x.length + 8)

                termCheckTM specification (ghost-initial-tapes style): started on the input tape of x with head at cell 1, all work tapes parked (head ≥ 1, not reading ▷) and the output tape ▷-clean with head at cell 1, the machine halts within 2·|x| + 8 steps having written the terminatedRegionB x verdict (1 = holds, 0 = fails) at output cell 1. The input head returns to cell 1, every work tape is preserved exactly, and the output head is parked back at cell 1.