Tape-symbol acceptance equals state acceptance

This file proves that the tape-acceptance characterization is_Recursive_byTape (defined in Automata.Recursive.Basic.TapeCharacterization) agrees with the state-based is_Recursive: is_Recursive_byTape L → is_Recursive L.

The forward direction is the useful one — it lets a construction that produces the decision on the tape (which is what the Code → TM translation chain exposes) be repackaged into the state-based is_Recursive.

Construction

Given a machine M that halts with the answer under the head, readerMachine M acceptSym runs M; the instant M would halt it instead reads the current symbol γ and moves to the distinguished halting state Sum.inr (decide (γ = acceptSym)), which records the verdict. The acceptance predicate just reads that Boolean off the state.

def AcceptByTape.liftCfg {Γ : Type} [Inhabited Γ] {Λ : Type} (c : Turing.TM0.Cfg Γ Λ) : Turing.TM0.Cfg Γ (Λ ⊕ Bool)

Lift a TM0 configuration to the reader's state space Λ ⊕ Bool.

Equations

• AcceptByTape.liftCfg c = { q := Sum.inl c.q, Tape := c.Tape }

def AcceptByTape.readerMachine {Γ : Type} [DecidableEq Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (acceptSym : Γ) : Turing.TM0.Machine Γ (Λ ⊕ Bool)

Turn a machine that signals acceptance by leaving acceptSym under the head into one that signals acceptance by its final state. When M would halt, the reader reads the current symbol and halts in state Sum.inr b where b records whether the symbol was acceptSym.

Equations

• One or more equations did not get rendered due to their size.
• AcceptByTape.readerMachine M acceptSym (Sum.inr val) γ = none

def AcceptByTape.readerAccept {Λ : Type} : Λ ⊕ Bool → Bool

The state-based acceptance predicate of the reader.

Equations

• AcceptByTape.readerAccept (Sum.inl q_1) = false
• AcceptByTape.readerAccept (Sum.inr val) = val

theorem AcceptByTape.reader_step_of_step {Γ : Type} [Inhabited Γ] [DecidableEq Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (acceptSym : Γ) (c c' : Turing.TM0.Cfg Γ Λ) (hs : c' ∈ Turing.TM0.step M c) : Turing.TM0.step (readerMachine M acceptSym) (liftCfg c) = some (liftCfg c')

theorem AcceptByTape.reader_reaches_of_reaches {Γ : Type} [Inhabited Γ] [DecidableEq Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (acceptSym : Γ) (c c' : Turing.TM0.Cfg Γ Λ) (hr : Turing.Reaches (Turing.TM0.step M) c c') : Turing.Reaches (Turing.TM0.step (readerMachine M acceptSym)) (liftCfg c) (liftCfg c')

theorem AcceptByTape.reader_halt_step {Γ : Type} [Inhabited Γ] [DecidableEq Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (acceptSym : Γ) (c : Turing.TM0.Cfg Γ Λ) (hstep : Turing.TM0.step M c = none) : Turing.TM0.step (readerMachine M acceptSym) (liftCfg c) = some { q := Sum.inr (decide (c.Tape.head = acceptSym)), Tape := Turing.Tape.write c.Tape.head c.Tape }

theorem AcceptByTape.reader_inr_step {Γ : Type} [Inhabited Γ] [DecidableEq Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (acceptSym : Γ) (b : Bool) (tape : Turing.Tape Γ) : Turing.TM0.step (readerMachine M acceptSym) { q := Sum.inr b, Tape := tape } = none

theorem AcceptByTape.reader_eval {Γ : Type} [Inhabited Γ] [DecidableEq Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (acceptSym : Γ) (l : List Γ) (hdom : (Turing.eval (Turing.TM0.step M) (Turing.TM0.init l)).Dom) : (Turing.eval (Turing.TM0.step (readerMachine M acceptSym)) (Turing.TM0.init l)).Dom ∧ ∀ (h : (Turing.eval (Turing.TM0.step (readerMachine M acceptSym)) (Turing.TM0.init l)).Dom), ((Turing.eval (Turing.TM0.step (readerMachine M acceptSym)) (Turing.TM0.init l)).get h).q = Sum.inr (decide (((Turing.eval (Turing.TM0.step M) (Turing.TM0.init l)).get hdom).Tape.head = acceptSym))

The reader halts whenever M does, and its final state records whether the symbol under the head at M's halting configuration was acceptSym.

The two conventions agree

theorem is_Recursive_of_byTape {T : Type} {L : Language T} (h : is_Recursive_byTape L) : is_Recursive L

Tape acceptance implies state acceptance: every is_Recursive_byTape language is is_Recursive.