lastBitOne and lastBitZero: final-symbol languages

Strings whose last bit is 1 (resp. 0); the empty string is not in either language. Decided by a 3-state scannerTM instance: the scan state is the last bit seen so far, or none if no bit has been read.

Main definitions

• Language.lastBitOne, Language.lastBitZero.
• TM.lastBitTM target — scannerTM specialized to target : Bool.

Main results

• lastBitOne_in_DTIME, lastBitZero_in_DTIME — both in DTIME(n + 2).
• lastBitOne_mem_P, lastBitZero_mem_P.

def Complexity.TM.lastBitTM (target : Bool) : TM 0

Scanner for "last input bit equals target". Scan state: the last bit seen so far as an Option Bool (none initially).

Equations

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

def Complexity.Language.lastBitZero : Language

Strings whose last bit is 0 (empty string excluded).

Equations

• Complexity.Language.lastBitZero = {x : List Bool | x.getLast? = some false}

def Complexity.Language.lastBitOne : Language

Strings whose last bit is 1 (empty string excluded).

Equations

• Complexity.Language.lastBitOne = {x : List Bool | x.getLast? = some true}

theorem Complexity.lastBitZero_in_DTIME : Language.lastBitZero ∈ DTIME fun (n : ℕ) => n + 2

lastBitZero ∈ DTIME(n + 2).

theorem Complexity.lastBitOne_in_DTIME : Language.lastBitOne ∈ DTIME fun (n : ℕ) => n + 2

lastBitOne ∈ DTIME(n + 2).

theorem Complexity.lastBitZero_mem_P : Language.lastBitZero ∈ P

lastBitZero ∈ P.

theorem Complexity.lastBitOne_mem_P : Language.lastBitOne ∈ P

lastBitOne ∈ P.