Start general definitions for computation models

Cslib.lean

@@ -29,6 +29,7 @@ public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Machines.ComputationModel.Basic
 public import Cslib.Computability.Machines.SingleTapeTuring.Basic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable

Cslib/Computability/Machines/ComputationModel/Basic.lean

@@ -0,0 +1,195 @@
+/-
+Copyright (c) 2026 Maximilian Keßler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Maximilian Keßler
+-/
+
+module
+
+public import Mathlib.Algebra.Polynomial.Eval.Defs
+public import Mathlib.Data.ENat.Lattice
+public import Mathlib.Logic.Function.Iterate
+public import Cslib.Foundations.Data.RelatesInSteps
+
+/-! # Transition Based Computation Models
+
+Defines typeclasses and definitions for computation systems based on a transition function
+`step : cfg → Option cfg`, where `cfg` is the type of configurations of such a system.
+Additionally, we bundle this with input/output functions from/to words over an alphabet
+to obtain a model of computation between lists of symbols that has a notion of execution time
+(given by the needed number of applications of the `step` function).
+
+The main example of such a transition machine are turing machines:
+Typical turing models work by inputting a word (over a fixed alphabet)
+on a specific tape, then iterating a step function until an accepting state is reached,
+and the output is defined as a word (potentially over a different alphabet than the input),
+typically read from a specific tape.
+For all such turing machines (independent of the exact design choices), we can define instances
+to `TransitionMachine` and thereby use the same definitions of computation and time for all
+models, and in particular state equivalences of such computation models.
+
+## Design
+
+- Termination of such a machine is modeled by the step function yielding `none`
+- We expose the alphabet types in the definition of `TransitionMachine`.
+- The output function is *partial* in the sense that it can return `none`. In this case,
+  there is no output of a computation (this can occur even if the computation terminates).
+
+## Important declarations
+- `TransitionSystem τ`: Terms `(t : τ)` have an associated *configuration type* `cfg t`
+- `TransitionMachine τ Γᵢ Γₒ`: In addition to this being a `TransitionSystem τ`, there is
+  - an input function `init : List Γᵢ → cfg t`
+  - an output function `output : cfg t → Option (List Γₒ)`
+- `OutputsInTime t n l l'`: States that `t` outputs `l'` from `l` in at most `n` steps.
+- `ComputesInPolyTime t f`: The machine `t` computes the function `f : List Γᵢ → List Γₒ` in
+  polynomial time.
+
+## TODO:
+It might be useful to work with `ℕ∞` instead of `ℕ` for predicates such as `EvalsToInTime`.
+This would allow us to recover the regular notion of `EvalsTo` (without time constraints)
+as the special case of the time bound `ω`.
+We could then introduce abbreviations for `EvalsTo` or `Outputs` that insert `ω`.
+
+-/
+
+@[expose] public section
+
+namespace Computation
+
+/--
+For each element `(t : τ)`, there is a bundle of a type `cfg t` with a step / transition function
+`cfg t → Option (cfg t)`.
+-/
+class TransitionSystem (τ : Type u) where
+  cfg (t : τ) : Type*
+  step {t : τ} : cfg t → Option (cfg t)
+
+/--
+Bundles a `TransitionSystem` with input and output functions from/to words over an alphabet.
+This way, we can think of elements of `τ` as allowing computations `List Γᵢ → List Γₒ`
+by lifting inputs into the computation context, iterating the `step` function,
+and taking output from this computation context.
+-/
+class TransitionMachine (τ : Type u) (Γᵢ Γₒ : outParam (Type v)) extends TransitionSystem τ where
+  init {t : τ} : List Γᵢ → cfg t
+  output {t : τ} : cfg t → Option (List Γₒ)
+
+
+namespace TransitionSystem
+
+variable {τ : Type u} [TransitionSystem τ]
+
+def stepRelation (t : τ) : (Option (cfg t)) → (Option (cfg t)) → Prop
+  | a, b => a.bind step = b
+
+/--
+A "proof" of the fact that `t` eventually reaches `b` when repeatedly evaluated on `a`,
+remembering the number of steps it takes.
+-/
+structure EvalsTo (t : τ) (a b : Option (cfg t)) where
+  steps : ℕ
+  evals : (flip bind step)^[steps] a = b
+
+/--
+A "proof" that `t` reaches `b` from `a` in at most `n` steps, remembering the specific number
+of steps.
+-/
+structure EvalsToInTime (t : τ) (a b : Option (cfg t)) (n : ℕ) extends EvalsTo t a b where
+  steps_le : steps ≤ n
+
+variable {t : τ} {a b c : Option (cfg t)} {n n₁ n₂ : ℕ}
+
+def EvalsTo.refl : EvalsTo t a a where
+  steps := 0
+  evals := rfl
+
+def EvalsTo.trans (h₁ : EvalsTo t a b) (h₂ : EvalsTo t b c) : EvalsTo t a c where
+  steps := h₂.steps + h₁.steps
+  evals := by rw [Function.iterate_add_apply, h₁.evals, h₂.evals]
+
+def EvalsToInTime.refl : EvalsToInTime t a a 0 where
+  toEvalsTo := EvalsTo.refl
+  steps_le := by rfl
+
+def EvalsToInTime.trans (h₁ : EvalsToInTime t a b n₁) (h₂ : EvalsToInTime t b c n₂) :
+    EvalsToInTime t a c (n₂ + n₁) where
+  toEvalsTo := EvalsTo.trans h₁.toEvalsTo h₂.toEvalsTo
+  steps_le := add_le_add h₂.steps_le h₁.steps_le
+
+def EvalsToInTime.of_le (h : EvalsToInTime t a b n₁) (hn : n₁ ≤ n₂) :
+    EvalsToInTime t a b n₂ where
+  toEvalsTo := h.toEvalsTo
+  steps_le := le_trans h.steps_le hn
+
+
+end TransitionSystem
+
+namespace TransitionMachine
+open TransitionSystem
+
+variable {τ : Type*} {Γᵢ Γₒ : Type} [TransitionMachine τ Γᵢ Γₒ]
+
+/--
+The transition machine `t` outputs `l'` on input `l`.
+-/
+structure Outputs (t : τ) (l : List Γᵢ) (l' : List Γₒ) where
+  haltState : (cfg t)
+  haltState_halts : TransitionSystem.step haltState = none
+  evalsTo : TransitionSystem.EvalsTo t (some (init l)) (some haltState)
+  output_eq : output haltState =  some l'
+
+/--
+The transition machine `t` outputs `l'` on input `l` in at most `n` steps.
+-/
+structure OutputsInTime (t : τ) (n : ℕ) (l : List Γᵢ) (l' : List Γₒ) where
+  haltState : (cfg t)
+  haltState_halts : TransitionSystem.step haltState = none
+  evals_to : TransitionSystem.EvalsToInTime t (some (init l)) (some haltState) n
+  output_eq : output haltState = some l'
+
+/--
+Time bounds of `OutputsInTime` can be increased.
+-/
+def OutputsInTime.of_le {t : τ} {n m : ℕ} {l : List Γᵢ} {l' : List Γₒ} (hnm : n ≤ m)
+    (hv : OutputsInTime t n l l') : OutputsInTime t m l l' where
+  haltState := hv.haltState
+  haltState_halts := hv.haltState_halts
+  evals_to := TransitionSystem.EvalsToInTime.of_le hv.evals_to hnm
+  output_eq := hv.output_eq
+
+/--
+The output of any computation of transition machines is unique.
+-/
+lemma OutputsInTime.output_unique {t : τ} {n₁ n₂ : ℕ} {l : List Γᵢ} {l'₁ l'₂ : List Γₒ}
+    (ho₁ : OutputsInTime t n₁ l l'₁) (ho₂ : OutputsInTime t n₂ l l'₂) :
+    l'₁ = l'₂ := by
+  wlog hle : ho₁.evals_to.steps ≤ ho₂.evals_to.steps
+  · symm
+    exact this ho₂ ho₁ (Nat.le_of_not_le hle)
+  · have : ho₁.evals_to.steps = ho₂.evals_to.steps := by
+      obtain ⟨d, hd⟩ := Nat.exists_eq_add_of_le' hle
+      cases d with
+      | zero => symm; simpa using hd
+      | succ d' =>
+          have := ho₂.evals_to.evals
+          rw [hd, Function.iterate_add_apply, ho₁.evals_to.evals,
+            Function.iterate_succ_apply, Option.bind_eq_bind, flip, Option.bind_some,
+            ho₁.haltState_halts, Function.iterate_fixed rfl] at this
+          contradiction
+    have : ho₁.haltState = ho₂.haltState := by
+      apply Option.some.inj
+      rw [← ho₁.evals_to.evals, ← ho₂.evals_to.evals, this]
+    rw [← Option.some_inj, ← ho₁.output_eq, ← ho₂.output_eq, this]
+
+/--
+"Proof" that the transition system `t` computes the function `f` in polynomial time.
+The witness polynomial is bundled as part of this structure.
+-/
+structure ComputesInPolyTime (t : τ) (f : List Γᵢ → List Γₒ) where
+  time : Polynomial ℕ
+  outputsFun : ∀ w, OutputsInTime t (time.eval w.length) w (f w)
+
+end TransitionMachine
+
+
+end Computation