From f63e9d81a2114b012bf6cf82b6b4202684b97923 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= Date: Wed, 6 May 2026 13:58:05 +0200 Subject: [PATCH 1/3] start outlining general definitions for computation models --- Cslib.lean | 1 + .../Machines/ComputationModel/Basic.lean | 125 ++++++++++++++++++ 2 files changed, 126 insertions(+) create mode 100644 Cslib/Computability/Machines/ComputationModel/Basic.lean diff --git a/Cslib.lean b/Cslib.lean index 37a038ee4..a0f9a2641 100644 --- a/Cslib.lean +++ b/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 diff --git a/Cslib/Computability/Machines/ComputationModel/Basic.lean b/Cslib/Computability/Machines/ComputationModel/Basic.lean new file mode 100644 index 000000000..83d106609 --- /dev/null +++ b/Cslib/Computability/Machines/ComputationModel/Basic.lean @@ -0,0 +1,125 @@ +/- +Copyright (c) 2025 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Maximilian Keßler +-/ + +module + +public import Cslib.Foundations.Data.RelatesInSteps +public import Mathlib.Data.ENat.Lattice +public import Mathlib.Logic.Function.Iterate + +/-! # Transition Based Computation Models + + +-/ + +@[expose] public section + +namespace Turing + +/-- Bundle of a type `σ` with a step function `σ → Option σ`. -/ +class TransitionModel (τ : Type*) where + σ (a : τ) : Type + step {a : τ} : σ a → Option (σ a) + +/-- An abstract version of a turing machine with input alphabet `Γ₀` and output alphabet `Γ₁`. -/ +class TransitionComputer (τ : Type*) (Γ₀ Γ₁ : Type) extends TransitionModel τ where + init {a : τ} : List Γ₀ → σ a + output {a : τ} : σ a → List Γ₁ + +notation "σ[" x "]" => TransitionModel.σ x + + +namespace TransitionModel + +variable {τ : Type*} [TransitionModel τ] + +def stepRelation (tm : τ) : (Option σ[tm]) → (Option σ[tm]) → Prop + | a, b => a.bind step = b + +/-- A "proof" of the fact that `f` eventually reaches `b` when repeatedly evaluated on `a`, +remembering the number of steps it takes. -/ +structure EvalsTo (tm : τ) (a b : Option σ[tm]) where + steps : ℕ + evals : (flip bind step)^[steps] a = b + +structure EvalsToInTime (tm : τ) (a b : Option σ[tm]) (n : ℕ) extends EvalsTo tm a b where + steps_le : steps ≤ n + +variable {tm : τ} {a b c : Option σ[tm]} {n n₁ n₂ : ℕ} + +def EvalsTo.refl : EvalsTo tm a a where + steps := 0 + evals := rfl + +def EvalsTo.trans (h₁ : EvalsTo tm a b) (h₂ : EvalsTo tm b c) : EvalsTo tm a c where + steps := h₂.steps + h₁.steps + evals := by rw [Function.iterate_add_apply, h₁.evals, h₂.evals] + +def EvalsToInTime.refl : EvalsToInTime tm a a 0 where + toEvalsTo := EvalsTo.refl + steps_le := by rfl + +def EvalsToInTime.trans (h₁ : EvalsToInTime tm a b n₁) (h₂ : EvalsToInTime tm b c n₂) : + EvalsToInTime tm 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 tm a b n₁) (hn : n₁ ≤ n₂) : + EvalsToInTime tm a b n₂ where + toEvalsTo := h.toEvalsTo + steps_le := le_trans h.steps_le hn + + +end TransitionModel + +namespace TransitionComputer + +variable {τ : Type*} {Γ₀ Γ₁ : Type} [TransitionComputer τ Γ₀ Γ₁] + +structure Outputs (tm : τ) (l : List Γ₀) (l' : List Γ₁) where + haltState : σ[tm] + haltState_halts : TransitionModel.step haltState = none + evalsTo : TransitionModel.EvalsTo tm (some (init l)) (some haltState) + output_eq : output haltState = l' + +structure OutputsInTime (tm : τ) (n : ℕ) (l : List Γ₀) (l' : List Γ₁) where + haltState : σ[tm] + haltState_halts : TransitionModel.step haltState = none + evals_to : TransitionModel.EvalsToInTime tm (some (init l)) (some haltState) n + output_eq : output haltState = l' + +def OutputsInTime.of_le {tm : τ} {n m : ℕ} {l : List Γ₀} {l' : List Γ₁} (hnm : n ≤ m) + (hv : OutputsInTime tm n l l') : OutputsInTime tm m l l' where + haltState := hv.haltState + haltState_halts := hv.haltState_halts + evals_to := TransitionModel.EvalsToInTime.of_le hv.evals_to hnm + output_eq := hv.output_eq + +lemma OutputsInTime.output_unique {tm : τ} {n₁ n₂ : ℕ} {l : List Γ₀} {l'₁ l'₂ : List Γ₁} + (ho₁ : OutputsInTime tm n₁ l l'₁) (ho₂ : OutputsInTime tm 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 [← ho₁.output_eq, ← ho₂.output_eq, this] + +end TransitionComputer + + +end Turing From 0f34e5746f8844526a0446d70aa4ecaddeff01f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= Date: Thu, 7 May 2026 14:34:59 +0200 Subject: [PATCH 2/3] Better names for Transducer and parameters Thank you to Christian Reitwiessner for suggestions https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Typeclasses.20for.20computation.20models/near/593283668 --- .../Machines/ComputationModel/Basic.lean | 61 +++++++++---------- 1 file changed, 30 insertions(+), 31 deletions(-) diff --git a/Cslib/Computability/Machines/ComputationModel/Basic.lean b/Cslib/Computability/Machines/ComputationModel/Basic.lean index 83d106609..88ef884d5 100644 --- a/Cslib/Computability/Machines/ComputationModel/Basic.lean +++ b/Cslib/Computability/Machines/ComputationModel/Basic.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2025 Bolton Bailey. All rights reserved. +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 -/ @@ -19,36 +19,34 @@ public import Mathlib.Logic.Function.Iterate namespace Turing -/-- Bundle of a type `σ` with a step function `σ → Option σ`. -/ -class TransitionModel (τ : Type*) where - σ (a : τ) : Type - step {a : τ} : σ a → Option (σ a) +/-- Bundle of a type `cfg` with a step function `cfg → Option cfg`. -/ +class TransitionSystem (τ : Type*) where + cfg (a : τ) : Type* + step {a : τ} : cfg a → Option (cfg a) /-- An abstract version of a turing machine with input alphabet `Γ₀` and output alphabet `Γ₁`. -/ -class TransitionComputer (τ : Type*) (Γ₀ Γ₁ : Type) extends TransitionModel τ where - init {a : τ} : List Γ₀ → σ a - output {a : τ} : σ a → List Γ₁ +class Transducer (τ : Type*) (Γᵢₙ Γₒᵤₜ : Type) extends TransitionSystem τ where + init {a : τ} : List Γᵢₙ → cfg a + output {a : τ} : cfg a → List Γₒᵤₜ -notation "σ[" x "]" => TransitionModel.σ x +namespace TransitionSystem -namespace TransitionModel +variable {τ : Type*} [TransitionSystem τ] -variable {τ : Type*} [TransitionModel τ] - -def stepRelation (tm : τ) : (Option σ[tm]) → (Option σ[tm]) → Prop +def stepRelation (tm : τ) : (Option (cfg tm)) → (Option (cfg tm)) → Prop | a, b => a.bind step = b /-- A "proof" of the fact that `f` eventually reaches `b` when repeatedly evaluated on `a`, remembering the number of steps it takes. -/ -structure EvalsTo (tm : τ) (a b : Option σ[tm]) where +structure EvalsTo (tm : τ) (a b : Option (cfg tm)) where steps : ℕ evals : (flip bind step)^[steps] a = b -structure EvalsToInTime (tm : τ) (a b : Option σ[tm]) (n : ℕ) extends EvalsTo tm a b where +structure EvalsToInTime (tm : τ) (a b : Option (cfg tm)) (n : ℕ) extends EvalsTo tm a b where steps_le : steps ≤ n -variable {tm : τ} {a b c : Option σ[tm]} {n n₁ n₂ : ℕ} +variable {tm : τ} {a b c : Option (cfg tm)} {n n₁ n₂ : ℕ} def EvalsTo.refl : EvalsTo tm a a where steps := 0 @@ -73,32 +71,33 @@ def EvalsToInTime.of_le (h : EvalsToInTime tm a b n₁) (hn : n₁ ≤ n₂) : steps_le := le_trans h.steps_le hn -end TransitionModel +end TransitionSystem -namespace TransitionComputer +namespace Transducer +open TransitionSystem -variable {τ : Type*} {Γ₀ Γ₁ : Type} [TransitionComputer τ Γ₀ Γ₁] +variable {τ : Type*} {Γᵢₙ Γₒᵤₜ : Type} [Transducer τ Γᵢₙ Γₒᵤₜ] -structure Outputs (tm : τ) (l : List Γ₀) (l' : List Γ₁) where - haltState : σ[tm] - haltState_halts : TransitionModel.step haltState = none - evalsTo : TransitionModel.EvalsTo tm (some (init l)) (some haltState) +structure Outputs (tm : τ) (l : List Γᵢₙ) (l' : List Γₒᵤₜ) where + haltState : (cfg tm) + haltState_halts : TransitionSystem.step haltState = none + evalsTo : TransitionSystem.EvalsTo tm (some (init l)) (some haltState) output_eq : output haltState = l' -structure OutputsInTime (tm : τ) (n : ℕ) (l : List Γ₀) (l' : List Γ₁) where - haltState : σ[tm] - haltState_halts : TransitionModel.step haltState = none - evals_to : TransitionModel.EvalsToInTime tm (some (init l)) (some haltState) n +structure OutputsInTime (tm : τ) (n : ℕ) (l : List Γᵢₙ) (l' : List Γₒᵤₜ) where + haltState : (cfg tm) + haltState_halts : TransitionSystem.step haltState = none + evals_to : TransitionSystem.EvalsToInTime tm (some (init l)) (some haltState) n output_eq : output haltState = l' -def OutputsInTime.of_le {tm : τ} {n m : ℕ} {l : List Γ₀} {l' : List Γ₁} (hnm : n ≤ m) +def OutputsInTime.of_le {tm : τ} {n m : ℕ} {l : List Γᵢₙ} {l' : List Γₒᵤₜ} (hnm : n ≤ m) (hv : OutputsInTime tm n l l') : OutputsInTime tm m l l' where haltState := hv.haltState haltState_halts := hv.haltState_halts - evals_to := TransitionModel.EvalsToInTime.of_le hv.evals_to hnm + evals_to := TransitionSystem.EvalsToInTime.of_le hv.evals_to hnm output_eq := hv.output_eq -lemma OutputsInTime.output_unique {tm : τ} {n₁ n₂ : ℕ} {l : List Γ₀} {l'₁ l'₂ : List Γ₁} +lemma OutputsInTime.output_unique {tm : τ} {n₁ n₂ : ℕ} {l : List Γᵢₙ} {l'₁ l'₂ : List Γₒᵤₜ} (ho₁ : OutputsInTime tm n₁ l l'₁) (ho₂ : OutputsInTime tm n₂ l l'₂) : l'₁ = l'₂ := by wlog hle : ho₁.evals_to.steps ≤ ho₂.evals_to.steps @@ -119,7 +118,7 @@ lemma OutputsInTime.output_unique {tm : τ} {n₁ n₂ : ℕ} {l : List Γ₀} { rw [← ho₁.evals_to.evals, ← ho₂.evals_to.evals, this] rw [← ho₁.output_eq, ← ho₂.output_eq, this] -end TransitionComputer +end Transducer end Turing From fdc4b1f4f6c66849008d57acd360fd4ad5ac9f0c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= Date: Tue, 12 May 2026 14:21:25 +0200 Subject: [PATCH 3/3] Cleanup. Add comments. --- .../Machines/ComputationModel/Basic.lean | 155 +++++++++++++----- 1 file changed, 113 insertions(+), 42 deletions(-) diff --git a/Cslib/Computability/Machines/ComputationModel/Basic.lean b/Cslib/Computability/Machines/ComputationModel/Basic.lean index 88ef884d5..5cdf0c435 100644 --- a/Cslib/Computability/Machines/ComputationModel/Basic.lean +++ b/Cslib/Computability/Machines/ComputationModel/Basic.lean @@ -6,99 +6,162 @@ Authors: Maximilian Keßler module -public import Cslib.Foundations.Data.RelatesInSteps +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 Turing +namespace Computation -/-- Bundle of a type `cfg` with a step function `cfg → Option cfg`. -/ -class TransitionSystem (τ : Type*) where - cfg (a : τ) : Type* - step {a : τ} : cfg a → Option (cfg a) - -/-- An abstract version of a turing machine with input alphabet `Γ₀` and output alphabet `Γ₁`. -/ -class Transducer (τ : Type*) (Γᵢₙ Γₒᵤₜ : Type) extends TransitionSystem τ where - init {a : τ} : List Γᵢₙ → cfg a - output {a : τ} : cfg a → List Γₒᵤₜ +/-- +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*} [TransitionSystem τ] +variable {τ : Type u} [TransitionSystem τ] -def stepRelation (tm : τ) : (Option (cfg tm)) → (Option (cfg tm)) → Prop +def stepRelation (t : τ) : (Option (cfg t)) → (Option (cfg t)) → Prop | a, b => a.bind step = b -/-- A "proof" of the fact that `f` eventually reaches `b` when repeatedly evaluated on `a`, -remembering the number of steps it takes. -/ -structure EvalsTo (tm : τ) (a b : Option (cfg tm)) where +/-- +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 -structure EvalsToInTime (tm : τ) (a b : Option (cfg tm)) (n : ℕ) extends EvalsTo tm a b where +/-- +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 {tm : τ} {a b c : Option (cfg tm)} {n n₁ n₂ : ℕ} +variable {t : τ} {a b c : Option (cfg t)} {n n₁ n₂ : ℕ} -def EvalsTo.refl : EvalsTo tm a a where +def EvalsTo.refl : EvalsTo t a a where steps := 0 evals := rfl -def EvalsTo.trans (h₁ : EvalsTo tm a b) (h₂ : EvalsTo tm b c) : EvalsTo tm a c where +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 tm a a 0 where +def EvalsToInTime.refl : EvalsToInTime t a a 0 where toEvalsTo := EvalsTo.refl steps_le := by rfl -def EvalsToInTime.trans (h₁ : EvalsToInTime tm a b n₁) (h₂ : EvalsToInTime tm b c n₂) : - EvalsToInTime tm a c (n₂ + n₁) where +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 tm a b n₁) (hn : n₁ ≤ n₂) : - EvalsToInTime tm a b n₂ where +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 Transducer +namespace TransitionMachine open TransitionSystem -variable {τ : Type*} {Γᵢₙ Γₒᵤₜ : Type} [Transducer τ Γᵢₙ Γₒᵤₜ] +variable {τ : Type*} {Γᵢ Γₒ : Type} [TransitionMachine τ Γᵢ Γₒ] -structure Outputs (tm : τ) (l : List Γᵢₙ) (l' : List Γₒᵤₜ) where - haltState : (cfg tm) +/-- +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 tm (some (init l)) (some haltState) - output_eq : output haltState = l' + evalsTo : TransitionSystem.EvalsTo t (some (init l)) (some haltState) + output_eq : output haltState = some l' -structure OutputsInTime (tm : τ) (n : ℕ) (l : List Γᵢₙ) (l' : List Γₒᵤₜ) where - haltState : (cfg tm) +/-- +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 tm (some (init l)) (some haltState) n - output_eq : output haltState = l' + evals_to : TransitionSystem.EvalsToInTime t (some (init l)) (some haltState) n + output_eq : output haltState = some l' -def OutputsInTime.of_le {tm : τ} {n m : ℕ} {l : List Γᵢₙ} {l' : List Γₒᵤₜ} (hnm : n ≤ m) - (hv : OutputsInTime tm n l l') : OutputsInTime tm m l l' where +/-- +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 -lemma OutputsInTime.output_unique {tm : τ} {n₁ n₂ : ℕ} {l : List Γᵢₙ} {l'₁ l'₂ : List Γₒᵤₜ} - (ho₁ : OutputsInTime tm n₁ l l'₁) (ho₂ : OutputsInTime tm n₂ l l'₂) : +/-- +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 @@ -116,9 +179,17 @@ lemma OutputsInTime.output_unique {tm : τ} {n₁ n₂ : ℕ} {l : List Γᵢₙ have : ho₁.haltState = ho₂.haltState := by apply Option.some.inj rw [← ho₁.evals_to.evals, ← ho₂.evals_to.evals, this] - rw [← ho₁.output_eq, ← ho₂.output_eq, 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 Transducer +end TransitionMachine -end Turing +end Computation