Running two single-tape machines one after the other

DefinitionEmbedding the first machine's configurations into a composite#✓fully proved

Let \(M_1\) and \(M_2\) be single-tape Turing machines over the same alphabet, and let \(M\) be their composite, whose states are the disjoint union of those of \(M_1\) and of \(M_2\): \(M\) starts in the start state of \(M_1\) and runs \(M_1\), where \(M_1\) would halt it enters the start state of \(M_2\) instead, and it then runs \(M_2\) and halts where \(M_2\) halts. A configuration of \(M_1\) with tape \(t\) is sent to the configuration of \(M\) with the same tape \(t\) whose state is the copy of \(q\) if \(M_1\) is in state \(q\), and the start state of \(M_2\) if \(M_1\) has halted.

def compCfgLeft (c : tm1.Cfg) : (compComputer tm1 tm2).Cfg :=
  ⟨some (c.state.elim (.inr tm2.q₀) .inl), c.BiTape⟩

Sources

public version of upstream CSLib's private toCompCfg_left.

Used by 4

Used byOutputs compose · Timed outputs compose · Halting of a composite · The composite simulates steps of the first machine

DefinitionEmbedding the second machine's configurations into a composite#✓fully proved

Let \(M_1\) and \(M_2\) be single-tape Turing machines over the same alphabet, and let \(M\) be their composite, whose states are the disjoint union of those of \(M_1\) and of \(M_2\): \(M\) starts in the start state of \(M_1\) and runs \(M_1\), where \(M_1\) would halt it enters the start state of \(M_2\) instead, and it then runs \(M_2\) and halts where \(M_2\) halts. A configuration of \(M_2\) with tape \(t\) is sent to the configuration of \(M\) with the same tape \(t\) whose state is the copy of \(q\) if \(M_2\) is in state \(q\), and which is halted if \(M_2\) has halted.

def compCfgRight (c : tm2.Cfg) : (compComputer tm1 tm2).Cfg :=
  ⟨c.state.map .inr, c.BiTape⟩

Sources

public version of upstream CSLib's private toCompCfg_right.

Used by 6

Used byOutputs compose · Timed outputs compose · Runs of a composite from configurations of the second machine · Halting of a composite · Step function of a composite on configurations of the second machine · The composite simulates steps of the second machine

TheoremThe composite simulates steps of the first machine#✓fully proved

Let \(M_1\) and \(M_2\) be single-tape Turing machines over the same alphabet, and let \(M\) be their composite, whose states are the disjoint union of those of \(M_1\) and of \(M_2\): \(M\) starts in the start state of \(M_1\) and runs \(M_1\), where \(M_1\) would halt it enters the start state of \(M_2\) instead, and it then runs \(M_2\) and halts where \(M_2\) halts. Let \(\iota_1\) send a configuration of \(M_1\) to the configuration of \(M\) with the same tape whose state is the copy of the state of \(M_1\), or the start state of \(M_2\) if \(M_1\) has halted. If \(M_1\) moves from a configuration \(c\) to a configuration \(c'\) in one step, then \(M\) moves from \(\iota_1(c)\) to \(\iota_1(c')\) in one step.

theorem transitionRelation_compCfgLeft {c c' : tm1.Cfg} (h : tm1.TransitionRelation c c') :
    (compComputer tm1 tm2).TransitionRelation (compCfgLeft tm1 tm2 c) (compCfgLeft tm1 tm2 c')

Sources

upstream CSLib's private map_toCompCfg_left_step, stated as a relation.

Uses 1 · Used by 3

Statement usesEmbedding the first machine's configurations into a composite

Used byOutputs compose · Timed outputs compose · Halting of a composite

TheoremStep function of a composite on configurations of the second machine#✓fully proved

Let \(M_1\) and \(M_2\) be single-tape Turing machines over the same alphabet, and let \(M\) be their composite, whose states are the disjoint union of those of \(M_1\) and of \(M_2\): \(M\) starts in the start state of \(M_1\) and runs \(M_1\), where \(M_1\) would halt it enters the start state of \(M_2\) instead, and it then runs \(M_2\) and halts where \(M_2\) halts. Let \(\iota_2\) send a configuration of \(M_2\) to the configuration of \(M\) with the same tape whose state is the copy of the state of \(M_2\), halted if \(M_2\) has halted. For every configuration \(c\) of \(M_2\): if \(M_2\) moves from \(c\) to \(c'\) in one step, then \(M\) moves from \(\iota_2(c)\) to \(\iota_2(c')\) in one step, and if \(c\) has no successor in \(M_2\), then \(\iota_2(c)\) has no successor in \(M\).

theorem step_compCfgRight (c : tm2.Cfg) :
    (compComputer tm1 tm2).step (compCfgRight tm1 tm2 c) =
      (tm2.step c).map (compCfgRight tm1 tm2)

Sources

upstream CSLib's private map_toCompCfg_right_step.

Uses 1 · Used by 2

Statement usesEmbedding the second machine's configurations into a composite

Used byRuns of a composite from configurations of the second machine · The composite simulates steps of the second machine

TheoremThe composite simulates steps of the second machine#✓fully proved

Let \(M_1\) and \(M_2\) be single-tape Turing machines over the same alphabet, and let \(M\) be their composite, whose states are the disjoint union of those of \(M_1\) and of \(M_2\): \(M\) starts in the start state of \(M_1\) and runs \(M_1\), where \(M_1\) would halt it enters the start state of \(M_2\) instead, and it then runs \(M_2\) and halts where \(M_2\) halts. Let \(\iota_2\) send a configuration of \(M_2\) to the configuration of \(M\) with the same tape whose state is the copy of the state of \(M_2\), halted if \(M_2\) has halted. If \(M_2\) moves from a configuration \(c\) to a configuration \(c'\) in one step, then \(M\) moves from \(\iota_2(c)\) to \(\iota_2(c')\) in one step.

theorem transitionRelation_compCfgRight {c c' : tm2.Cfg} (h : tm2.TransitionRelation c c') :
    (compComputer tm1 tm2).TransitionRelation (compCfgRight tm1 tm2 c)
      (compCfgRight tm1 tm2 c')

Uses 2 · Used by 3

Statement usesEmbedding the second machine's configurations into a composite

Proof usesStep function of a composite on configurations of the second machine

Used byOutputs compose · Timed outputs compose · Halting of a composite

TheoremRuns of a composite from configurations of the second machine#✓fully proved

Let \(M_1\) and \(M_2\) be single-tape Turing machines over the same alphabet, and let \(M\) be their composite, whose states are the disjoint union of those of \(M_1\) and of \(M_2\): \(M\) starts in the start state of \(M_1\) and runs \(M_1\), where \(M_1\) would halt it enters the start state of \(M_2\) instead, and it then runs \(M_2\) and halts where \(M_2\) halts. Let \(\iota_2\) send a configuration of \(M_2\) to the configuration of \(M\) with the same tape whose state is the copy of the state of \(M_2\), halted if \(M_2\) has halted. If \(c\) is a configuration of \(M_2\) and \(M\) moves from \(\iota_2(c)\) to a configuration \(d\) in finitely many (possibly zero) steps, then there is a configuration \(c'\) of \(M_2\) such that \(M_2\) moves from \(c\) to \(c'\) in finitely many (possibly zero) steps and \(d = \iota_2(c')\).

theorem exists_of_reflTransGen_compCfgRight {c : tm2.Cfg} {d : (compComputer tm1 tm2).Cfg}
    (h : ReflTransGen (compComputer tm1 tm2).TransitionRelation (compCfgRight tm1 tm2 c) d) :
    ∃ c', ReflTransGen tm2.TransitionRelation c c' ∧ d = compCfgRight tm1 tm2 c'

Uses 2 · Used by 1

Statement usesEmbedding the second machine's configurations into a composite

Proof usesStep function of a composite on configurations of the second machine

Used byHalting of a composite

TheoremOutputs compose#✓fully proved

Let \(M_1\) and \(M_2\) be single-tape Turing machines over the same alphabet, and let \(M\) be their composite, whose states are the disjoint union of those of \(M_1\) and of \(M_2\): \(M\) starts in the start state of \(M_1\) and runs \(M_1\), where \(M_1\) would halt it enters the start state of \(M_2\) instead, and it then runs \(M_2\) and halts where \(M_2\) halts. Say that a machine outputs a word \(w\) on a word \(v\) when, started in its start state on a tape holding \(v\), it reaches the halted configuration whose tape holds exactly \(w\), with the head at the start of \(w\). For all words \(a\), \(b\), \(c\): if \(M_1\) outputs \(b\) on \(a\) and \(M_2\) outputs \(c\) on \(b\), then \(M\) outputs \(c\) on \(a\).

theorem Outputs.compComputer {a b c : List Symbol} (h₁ : tm1.Outputs a b)
    (h₂ : tm2.Outputs b c) : (compComputer tm1 tm2).Outputs a c

Uses 4 · Used by 1

Proof usesEmbedding the first machine's configurations into a composite · Embedding the second machine's configurations into a composite · The composite simulates steps of the first machine · The composite simulates steps of the second machine

Used byThe decider outputs the answer bit

TheoremTimed outputs compose#✓fully proved

Let \(M_1\) and \(M_2\) be single-tape Turing machines over the same alphabet, and let \(M\) be their composite, whose states are the disjoint union of those of \(M_1\) and of \(M_2\): \(M\) starts in the start state of \(M_1\) and runs \(M_1\), where \(M_1\) would halt it enters the start state of \(M_2\) instead, and it then runs \(M_2\) and halts where \(M_2\) halts. Say that a machine outputs a word \(w\) on a word \(v\) within \(t\) steps when, started in its start state on a tape holding \(v\), it reaches in at most \(t\) steps the halted configuration whose tape holds exactly \(w\), with the head at the start of \(w\). For all words \(a\), \(b\), \(c\) and all natural numbers \(t_1\), \(t_2\): if \(M_1\) outputs \(b\) on \(a\) within \(t_1\) steps and \(M_2\) outputs \(c\) on \(b\) within \(t_2\) steps, then \(M\) outputs \(c\) on \(a\) within \(t_1 + t_2\) steps.

theorem OutputsWithinTime.compComputer {a b c : List Symbol} {t₁ t₂ : ℕ}
    (h₁ : tm1.OutputsWithinTime a b t₁) (h₂ : tm2.OutputsWithinTime b c t₂) :
    (compComputer tm1 tm2).OutputsWithinTime a c (t₁ + t₂)

Uses 4 · Used by 1

Proof usesEmbedding the first machine's configurations into a composite · Embedding the second machine's configurations into a composite · The composite simulates steps of the first machine · The composite simulates steps of the second machine

Used byThe decider within time

TheoremHalting of a composite#✓fully proved

Let \(M_1\) and \(M_2\) be single-tape Turing machines over the same alphabet, and let \(M\) be their composite, whose states are the disjoint union of those of \(M_1\) and of \(M_2\): \(M\) starts in the start state of \(M_1\) and runs \(M_1\), where \(M_1\) would halt it enters the start state of \(M_2\) instead, and it then runs \(M_2\) and halts where \(M_2\) halts. Say that a machine outputs a word \(w\) on a word \(v\) when, started in its start state on a tape holding \(v\), it reaches the halted configuration whose tape holds exactly \(w\), with the head at the start of \(w\). For all words \(a\) and \(b\) such that \(M_1\) outputs \(b\) on \(a\): \(M\), started in its start state on a tape holding \(a\), halts if and only if \(M_2\), started in its start state on a tape holding \(b\), halts.

theorem haltsOn_compComputer_iff {a b : List Symbol} (h₁ : tm1.Outputs a b) :
    (compComputer tm1 tm2).HaltsOn a ↔ tm2.HaltsOn b

Uses 7 · Used by 1

Statement usesHalting on an input

Proof usesEmbedding the first machine's configurations into a composite · Embedding the second machine's configurations into a composite · Runs of a composite from configurations of the second machine · Single-tape Turing machines are deterministic · The composite simulates steps of the first machine · The composite simulates steps of the second machine

Used byThe recognizer halts iff the multi-stack machine does

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.