Languages determined by the first input cell

Non-trivial languages whose membership can be decided by reading just the first cell after ▷ on the input tape. We build a single 3-state TM decideFirstCellTM parameterized by a predicate yesOn : Γ → Bool, prove it runs in exactly 2 steps, and specialize it to several concrete languages.

Main definitions

• firstCell — the first input cell after ▷ (a Γ symbol).
• TM.decideFirstCellTM yesOn — the 3-state parametric TM.

Concrete languages

• Language.singletonEmpty — {[]} (empty string only).
• Language.firstBitOne — strings beginning with 1.
• Language.firstBitZero — strings beginning with 0.
• Language.nonempty — nonempty strings.

Main results

• decideFirstCellTM_reachesIn — the TM halts in 2 steps with the correct output.
• singletonEmpty_in_DTIME, firstBitOne_in_DTIME, firstBitZero_in_DTIME, nonempty_in_DTIME — all decidable in DTIME(fun _ => 2).
• singletonEmpty_mem_P, firstBitOne_mem_P, firstBitZero_mem_P, nonempty_mem_P — all in P (and hence in every larger class).
• nonempty_eq_compl_singletonEmpty — the nonempty language is the complement of {[]}, giving a second derivation of its P-membership.
• firstBitZero_union_firstBitOne_eq_nonempty — explicit Boolean identity used to present nonempty as a union.

def Complexity.firstCell : List Bool → Γ

The first cell after ▷ on the initial input tape, as a Γ symbol. This is the cell the machine reads on its second step.

Equations

• Complexity.firstCell [] = Complexity.Γ.blank
• Complexity.firstCell (b :: tail) = Complexity.Γ.ofBool b

@[simp]

theorem Complexity.firstCell_nil : firstCell [] = Γ.blank

@[simp]

theorem Complexity.firstCell_cons (b : Bool) (xs : List Bool) : firstCell (b :: xs) = Γ.ofBool b

theorem Complexity.firstCell_eq_initTape_cells_one (x : List Bool) : firstCell x = (Tape.init (List.map Γ.ofBool x)).cells 1

firstCell x reads cell 1 of the initial input tape.

inductive Complexity.TM.FirstCellPhase : Type

Control states of decideFirstCellTM.

• advance : FirstCellPhase
• decide : FirstCellPhase
• done : FirstCellPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqFirstCellPhase : DecidableEq FirstCellPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeFirstCellPhase : Fintype FirstCellPhase

Equations

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

def Complexity.TM.decideFirstCellTM {n : ℕ} (yesOn : Γ → Bool) : TM n

Parametric 3-state TM: advance past ▷ on input and output, then read input cell 1 and write 1 if yesOn iHead, else 0. Always halts in exactly 2 steps.

Equations

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

theorem Complexity.TM.decideFirstCellTM_reachesIn {n : ℕ} (yesOn : Γ → Bool) (x : List Bool) : ∃ (c' : Cfg n (decideFirstCellTM yesOn).Q), (decideFirstCellTM yesOn).reachesIn 2 ((decideFirstCellTM yesOn).initCfg x) c' ∧ (decideFirstCellTM yesOn).halted c' ∧ c'.output.cells 1 = if yesOn (firstCell x) = true then Γ.one else Γ.zero

decideFirstCellTM yesOn halts in exactly 2 steps on every input, with output cell 1 set to Γ.one if yesOn (firstCell x) is true and Γ.zero otherwise.

theorem Complexity.TM.decideFirstCellTM_decidesInTime {yesOn : Γ → Bool} {L : Language} (hL : ∀ (x : List Bool), x ∈ L ↔ yesOn (firstCell x) = true) : (decideFirstCellTM yesOn).DecidesInTime L fun (x : ℕ) => 2

Generic bridge from decideFirstCellTM_reachesIn to DecidesInTime. Whenever a language L is characterized by x ∈ L ↔ yesOn (firstCell x), the 0-work-tape version of decideFirstCellTM yesOn decides L in 2 steps.

@[reducible, inline]

abbrev Complexity.Language.singletonEmpty : Language

The language {[]}: the only accepted string is the empty one.

Equations

• Complexity.Language.singletonEmpty = {[]}

def Complexity.Language.firstBitOne : Language

Strings whose first bit is 1.

Equations

• Complexity.Language.firstBitOne = {x : List Bool | ∃ (xs : List Bool), x = true :: xs}

def Complexity.Language.firstBitZero : Language

Strings whose first bit is 0.

Equations

• Complexity.Language.firstBitZero = {x : List Bool | ∃ (xs : List Bool), x = false :: xs}

def Complexity.Language.nonempty : Language

Nonempty strings.

Equations

• Complexity.Language.nonempty = {x : List Bool | x ≠ []}

theorem Complexity.mem_singletonEmpty_iff (x : List Bool) : x ∈ Language.singletonEmpty ↔ decide (firstCell x = Γ.blank) = true

theorem Complexity.mem_firstBitOne_iff (x : List Bool) : x ∈ Language.firstBitOne ↔ decide (firstCell x = Γ.one) = true

theorem Complexity.mem_firstBitZero_iff (x : List Bool) : x ∈ Language.firstBitZero ↔ decide (firstCell x = Γ.zero) = true

theorem Complexity.mem_nonempty_iff (x : List Bool) : x ∈ Language.nonempty ↔ decide (firstCell x ≠ Γ.blank) = true

theorem Complexity.singletonEmpty_in_DTIME : Language.singletonEmpty ∈ DTIME fun (x : ℕ) => 2

{[]} ∈ DTIME(2): decided in 2 steps by decideFirstCellTM (· = Γ.blank).

theorem Complexity.firstBitOne_in_DTIME : Language.firstBitOne ∈ DTIME fun (x : ℕ) => 2

firstBitOne ∈ DTIME(2).

theorem Complexity.firstBitZero_in_DTIME : Language.firstBitZero ∈ DTIME fun (x : ℕ) => 2

firstBitZero ∈ DTIME(2).

theorem Complexity.nonempty_in_DTIME : Language.nonempty ∈ DTIME fun (x : ℕ) => 2

nonempty ∈ DTIME(2).

theorem Complexity.singletonEmpty_mem_P : Language.singletonEmpty ∈ P

{[]} ∈ P.

theorem Complexity.firstBitOne_mem_P : Language.firstBitOne ∈ P

firstBitOne ∈ P.

theorem Complexity.firstBitZero_mem_P : Language.firstBitZero ∈ P

firstBitZero ∈ P.

theorem Complexity.nonempty_mem_P : Language.nonempty ∈ P

nonempty ∈ P.

theorem Complexity.nonempty_eq_compl_singletonEmpty : Language.nonempty = Language.singletonEmptyᶜ

nonempty is the complement of {[]}.

theorem Complexity.firstBitZero_union_firstBitOne_eq_nonempty : Language.firstBitZero ∪ Language.firstBitOne = Language.nonempty

nonempty is the union of "first bit 0" and "first bit 1".

theorem Complexity.nonempty_mem_P_via_compl : Language.nonempty ∈ P

Alternative proof: nonempty ∈ P via P_compl applied to {[]} ∈ P.

theorem Complexity.nonempty_mem_P_via_union : Language.nonempty ∈ P

Alternative proof: nonempty ∈ P via P_union.