Rational hitting lists: stack language

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/StackLanguage.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

def Complexity.RationalHitting.TMTime.exec {α : Type u_1} (step : α → Option α) : ℕ → α → Option α

Execute a partial transition function for exactly the specified number of steps.

Equations

• Complexity.RationalHitting.TMTime.exec step 0 x✝ = some x✝
• Complexity.RationalHitting.TMTime.exec step t.succ x✝ = (step x✝).bind (Complexity.RationalHitting.TMTime.exec step t)

@[simp]

theorem Complexity.RationalHitting.TMTime.exec_zero {α : Type u_1} (step : α → Option α) (a : α) : exec step 0 a = some a

theorem Complexity.RationalHitting.TMTime.exec_add {α : Type u_1} (step : α → Option α) (s t : ℕ) (a : α) : exec step (s + t) a = (exec step s a).bind (exec step t)

theorem Complexity.RationalHitting.TMTime.exec_trans {α : Type u_1} {step : α → Option α} {s t : ℕ} {a b c : α} (h : exec step s a = some b) (h' : exec step t b = some c) : exec step (s + t) a = some c

theorem Complexity.RationalHitting.TMTime.exec_positive_congr {α : Type u_1} {step : α → Option α} {t : ℕ} (ht : 0 < t) {a b : α} (h : step a = step b) : exec step t a = exec step t b

def Complexity.RationalHitting.TMTime.OneToZero.weight {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} : Turing.TM1.Stmt Γ Λ σ → ℕ

Syntactic statement bound, fixed once the finite machine is fixed.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.TMTime.OneToZero.weight (Turing.TM1.Stmt.move a q) = Complexity.RationalHitting.TMTime.OneToZero.weight q + 1
• Complexity.RationalHitting.TMTime.OneToZero.weight (Turing.TM1.Stmt.write a q) = Complexity.RationalHitting.TMTime.OneToZero.weight q + 1
• Complexity.RationalHitting.TMTime.OneToZero.weight (Turing.TM1.Stmt.load a q) = Complexity.RationalHitting.TMTime.OneToZero.weight q + 1
• Complexity.RationalHitting.TMTime.OneToZero.weight (Turing.TM1.Stmt.goto a) = 1
• Complexity.RationalHitting.TMTime.OneToZero.weight Turing.TM1.Stmt.halt = 1

theorem Complexity.RationalHitting.TMTime.OneToZero.weight_pos {Γ : Type v_1} {Λ : Type v_2} {σ : Type v_3} (q : Turing.TM1.Stmt Γ Λ σ) : 0 < weight q

theorem Complexity.RationalHitting.TMTime.OneToZero.statement_time {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] (M : Λ → Turing.TM1.Stmt Γ Λ σ) (q : Turing.TM1.Stmt Γ Λ σ) (v : σ) (T : Turing.Tape Γ) : ∃ (t : ℕ), 0 < t ∧ t ≤ weight q ∧ exec (Turing.TM0.step (Turing.TM1to0.tr M)) t { q := (some q, v), Tape := T } = some (Turing.TM1to0.trCfg M (Turing.TM1.stepAux q v T))

Each TM1 macro-step takes at most its statement size in real TM0 steps. Load and branch are absorbed into the next primitive step by Mathlib's compiler.

theorem Complexity.RationalHitting.TMTime.OneToZero.execution_time {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hs : Turing.TM1.Supports M S) (C : ℕ) (hC : ∀ l ∈ S, weight (M l) ≤ C) (t : ℕ) (a b : Turing.TM1.Cfg Γ Λ σ) (ha : a.l ∈ Finset.insertNone S) (hr : exec (Turing.TM1.step M) t a = some b) : ∃ u ≤ C * t, exec (Turing.TM0.step (Turing.TM1to0.tr M)) u (Turing.TM1to0.trCfg M a) = some (Turing.TM1to0.trCfg M b)

Linear transition overhead for a finitely supported TM1 program.

@[simp]

theorem Complexity.RationalHitting.TMTime.OneToZero.halts {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] (M : Λ → Turing.TM1.Stmt Γ Λ σ) (a : Turing.TM1.Cfg Γ Λ σ) (h : Turing.TM1.step M a = none) : Turing.TM0.step (Turing.TM1to0.tr M) (Turing.TM1to0.trCfg M a) = none

inductive Complexity.RationalHitting.StackLanguage.Program (K : Type) : Type

Finite Boolean-stack programs with branching, composition, and while loops.

• skip {K : Type} : Program K

  Leave all registers unchanged.

• push {K : Type} : K → Bool → Program K

  Push one Boolean symbol onto a register.

• drop {K : Type} : K → Program K

  Discard the head of a register, if present.

• transfer {K : Type} : K → K → Program K

  Move one head symbol between registers.

• seq {K : Type} : Program K → Program K → Program K

  Execute two programs in sequence.

• branch {K : Type} : K → Program K → Program K → Program K → Program K

  Choose a program for an empty, false-headed, or true-headed register.

• loop {K : Type} : K → Program K → Program K

  Repeat a program while the specified register is nonempty.

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instDecidableEqProgram {K✝ : Type} [DecidableEq K✝] : DecidableEq (Program K✝)

Equations

• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram = Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq

def Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq {K✝ : Type} [DecidableEq K✝] (x✝ x✝¹ : Program K✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq Complexity.RationalHitting.StackLanguage.Program.skip Complexity.RationalHitting.StackLanguage.Program.skip = isTrue ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq Complexity.RationalHitting.StackLanguage.Program.skip (Complexity.RationalHitting.StackLanguage.Program.drop a) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq Complexity.RationalHitting.StackLanguage.Program.skip (a.seq a_1) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (Complexity.RationalHitting.StackLanguage.Program.push a a_1) (a_2.seq a_3) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (Complexity.RationalHitting.StackLanguage.Program.drop a) Complexity.RationalHitting.StackLanguage.Program.skip = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (Complexity.RationalHitting.StackLanguage.Program.drop a) (a_1.seq a_2) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (Complexity.RationalHitting.StackLanguage.Program.transfer a a_1) (a_2.seq a_3) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (a.seq a_1) Complexity.RationalHitting.StackLanguage.Program.skip = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (a.seq a_1) (Complexity.RationalHitting.StackLanguage.Program.push a_2 a_3) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (a.seq a_1) (Complexity.RationalHitting.StackLanguage.Program.drop a_2) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (a.seq a_1) (Complexity.RationalHitting.StackLanguage.Program.transfer a_2 a_3) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (a.seq a_1) (Complexity.RationalHitting.StackLanguage.Program.branch a_2 a_3 a_4 a_5) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (a.seq a_1) (Complexity.RationalHitting.StackLanguage.Program.loop a_2 a_3) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (Complexity.RationalHitting.StackLanguage.Program.branch a a_1 a_2 a_3) (a_4.seq a_5) = isFalse ⋯
• Complexity.RationalHitting.StackLanguage.instDecidableEqProgram.decEq (Complexity.RationalHitting.StackLanguage.Program.loop a a_1) (a_2.seq a_3) = isFalse ⋯

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Store (K : Type) : Type

The Boolean word stored in each register.

Equations

• Complexity.RationalHitting.StackLanguage.Store K = (K → List Bool)

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Labels (K : Type) : Type

The initial label or a list of remaining program commands.

Equations

• Complexity.RationalHitting.StackLanguage.Labels K = Option (List (Complexity.RationalHitting.StackLanguage.Program K))

def Complexity.RationalHitting.StackLanguage.transfer {K : Type} [DecidableEq K] (a b : K) (s : Store K) : Store K

Move one head symbol if present, popping the first register before updating the second, including when both registers coincide.

Equations

• One or more equations did not get rendered due to their size.

inductive Complexity.RationalHitting.StackLanguage.Eval {K : Type} [DecidableEq K] : Program K → Store K → Store K → ℕ → Prop

Big-step execution with an exact count of stack-program transitions.

• skip {K : Type} [DecidableEq K] (s : Store K) : Eval Program.skip s s 1

  Skipping costs one transition.

• push {K : Type} [DecidableEq K] (k : K) (b : Bool) (s : Store K) : Eval (Program.push k b) s (Function.update s k (b :: s k)) 1

  Pushing a symbol costs one transition.

• drop {K : Type} [DecidableEq K] (k : K) (s : Store K) : Eval (Program.drop k) s (Function.update s k (s k).tail) 1

  Dropping a symbol costs one transition.

• transfer {K : Type} [DecidableEq K] (a b : K) (s : Store K) : Eval (Program.transfer a b) s (StackLanguage.transfer a b s) 1

  A symbol transfer costs one transition.

• seq {K : Type} [DecidableEq K] {p q : Program K} {s u v : Store K} {t w : ℕ} : Eval p s u t → Eval q u v w → Eval (p.seq q) s v (1 + t + w)

  Sequential composition adds both execution times and one control transition.

• branchNone {K : Type} [DecidableEq K] {k : K} {p q r : Program K} {s v : Store K} {t : ℕ} : s k = [] → Eval p s v t → Eval (Program.branch k p q r) s v (1 + t)

  Take the empty-register branch after one control transition.

• branchFalse {K : Type} [DecidableEq K] {k : K} {p q r : Program K} {s v : Store K} {t : ℕ} {ls : List Bool} : s k = false :: ls → Eval q s v t → Eval (Program.branch k p q r) s v (1 + t)

  Take the false-symbol branch after one control transition.

• branchTrue {K : Type} [DecidableEq K] {k : K} {p q r : Program K} {s v : Store K} {t : ℕ} {ls : List Bool} : s k = true :: ls → Eval r s v t → Eval (Program.branch k p q r) s v (1 + t)

  Take the true-symbol branch after one control transition.

• whileNil {K : Type} [DecidableEq K] {k : K} {p : Program K} {s : Store K} : s k = [] → Eval (Program.loop k p) s s 1

  An empty loop register terminates the loop in one transition.

• whileCons {K : Type} [DecidableEq K] {k : K} {p : Program K} {s u v : Store K} {t w : ℕ} : s k ≠ [] → Eval p s u t → Eval (Program.loop k p) u v w → Eval (Program.loop k p) s v (1 + t + w)

  A nonempty loop register executes the body and repeats.

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Stmt (K : Type) : Type

Mathlib stack-machine statements used to compile the finite program.

Equations

• Complexity.RationalHitting.StackLanguage.Stmt K = Turing.TM2.Stmt (fun (x : K) => Bool) (Complexity.RationalHitting.StackLanguage.Labels K) (Option Bool)

def Complexity.RationalHitting.StackLanguage.jump {K : Type} (ps : List (Program K)) : Stmt K

Reset the temporary symbol and continue with the remaining commands.

Equations

• Complexity.RationalHitting.StackLanguage.jump ps = Turing.TM2.Stmt.load (fun (x : Option Bool) => none) (Turing.TM2.Stmt.goto fun (x : Option Bool) => some ps)

def Complexity.RationalHitting.StackLanguage.instruction {K : Type} : List (Program K) → Stmt K

Compile the next program command into stack-machine instructions.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.StackLanguage.instruction [] = Turing.TM2.Stmt.halt
• Complexity.RationalHitting.StackLanguage.instruction (Complexity.RationalHitting.StackLanguage.Program.skip :: ps) = Complexity.RationalHitting.StackLanguage.jump ps
• Complexity.RationalHitting.StackLanguage.instruction (p.seq q :: ps) = Complexity.RationalHitting.StackLanguage.jump (p :: q :: ps)

def Complexity.RationalHitting.StackLanguage.machine {K : Type} (p : Program K) : Labels K → Stmt K

The stack-machine transition map for a finite program.

Equations

• Complexity.RationalHitting.StackLanguage.machine p none = Complexity.RationalHitting.StackLanguage.jump [p]
• Complexity.RationalHitting.StackLanguage.machine p (some ps) = Complexity.RationalHitting.StackLanguage.instruction ps

def Complexity.RationalHitting.StackLanguage.cfg {K : Type} (ps : List (Program K)) (s : Store K) : Turing.TM2.Cfg (fun (x : K) => Bool) (Labels K) (Option Bool)

The stack-machine configuration for a continuation and register store.

Equations

• Complexity.RationalHitting.StackLanguage.cfg ps s = { l := some (some ps), var := none, stk := s }

@[simp]

theorem Complexity.RationalHitting.StackLanguage.jump_eval {K : Type} [DecidableEq K] (ps : List (Program K)) (v : Option Bool) (s : Store K) : Turing.TM2.stepAux (jump ps) v s = cfg ps s

theorem Complexity.RationalHitting.StackLanguage.eval_compiles {K : Type} [DecidableEq K] {p : Program K} {s v : Store K} {t : ℕ} (h : Eval p s v t) (main : Program K) (ps : List (Program K)) : TMTime.exec (Turing.TM2.step (machine main)) t (cfg (p :: ps) s) = some (cfg ps v)

Exact big-step correctness in real TM2 steps, with no unbounded internal state or alphabet.

def Complexity.RationalHitting.StackLanguage.successors {K : Type} [DecidableEq K] : List (Program K) → Finset (List (Program K))

Possible jump targets; inspecting a head has only three finite cases.

Equations

• Complexity.RationalHitting.StackLanguage.successors [] = ∅
• Complexity.RationalHitting.StackLanguage.successors (Complexity.RationalHitting.StackLanguage.Program.skip :: ps) = {ps}
• Complexity.RationalHitting.StackLanguage.successors (Complexity.RationalHitting.StackLanguage.Program.push k b :: ps) = {ps}
• Complexity.RationalHitting.StackLanguage.successors (Complexity.RationalHitting.StackLanguage.Program.drop k :: ps) = {ps}
• Complexity.RationalHitting.StackLanguage.successors (Complexity.RationalHitting.StackLanguage.Program.transfer a b :: ps) = {ps}
• Complexity.RationalHitting.StackLanguage.successors (p.seq q :: ps) = {p :: q :: ps}
• Complexity.RationalHitting.StackLanguage.successors (Complexity.RationalHitting.StackLanguage.Program.branch k p q r :: ps) = {p :: ps, q :: ps, r :: ps}
• Complexity.RationalHitting.StackLanguage.successors (Complexity.RationalHitting.StackLanguage.Program.loop k p :: ps) = {ps, p :: Complexity.RationalHitting.StackLanguage.Program.loop k p :: ps}

def Complexity.RationalHitting.StackLanguage.locations {K : Type} [DecidableEq K] : Program K → List (Program K) → Finset (List (Program K))

Finite control locations, computed structurally, despite unbounded loop iteration counts.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.StackLanguage.locations Complexity.RationalHitting.StackLanguage.Program.skip x✝ = {Complexity.RationalHitting.StackLanguage.Program.skip :: x✝, x✝}
• Complexity.RationalHitting.StackLanguage.locations (Complexity.RationalHitting.StackLanguage.Program.push a a_1) x✝ = {Complexity.RationalHitting.StackLanguage.Program.push a a_1 :: x✝, x✝}
• Complexity.RationalHitting.StackLanguage.locations (Complexity.RationalHitting.StackLanguage.Program.drop a) x✝ = {Complexity.RationalHitting.StackLanguage.Program.drop a :: x✝, x✝}

@[simp]

theorem Complexity.RationalHitting.StackLanguage.entry_mem {K : Type} [DecidableEq K] (p : Program K) (ps : List (Program K)) : p :: ps ∈ locations p ps

@[simp]

theorem Complexity.RationalHitting.StackLanguage.exit_mem {K : Type} [DecidableEq K] (p : Program K) (ps : List (Program K)) : ps ∈ locations p ps

theorem Complexity.RationalHitting.StackLanguage.root_closed {K : Type} [DecidableEq K] (p : Program K) (ps : List (Program K)) (S : Finset (List (Program K))) (hs : locations p ps ⊆ S) : successors (p :: ps) ⊆ S

theorem Complexity.RationalHitting.StackLanguage.locations_closed {K : Type} [DecidableEq K] (p : Program K) (ps : List (Program K)) (S : Finset (List (Program K))) (hs : locations p ps ⊆ S) (hk : successors ps ⊆ S) (l : List (Program K)) : l ∈ locations p ps → successors l ⊆ S

def Complexity.RationalHitting.StackLanguage.support {K : Type} [DecidableEq K] (p : Program K) : Finset (Labels K)

The finite set of control labels used by the compiled program.

Equations

• Complexity.RationalHitting.StackLanguage.support p = insert none (Finset.image some (Complexity.RationalHitting.StackLanguage.locations p []))

theorem Complexity.RationalHitting.StackLanguage.instruction_supported {K : Type} [DecidableEq K] (S : Finset (Labels K)) (ps : List (Program K)) (h : ∀ q ∈ successors ps, some q ∈ S) : Turing.TM2.SupportsStmt S (instruction ps)

theorem Complexity.RationalHitting.StackLanguage.machine_supported {K : Type} [DecidableEq K] (p : Program K) : Turing.TM2.Supports (machine p) (support p)

theorem Complexity.RationalHitting.StackLanguage.complete_run {K : Type} [DecidableEq K] {p : Program K} {s v : Store K} {t : ℕ} (h : Eval p s v t) : TMTime.exec (Turing.TM2.step (machine p)) (t + 2) { l := some none, var := none, stk := s } = some { l := none, var := none, stk := v }

Entry and halting are one actual macrostep apiece.