Checking a guessed symbol against the input head

A scan reads work tapes. The one thing it cannot see is the input tape, so a machine that simulates another machine's input head has to compare the symbol under that head against what it guessed by hand.

TM.inMatchTM does exactly that, in two steps: it compares the two cells of a register against the two bits a caller-supplied encoding assigns to the symbol under the input head, and leaves the verdict on a result register. The input head does not move, so a simulation whose input head sits at the simulated position keeps it there.

Main definitions

• TM.inMatchTM — the check
• TM.inMoveTM — moving the input head by a guessed direction held in two one-cell registers, so it tracks the simulated one
• TM.copyCellTM — copying one register's cell onto another, which is how a scan's verdict leaves the result tape
• TM.andCellTM — conjoining one register's cell into another, which is how a machine with no early exit remembers that a check failed

Main results

• TM.inMatchTM_hoareTime — its contract: two steps, the verdict on the result register, the compared register rewound, every other tape untouched
• TM.inMoveTM_hoareTime — and the move's: one step, the input head where the register says
• TM.copyCellTM_hoareTime — and the copy's
• TM.andCellTM_hoareTime — and the conjunction's
• TM.guessProtocol_andCellTM — the conjunction never consults the guess tape

inductive Complexity.TM.InMatchPhase : Type

Control states of TM.inMatchTM: compare the first bit, then the second, then halt.

• first : InMatchPhase
• second : InMatchPhase
• done : InMatchPhase

@[instance_reducible]

instance Complexity.TM.instDecidableEqInMatchPhase : DecidableEq InMatchPhase

Equations

• Complexity.TM.instDecidableEqInMatchPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.TM.instFintypeInMatchPhase : Fintype InMatchPhase

Equations

• Complexity.TM.instFintypeInMatchPhase = { elems := {Complexity.TM.InMatchPhase.first, Complexity.TM.InMatchPhase.second, Complexity.TM.InMatchPhase.done}, complete := ⋯ }

def Complexity.TM.inMatchTM {n : ℕ} (expect : Γ → Bool × Bool) (sym res : Fin n) : TM n

Check a guessed symbol against the input head. Register sym, parked at cell one, holds two bits; expect says which two bits the symbol under the input head should give. The verdict lands on register res, and sym is left where it started.

Equations

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

def Complexity.TM.inMatchVerdict (expect : Γ → Bool × Bool) (g c₁ c₂ : Γ) : Bool

The verdict TM.inMatchTM writes: both cells of sym agree with the two bits the symbol under the input head is expected to give.

Equations

• Complexity.TM.inMatchVerdict expect g c₁ c₂ = (decide (c₁ = Complexity.Γ.ofBool (expect g).1) && decide (c₂ = Complexity.Γ.ofBool (expect g).2))

def Complexity.TM.inMatchRes (expect : Γ → Bool × Bool) (g c₁ c₂ : Γ) (t : Tape) : Tape

The tape TM.inMatchTM leaves on its result register.

Equations

• Complexity.TM.inMatchRes expect g c₁ c₂ t = { head := 1, cells := Function.update t.cells 1 (Complexity.Γ.ofBool (Complexity.TM.inMatchVerdict expect g c₁ c₂)) }

theorem Complexity.TM.inMatchTM_hoareTime {n : ℕ} (expect : Γ → Bool × Bool) (sym res : Fin n) (hsr : sym ≠ res) (inp₀ out₀ : Tape) (W₀ : Fin n → Tape) (hinv : ∀ (i : Fin n), (W₀ i).StartInvariant) (hh : ∀ (i : Fin n), 1 ≤ (W₀ i).head) (hinp : inp₀.read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) (hsym : (W₀ sym).head = 1) (hres : (W₀ res).head = 1) : (inMatchTM expect sym res).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = W₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ (∀ (i : Fin n), i ≠ res → work i = W₀ i) ∧ work res = inMatchRes expect inp₀.read ((W₀ sym).cells 1) ((W₀ sym).cells 2) (W₀ res)) 2

The contract of the input-symbol check. Two steps; the verdict lands on cell one of the result register, the compared register comes back to cell one with its contents intact, and every other tape — the input tape included — is untouched.

Moving the input head with the simulated one

inductive Complexity.TM.InMovePhase : Type

Control states of TM.inMoveTM.

• go : InMovePhase
• done : InMovePhase

@[instance_reducible]

instance Complexity.TM.instDecidableEqInMovePhase : DecidableEq InMovePhase

Equations

• Complexity.TM.instDecidableEqInMovePhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.TM.instFintypeInMovePhase : Fintype InMovePhase

Equations

• Complexity.TM.instFintypeInMovePhase = { elems := {Complexity.TM.InMovePhase.go, Complexity.TM.InMovePhase.done}, complete := ⋯ }

def Complexity.TM.inMoveTM {n : ℕ} (decode : Γ → Γ → Dir3) (mv dir : Fin n) : TM n

Move the input head by the direction two registers' cells name. A guessed cell holds a bit, so it cannot name one of three directions on its own; a machine's transition sees every head at once, so two one-cell registers do it in a single step. Reading ▷ still forces a move right, as it must.

Equations

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

theorem Complexity.TM.inMoveTM_hoareTime {n : ℕ} (decode : Γ → Γ → Dir3) (mv dir : Fin n) (inp₀ out₀ : Tape) (W₀ : Fin n → Tape) (hinv : ∀ (i : Fin n), (W₀ i).StartInvariant) (hh : ∀ (i : Fin n), 1 ≤ (W₀ i).head) (hinp : inp₀.read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (inMoveTM decode mv dir).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = W₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀.move (decode (W₀ mv).read (W₀ dir).read) ∧ work = W₀ ∧ out = out₀) 1

The contract of the input-head move. One step; the input head moves as the register says, and every other tape is untouched.

Copying one cell to another register

def Complexity.TM.copyCellTM {n : ℕ} (src dst : Fin n) : TM n

Copy the symbol under one register's head onto another register. A scan leaves its verdict on the machine's result tape, which no scan can read; moving it onto an ordinary register is what lets a later check take it into account.

Equations

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

theorem Complexity.TM.copyCellTM_hoareTime {n : ℕ} (src dst : Fin n) (inp₀ out₀ : Tape) (W₀ : Fin n → Tape) (hinv : ∀ (i : Fin n), (W₀ i).StartInvariant) (hh : ∀ (i : Fin n), 1 ≤ (W₀ i).head) (hinp : inp₀.read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (copyCellTM src dst).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = W₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ (∀ (i : Fin n), i ≠ dst → work i = W₀ i) ∧ work dst = { head := (W₀ dst).head, cells := Function.update (W₀ dst).cells (W₀ dst).head (readBackWrite (W₀ src).read).toΓ }) 1

The contract of the cell copy. One step; the destination's cell under its head becomes the source's, and nothing else moves.

def Complexity.TM.andCellTM {n : ℕ} (src dst : Fin n) : TM n

Conjoin one register's cell into another. The destination's cell under its head becomes 1 exactly when both it and the source's cell held 1. A loop driver with no early exit — such as TM.binaryForTM — cannot stop at the first failed check, so its body accumulates the verdicts here instead.

Equations

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

theorem Complexity.TM.andCellTM_hoareTime {n : ℕ} (src dst : Fin n) (inp₀ out₀ : Tape) (W₀ : Fin n → Tape) (hinv : ∀ (i : Fin n), (W₀ i).StartInvariant) (hh : ∀ (i : Fin n), 1 ≤ (W₀ i).head) (hinp : inp₀.read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (andCellTM src dst).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = W₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ (∀ (i : Fin n), i ≠ dst → work i = W₀ i) ∧ work dst = { head := (W₀ dst).head, cells := Function.update (W₀ dst).cells (W₀ dst).head (if (W₀ src).read = Γ.one ∧ (W₀ dst).read = Γ.one then Γ.one else Γ.zero) }) 1

The contract of the cell conjunction. One step; the destination's cell under its head becomes the conjunction of the two cells, and nothing else moves.

theorem Complexity.TM.guessProtocol_andCellTM {k : ℕ} (src dst : Fin (k + 1)) (hsrc : src ≠ Fin.last k) (hdst : dst ≠ Fin.last k) : (andCellTM src dst).GuessProtocol fun (x : (andCellTM src dst).Q) => false

The cell conjunction never consults the guess tape, so it may sit inside a nondeterministic assembly.