Deterministic Multi-Tape Turing Machines

A deterministic Turing machine is a nondeterministic machine whose transition relation has exactly one action for every combination of state and symbols read. From the transition relation it derives a transition function tr and a function step which maps each configuration to its unique successor configuration (a halted configuration maps to itself).

The design choices for configurations and actions are documented in Cslib.Computability.Machines.Turing.MultiTape.Configuration.

Important Declarations

We define a number of structures and concepts related to multi-tape Turing machine computation:

• MultiTapeNTM.IsDeterministic: the transition relation relates every state and tuple of read symbols to exactly one action
• MultiTapeTM: the TM itself
• tr, ofTr: the derived transition function and construction from a function
• adapt: the machine run through an adapter
• combine: two machines on the same tapes combined into one
• step, runFrom: the successor configuration and iteration of this function
• MultiTapeNTM.RunPath.ofDeterministic, MultiTapeNTM.ComputationPath.ofDeterministic: paths of a given length from an arbitrary or initial configuration
• Computes: the machine halts with the given output on an input
• ComputesInTimeAndSpace: the machine produces an output within the shared resource bounds
• ComputesFunInTimeAndSpace: function computation with the shared time and space bounds
• ComputableInTimeAndSpace: such a machine exists with binary alphabet and finitely many states.
• ComputableInTimeAndSpaceOfLength: the specialization to bounds on encoded input length.
• DecidableInTimeAndSpace: a proof that a TM decides a language within a certain time and space bound.

def Turing.MultiTapeNTM.IsDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (ntm : MultiTapeNTM k Symbol State) : Prop

Every state and tuple of read symbols is related to exactly one action by ntm's transition relation.

Equations

• ntm.IsDeterministic = ∀ (q : State) (input : Option Symbol) (work : Fin k → Option Symbol), ∃! action : Turing.Action k Symbol State, ntm.Tr q input work action

structure Turing.MultiTapeTM (k : ℕ) (Symbol : Type u_3) (State : Type u_4) extends Turing.MultiTapeNTM k Symbol State : Type (max u_3 u_4)

A multi-tape Turing machine with k work tapes over the alphabet of Option Symbol (where none is the blank tape symbol). Note that it is not required that Symbol or State are finite to keep the definition more general. The restriction will be introduced once we start talking about computability by Turing machines in general.

• q₀ : State
• Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) (action : Action k Symbol State) : Prop
• deterministic : self.IsDeterministic

  Every state and tuple of read symbols is related to exactly one action by the transition relation.

@[instance_reducible]

instance Turing.instCoeOutMultiTapeTMMultiTapeNTM {k : ℕ} {State : Type u_1} {Symbol : Type u_2} : CoeOut (MultiTapeTM k Symbol State) (MultiTapeNTM k Symbol State)

Equations

• Turing.instCoeOutMultiTapeTMMultiTapeNTM = { coe := Turing.MultiTapeTM.toMultiTapeNTM }

noncomputable def Turing.MultiTapeTM.tr {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : Action k Symbol State

The unique action related to the given state and read symbols by Tr.

Equations

• tm.tr q input work = Exists.choose ⋯

@[simp]

theorem Turing.MultiTapeTM.tr_iff {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {q : State} {input : Option Symbol} {work : Fin k → Option Symbol} {action : Action k Symbol State} : tm.Tr q input work action ↔ tm.tr q input work = action

Tr relates a state and read symbols to an action exactly when tr returns that action.

def Turing.MultiTapeTM.ofTr {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (q₀ : State) (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State) : MultiTapeTM k Symbol State

Construct a deterministic machine from an initial state and transition function.

Equations

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

@[simp]

theorem Turing.MultiTapeTM.q₀_ofTr {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (q₀ : State) (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State) : (ofTr q₀ tr).q₀ = q₀

The initial state of ofTr is the supplied one.

@[simp]

theorem Turing.MultiTapeTM.tr_ofTr {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (q₀ : State) (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State) (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : (ofTr q₀ tr).tr q input work = tr q input work

Extracting the transition of ofTr recovers the supplied function.

noncomputable def Turing.MultiTapeTM.adaptedTr {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {k' : ℕ} {State' : Type u_3} (tm : MultiTapeTM k Symbol State) (adapter : MultiTapeNTM.Adapter k k' Symbol State State') (q : State) (inp : Option Symbol) (work : Fin k' → Option Symbol) : Action k' Symbol State'

The transitions of tm performed through adapter: it reads what tm reads through adapter and performs the adaptation of the action of tm.

Equations

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

noncomputable def Turing.MultiTapeTM.adapt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {k' : ℕ} (tm : MultiTapeTM k Symbol State) (adapter : MultiTapeNTM.Adapter k k' Symbol State State) : MultiTapeTM k' Symbol State

tm run through adapter, a MultiTapeNTM.Adapter: the adapter computes what tm reads from the symbols under the heads of the new machine, and gives the action of the new machine performing each action of tm. In state q, tm.adapt adapter performs the adaptation of the action of tm in q on what the adapter reads.

Equations

• tm.adapt adapter = Turing.MultiTapeTM.ofTr tm.q₀ (tm.adaptedTr adapter)

theorem Turing.MultiTapeTM.follows_adapt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {k' : ℕ} {adapter : MultiTapeNTM.Adapter k k' Symbol State State} : (tm.adapt adapter).Follows tm.toMultiTapeNTM id adapter

tm.adapt adapter follows tm.

noncomputable def Turing.MultiTapeTM.combine {k : ℕ} {Symbol : Type u_2} {State₀ : Type u_3} {State₁ : Type u_4} (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) (next₀ : Option State₀ → Option (State₀ ⊕ State₁)) (next₁ : Option State₁ → Option (State₀ ⊕ State₁)) (q₀ : State₀ ⊕ State₁) : MultiTapeTM k Symbol (State₀ ⊕ State₁)

tm₀ and tm₁ combined into one machine on their shared tapes, which starts in q₀: in a state inl q it performs the transition of tm₀ in q, and in inr q that of tm₁. The maps next₀ and next₁ say where the steps of each machine lead: within the same machine, to the other machine, or to halting.

Equations

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

def Turing.MultiTapeTM.handOver {State₀ : Type u_3} {State₁ : Type u_4} (q₁ : State₁) (state : Option State₀) : Option (State₀ ⊕ State₁)

Where the steps of a first machine lead when it runs in its own states: halting hands over to the second machine in its state q₁.

Equations

• Turing.MultiTapeTM.handOver q₁ state = some (state.elim (Sum.inr q₁) Sum.inl)

@[simp]

theorem Turing.MultiTapeTM.handOver_some {State₀ : Type u_3} {State₁ : Type u_4} (q₁ : State₁) (q : State₀) : handOver q₁ (some q) = some (Sum.inl q)

@[simp]

theorem Turing.MultiTapeTM.handOver_none {State₀ : Type u_3} {State₁ : Type u_4} (q₁ : State₁) : handOver q₁ none = some (Sum.inr q₁)

theorem Turing.MultiTapeTM.follows_combine_left {k : ℕ} {Symbol : Type u_2} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {next₁ : Option State₁ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} : (tm₀.combine tm₁ next₀ next₁ q₀).Follows tm₀.toMultiTapeNTM Sum.inl (MultiTapeNTM.Adapter.mapState next₀)

In its states inl q, the combined machine follows tm₀, its steps leading along next₀.

theorem Turing.MultiTapeTM.follows_combine_right {k : ℕ} {Symbol : Type u_2} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {next₁ : Option State₁ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} : (tm₀.combine tm₁ next₀ next₁ q₀).Follows tm₁.toMultiTapeNTM Sum.inr (MultiTapeNTM.Adapter.mapState next₁)

In its states inr q, the combined machine follows tm₁, its steps leading along next₁.

noncomputable def Turing.MultiTapeTM.combineLeftHom {k : ℕ} {Symbol : Type u_2} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {next₁ : Option State₁ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} {input : List Symbol} (h : ∀ (q : State₀), next₀ (some q) = some (Sum.inl q)) : (tm₀.runningStepRel input).Hom ((tm₀.combine tm₁ next₀ next₁ q₀).stepRel input)

If next₀ keeps the live states of tm₀ in tm₀, the combined machine mirrors the running steps of tm₀, its states relabeled along next₀.

Equations

• Turing.MultiTapeTM.combineLeftHom h = ⋯.runningStepHom (Turing.Cfg.mapState next₀) ⋯ ⋯ ⋯

@[simp]

theorem Turing.MultiTapeTM.combineLeftHom_apply {k : ℕ} {Symbol : Type u_2} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {next₁ : Option State₁ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} {input : List Symbol} (h : ∀ (q : State₀), next₀ (some q) = some (Sum.inl q)) (c : Cfg k Symbol State₀ input) : (combineLeftHom h) c = Cfg.mapState next₀ c

noncomputable def Turing.MultiTapeTM.combineRightHom {k : ℕ} {Symbol : Type u_2} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} {input : List Symbol} : (tm₁.stepRel input).Hom ((tm₀.combine tm₁ next₀ (Option.map Sum.inr) q₀).stepRel input)

If the steps of tm₁ stay in tm₁, the combined machine mirrors them.

Equations

• Turing.MultiTapeTM.combineRightHom = ⋯.stepHom (Turing.Cfg.mapState (Option.map Sum.inr)) ⋯ ⋯ ⋯

@[simp]

theorem Turing.MultiTapeTM.combineRightHom_apply {k : ℕ} {Symbol : Type u_2} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} {input : List Symbol} (c : Cfg k Symbol State₁ input) : combineRightHom c = Cfg.mapState (Option.map Sum.inr) c

Stepping a Turing Machine

The step function lets the machine transition from one configuration to the next, and runFrom gives the configuration reached after a number of steps. Configurations themselves are defined in Cslib.Computability.Machines.Turing.MultiTape.Configuration.

noncomputable def Turing.MultiTapeTM.step {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) : Cfg k Symbol State input

The unique successor configuration related to cfg by the inherited step relation.

Equations

• Turing.MultiTapeTM.step cfg = Exists.choose ⋯

@[simp]

theorem Turing.MultiTapeTM.step_iff {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ step c = c'

Step relates c to c' exactly when step c = c'.

theorem Turing.MultiTapeTM.step_of_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {q : State} (h : cfg.state = some q) : step cfg = (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).apply cfg

A running configuration takes the action selected by the transition function.

theorem Turing.MultiTapeTM.step_inputPos_of_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {q : State} (h : cfg.state = some q) : (step cfg).inputPos = moveInputPos cfg.inputPos (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputTape

The input head after a live step.

theorem Turing.MultiTapeTM.step_workTapes_of_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {q : State} (h : cfg.state = some q) (i : Fin k) : (step cfg).workTapes i = match (motive := Option (Option Symbol) → ℤ → Option Symbol) ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workTapes i).1 with | none => cfg.workTapes i | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s

A work tape after a live step.

theorem Turing.MultiTapeTM.step_workTapePos_of_state {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {q : State} (h : cfg.state = some q) (i : Fin k) : (step cfg).workTapePos i = cfg.workTapePos i + ↑((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workTapes i).2

A work tape head after a live step.

@[simp]

theorem Turing.MultiTapeTM.step_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} (h : cfg.state = none) : step cfg = cfg

noncomputable def Turing.MultiTapeNTM.RunPath.ofDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : tm.RunPath input

The path of the first t steps from cfg.

Equations

• Turing.MultiTapeNTM.RunPath.ofDeterministic tm cfg t = { length := t, toFun := fun (n : Fin (t + 1)) => Turing.MultiTapeTM.step^[↑n] cfg, step := ⋯ }

theorem Turing.MultiTapeNTM.RunPath.eq_ofDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.RunPath input) : p = ofDeterministic tm (RelSeries.head p) p.time

Every deterministic run path is the canonical path from its head for its duration.

noncomputable def Turing.MultiTapeNTM.ComputationPath.ofDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : tm.ComputationPath input

The path of the first t steps on input, starting at the initial configuration.

Equations

• Turing.MultiTapeNTM.ComputationPath.ofDeterministic tm input t = { toRunPath := Turing.MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) t, head_eq := ⋯ }

theorem Turing.MultiTapeNTM.ComputationPath.eq_ofDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.ComputationPath input) : p = ofDeterministic tm input p.time

Every deterministic computation path is the canonical path for its duration.

theorem Turing.MultiTapeNTM.RunPath.eq_take {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {p q : tm.RunPath input} (hhead : RelSeries.head p = RelSeries.head q) (h : p.length ≤ q.length) : p = RelSeries.take q ⟨p.length, ⋯⟩

Deterministic run paths from the same configuration are prefixes of one another: the shorter one is the longer one, cut at its length.

theorem Turing.MultiTapeNTM.ComputationPath.spaceUsedByTape_le_of_space_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.ComputationPath input) {q : tm.ComputationPath input} (h : p.space ≤ q.space) : p.spaceUsedByTape ≤ q.spaceUsedByTape

The computation paths of a deterministic machine are prefixes of one another, so a path visiting at most as many cells as another visits at most as many on each tape.

theorem Turing.MultiTapeNTM.RunPath.map_ofDeterministic {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {k' : ℕ} {State' : Type u_3} {input' : List Symbol} {tm' : MultiTapeTM k' Symbol State'} (f : (tm.stepRel input).Hom (tm'.stepRel input')) (cfg : Cfg k Symbol State input) (t : ℕ) : (ofDeterministic tm cfg t).map f = ofDeterministic tm' (f cfg) t

A step-preserving map sends the path of t steps from cfg to the path of t steps from the image of cfg.

noncomputable def Turing.MultiTapeTM.runFrom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input

The configuration reached by running the Turing machine for t steps from cfg. If the Turing machine halts, it will stay at the halting configuration.

Equations

• Turing.MultiTapeTM.runFrom cfg t = Turing.MultiTapeTM.step^[t] cfg

theorem Turing.MultiTapeTM.runPath_apply_eq_runFrom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.RunPath input) (i : Fin (p.length + 1)) : p.toFun i = runFrom (RelSeries.head p) ↑i

Every path of a deterministic machine follows its iterated step function.

theorem Turing.MultiTapeTM.computationPath_last_eq_runFrom {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (p : tm.ComputationPath input) : p.last = runFrom (tm.initCfg input) p.time

A deterministic computation ends at the corresponding iterate.

theorem Turing.MultiTapeTM.runFrom_map {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {k' : ℕ} {State' : Type u_3} {input' : List Symbol} {tm' : MultiTapeTM k' Symbol State'} (f : (tm.stepRel input).Hom (tm'.stepRel input')) (cfg : Cfg k Symbol State input) (t : ℕ) : runFrom (f cfg) t = f (runFrom cfg t)

Running from the image of a configuration under a step-preserving map reaches the image of the original run.

theorem Turing.MultiTapeTM.runFrom_eq_of_halt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) (hhalt : (runFrom cfg τ).state = none) : runFrom cfg t = runFrom cfg τ

Nothing changes after the machine has halted.

theorem Turing.MultiTapeTM.runsInTime_of_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {t : ℕ} (h : (runFrom (tm.initCfg input) t).Halted) : tm.RunsInTime input t

A deterministic machine halted after t steps satisfies the shared time bound.

theorem Turing.MultiTapeTM.inputPos_runFrom_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : ↑(runFrom cfg t).inputPos ≤ ↑cfg.inputPos + t

In t steps the input head moves at most t positions to the right.

def Turing.MultiTapeTM.Computes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) (input output : List Symbol) : Prop

The machine eventually halts on input with the given output.

Equations

• tm.Computes input output = ∃ (u : ℕ), (Turing.MultiTapeTM.runFrom (tm.initCfg input) u).Halted ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg input) u).output = output

def Turing.MultiTapeTM.ComputesInTimeAndSpace {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) (input output : List Symbol) (t s : ℕ) : Prop

The machine computes output from input within the shared time and space bounds.

Equations

• tm.ComputesInTimeAndSpace input output t s = (tm.Computes input output ∧ tm.RunsInTime input t ∧ tm.RunsInSpace input s)

def Turing.MultiTapeTM.ComputesFunInTimeAndSpace {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {α : Type u_3} {β : Type u_4} (tm : MultiTapeTM k Symbol State) (encIn : α ↪ List Symbol) (encOut : β ↪ List Symbol) (f : α → β) (t s : α → ℕ) : Prop

The machine computes f relative to given encodings within the given time and space bounds.

Equations

• tm.ComputesFunInTimeAndSpace encIn encOut f t s = ∀ (a : α), tm.ComputesInTimeAndSpace (encIn a) (encOut (f a)) (t a) (s a)

theorem Turing.MultiTapeTM.ComputesFunInTimeAndSpace.mono {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {α : Type u_3} {β : Type u_4} {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol} {f : α → β} {t s t' s' : α → ℕ} (h : tm.ComputesFunInTimeAndSpace encIn encOut f t s) (ht : ∀ (a : α), t a ≤ t' a) (hs : ∀ (a : α), s a ≤ s' a) : tm.ComputesFunInTimeAndSpace encIn encOut f t' s'

Resource bounds can be weakened independently on every input.

def Turing.MultiTapeTM.ComputableInTimeAndSpace {α : Type u_3} {β : Type u_4} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (t s : α → ℕ) : Prop

Computability by a deterministic machine with a binary tape alphabet and finitely many states, within the supplied input-indexed bounds.

Equations

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

@[reducible, inline]

abbrev Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength {α : Type u_3} {β : Type u_4} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (t s : ℕ → ℕ) : Prop

There exists a binary Turing machine with finitely many states that, for every input a, computes encOut (f a) from encIn a in at most t (encIn a).length steps, using at most s (encIn a).length work-tape cells.

Equations

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

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.mono {α : Type u_3} {β : Type u_4} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s t' s' : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) (ht : ∀ (a : α), t a ≤ t' a) (hs : ∀ (a : α), s a ≤ s' a) : ComputableInTimeAndSpace f encIn encOut t' s'

Computability is monotone in the resource bounds.

noncomputable def Turing.MultiTapeTM.indicator {α : Type u_3} (L : Set α) : α → Bool

The Boolean indicator function of a set.

Equations

• Turing.MultiTapeTM.indicator L x = if x ∈ L then true else false

def Turing.MultiTapeTM.DecidableInTimeAndSpace {α : Type u_3} (L : Set α) (enc : α ↪ List Bool) (t s : α → ℕ) : Prop

A set is decidable within the given input-indexed bounds when its Boolean indicator is computable in those bounds.

Equations

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

theorem Turing.MultiTapeTM.not_halts_of_repeat_nonhalt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} (cfg : Cfg k Symbol State input) (h_not_halt : cfg.state ≠ none) (t : ℕ) (heq : runFrom cfg (t + 1) = cfg) (t' : ℕ) : (runFrom cfg t').state ≠ none

If a deterministic machine repeats a non-halting configuration, it never halts, because the sequence between the two configurations will loop forever. Note that this can be applied to two arbitrary and different time steps t and t + Δ using Function.iterate_add_apply.