Simulating multi-stack machines on a single tape

AbbreviationTwo-step single-tape translation of a multi-stack machine#✓fully proved

For a multi-stack Turing machine \(M\) with stacks indexed by \(K\) and stack alphabets \(\Gamma_k\), this is the single-tape machine obtained by translating \(M\) first into a single-tape machine with a store and then into a plain single-tape machine. Its tape alphabet consists of a bottom-of-stack flag together with one optional symbol of \(\Gamma_k\) for each stack \(k\). Its states are pairs of an optional statement of the intermediate machine and a value of the internal state of \(M\).

abbrev tr : TM0.Machine (TM2to1.Γ' K Γ) (TM1to0.Λ' (TM2to1.tr M)) :=
  TM1to0.tr (TM2to1.tr M)

Used by 12

Used byThe decider within time · Single-tape emulation of halting multi-stack runs · Quadratic overhead of the single-tape emulation · Each step of the \(\mathrm{TM1}\) emulator is at most three single-tape steps · The emulation halts where the multi-stack machine halts · The halting problem for single-tape machines is undecidable · The decider outputs the answer bit · Finite single-tape emulation of a multi-stack machine · The emulation's final tape · The recognizer halts iff the multi-stack machine does · The emulation halts iff the multi-stack machine halts · The emulation visits finitely many states

TheoremThe emulation halts iff the multi-stack machine halts#✓fully proved

Let \(M\) be a multi-stack Turing machine with stacks indexed by \(K\), let \(k \in K\), and let \(L\) be a list over the alphabet of stack \(k\). The single-tape emulation of \(M\), started on the tape encoding of the stacks with \(L\) on stack \(k\) and all other stacks empty, halts if and only if \(M\), started with \(L\) on stack \(k\) and all other stacks empty, halts.

theorem tr_eval_dom (k : K) (L : List (Γ k)) :
    (TM0.eval (tr M) (TM2to1.trInit k L)).Dom ↔ (TM2.eval M k L).Dom

Uses 1 · Used by 2

Statement usesTwo-step single-tape translation of a multi-stack machine

Used byThe halting problem for single-tape machines is undecidable · The recognizer halts iff the multi-stack machine does

TheoremThe emulation visits finitely many states#✓fully proved

Let \(M\) be a multi-stack Turing machine whose internal state type is finite, and let \(S\) be a finite set of labels that supports \(M\). Then the single-tape emulation of \(M\) is supported by an explicit finite set of states built from \(S\) through the two translations: this set contains the initial state and is closed under the transitions of the emulation.

theorem tr_supports [Fintype σ] {S : Finset Λ} (ss : TM2.Supports M S) :
    TM0.Supports (tr M) ↑(TM1to0.trStmts (TM2to1.tr M) (TM2to1.trSupp M S))

Uses 1 · Used by 5

Statement usesTwo-step single-tape translation of a multi-stack machine

Used byThe decider within time · The halting problem for single-tape machines is undecidable · The decider outputs the answer bit · Finite single-tape emulation of a multi-stack machine · The recognizer halts iff the multi-stack machine does

TheoremEvery statement is supported by all labels#✓fully proved

If the label type \(\Lambda\) is finite, then every statement of a multi-stack Turing machine with labels \(\Lambda\) is supported by the finite set of all labels: every label it can jump to lies in this set.

theorem supportsStmt_univ [Fintype Λ] : ∀ q : TM2.Stmt Γ Λ σ, TM2.SupportsStmt Finset.univ q

Used by 1

Used byA multi-stack machine is supported by all its labels

TheoremA multi-stack machine is supported by all its labels#✓fully proved

A multi-stack Turing machine with finitely many labels is supported by the set of all its labels: this set contains the default label, and every statement of the machine is supported by it.

theorem supports_univ [Fintype Λ] : TM2.Supports M Finset.univ

Uses 1 · Used by 5

Proof usesEvery statement is supported by all labels

Used byThe decider within time · The halting problem for single-tape machines is undecidable · The decider outputs the answer bit · Finite single-tape emulation of a multi-stack machine · The recognizer halts iff the multi-stack machine does

TheoremThe initial configuration of a bundled multi-stack machine#✓fully proved

For a bundled multi-stack Turing machine and every list \(l\) over the alphabet of its input stack, the initial configuration of the bundled machine on \(l\) equals the generic multi-stack initial configuration with \(l\) on the input stack, when the main label is taken as the default label.

theorem initList_eq_init (tm : FinTM2) (l : List (tm.Γ tm.k₀)) :
    initList tm l = TM2.init tm.k₀ l

Used by 3

Used byQuadratic overhead of the single-tape emulation · Halting agrees with evaluation for multi-stack machines · The emulation's final tape

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.