Single-Tape Turing Machines

Defines a single-tape Turing machine for computing functions on List Symbol for finite alphabet Symbol.

Design

Here are some design choices made in this file:

These machines have access to a single bidirectionally-infinite tape (BiTape) which uses symbols from Option Symbol.

The transition function of the machine takes a state and a tape alphabet character under the read-head (i.e. an Option Symbol) and returns a Stmt describing the tape action to take, as well as an optional new state to transition to (where none means halt).

We do not make the "halting state" a member of the state type for a few reasons:

• To avoid the need for passing a subtype of "non-halting states" to the transition function.
• To make clear that TMs are not expected to continue on after entering this special state (in contrast to, say, a DFA entering/leaving an accepting state).
• To make it simpler to match on halting when modifying a machine.

We also include the possibility for non-movement actions, for convenience in composition of machines.

Important Declarations

We define a number of structures related to Turing machine computation:

• Stmt: the write and movement operations a TM can do in a single step.
• SingleTapeTM: the TM itself.
• Cfg: the configuration of a TM, including internal and tape state.
• TimeComputable f: a TM for computing f, packaged with a bound on runtime.
• PolyTimeComputable f: TimeComputable f packaged with a polynomial bound on runtime.

We also provide ways of constructing polynomial-runtime TMs

• PolyTimeComputable.id: computes the identity function
• PolyTimeComputable.comp: computes the composition of polynomial time machines

TODOs

• Encoding of types in lists to represent computations on arbitrary types.
• Add ∘ notation for compComputer.

structure Turing.SingleTapeTM.Stmt (Symbol : Type) : Type

A Turing machine "statement" is just a Optional command to move left or right, and write a symbol (i.e. an Option Symbol, where none is the blank symbol) on the BiTape

• symbol : Option Symbol

  The symbol to write at the current head position

• movement : Option Dir

  The direction to move the tape head

@[implicit_reducible]

instance Turing.SingleTapeTM.instInhabitedStmt {a✝ : Type} : Inhabited (Stmt a✝)

Equations

• Turing.SingleTapeTM.instInhabitedStmt = { default := Turing.SingleTapeTM.instInhabitedStmt.default }

def Turing.SingleTapeTM.instInhabitedStmt.default {a✝ : Type} : Stmt a✝

Equations

• Turing.SingleTapeTM.instInhabitedStmt.default = { symbol := default, movement := default }

structure Turing.SingleTapeTM (Symbol : Type) [Inhabited Symbol] [Fintype Symbol] : Type 1

A single-tape Turing machine over the alphabet of Option Symbol (where none is the blank BiTape symbol).

• State : Type

  type of state labels

• stateFintype : Fintype self.State

  finiteness of the state type

• q₀ : self.State

  Initial state

• tr : self.State → Option Symbol → Stmt Symbol × Option self.State

  Transition function, mapping a state and a head symbol to a Stmt to invoke, and optionally the new state to transition to afterwards (none for halt)

Configurations of a Turing Machine

This section defines the configurations of a Turing machine, the step function that lets the machine transition from one configuration to the next, and the intended initial and final configurations.

@[implicit_reducible]

instance Turing.SingleTapeTM.instInhabitedState {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : Inhabited tm.State

Equations

• tm.instInhabitedState = { default := tm.q₀ }

@[implicit_reducible]

instance Turing.SingleTapeTM.instFintypeState {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : Fintype tm.State

Equations

• tm.instFintypeState = tm.stateFintype

@[implicit_reducible]

instance Turing.SingleTapeTM.inhabitedStmt {Symbol : Type} : Inhabited (Stmt Symbol)

Equations

• Turing.SingleTapeTM.inhabitedStmt = inferInstance

structure Turing.SingleTapeTM.Cfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : Type

The configurations of a Turing machine consist of: an Optional state (or none for the halting state), and a BiTape representing the tape contents.

• state : Option tm.State

  the state of the TM (or none for the halting state)

• BiTape : Turing.BiTape Symbol

  the BiTape contents

def Turing.SingleTapeTM.instInhabitedCfg.default {a✝ : Type} {a✝¹ : Inhabited a✝} {a✝² : Fintype a✝} {a✝³ : SingleTapeTM a✝} : a✝³.Cfg

Equations

• Turing.SingleTapeTM.instInhabitedCfg.default = { state := default, BiTape := default }

@[implicit_reducible]

instance Turing.SingleTapeTM.instInhabitedCfg {a✝ : Type} {a✝¹ : Inhabited a✝} {a✝² : Fintype a✝} {a✝³ : SingleTapeTM a✝} : Inhabited a✝³.Cfg

Equations

• Turing.SingleTapeTM.instInhabitedCfg = { default := Turing.SingleTapeTM.instInhabitedCfg.default }

def Turing.SingleTapeTM.step {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : tm.Cfg → Option tm.Cfg

The step function corresponding to a SingleTapeTM.

Equations

• tm.step { state := none, BiTape := BiTape } = none
• tm.step { state := some q', BiTape := t } = match tm.tr q' t.head with | ({ symbol := wr, movement := dir }, q'') => some { state := q'', BiTape := (t.write wr).optionMove dir }

def Turing.SingleTapeTM.initCfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg

The initial configuration corresponding to a list in the input alphabet. Note that the entries of the tape constructed by BiTape.mk₁ are all some values. This is to ensure that distinct lists map to distinct initial configurations.

Equations

• tm.initCfg s = { state := some tm.q₀, BiTape := Turing.BiTape.mk₁ s }

def Turing.SingleTapeTM.haltCfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg

The final configuration corresponding to a list in the output alphabet. (We demand that the head halts at the leftmost position of the output.)

Equations

• tm.haltCfg s = { state := none, BiTape := Turing.BiTape.mk₁ s }

def Turing.SingleTapeTM.Cfg.space_used {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (cfg : tm.Cfg) : ℕ

The space used by a configuration is the space used by its tape.

Equations

• Turing.SingleTapeTM.Cfg.space_used tm cfg = cfg.BiTape.space_used

theorem Turing.SingleTapeTM.Cfg.space_used_initCfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (s : List Symbol) : space_used tm (tm.initCfg s) = max 1 s.length

theorem Turing.SingleTapeTM.Cfg.space_used_haltCfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (s : List Symbol) : space_used tm (tm.haltCfg s) = max 1 s.length

theorem Turing.SingleTapeTM.Cfg.space_used_step {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {tm : SingleTapeTM Symbol} (cfg cfg' : tm.Cfg) (hstep : tm.step cfg = some cfg') : space_used tm cfg' ≤ space_used tm cfg + 1

def Turing.SingleTapeTM.TransitionRelation {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (c₁ c₂ : tm.Cfg) : Prop

The TransitionRelation corresponding to a SingleTapeTM Symbol is defined by the step function, which maps a configuration to its next configuration, if it exists.

Equations

• tm.TransitionRelation c₁ c₂ = (tm.step c₁ = some c₂)

def Turing.SingleTapeTM.Outputs {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l l' : List Symbol) : Prop

A proof of tm outputting l' on input l.

Equations

• tm.Outputs l l' = Relation.ReflTransGen tm.TransitionRelation (tm.initCfg l) (tm.haltCfg l')

def Turing.SingleTapeTM.OutputsWithinTime {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l l' : List Symbol) (m : ℕ) : Prop

A proof of tm outputting l' on input l in at most m steps.

Equations

• tm.OutputsWithinTime l l' m = Relation.RelatesWithinSteps tm.TransitionRelation (tm.initCfg l) (tm.haltCfg l') m

theorem Turing.SingleTapeTM.output_length_le_input_length_add_time {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l l' : List Symbol) (t : ℕ) (h : tm.OutputsWithinTime l l' t) : l'.length ≤ max 1 l.length + t

This lemma bounds the size blow-up of the output of a Turing machine. It states that the increase in length of the output over the input is bounded by the runtime. This is important for guaranteeing that composition of polynomial time Turing machines remains polynomial time, as the input to the second machine is bounded by the output length of the first machine.

def Turing.SingleTapeTM.idComputer {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] : SingleTapeTM Symbol

A Turing machine computing the identity.

Equations

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

def Turing.SingleTapeTM.compComputer {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm1 tm2 : SingleTapeTM Symbol) : SingleTapeTM Symbol

A Turing machine computing the composition of two other Turing machines.

If f and g are computed by Turing machines tm1 and tm2 then we can construct a Turing machine which computes g ∘ f by first running tm1 and then, when tm1 halts, transitioning to the start state of tm2 and running tm2.

Equations

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

Composition Computer Lemmas

theorem Turing.SingleTapeTM.compComputer_q₀_eq {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm1 tm2 : SingleTapeTM Symbol) : (tm1.compComputer tm2).q₀ = Sum.inl tm1.q₀

Time Computability

This section defines the notion of time-bounded Turing Machines

structure Turing.SingleTapeTM.TimeComputable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (f : List Symbol → List Symbol) : Type 1

A Turing machine + a time function + a proof it outputs f in at most time(input.length) steps.

• tm : SingleTapeTM Symbol

  the underlying bundled SingleTapeTM

• time_bound : ℕ → ℕ

  a bound on runtime

• outputsFunInTime (a : List Symbol) : self.tm.OutputsWithinTime a (f a) (self.time_bound a.length)

  proof this machine outputs f in at most time_bound(input.length) steps

def Turing.SingleTapeTM.TimeComputable.id {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] : TimeComputable _root_.id

The identity map on Symbol is computable in constant time.

Equations

• Turing.SingleTapeTM.TimeComputable.id = { tm := Turing.SingleTapeTM.idComputer, time_bound := fun (x : ℕ) => 1, outputsFunInTime := ⋯ }

def Turing.SingleTapeTM.TimeComputable.comp {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {f g : List Symbol → List Symbol} (hf : TimeComputable f) (hg : TimeComputable g) (h_mono : Monotone hg.time_bound) : TimeComputable (g ∘ f)

Time bounds for compComputer.

The compComputer of two machines which have time bounds is bounded by

• The time taken by the first machine on the input size
• added to the time taken by the second machine on the output size of the first machine (which is itself bounded by the time taken by the first machine)

Note that we require the time function of the second machine to be monotone; this is to ensure that if the first machine returns an output which is shorter than the maximum possible length of output for that input size, then the time bound for the second machine still holds for that shorter input to the second machine.

Equations

• hf.comp hg h_mono = { tm := hf.tm.compComputer hg.tm, time_bound := fun (l : ℕ) => hf.time_bound l + hg.time_bound (max 1 l + hf.time_bound l), outputsFunInTime := ⋯ }

Polynomial Time Computability

This section defines polynomial time computable functions on Turing machines, and proves that:

• The identity function is polynomial time computable
• The composition of two polynomial time computable functions is polynomial time computable

structure Turing.SingleTapeTM.PolyTimeComputable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (f : List Symbol → List Symbol) extends Turing.SingleTapeTM.TimeComputable f : Type 1

A Turing machine + a polynomial time function + a proof it outputs f in at most time(input.length) steps.

• tm : SingleTapeTM Symbol
• time_bound : ℕ → ℕ
• outputsFunInTime (a : List Symbol) : self.tm.OutputsWithinTime a (f a) (self.time_bound a.length)
• poly : Polynomial ℕ

  a polynomial time bound

• bounds (n : ℕ) : self.time_bound n ≤ Polynomial.eval n self.poly

  proof that this machine outputs f in at most time(input.length) steps

noncomputable def Turing.SingleTapeTM.PolyTimeComputable.id {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] : PolyTimeComputable _root_.id

A proof that the identity map on Symbol is computable in polytime.

Equations

• Turing.SingleTapeTM.PolyTimeComputable.id = { toTimeComputable := Turing.SingleTapeTM.TimeComputable.id, poly := 1, bounds := ⋯ }

noncomputable def Turing.SingleTapeTM.PolyTimeComputable.comp {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {f g : List Symbol → List Symbol} (hf : PolyTimeComputable f) (hg : PolyTimeComputable g) (h_mono : Monotone hg.time_bound) : PolyTimeComputable (g ∘ f)

A proof that the composition of two polytime computable functions is polytime computable.

Equations

• hf.comp hg h_mono = { toTimeComputable := hf.comp hg.toTimeComputable h_mono, poly := hf.poly + hg.poly.comp (1 + Polynomial.X + hf.poly), bounds := ⋯ }