From bd478cdee408a190a7a92d16b21160cb9d069896 Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 23 May 2026 20:03:13 +0200 Subject: [PATCH 1/2] Abstract machine model. --- .../Computability/Machines/MachineModel.lean | 341 ++++++++++++++++++ 1 file changed, 341 insertions(+) create mode 100644 Cslib/Computability/Machines/MachineModel.lean diff --git a/Cslib/Computability/Machines/MachineModel.lean b/Cslib/Computability/Machines/MachineModel.lean new file mode 100644 index 000000000..f5d3da74b --- /dev/null +++ b/Cslib/Computability/Machines/MachineModel.lean @@ -0,0 +1,341 @@ +/- +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 Mathlib.Data.Part +public import Cslib.Computability.Machines.SingleTapeTuring.Basic +public import Mathlib.Data.Nat.Bits +public import Mathlib.Tactic.DeriveFintype +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta +public import Mathlib.Tactic.Sat.FromLRAT + +@[expose] public section + +open Cslib Relation + +namespace Complexity + +/-- A generic model of a machine that performs computations on a data type that is specific +to the machine type. -/ +class MachineModel (Machine : Type*) where + /-- The input and output data type of the machine. -/ + DataType : Type + /-- A size measure for the data type. -/ + size : DataType → ℕ + /-- Execute the machine `m` on input `x` and return the output, the consumed time + and the consumed space (if it terminates). -/ + runEncoded (m : Machine) (x : DataType) : Part (DataType × ℕ × ℕ) + +/-- This class specifies a way to encode arbitrary lean types into the internal type of the +machine. -/ +class MachineEncodable (Machine : Type*) [MachineModel Machine] (α : Type) where + encode : α → (MachineModel.DataType Machine) + decode : (MachineModel.DataType Machine) → Option α + encodeDecode : ∀ x, decode (encode x) = some x + +namespace MachineModel + +variable {Machine : Type*} [MachineModel Machine] + {α β : Type} [MachineEncodable Machine α] [MachineEncodable Machine β] + +/-- Run the machine `m` on `x` and return the output, the consumed time and the consumed space +(if it terminates). +Failure to decode the ouput is treated in the same way as non-termination. +This is a lifted version of `runEncoded` to work with encodable types. -/ +def run (m : Machine) (x : α) : Part (β × ℕ × ℕ) := do + (runEncoded m (MachineEncodable.encode x)).bind fun (out, time, space) => + match MachineEncodable.decode out with + | some out' => Part.some (out', time, space) + | none => Part.none + +/-- The size of an encodable lean type in the internal data type. -/ +def encodedSize (x : α) : ℕ := size (MachineEncodable.encode (Machine := Machine) x) + +/-- The output of the machine `m` on input `input`, if it terminates. -/ +def runOutput (m : Machine) (input : α) : Part β := + (run m input).map fun (out, _, _) => out + +/-- The time consumption of the machine `m` on input `input`, if it terminates. -/ +def runTime (m : Machine) (input : α) : Part ℕ := + (run (β := β) m input).map fun (_, time, _) => time + +/-- The space consumption of the machine `m` on input `input`, if it terminates. -/ +def runSpace (m : Machine) (input : α) : Part ℕ := + (run (β := β) m input).map fun (_, _, space) => space + +/-- A machine `m` computes the function `f` using the encoding of the machine model. -/ +def ComputesFunction (m : Machine) (f : α → β) : Prop := + ∀ x : α, runOutput m x = Part.some (f x) + +/-- A machine `m` terminates in `O(t(n))` time on inputs of size `n`. -/ +def RunsInOTime (m : Machine) (t : ℕ → ℕ) : Prop := + ∃ c₁ c₂ : ℕ, ∀ x : α, ∃ t' : ℕ, + runTime (β := β) m x = Part.some t' ∧ + t' ≤ c₁ * (t (encodedSize (Machine := Machine) x)) + c₂ + +/-- The machine model can compute the function `f` in time `O(t)`. -/ +def ComputableInOTime (f : α → β) (t : ℕ → ℕ) : Prop := + ∃ m : Machine, RunsInOTime (α := α) (β := β) m t ∧ ComputesFunction m f + +/-- A machine `m` terminates using `O(s)` space. -/ +def RunsInOSpace (m : Machine) (s : ℕ → ℕ) : Prop := + ∃ c₁ c₂ : ℕ, ∀ x : α, ∃ s' : ℕ, + runSpace (β := β) m x = Part.some s' ∧ + s' ≤ c₁ * s (encodedSize (Machine := Machine) x) + c₂ + +/-- The machine model can compute the function `f` in space `O(s)`. -/ +def ComputableInOSpace (f : α → β) (s : ℕ → ℕ) : Prop := + ∃ m : Machine, RunsInOSpace (α := α) (β := β) m s ∧ ComputesFunction m f + +/-- The machine `m` is a universal machine in the machine model in the sense that it can +simulate all other machines of the same model. +TODO: We should require that we can always encode the tuple. -/ +def UniversalMachine {Machine : Type} [MachineModel Machine] + [MachineEncodable Machine Machine] (u : Machine) : Prop := + ∀ m : Machine, ∀ α β : Type, ∀ [MachineEncodable Machine α] [MachineEncodable Machine β], + ∀ [MachineEncodable Machine (Machine × α)], + ∀ x : α, runOutput (β := β) u (m, x) = runOutput m x + +/- The next two definitions are important: If two machine models are linearly space-related +and polynomially time-related, it is generally agreed that they capture the same kind of +complexity theory. + +For some computation models, this is true except for space bounds below linear - we could +have a special exception for those. -/ + +/-- Two machine models are linearly space-related, if all functions that are encodable in both +models are computable in the same space bound. -/ +def LinearlySpaceRelated (Machine₁ Machine₂ : Type) + [MachineModel Machine₁] [MachineModel Machine₂] : Prop := + ∀ α β : Type, ∀ [MachineEncodable Machine₁ α] [MachineEncodable Machine₁ β] + [MachineEncodable Machine₂ α] [MachineEncodable Machine₂ β], + ∀ f : α → β, ∀ s, + ComputableInOSpace (Machine := Machine₁) f s ↔ ComputableInOSpace (Machine := Machine₂) f s + +/-- Two machine models are polynomially time-related if all functions that are encodable in both +models can be simulated with a polynomial overhead. -/ +def PolynomiallyTimeRelated (Machine₁ Machine₂ : Type) + [MachineModel Machine₁] [MachineModel Machine₂] : Prop := + ∃ k₁ k₂, + ∀ α β : Type, ∀ [MachineEncodable Machine₁ α] [MachineEncodable Machine₁ β] + [MachineEncodable Machine₂ α] [MachineEncodable Machine₂ β], + ∀ f : α → β, ∀ t, + ComputableInOTime (Machine := Machine₁) f t → + ComputableInOTime (Machine := Machine₂) f (fun n => (t n) ^ k₁) ∧ + ComputableInOTime (Machine := Machine₂) f t → + ComputableInOTime (Machine := Machine₁) f (fun n => (t n) ^ k₂) + +/-- The function `s` is space constructible if there is a machine that has `s(n)` as its +space consumption on any input of length `n`. +Note: Usually one supplies `1^n` as input, but there is no canonical way to do this here. +The point is that the input has size `n` and no other information apart from that, but we should +get the same result by requiring the (exact) same space consumption for all inputs of this size. -/ +def SpaceConstructible (s : ℕ → ℕ) : Prop := + ∃ m : Machine, ∀ n, ∀ α, ∀ [MachineEncodable Machine α], ∀ x : α, + encodedSize (Machine := Machine) (α := α) x = n → runSpace (β := β) m x = Part.some (s n) + +/-- The function `t` is time constructible if there is a machine that has `t` as its time +consumption. +Note: Usually one supplies `1^n` as input, but there is no canonical way to do this here. +The point is that the input has size `n` and no other information apart from that, but we should +get the same result by requiring the (exact) same space consumption for all inputs of this size. -/ +def TimeConstructible (t : ℕ → ℕ) : Prop := + ∃ m : Machine, ∀ n, ∀ α, ∀ [MachineEncodable Machine α], ∀ x : α, + encodedSize (Machine := Machine) (α := α) x = n ∧ runTime (β := β) m x = Part.some (t n) + + +end MachineModel + +/- +The rest if this file is just some examples that show how MachineModel is used. +-/ + +namespace SingleTapeTMMachineModel + +/- +Example instances using single-tape Turing machines. +We use one machine model per alphabet. In complexity theory, most results are relative to some +alphabet with at least two elements and the alphabet is often omitted, so I think this is fine. +-/ + +open Turing.SingleTapeTM + +variable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] + +/-- If the Turing machine `tm` halts on input `input` after exactly `n` steps in a valid output +configuration, returns the output. Otherwise, returns `none`. +This translates the reachability-based definition of SingleTapeTM to a step-based one. -/ +def outputAfterStep (tm : Turing.SingleTapeTM Symbol) (input : List Symbol) (n : ℕ) : + Option (List Symbol) := + match (Option.bind · tm.step)^[n] (some (initCfg tm input)) with + | some ⟨none, t⟩ => + if t.left.toList = [] then + (t.head :: t.right.toList).reduceOption + else + none + | _ => none + +instance : MachineModel (Turing.SingleTapeTM Symbol) where + DataType := List Symbol + size := List.length + runEncoded (tm : Turing.SingleTapeTM Symbol) (input : List Symbol) := + ⟨(∃ n, (outputAfterStep tm input n).isSome), + fun h => + let n := Nat.find h + let output := (outputAfterStep tm input n).get (Nat.find_spec h) + (output, n, 0)⟩ + +/- Let us use an alphabet and define some encodings. -/ + +inductive Alph : Type + | zero + | one + | left + | right + deriving Inhabited, Fintype + +abbrev TM := Turing.SingleTapeTM Alph + +def encodeBool : Bool → Alph + | false => .zero + | true => .one + +def decodeBool : Alph → Option Bool + | .zero => some false + | .one => some true + | _ => none + +instance : MachineEncodable TM Bool where + encode x := [encodeBool x] + decode c := c.head?.bind decodeBool + encodeDecode x := by cases x <;> rfl + +instance : MachineEncodable TM ℕ where + encode n := (Nat.bits n).map encodeBool + decode s := sorry + encodeDecode n := sorry + +inductive Literal where + | pos (i : ℕ) + | neg (i : ℕ) + +instance : MachineEncodable TM Literal where + encode l := match l with + | .pos i => Alph.zero :: (MachineEncodable.encode (Machine := TM) i) + | .neg i => Alph.one :: (MachineEncodable.encode (Machine := TM) i) + decode := sorry + encodeDecode := sorry + +variable {α β : Type} [MachineEncodable TM α] + [MachineEncodable TM β] + +instance : MachineEncodable TM (List α) where + encode l := + Alph.left :: (l.map (MachineEncodable.encode (Machine := TM))).flatten + ++ [Alph.right] + decode := sorry + encodeDecode := sorry + +instance : MachineEncodable TM (α × β) where + encode := fun (a, b) => + Alph.left :: MachineEncodable.encode (Machine := TM) a + ++ Alph.right :: Alph.left + :: MachineEncodable.encode (Machine := TM) b + ++ [Alph.right] + decode := sorry + encodeDecode := sorry + +/-- A list of positive-assigned variables satisfies a cnf -/ +def satisfies (pos_vars : List ℕ) (cnf : List (List Literal)) : Bool := + cnf.all (fun c => c.any (fun l => match l with + | .pos i => i ∈ pos_vars + | .neg i => i ∉ pos_vars)) + +/-- A theorem that states that boolean formula evaluation (given in CNF) is in cubic time. -/ +theorem formula_evaluation_in_p : + MachineModel.ComputableInOTime (Machine := TM) (β := Bool) + (fun (pos_vars, cnf) => satisfies pos_vars cnf) (fun n => n ^ 3) := sorry + +end SingleTapeTMMachineModel + +namespace LambdaCalculusMachineModel + +/- +Now let us take a look at lambda calculus. +Disclaimer: I don't know much about lambda calculus. +The aspect to illustrate here is that the internal data type is not a list of symbols from a +finite alphabet. Still, there is a reasonable size measure and a computation notion that +happens directly on that type. +-/ + +open LambdaCalculus.LocallyNameless.Untyped + +variable {Var : Type} + +/-- The size of a lambda term. +Note: Not sure if that has been defined somewhere else. -/ +def size : Term Var → ℕ + | Term.bvar _ => 1 + | Term.fvar _ => 1 + | Term.abs t => 1 + size t + | Term.app l r => 1 + size l + size r + +/-- Performs a single leftmost-outermost β-reduction step. +Returns `some t'` if a redex was contracted, `none` if `t` is in β-normal form. +Note: I could not find a computable beta reduction in Cslib. +I also do not know if this here is correct. -/ +def betaStep : Term Var → Option (Term Var) + | Term.app (Term.abs M) N => some (Term.open' M N) + | Term.app f a => + match betaStep f with + | some f' => some (Term.app f' a) + | none => + match betaStep a with + | some a' => some (Term.app f a') + | none => none + | Term.abs M => + match betaStep M with + | some M' => some (Term.abs M') + | none => none + | Term.bvar _ | Term.fvar _ => none + +/-- Iterates `betaStep` for at most `fuel` steps. Returns `some (t', steps, maxSize)` where +`t'` is the β-normal form reached, `steps` is the number of β-reductions performed, and +`maxSize` is the maximum `size` of any intermediate term (including the starting term and the +normal form). Returns `none` if the normal form was not reached within `fuel` steps. -/ +def reduceToNormal (fuel : ℕ) (term : Term Var) : Option (Term Var × ℕ × ℕ) := + match betaStep term with + | none => some (term, 0, size term) + | some t' => + match fuel with + | 0 => none + | n + 1 => + (reduceToNormal n t').map fun (r, k, m) => (r, k + 1, max (size term) m) + +instance : MachineModel (Term Var) where + DataType := Term Var + size := size + runEncoded m input := + let start := Term.app m input + { Dom := ∃ n, (reduceToNormal n start).isSome + get := fun h => (reduceToNormal (Nat.find h) start).get (Nat.find_spec h) } + +end LambdaCalculusMachineModel + +/- +I am working on another machine model where the internal representation is + +inductive Data where + | l : List Data → Data + +and the computation is stated in a functional way that is not step-based, but has a clear +notion of "time consumed" and "space consumed", so this would be another reason to specify +the machine model in such an abstract way. + +-/ + +end Complexity From eecd7633ca4060b34a3cdca33aef05aa68a7b251 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 24 May 2026 11:59:07 +0200 Subject: [PATCH 2/2] Add requirement that encodings are linearly related. --- .../Computability/Machines/MachineModel.lean | 37 ++++++++++++++----- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/Cslib/Computability/Machines/MachineModel.lean b/Cslib/Computability/Machines/MachineModel.lean index f5d3da74b..202f489a0 100644 --- a/Cslib/Computability/Machines/MachineModel.lean +++ b/Cslib/Computability/Machines/MachineModel.lean @@ -105,24 +105,41 @@ and polynomially time-related, it is generally agreed that they capture the same complexity theory. For some computation models, this is true except for space bounds below linear - we could -have a special exception for those. -/ +have a special exception for those. + +In order to make this consistent relative to encodings, we need to ensure that the encodings +do not blow up the input too much: -/ + +/-- The encodings of two machine models are linearly related in size for a type `α`. -/ +def LinearlySizeRelatedEncodings (Machine₁ Machine₂ : Type) [MachineModel Machine₁] [MachineModel Machine₂] + (α : Type) [MachineEncodable Machine₁ α] [MachineEncodable Machine₂ α] : Prop := + ∃ k, ∀ x : α, + encodedSize (Machine := Machine₁) x ≤ k * encodedSize (Machine := Machine₂) x ∧ + encodedSize (Machine := Machine₂) x ≤ k * encodedSize (Machine := Machine₁) x + /-- Two machine models are linearly space-related, if all functions that are encodable in both models are computable in the same space bound. -/ -def LinearlySpaceRelated (Machine₁ Machine₂ : Type) - [MachineModel Machine₁] [MachineModel Machine₂] : Prop := - ∀ α β : Type, ∀ [MachineEncodable Machine₁ α] [MachineEncodable Machine₁ β] - [MachineEncodable Machine₂ α] [MachineEncodable Machine₂ β], +def LinearlySpaceRelated + (Machine₁ Machine₂ : Type) [MachineModel Machine₁] [MachineModel Machine₂] + (α β : Type) + [MachineEncodable Machine₁ α] [MachineEncodable Machine₁ β] + [MachineEncodable Machine₂ α] [MachineEncodable Machine₂ β] : Prop := + LinearlySizeRelatedEncodings Machine₁ Machine₂ α → + LinearlySizeRelatedEncodings Machine₁ Machine₂ β → ∀ f : α → β, ∀ s, ComputableInOSpace (Machine := Machine₁) f s ↔ ComputableInOSpace (Machine := Machine₂) f s /-- Two machine models are polynomially time-related if all functions that are encodable in both models can be simulated with a polynomial overhead. -/ -def PolynomiallyTimeRelated (Machine₁ Machine₂ : Type) - [MachineModel Machine₁] [MachineModel Machine₂] : Prop := - ∃ k₁ k₂, - ∀ α β : Type, ∀ [MachineEncodable Machine₁ α] [MachineEncodable Machine₁ β] - [MachineEncodable Machine₂ α] [MachineEncodable Machine₂ β], +def PolynomiallyTimeRelated + (Machine₁ Machine₂ : Type) [MachineModel Machine₁] [MachineModel Machine₂] + (α β : Type) + [MachineEncodable Machine₁ α] [MachineEncodable Machine₁ β] + [MachineEncodable Machine₂ α] [MachineEncodable Machine₂ β] : Prop := + LinearlySizeRelatedEncodings Machine₁ Machine₂ α → + LinearlySizeRelatedEncodings Machine₁ Machine₂ β → + ∃ k₁ k₂, ∀ f : α → β, ∀ t, ComputableInOTime (Machine := Machine₁) f t → ComputableInOTime (Machine := Machine₂) f (fun n => (t n) ^ k₁) ∧