OAI/Combinatorics/UniformKServer/FlatTM2.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Flatten Mathlib's finitely supported TM2 programs into literal single stack primitives. Every variable type and alphabet in this compiler is finite. In particular a TM2 expression's arithmetic is not counted as one bit step.

  1. abbrev OAI.UniformKServer.FlatTM2.Node line 18
  2. abbrev OAI.UniformKServer.FlatTM2.Local line 19
  3. def OAI.UniformKServer.FlatTM2.nodes line 21
  4. def OAI.UniformKServer.FlatTM2.keys line 22
  5. def OAI.UniformKServer.FlatTM2.letters line 23
  6. def OAI.UniformKServer.FlatTM2.done line 25
  7. def OAI.UniformKServer.FlatTM2.root line 27
  8. def OAI.UniformKServer.FlatTM2.sub line 31
  9. def OAI.UniformKServer.FlatTM2.action line 36

    Source documentation

    The action is allowed to inspect only stack heads and the finite local variable. Its maps have finite domain and finite range.

    def action (x : Local M S) (hds : Fin (Fintype.card K) → Option (Fin (Fintype.card Γ))) :
    Action (Fintype.card (Local M S)) (Fintype.card K) (Fintype.card Γ) :=
…

    Mentions: OAI.UniformKServer.FlatTM2.Local

  10. def OAI.UniformKServer.FlatTM2.processor line 59

    Source documentation

    A finitely supported Mathlib TM2 has an actual finite-control processor. It will be initialized with its input on its designated stack.

    def processor (v₀ : V) : Processor (Fintype.card (Local M S)) (Fintype.card K) (Fintype.card Γ) where
…

    Mentions: OAI.UniformKServer.FlatTM2.Local