Binary encodings of Mathlib's stack-machine configurations

Each stack retains its own alphabet. Labels, registers and symbols use the existing finite-type encoding; the stack family uses the dependent finite-table encoding. No tape direction or word reversal is involved.

Main definitions

• Turing.TM2.encCfg: encode a Mathlib TM2 configuration as a binary word.

Main results

• Turing.TM2.length_encCfg_le: bounded stack lengths give a linear configuration-size bound.

References

The configurations are those of Mathlib.Computability.TuringMachine.StackTuringMachine.

noncomputable def Turing.TM2.encCfg {K : Type} [Fintype K] {Γ : K → Type} {Λ σ : Type} [Finite Λ] [Finite σ] [∀ (k : K), Finite (Γ k)] : Cfg Γ Λ σ ↪ List Bool

Store the label, registers and all stacks using the library's standard binary encodings.

@[simp]

theorem Turing.TM2.encCfg_apply {K : Type} [Fintype K] {Γ : K → Type} {Λ σ : Type} [Finite Λ] [Finite σ] [∀ (k : K), Finite (Γ k)] (cfg : Cfg Γ Λ σ) : encCfg cfg = (MultiTapeTM.encPair (MultiTapeTM.encFinite (Option Λ)) (MultiTapeTM.encPair (MultiTapeTM.encFinite σ) (MultiTapeTM.encDPi fun (k : K) => MultiTapeTM.encList (MultiTapeTM.encFinite (Γ k))))) (cfg.l, cfg.var, cfg.stk)

theorem Turing.TM2.length_encCfg_le {K : Type} [Fintype K] {Γ : K → Type} {Λ σ : Type} [Finite Λ] [Finite σ] [∀ (k : K), Finite (Γ k)] : ∃ (C : ℕ), ∀ (cfg : Cfg Γ Λ σ) (bound : ℕ), (∀ (k : K), (cfg.stk k).length ≤ bound) → (encCfg cfg).length ≤ C * (bound + 1)

The constant depends only on the fixed stack alphabets, labels and registers.