From f60d231340ca9b1fc7e8fb7407c9e6bed667c2c8 Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 13 Jun 2026 10:53:38 +0200 Subject: [PATCH] Sketch of hierarchy theorem. --- .../Machines/RTM/HierarchyTheorems.lean | 170 ++++++++++++++++++ Cslib/Computability/Machines/RTM/PB.lean | 57 ++++++ Cslib/Computability/Machines/RTM/Prog.lean | 4 + Cslib/Computability/Machines/RTM/Tools.lean | 32 ++++ references.bib | 9 + 5 files changed, 272 insertions(+) create mode 100644 Cslib/Computability/Machines/RTM/HierarchyTheorems.lean diff --git a/Cslib/Computability/Machines/RTM/HierarchyTheorems.lean b/Cslib/Computability/Machines/RTM/HierarchyTheorems.lean new file mode 100644 index 0000000000..e98c62e486 --- /dev/null +++ b/Cslib/Computability/Machines/RTM/HierarchyTheorems.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.RTM.TMSimulator +public import Cslib.Computability.Machines.RTM.PB + +/-! +# Hierarchy Theorems + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak2009], Chapter 4 + +-/ + + +@[expose] public section + +namespace Turing + +namespace RoseTreeMachine + + +variable {env : List Value} {α β : Type} [DataEncode α] [DataEncode β] + +/-- A TM normalized to use `Fin k` for its `State` and `Symbol` type. -/ +structure NormalizedTM where + states : ℕ + symbols : ℕ + toSingleTapeTM : SingleTapeTM (Fin (symbols + 2)) + h_states : toSingleTapeTM.State = Fin (states + 1) + +def NormalizedTM.Cfg (tm : NormalizedTM) := tm.toSingleTapeTM.Cfg + +def NormalizedTM.step (tm : NormalizedTM) (cfg : tm.Cfg) : tm.Cfg := + match tm.toSingleTapeTM.step cfg with + | none => cfg + | some cfg' => cfg' + +def binaryToFin {n : ℕ} (x : List Bool) : List (Fin (n + 2)) := + List.map (fun b => if b then 1 else 0) x + +/-- If the TM `tm` is in the final state after at most `t` steps, returns the output. +Note that this is a slightly different output notion since we do not require the tape to be in +its canonical state. Also we just filter out any symbol that is not the encoding of a bool. -/ +def NormalizedTM.output? (tm : NormalizedTM) (input : List Bool) (t : ℕ) : Option (List Bool) := + let cfg := tm.step^[t] (tm.toSingleTapeTM.initCfg (binaryToFin input)) + if cfg.state = none then + (cfg.BiTape.head :: cfg.BiTape.right.toList).filterMap + (fun c => match c with | some 0 => some false | some 1 => some true | _ => none) + else + none + +def NormalizedTM.ComputesFunInTime (tm : NormalizedTM) (f : List Bool → List Bool) (t : ℕ → ℕ) : + Prop := + ∀ input, ∃ t' < t input.length, tm.output? input t' = some (f input) + +def DSPACE (t : ℕ → ℕ) := { f : List Bool → Bool | ∃ tm : NormalizedTM, ∃ a, + tm.ComputesFunInTime (fun x => [f x]) fun n => a * t n + a } + +/-- An enumeration of Turing machines such that every TM appears infinitely often in the +enumeration. -/ +def Enumerates (e : ℕ → NormalizedTM) : Prop := ∀ tm n, ∃ n' > n, e n' = tm + +-- /-- A universal machine for an enumeration can simulate any Turing machine from the enumeration +-- with quadratic overhead. +-- TODO: It is possible to have an overhead of `t log t`, but quadratic is fine for now. -/ +-- def UniversalMachineSemantics_old +-- (allTMs : ℕ → NormalizedTM) +-- (p : PB → PB) : Prop := +-- ∃ a, ∀ m input t, ∃ s, PB.ComputesEncInTimeAndSpace p +-- (t, input, m) +-- ((allTMs m).output? input t) +-- ((a * (allTMs m).states * (allTMs m).symbols * t * t) + a) +-- s + +def simulator (allTMs : ℕ → NormalizedTM) (m : ℕ) (input : List Bool) (t : ℕ) : + Option (List Bool) := + (allTMs m).output? input t + +/-- A universal machine for an enumeration can simulate any Turing machine from the enumeration +with quadratic overhead. +TODO: It is possible to have an overhead of `t log t`, but quadratic is fine for now. -/ +def UniversalMachineSemantics + (allTMs : ℕ → NormalizedTM) + (p : PB → PB) : Prop := + ∃ a, ∃ s, PB.ComputesFunEncInTimeAndSpace p + (fun (m, input, t) => simulator allTMs m input t) + (fun (m, _, t) => + -- The runtime of the simulation has an overhead in the "size" of the TM, but does not + -- depend on the input. + (a * (allTMs m).states * (allTMs m).symbols * t * t) + a) + s + +def succ (x : PB) : PB := sorry + +def length (x : PB) : PB := sorry + +theorem length_computes {p : PB} {x : List α} (h_p : p.ComputesEnc env x) : + (length p).ComputesEnc env x.length := by + sorry + +/-- Computes `x * x` -/ +def mul (x y : PB) : PB := sorry + +theorem mul_computes {p q : PB} {x y : ℕ} (h_p : p.ComputesEnc env x) (h_q : q.ComputesEnc env y) : + (mul p q).ComputesEnc env (x * y) := by + sorry + +def cube (x : PB) : PB := mul (mul x x) x + +theorem cube_computes {p : PB} {x : ℕ} (h_p : p.ComputesEnc env x) : + (cube p).ComputesEnc env (x * x * x) := by + exact mul_computes (mul_computes h_p h_p) h_p + +/-- Run the universal machine on (x, x, |x|^3) and invert its output, if it halts. -/ +def diagonalizer (p : PB → PB) (x : PB) : PB := + let output := p (PB.toPair x (PB.toPair x (cube (length x)))) + PB.ifEq output (PB.constantEnc (Option.some [true])) + (PB.constantEnc [false]) + (PB.constantEnc [true]) + +/-- Semantic core of the diagonalizer (resources ignored): if the inner universal-machine call +outputs `some [b]`, the diagonalizer outputs the inverted bit `[!b]`. This isolates the inversion +logic from the resource bound and from the `log`/`mul`/`cube` stubs. -/ +theorem diagonalizer_inverts + {p_u : PB → PB} + {f_u : ℕ × List Bool × ℕ → List Bool} + {h_u : PB.ComputesFunEnc p_u f_u} + {p_in : PB} + {x : ℕ} + {h_in : p_in.ComputesEnc env x} : + (diagonalizer p_u p_in).ComputesEnc env [!(f_u (x, Nat.bits x, x * x * x) = [true])] := + match f_u (x, Nat.bits x, x * x * x) with + | [true] => by + refine PB.ifeq_eq_computes ?_ PB.constantEnc_computesEnc PB.constantEnc_computesEnc + sorry + | _ => by + -- refine PB.ifeq_ne_computes ?_ PB.constantEnc_computesEnc ?_ ?_ + sorry + +theorem hierarchy + (enum : ℕ → NormalizedTM) + (h_enum : Enumerates enum) + (h_exists_univ : ∃ p, UniversalMachineSemantics enum p) : + DSPACE id ≠ DSPACE (fun n => n^5) := by + obtain ⟨h, h_u⟩ := h_exists_univ + let diag := fun x : List Bool => + let n := Nat.ofBits x.get + simulator enum n x (n * n * n) != some [true] + let m := diagonalizer h + -- TODO m computes diagm in a certain time, therfore it is in DSPACE (fun n => n^5) + have h_diag_in_quint : diag ∈ DSPACE (fun n => n^5) := by + sorry + have h_notin_linear : diag ∉ DSPACE id := by + intro h_linear + obtain ⟨tm, a, h_tm⟩ := h_linear + + sorry + intro h_eq + simp_all + +end RoseTreeMachine + +end Turing diff --git a/Cslib/Computability/Machines/RTM/PB.lean b/Cslib/Computability/Machines/RTM/PB.lean index 37e3f12fa0..da58c78fa7 100644 --- a/Cslib/Computability/Machines/RTM/PB.lean +++ b/Cslib/Computability/Machines/RTM/PB.lean @@ -78,6 +78,27 @@ def app (f a : PB) : PB := fun n => .app (f n) (a n) /-- Close a builder into a concrete `Prog`. -/ def build (p : PB) : Prog := p 0 +/-- A proof that a `PB` that takes another `PB` as input computes a certain value. +This is mainly used for final results. During composition, `computesFun₁` is more useful +since it allows capturing the environment. -/ +def ComputesFunInTimeAndSpace (p : PB → PB) (input output : Data) (t s : ℕ) : Prop := + ∀ env, ProgSem (env ++ [.data input]) (p (PB.var env.length) (env.length + 1)) + (.data output) t s + +/-- The `PB → PB` analogue of `Prog.ComputesInTimeAndSpace`: viewing `p` as a transformation from +an argument builder to a result builder, `p` computes `output` from `input` using `t` time and `s` +space. The input is supplied as the last entry of the environment and read back through a variable, +and the `∀ env` makes the statement hold under any outer environment (so it can be plugged into a +larger program). -/ +def ComputesInTimeAndSpace (p : PB → PB) (input output : Data) (t s : ℕ) : Prop := + ∀ env, ProgSem (env ++ [.data input]) (p (PB.var env.length) (env.length + 1)) + (.data output) t s + +/-- Encoded form of `ComputesInTimeAndSpace`: `p` maps a value encoding `input : α` to one encoding +`output : β`, using `t` time and `s` space. -/ +def ComputesEncInTimeAndSpace {α β : Type} [DataEncode α] [DataEncode β] + (p : PB → PB) (input : α) (output : β) (t s : ℕ) : Prop := + ComputesInTimeAndSpace p (DataEncode.encode input) (DataEncode.encode output) t s variable {env : List Value} @@ -114,6 +135,42 @@ This allows statements that `PB`s compute functions on lean datatypes. -/ def ComputesEnc {α : Type} [DataEncode α] (env : List Value) (impl : PB) (x : α) := Computes env impl (.data (DataEncode.encode x)) +/-- A `PB → PB` transformation `p` computes the (mathematical) function `φ`. Stated parametrically +over the *argument builder* `a` together with a hypothesis that `a` computes the input: this is the +shape of all the `_computes` lemmas (e.g. `tmMainLoop_computes`, `bitapeLeft_computes`), and it is +what makes them composable. Resource-erased; for resource bounds see `ComputesInTimeAndSpace`. -/ +def ComputesFunEnc {α β : Type} [DataEncode α] [DataEncode β] + (p : PB → PB) (φ : α → β) : Prop := + ∀ (env : List Value) (a : PB) (x : α), a.ComputesEnc env x → (p a).ComputesEnc env (φ x) + +/-- Composition of `PB → PB` transformations is function composition of the computed functions. +This is the formal statement of the implicit composition used throughout `TMSimulator`. -/ +theorem ComputesFunEnc.comp {α β γ : Type} [DataEncode α] [DataEncode β] [DataEncode γ] + {p q : PB → PB} {φ : α → β} {ψ : β → γ} + (hp : ComputesFunEnc p φ) (hq : ComputesFunEnc q ψ) : + ComputesFunEnc (fun a => q (p a)) (ψ ∘ φ) := + fun env a x h => hq env (p a) (φ x) (hp env a x h) + +/-- The identity transformation computes the identity function. -/ +theorem ComputesFunEnc.id {α : Type} [DataEncode α] : + ComputesFunEnc (α := α) (fun a => a) id := + fun _ _ _ h => h + +/-- Resource-tracked analogue of `ComputesFunEnc`: `p` computes `φ`, charging its own time `t x` +and space `s x` *on top of* the argument's cost. The costs are functions of the (decoded) input, so +the bound can scale with the actual argument (e.g. with the simulated machine and step count). Given +any argument builder `a` that computes `x` in time `ta` and space `sa`, the result builder `p a` +computes `φ x` in time `t x + ta` and space `max (s x) sa`. Threading the argument cost this way is +what makes the bounds additive under composition. -/ +def ComputesFunEncInTimeAndSpace {α β : Type} [DataEncode α] [DataEncode β] + (p : PB → PB) (φ : α → β) (t s : α → ℕ) : Prop := + ∀ (env : List Value) (a : PB) (x : α) (ta sa : ℕ), + (∀ ext : List Value, ProgSem (env ++ ext) (a (env.length + ext.length)) + (.data (DataEncode.encode x)) ta sa) → + (∀ ext : List Value, ProgSem (env ++ ext) (p a (env.length + ext.length)) + (.data (DataEncode.encode (φ x))) (t x + ta) (max (s x) sa)) + + /-- Var-lookup: `PB.var i` reads the `i`-th entry of the environment. -/ @[simp] lemma var_computes {i : ℕ} (h : i < env.length) : diff --git a/Cslib/Computability/Machines/RTM/Prog.lean b/Cslib/Computability/Machines/RTM/Prog.lean index 53db589151..3d7305f751 100644 --- a/Cslib/Computability/Machines/RTM/Prog.lean +++ b/Cslib/Computability/Machines/RTM/Prog.lean @@ -225,6 +225,10 @@ inductive InPlace : Prog → Prop accumulator. -/ | while_ (hinit : InPlace init) (hbody : InPlace body) : InPlace (.while_ init (.fn body)) + /-- `app` whose operator is a literal one-argument function `fn body` (a `let` binding): + the abstraction is created and immediately consumed, so no closure escapes. -/ + | app (hbody : InPlace body) (harg : InPlace arg) : + InPlace (.app (.fn body) arg) end RoseTreeMachine diff --git a/Cslib/Computability/Machines/RTM/Tools.lean b/Cslib/Computability/Machines/RTM/Tools.lean index b3df4ffc48..0348c50393 100644 --- a/Cslib/Computability/Machines/RTM/Tools.lean +++ b/Cslib/Computability/Machines/RTM/Tools.lean @@ -265,6 +265,7 @@ lemma listHeadOption_computes {p : PB} {l : List α} (h : p.ComputesEnc env l) : apply PB.elim_cons_computes h (PB.computesFun₂_branch2 (fun ext => ?_)) refine PB.cons_computes (var_computes_fresh ext _) empty_computes + -- Evaluate a function `f` at `arg` where the function is given as a graph (list of pairs). -- Returns `some y` for the first `x` in the graph such that `f x = y` and `none` otherwise. def evalFunGraph (graph : PB) (arg : PB) : PB := @@ -402,6 +403,37 @@ lemma evalFunGraph_Computes_of_fun apply PB.head_computes h +def bitEq (x y : PB) : PB := + ifEq x y (constantEnc true) (constantEnc false) + +def bitNot (x : PB) : PB := + ifEq x (constantEnc true) (constantEnc false) (constantEnc true) + +def bitXor (x y : PB) : PB := + ifEq x y (constantEnc false) (constantEnc true) + +def succ (x : PB) : PB := + let loop_result := foldl + (fun st bit => + let carry := st.fst + let acc := st.snd + let new_carry := PB.ifEq carry (constantEnc true) + (PB.ifEq bit (constantEnc true) (constantEnc true) (constantEnc false)) + (constantEnc false) + let new_bit := PB.ifEq carry (constantEnc true) + (PB.ifEq bit (constantEnc true) (constantEnc false) (constantEnc true)) + bit + toPair new_carry (cons new_bit acc)) + (toPair (constantEnc true) empty) + x + let final_carry := loop_result.fst + let result_rev := loop_result.snd + -- If final carry, prepend 1; otherwise just reverse back + reverse (PB.ifEq final_carry (constantEnc true) + (cons (constantEnc true) result_rev) + result_rev) + + end PB end RoseTreeMachine diff --git a/references.bib b/references.bib index 973371b652..26b27eafe0 100644 --- a/references.bib +++ b/references.bib @@ -30,6 +30,15 @@ @article{AngluinLaird1988 doi = {10.1007/BF00116829} } +@book{AroraBarak2009, + title={Computational Complexity: A Modern Approach}, + author={Arora, Sanjeev and Barak, Boaz}, + year={2009}, + publisher={Cambridge University Press}, + address={New York, NY, USA}, + isbn={978-0-521-42426-4} +} + @book{Baader1998, author = {Baader, Franz and Nipkow, Tobias}, title = {Term rewriting and all that},