StackMachine.lean

/-
Letter-synchronous multi-stack machines.

A machine has a fixed control carrier and a fixed number `s` of stacks. On each
arriving input symbol it performs at most one of `push`/`keep`/`pop` on *each*
stack, choosing on the basis of the control state, the symbol, and the top
symbol of every stack. There is no length advice and no post-input step.
Finiteness is imposed when this operational model is specialized for the
published transfer theorem.
-/

namespace FPRD

/-- The three stack actions available in one synchronous step. -/
inductive StackOp (A : Type) where
  | push : A → StackOp A
  | keep : StackOp A
  | pop : StackOp A

namespace StackOp

variable {A : Type}

/-- Action on a stack held top-first.  `pop` of the empty stack is a no-op,
via `List.tail [] = []`; this is the "empty pop" case the encoding must also
get right. -/
def apply : StackOp A → List A → List A
  | .push a, l => a :: l
  | .keep, l => l
  | .pop, l => l.tail

@[simp] theorem apply_push (a : A) (l : List A) : (StackOp.push a).apply l = a :: l := rfl
@[simp] theorem apply_keep (l : List A) : (StackOp.keep : StackOp A).apply l = l := rfl
@[simp] theorem apply_pop (l : List A) : (StackOp.pop : StackOp A).apply l = l.tail := rfl

end StackOp

/-- A deterministic letter-synchronous `s`-stack machine.

`step q x tops` sees the top symbol of each stack (`none` for an empty stack)
and returns the next control state together with one action per stack. -/
structure StackMachine (Sym : Type) (Q : Type) (A : Type) (s : Nat) where
  step : Q → Sym → (Fin s → Option A) → Q × (Fin s → StackOp A)
  init : Q
  accept : Q → Bool

/-- A machine configuration: control state plus the contents of every stack,
each held top-first. -/
structure Config (Q : Type) (A : Type) (s : Nat) where
  ctrl : Q
  stacks : Fin s → List A

namespace StackMachine

variable {Sym Q A : Type} {s : Nat}

/-- One synchronous step on a configuration. -/
def stepConfig (M : StackMachine Sym Q A s) (c : Config Q A s) (x : Sym) :
    Config Q A s :=
  let r := M.step c.ctrl x (fun j => (c.stacks j).head?)
  { ctrl := r.1, stacks := fun j => (r.2 j).apply (c.stacks j) }

@[simp] theorem stepConfig_ctrl (M : StackMachine Sym Q A s) (c : Config Q A s) (x : Sym) :
    (M.stepConfig c x).ctrl = (M.step c.ctrl x (fun j => (c.stacks j).head?)).1 := rfl

@[simp] theorem stepConfig_stacks (M : StackMachine Sym Q A s) (c : Config Q A s)
    (x : Sym) (j : Fin s) :
    (M.stepConfig c x).stacks j =
      ((M.step c.ctrl x (fun j => (c.stacks j).head?)).2 j).apply (c.stacks j) := rfl

/-- The initial configuration: every stack empty. -/
def initConfig (M : StackMachine Sym Q A s) : Config Q A s where
  ctrl := M.init
  stacks := fun _ => []

/-- The configuration reached on a word. -/
def run (M : StackMachine Sym Q A s) (w : List Sym) : Config Q A s :=
  w.foldl M.stepConfig M.initConfig

/-- Acceptance: final control state only. -/
def decides (M : StackMachine Sym Q A s) (w : List Sym) : Bool :=
  M.accept (M.run w).ctrl

@[simp] theorem run_nil (M : StackMachine Sym Q A s) : M.run [] = M.initConfig := rfl

theorem run_append (M : StackMachine Sym Q A s) (w : List Sym) (x : Sym) :
    M.run (w ++ [x]) = M.stepConfig (M.run w) x := by
  simp [run, List.foldl_append]

end StackMachine

end FPRD