The output tape up to two symbols

A decision procedure halts with output [b]. Since the output tape is append-only, whether a run has produced exactly one symbol, and which one, is determined by a four-valued summary of the output written so far (Turing.OutView): nothing, one symbol b, or more than one. The summary is updated symbol by symbol (Turing.OutView.push), which is what lets reductions and circuit simulations track acceptance with a bounded amount of information per time step.

Main definitions

• Turing.OutView, Turing.OutView.ofList, Turing.OutView.push.
• Turing.OutView.index, Turing.OutView.ofIndex: numbering output views as 0, 1, 2, 3.

Main results

• Turing.OutView.ofList_append_toList: summarising commutes with emitting a symbol.
• Turing.OutView.ofList_eq_one_iff: the summary is one b exactly for the output [b].
• Turing.OutView.ofIndex_index, Turing.OutView.index_ofIndex: round-trip between output views and indices below 4.

inductive Turing.OutView : Type

What has been written on the output tape: nothing, a single symbol, or more than one. A decision procedure halts with output [b], and since the output tape is append-only this view is all that has to be tracked to see the answer.

• empty : OutView

  Nothing has been written.

• one (b : Bool) : OutView

  Exactly one symbol has been written.

• many : OutView

  At least two symbols have been written.

def Turing.instDecidableEqOutView.decEq (x✝ x✝¹ : OutView) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Turing.instDecidableEqOutView : DecidableEq OutView

@[instance_reducible]

instance Turing.instFintypeOutView : Fintype OutView

def Turing.OutView.ofList : List Bool → OutView

The view of an output word.

def Turing.OutView.push : OutView → Option Bool → OutView

The view after emitting an optional symbol.

def Turing.OutView.all : List OutView

All four views.

@[simp]

theorem Turing.OutView.length_all : all.length = 4

@[simp]

theorem Turing.OutView.mem_all (o : OutView) : o ∈ all

@[simp]

theorem Turing.OutView.ofList_nil : ofList [] = empty

theorem Turing.OutView.ofList_append_toList (l : List Bool) (o : Option Bool) : ofList (l ++ o.toList) = (ofList l).push o

theorem Turing.OutView.ofList_eq_one_iff {l : List Bool} {b : Bool} : ofList l = one b ↔ l = [b]

@[simp]

theorem Turing.OutView.card_eq : Fintype.card OutView = 4

def Turing.OutView.index : OutView → ℕ

The index of an output view, for numbering.

theorem Turing.OutView.index_injective : Function.Injective index

@[simp]

theorem Turing.OutView.index_lt (o : OutView) : o.index < 4

def Turing.OutView.ofIndex (m : ℕ) : OutView

The output view with a given index (0 for empty, 1 for one false, 2 for one true, and many otherwise).

@[simp]

theorem Turing.OutView.ofIndex_index (o : OutView) : ofIndex o.index = o

theorem Turing.OutView.index_ofIndex {m : ℕ} (hm : m < 4) : (ofIndex m).index = m