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
• TimeComputable.withMonotoneBound, PolyTimeComputable.withMonotoneBound: replace the time bound with a monotone one (its partialSups) without changing the machine

TODOs

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

structure Cslib.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 Turing.Dir

  The direction to move the tape head

@[instance_reducible]

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

structure Cslib.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.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

structure Cslib.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

@[instance_reducible]

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

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

The step function corresponding to a SingleTapeTM.

def Cslib.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.

def Cslib.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.)

def Cslib.Turing.SingleTapeTM.Cfg.spaceUsed {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.

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

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

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

def Cslib.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.

def Cslib.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.

def Cslib.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.

theorem Cslib.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 Cslib.Turing.SingleTapeTM.idComputer {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] : SingleTapeTM Symbol

A Turing machine computing the identity.

def Cslib.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.

Composition Computer Lemmas

theorem Cslib.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 Cslib.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

• timeBound : ℕ → ℕ

  a bound on runtime

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

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

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

The identity map on Symbol is computable in constant time.

def Cslib.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.timeBound) : 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.

def Cslib.Turing.SingleTapeTM.TimeComputable.withMonotoneBound {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {f : List Symbol → List Symbol} (hf : TimeComputable f) : TimeComputable f

Convert a TimeComputable to one with a monotone time bound, by replacing the time bound t with partialSups t, i.e. n ↦ max (t 0) ⋯ (t n). The underlying machine is unchanged.

theorem Cslib.Turing.SingleTapeTM.TimeComputable.withMonotoneBound_timeBound_monotone {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {f : List Symbol → List Symbol} (hf : TimeComputable f) : Monotone hf.withMonotoneBound.timeBound

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 Cslib.Turing.SingleTapeTM.PolyTimeComputable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (f : List Symbol → List Symbol) extends Cslib.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
• timeBound : ℕ → ℕ
• outputsFunInTime (a : List Symbol) : self.tm.OutputsWithinTime a (f a) (self.timeBound a.length)
• poly : Polynomial ℕ

  a polynomial time bound

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

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

noncomputable def Cslib.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.

noncomputable def Cslib.Turing.SingleTapeTM.PolyTimeComputable.withMonotoneBound {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {f : List Symbol → List Symbol} (hf : PolyTimeComputable f) : PolyTimeComputable f

Convert a PolyTimeComputable to one with a monotone time bound. The polynomial bound is unchanged, since polynomial evaluation over ℕ is monotone.

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

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

The time bound of hg is first replaced by a monotone one via withMonotoneBound, so that no monotonicity assumption is required of the caller.