Input and output alphabets for the compiled stack machine #
The adapter reads bits in stack-bottom order. Its input is therefore reversed before interpreting it as a TM2 stack, and its output is emitted in reverse stack order. Canonical string reversal accounts for both conventions. The finite-alphabet adapter keeps input and output alphabets independent; explicit binary coding is supplied by the endpoint simulator.
@[reducible, inline]
abbrev
Complexity.MathlibTM2.binaryAdapter
(tm : Turing.FinTM2)
[(k : tm.K) → Fintype (tm.Γ k)]
(input : tm.Γ tm.k₀ ≃ Bool)
(output : tm.Γ tm.k₁ ≃ Bool)
{Q : Type}
[Fintype Q]
[Inhabited Q]
(G : Turing.TM0.Machine (Turing.TM2to1.Γ' tm.K tm.Γ) Q)
:
Give a compiled stack machine an explicit marked-input and decoded-output interface.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
Complexity.MathlibTM2.alphabetAdapter
{α β : Type}
(tm : Turing.FinTM2)
[(k : tm.K) → Fintype (tm.Γ k)]
(input : tm.Γ tm.k₀ ≃ α)
(output : tm.Γ tm.k₁ ≃ β)
{Q : Type}
[Fintype Q]
[Inhabited Q]
(G : Turing.TM0.Machine (Turing.TM2to1.Γ' tm.K tm.Γ) Q)
:
Marked input and decoded output for independent finite source alphabets.
Equations
- One or more equations did not get rendered due to their size.