Rational hitting lists: procedures

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

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

inductive Complexity.RationalHitting.TimeBound : Type

A concrete syntax for nonnegative polynomial bounds. This is only used to bound actual stack transitions, never as an additional machine instruction.

• const : ℕ → TimeBound

  A fixed nonnegative bound.

• variable : TimeBound

  The input-size parameter.

• add : TimeBound → TimeBound → TimeBound

  Add two bounds.

• mul : TimeBound → TimeBound → TimeBound

  Multiply two bounds.

def Complexity.RationalHitting.instDecidableEqTimeBound.decEq (x✝ x✝¹ : TimeBound) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq (Complexity.RationalHitting.TimeBound.const a) Complexity.RationalHitting.TimeBound.variable = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq (Complexity.RationalHitting.TimeBound.const a) (a_1.add a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq (Complexity.RationalHitting.TimeBound.const a) (a_1.mul a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq Complexity.RationalHitting.TimeBound.variable (Complexity.RationalHitting.TimeBound.const a) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq Complexity.RationalHitting.TimeBound.variable Complexity.RationalHitting.TimeBound.variable = isTrue ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq Complexity.RationalHitting.TimeBound.variable (a.add a_1) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq Complexity.RationalHitting.TimeBound.variable (a.mul a_1) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq (a.add a_1) (Complexity.RationalHitting.TimeBound.const a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq (a.add a_1) Complexity.RationalHitting.TimeBound.variable = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq (a.add a_1) (a_2.mul a_3) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq (a.mul a_1) (Complexity.RationalHitting.TimeBound.const a_2) = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq (a.mul a_1) Complexity.RationalHitting.TimeBound.variable = isFalse ⋯
• Complexity.RationalHitting.instDecidableEqTimeBound.decEq (a.mul a_1) (a_2.add a_3) = isFalse ⋯

@[instance_reducible]

instance Complexity.RationalHitting.instDecidableEqTimeBound : DecidableEq TimeBound

Equations

• Complexity.RationalHitting.instDecidableEqTimeBound = Complexity.RationalHitting.instDecidableEqTimeBound.decEq

@[instance_reducible]

instance Complexity.RationalHitting.TimeBound.instOfNat {n : ℕ} : OfNat TimeBound n

Equations

• Complexity.RationalHitting.TimeBound.instOfNat = { ofNat := Complexity.RationalHitting.TimeBound.const n }

@[instance_reducible]

instance Complexity.RationalHitting.TimeBound.instAdd : Add TimeBound

Equations

• Complexity.RationalHitting.TimeBound.instAdd = { add := Complexity.RationalHitting.TimeBound.add }

@[instance_reducible]

instance Complexity.RationalHitting.TimeBound.instMul : Mul TimeBound

Equations

• Complexity.RationalHitting.TimeBound.instMul = { mul := Complexity.RationalHitting.TimeBound.mul }

def Complexity.RationalHitting.TimeBound.eval : TimeBound → ℕ → ℕ

Evaluate a nonnegative polynomial time-bound expression at an input size.

Equations

• (Complexity.RationalHitting.TimeBound.const c).eval x✝ = c
• Complexity.RationalHitting.TimeBound.variable.eval x✝ = x✝
• (a.add b).eval x✝ = a.eval x✝ + b.eval x✝
• (a.mul b).eval x✝ = a.eval x✝ * b.eval x✝

@[simp]

theorem Complexity.RationalHitting.TimeBound.eval_const (a n : ℕ) : (const a).eval n = a

@[simp]

theorem Complexity.RationalHitting.TimeBound.eval_variable (n : ℕ) : «variable».eval n = n

@[simp]

theorem Complexity.RationalHitting.TimeBound.eval_add (a b : TimeBound) (n : ℕ) : (a + b).eval n = a.eval n + b.eval n

@[simp]

theorem Complexity.RationalHitting.TimeBound.eval_mul (a b : TimeBound) (n : ℕ) : (a * b).eval n = a.eval n * b.eval n

@[simp]

theorem Complexity.RationalHitting.TimeBound.eval_numeral (a n : ℕ) : (OfNat.ofNat a).eval n = a

theorem Complexity.RationalHitting.TimeBound.monotone (p : TimeBound) : Monotone p.eval

def Complexity.RationalHitting.TimeBound.comp : TimeBound → TimeBound → TimeBound

Substitution is again a polynomial with nonnegative coefficients.

Equations

• (Complexity.RationalHitting.TimeBound.const c).comp x✝ = Complexity.RationalHitting.TimeBound.const c
• Complexity.RationalHitting.TimeBound.variable.comp x✝ = x✝
• (a.add b).comp x✝ = a.comp x✝ + b.comp x✝
• (a.mul b).comp x✝ = a.comp x✝ * b.comp x✝

@[simp]

theorem Complexity.RationalHitting.TimeBound.eval_comp (p q : TimeBound) (n : ℕ) : (p.comp q).eval n = p.eval (q.eval n)

theorem Complexity.RationalHitting.TimeBound.growth (p : TimeBound) : ∃ (C : ℕ) (k : ℕ), 0 < C ∧ 0 < k ∧ ∀ (n : ℕ), 1 ≤ n → p.eval n ≤ C * n ^ k

These certificates imply an ordinary fixed positive-coefficient, positive- degree power bound. This prevents any hidden superpolynomial time allowance.

def Complexity.RationalHitting.StackLanguage.single {K : Type} [DecidableEq K] (k : K) (w : List Bool) : Store K

A store with one specified register and all other registers empty.

Equations

• Complexity.RationalHitting.StackLanguage.single k w = Function.update (fun (x : K) => []) k w

@[simp]

theorem Complexity.RationalHitting.StackLanguage.single_self {K : Type} [DecidableEq K] (k : K) (w : List Bool) : single k w k = w

@[simp]

theorem Complexity.RationalHitting.StackLanguage.single_other {K : Type} [DecidableEq K] {k j : K} (w : List Bool) (h : j ≠ k) : single k w j = []

@[simp]

theorem Complexity.RationalHitting.StackLanguage.single_nil {K : Type} [DecidableEq K] (k : K) : single k [] = fun (x : K) => []

theorem Complexity.RationalHitting.StackLanguage.extend_single {K L : Type} [DecidableEq K] [DecidableEq L] (f : K → L) (hf : Function.Injective f) (k : K) (w : List Bool) : (Function.extend f (single k w) fun (x : L) => []) = single (f k) w

theorem Complexity.RationalHitting.StackLanguage.Eval.rename_single {K L : Type} [DecidableEq K] [DecidableEq L] {p : Program K} {i o : K} {x y : List Bool} {t : ℕ} (h : Eval p (single i x) (single o y) t) (f : K → L) (hf : Function.Injective f) : Eval (Program.rename f p) (single (f i) x) (single (f o) y) t

structure Complexity.RationalHitting.StackLanguage.Procedure {A B : Type} (ca : A → List Bool) (cb : B → List Bool) (f : A → B) : Type 1

A quantitative implementation, with completely clean stack input and output. Both execution and result size are polynomially bounded.

• Registers : Type

  Register labels for the procedure.

• finite : Fintype self.Registers

  A finite register bank.

• decEq : DecidableEq self.Registers

  Decidable register equality used by store updates.

• input : self.Registers

  The register containing the encoded input.

• output : self.Registers

  The register receiving the encoded output.

• program : Program self.Registers

  The finite program executed on the register bank.

• bound : TimeBound

  A polynomial bound on time and output length.

• correct (a : A) : ∃ t ≤ self.bound.eval ((ca a).length + 1), Eval self.program (single self.input (ca a)) (single self.output (cb (f a))) t

  Correct output and a clean final store within the bound.

• size (a : A) : (cb (f a)).length ≤ self.bound.eval ((ca a).length + 1)

  The encoded result fits within the same polynomial bound.

def Complexity.RationalHitting.StackLanguage.Feasible {A B : Type} (ca : A → List Bool) (cb : B → List Bool) (f : A → B) : Prop

A compositional polynomial-time feasibility predicate.

Equations

• Complexity.RationalHitting.StackLanguage.Feasible ca cb f = Nonempty (Complexity.RationalHitting.StackLanguage.Procedure ca cb f)

def Complexity.RationalHitting.StackLanguage.move {K : Type} (a b tmp : K) : Program K

Order-preserving transfer, implemented using two stack reversals.

Equations

• Complexity.RationalHitting.StackLanguage.move a b tmp = (Complexity.RationalHitting.StackLanguage.reverse a tmp).seq (Complexity.RationalHitting.StackLanguage.reverse tmp b)

theorem Complexity.RationalHitting.StackLanguage.eval_move {K : Type} [DecidableEq K] {a b tmp : K} (hab : a ≠ b) (hat : a ≠ tmp) (hbt : b ≠ tmp) (s : Store K) (hb : s b = []) (ht : s tmp = []) : Eval (move a b tmp) s (Function.update (Function.update s a []) b (s a)) (4 * (s a).length + 3)

theorem Complexity.RationalHitting.StackLanguage.Eval.move_single {K : Type} [DecidableEq K] {a b tmp : K} (hab : a ≠ b) (hat : a ≠ tmp) (hbt : b ≠ tmp) (w : List Bool) : Eval (move a b tmp) (single a w) (single b w) (4 * w.length + 3)

theorem Complexity.RationalHitting.StackLanguage.Eval.runAt {K L : Type} [DecidableEq K] [DecidableEq L] {p : Program K} {i o : K} {x y : List Bool} {t : ℕ} (h : Eval p (single i x) (single o y) t) (f : K → L) (hf : Function.Injective f) (s : Store L) (hs : ∀ (k : K), s (f k) = single i x k) : Eval (Program.rename f p) s (Function.update (Function.update s (f i) []) (f o) y) t

Run in an embedded register bank, preserving every register outside it.

def Complexity.RationalHitting.StackLanguage.Procedure.identity {A : Type} (ca : A → List Bool) : Procedure ca ca id

Identity has no operation of unbounded cost.

Equations

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

def Complexity.RationalHitting.StackLanguage.Procedure.comp {A B C : Type} {ca : A → List Bool} {cb : B → List Bool} {cc : C → List Bool} {f : A → B} {g : B → C} (q : Procedure cb cc g) (p : Procedure ca cb f) : Procedure ca cc (g ∘ f)

Composition uses disjoint scratch banks and an actual order-preserving stack transfer.

Equations

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

def Complexity.RationalHitting.StackLanguage.Procedure.recode {A B : Type} {ca : A → List Bool} {cb : B → List Bool} {f : A → B} {A' B' : Type} (p : Procedure ca cb f) (ca' : A' → List Bool) (cb' : B' → List Bool) (f' : A' → B') (e : A' → A) (hi : ∀ (a : A'), ca (e a) = ca' a) (ho : ∀ (a : A'), cb (f (e a)) = cb' (f' a)) : Procedure ca' cb' f'

Reinterpret equal input/output words, with no additional computation.

Equations

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