Rational hitting lists: compiler

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

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

@[instance_reducible]

def Complexity.RationalHitting.TMTime.Link.sumInhabited {Λ : Type u_2} {Δ : Type u_3} [Inhabited Λ] : Inhabited (Λ ⊕ Δ)

Composition starts in the first machine's default state.

Equations

• Complexity.RationalHitting.TMTime.Link.sumInhabited = { default := Sum.inl default }

def Complexity.RationalHitting.TMTime.Link.left {Γ : Type u_1} {Λ : Type u_2} {Δ : Type u_3} [Inhabited Γ] (a : Turing.TM0.Cfg Γ Λ) : Turing.TM0.Cfg Γ (Λ ⊕ Δ)

Tag a configuration as belonging to the first machine in a composition.

Equations

• Complexity.RationalHitting.TMTime.Link.left a = { q := Sum.inl a.q, Tape := a.Tape }

def Complexity.RationalHitting.TMTime.Link.right {Γ : Type u_1} {Λ : Type u_2} {Δ : Type u_3} [Inhabited Γ] (a : Turing.TM0.Cfg Γ Δ) : Turing.TM0.Cfg Γ (Λ ⊕ Δ)

Tag a configuration as belonging to the second machine in a composition.

Equations

• Complexity.RationalHitting.TMTime.Link.right a = { q := Sum.inr a.q, Tape := a.Tape }

def Complexity.RationalHitting.TMTime.Link.machine {Γ : Type u_1} {Λ : Type u_2} {Δ : Type u_3} [Inhabited Λ] [Inhabited Δ] (F : Turing.TM0.Machine Γ Λ) (G : Turing.TM0.Machine Γ Δ) : Turing.TM0.Machine Γ (Λ ⊕ Δ)

The transition map of the compiled machine in this compiler stage.

Equations

• Complexity.RationalHitting.TMTime.Link.machine F G (Sum.inl q) x✝ = match F q x✝ with | none => some (Sum.inr default, Turing.TM0.Stmt.write x✝) | some (r, s) => some (Sum.inl r, s)
• Complexity.RationalHitting.TMTime.Link.machine F G (Sum.inr q) x✝ = Option.map (fun (x : Δ × Turing.TM0.Stmt Γ) => match x with | (r, s) => (Sum.inr r, s)) (G q x✝)

theorem Complexity.RationalHitting.TMTime.Link.step_left {Γ : Type u_1} {Λ : Type u_2} {Δ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited Δ] (F : Turing.TM0.Machine Γ Λ) (G : Turing.TM0.Machine Γ Δ) {a b : Turing.TM0.Cfg Γ Λ} (h : Turing.TM0.step F a = some b) : Turing.TM0.step (machine F G) (left a) = some (left b)

theorem Complexity.RationalHitting.TMTime.Link.switch {Γ : Type u_1} {Λ : Type u_2} {Δ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited Δ] (F : Turing.TM0.Machine Γ Λ) (G : Turing.TM0.Machine Γ Δ) {a : Turing.TM0.Cfg Γ Λ} (h : Turing.TM0.step F a = none) : Turing.TM0.step (machine F G) (left a) = some (right { q := default, Tape := a.Tape })

theorem Complexity.RationalHitting.TMTime.Link.step_right {Γ : Type u_1} {Λ : Type u_2} {Δ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited Δ] (F : Turing.TM0.Machine Γ Λ) (G : Turing.TM0.Machine Γ Δ) (a : Turing.TM0.Cfg Γ Δ) : Turing.TM0.step (machine F G) (right a) = Option.map right (Turing.TM0.step G a)

theorem Complexity.RationalHitting.TMTime.Link.run_left {Γ : Type u_1} {Λ : Type u_2} {Δ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited Δ] (F : Turing.TM0.Machine Γ Λ) (G : Turing.TM0.Machine Γ Δ) (t : ℕ) {a b : Turing.TM0.Cfg Γ Λ} (h : exec (Turing.TM0.step F) t a = some b) : exec (Turing.TM0.step (machine F G)) t (left a) = some (left b)

theorem Complexity.RationalHitting.TMTime.Link.run_right {Γ : Type u_1} {Λ : Type u_2} {Δ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited Δ] (F : Turing.TM0.Machine Γ Λ) (G : Turing.TM0.Machine Γ Δ) (t : ℕ) (a : Turing.TM0.Cfg Γ Δ) : exec (Turing.TM0.step (machine F G)) t (right a) = Option.map right (exec (Turing.TM0.step G) t a)

theorem Complexity.RationalHitting.TMTime.Link.finite_sequence {Γ : Type u_1} {Λ : Type u_2} {Δ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited Δ] [Fintype Λ] [Fintype Δ] (F : Turing.TM0.Machine Γ Λ) (G : Turing.TM0.Machine Γ Δ) : ∃ (m : ℕ) (H : Turing.TM0.Machine Γ (Fin (m + 1))), ∀ (w v : List Γ) (t u : ℕ) (a : Turing.TM0.Cfg Γ Λ) (b : Turing.TM0.Cfg Γ Δ), exec (Turing.TM0.step F) t (Turing.TM0.init w) = some a → Turing.TM0.step F a = none → a.Tape = Turing.Tape.mk₁ v → exec (Turing.TM0.step G) u (Turing.TM0.init v) = some b → Turing.TM0.step G b = none → ∃ (c : Turing.TM0.Cfg Γ (Fin (m + 1))), exec (Turing.TM0.step H) (t + 1 + u) (Turing.TM0.init w) = some c ∧ Turing.TM0.step H c = none ∧ c.Tape = b.Tape

Splice two halting finite transducers with exactly one glue step. The intermediate output is the literal tape required by the second input.

@[reducible, inline]

abbrev Complexity.RationalHitting.TMTime.BinaryLift.A : Type

The fixed four-symbol alphabet of the final finite-state machine.

Equations

• Complexity.RationalHitting.TMTime.BinaryLift.A = Fin 4

def Complexity.RationalHitting.TMTime.BinaryLift.bit (b : Bool) : A

Represent a Boolean tape symbol in the fixed alphabet.

Equations

• Complexity.RationalHitting.TMTime.BinaryLift.bit b = if b = true then 1 else 0

def Complexity.RationalHitting.TMTime.BinaryLift.bitMap : Turing.PointedMap Bool A

The blank-preserving map from Boolean tape symbols into the fixed alphabet.

Equations

• Complexity.RationalHitting.TMTime.BinaryLift.bitMap = { f := Complexity.RationalHitting.TMTime.BinaryLift.bit, map_pt' := Complexity.RationalHitting.TMTime.BinaryLift.bitMap._proof_1 }

@[simp]

theorem Complexity.RationalHitting.TMTime.BinaryLift.bit_read (b : Bool) : (bit b == 1) = b

def Complexity.RationalHitting.TMTime.BinaryLift.stmt : Turing.TM0.Stmt Bool → Turing.TM0.Stmt A

Translate a Boolean-tape instruction to the fixed alphabet.

Equations

• Complexity.RationalHitting.TMTime.BinaryLift.stmt (Turing.TM0.Stmt.move d) = Turing.TM0.Stmt.move d
• Complexity.RationalHitting.TMTime.BinaryLift.stmt (Turing.TM0.Stmt.write b) = Turing.TM0.Stmt.write (Complexity.RationalHitting.TMTime.BinaryLift.bit b)

def Complexity.RationalHitting.TMTime.BinaryLift.machine {Λ : Type u_1} [Inhabited Λ] (F : Turing.TM0.Machine Bool Λ) : Turing.TM0.Machine A Λ

The transition map of the compiled machine in this compiler stage.

Equations

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

def Complexity.RationalHitting.TMTime.BinaryLift.cfg {Λ : Type u_1} (a : Turing.TM0.Cfg Bool Λ) : Turing.TM0.Cfg A Λ

Translate a Boolean-tape configuration to the fixed alphabet.

Equations

• Complexity.RationalHitting.TMTime.BinaryLift.cfg a = { q := a.q, Tape := Turing.Tape.map Complexity.RationalHitting.TMTime.BinaryLift.bitMap a.Tape }

theorem Complexity.RationalHitting.TMTime.BinaryLift.step {Λ : Type u_1} [Inhabited Λ] (F : Turing.TM0.Machine Bool Λ) (a : Turing.TM0.Cfg Bool Λ) : Turing.TM0.step (machine F) (cfg a) = Option.map cfg (Turing.TM0.step F a)

theorem Complexity.RationalHitting.TMTime.BinaryLift.run {Λ : Type u_1} [Inhabited Λ] (F : Turing.TM0.Machine Bool Λ) (t : ℕ) (a : Turing.TM0.Cfg Bool Λ) : exec (Turing.TM0.step (machine F)) t (cfg a) = Option.map cfg (exec (Turing.TM0.step F) t a)

theorem Complexity.RationalHitting.TMTime.BinaryLift.run_init {Λ : Type u_1} [Inhabited Λ] (F : Turing.TM0.Machine Bool Λ) (w : List Bool) (t : ℕ) (a : Turing.TM0.Cfg Bool Λ) (hr : exec (Turing.TM0.step F) t (Turing.TM0.init w) = some a) (hh : Turing.TM0.step F a = none) : exec (Turing.TM0.step (machine F)) t (Turing.TM0.init (List.map bit w)) = some (cfg a) ∧ Turing.TM0.step (machine F) (cfg a) = none

theorem Complexity.RationalHitting.TMTime.Alphabet.tape_init {Γ : Type u_1} [Inhabited Γ] {b : ℕ} (enc : Γ → List.Vector Bool b) (h0 : enc default = List.Vector.replicate b false) (w : List Γ) : Turing.TM1to1.trTape h0 (Turing.Tape.mk₁ w) = Turing.Tape.mk₁ (List.flatMap (fun (a : Γ) => (enc a).toList) w)

theorem Complexity.RationalHitting.StackLanguage.Compiler.raw_compilation {K : Type} [DecidableEq K] [Fintype K] (p : Program K) (ki ko : K) : ∃ (m : ℕ) (G : Turing.TM0.Machine (Fin 4) (Fin (m + 1))) (C : ℕ), 0 < C ∧ ∀ (w xs : List Bool) (t : ℕ), w ≠ [] → Eval p (Function.update (fun (x : K) => []) ki w) (Function.update (fun (x : K) => []) ko xs.reverse) t → ∃ u ≤ C * (w.length + t + xs.length + 3) ^ 2, ∃ (a : Turing.TM0.Cfg (Fin 4) (Fin (m + 1))), TMTime.exec (Turing.TM0.step G) u (Turing.TM0.init (List.map TMTime.InputAdapter.raw w)) = some a ∧ Turing.TM0.step G a = none ∧ a.Tape = Turing.Tape.mk₁ (List.map TMTime.OutputAdapter.raw xs)

End-to-end, finite-state, Fin4 one-tape compilation. Input and output are literal 1/2 digit strings, NOT different encodings hidden by an interface. The stack program is a single fixed finite syntax tree. Final scratch must be empty; the designated output stack has reversed output order, as explicitly stated.

def Complexity.RationalHitting.ExecutableGenerator.unaryWord (n s : ℕ) : List Bool

A fixed finite stack program with literal unary input and exact canonical output, bounded by a fixed polynomial in the input length.

Equations

• Complexity.RationalHitting.ExecutableGenerator.unaryWord n s = List.replicate n true ++ [false] ++ List.replicate s true

def Complexity.RationalHitting.ExecutableGenerator.StackImplementation : Prop

A single finite stack program generating exact hitting-list encodings in polynomial time.

Equations

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

theorem Complexity.RationalHitting.ExecutableGenerator.run_eq_exec {m : ℕ} (G : Machine m) (t : ℕ) (a : Config m) : run G t a = TMTime.exec (Turing.TM0.step G) t a

theorem Complexity.RationalHitting.ExecutableGenerator.unaryWord_raw (n s : ℕ) : List.map TMTime.InputAdapter.raw (unaryWord n s) = unaryInput n s

theorem Complexity.RationalHitting.ExecutableGenerator.encoded_raw (n s : ℕ) : List.map TMTime.OutputAdapter.raw (encoded n s) = List.map tapeBit (encodeOutput (list n s))

theorem Complexity.RationalHitting.ExecutableGenerator.compilation_sum_bound (x t y R C A : ℕ) (hx : x ≤ R) (ht : t ≤ C * R) (hy : y ≤ A * R) (hR : 1 ≤ R) : x + t + y + 3 ≤ (C + A + 4) * R

theorem Complexity.RationalHitting.ExecutableGenerator.compilation_square_bound (D C A x E : ℕ) : D * ((C + A + 4) * x ^ E) ^ 2 = D * (C + A + 4) ^ 2 * x ^ (2 * E)

theorem Complexity.RationalHitting.ExecutableGenerator.implementation_of_stack (h : StackImplementation) : Implementation

The raw compiler preserves literal input/output and gives a fixed finite alphabet and state space with a polynomial transition bound.