feat(MultitapeTM): Prove an exponential upper bound in the number of configurations reachable in bounded space by crei · Pull Request #772 · leanprover/cslib

crei · 2026-08-03T10:12:25Z

Proves an upper bound on the number of configurations reachable in bounded space on a multi-tape TM.

The proof introduces the concept of Storage, the projection of Cfg that only contain the state and the work tapes. It shows that if the TM uses at most s space, there is an injection to a structure that only uses [-s, s] to index the tape.

…hable in bounded space.

crei · 2026-08-19T13:31:21Z

#819 should be merged first, I'll update this one in a minute.

…bounded_space

crei · 2026-08-29T09:57:30Z

This is now updated to the new definition of Cfg. I kept most of it so that it also applies to nondeterministic machines, so once that is merged, it should be easy to adapt.

barni120400 · 2026-08-29T10:59:44Z

+lemma Storage.FitsIn_mono {x : UnboundedStorage Symbol State k} : Monotone x.FitsIn := by
+  intro w₁ w₂ h_le h_fits
+  refine ⟨?_, ?_⟩
+  · intro j
+    grind [h_fits.pos_le j, h_le j]
+  · intro j z h_ne
+    grind [h_fits.cell_le j z h_ne, h_le j]


Suggested change

lemma Storage.FitsIn_mono {x : UnboundedStorage Symbol State k} : Monotone x.FitsIn := by

intro w₁ w₂ h_le h_fits

refine ⟨?_, ?_⟩

· intro j

grind [h_fits.pos_le j, h_le j]

· intro j z h_ne

grind [h_fits.cell_le j z h_ne, h_le j]

lemma Storage.FitsIn_mono {x : UnboundedStorage Symbol State k} : Monotone x.FitsIn :=

fun _ _ hle h => ⟨fun j => (h.pos_le j).trans (hle j),

fun j z hz => (h.cell_le j z hz).trans (hle j)⟩

I mean this is shorter, but not sure it is better. I replaced grind by your explicit proofs, though, so one sees that nothing "fancy" is going on.

barni120400 · 2026-08-29T10:59:44Z

+  rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy
+  simp only [Storage.toBounded, Storage.mk.injEq] at hxy
+  obtain ⟨hstate, htapes, hpos⟩ := hxy
+  refine Storage.ext hstate (funext₂ fun j z => ?_) (funext fun j => ?_)
+  · by_cases hz : z ∈ window (w j)
+    · exact congrFun (congrFun htapes j) ⟨z, hz⟩
+    · grind
+  · grind [congrFun hpos j]


Suggested change

rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy

simp only [Storage.toBounded, Storage.mk.injEq] at hxy

obtain ⟨hstate, htapes, hpos⟩ := hxy

refine Storage.ext hstate (funext₂ fun j z => ?_) (funext fun j => ?_)

· by_cases hz : z ∈ window (w j)

· exact congrFun (congrFun htapes j) ⟨z, hz⟩

· grind

· grind [congrFun hpos j]

rintro x hx y hy hxy

simp only [Storage.toBounded, Storage.mk.injEq, funext_iff, Subtype.forall,

Storage.mem_window] at hxy

ext j z j' <;> grind [hx.pos_le, hx.cell_le, hy.pos_le, hy.cell_le]

barni120400 · 2026-08-29T10:59:44Z

+  calc {x : UnboundedStorage Symbol State k | x.FitsIn w}.encard
+      = ((Storage.toBounded · w) '' {x | x.FitsIn w}).encard :=
+        ((Storage.toBounded_injOn w).encard_image).symm
+    _ ≤ (Set.univ : Set (BoundedStorage Symbol State w)).encard :=
+        Set.encard_le_encard (Set.subset_univ _)
+    _ = Fintype.card (BoundedStorage Symbol State w) := by
+        simp [Set.encard_univ, ENat.card_eq_coe_fintype_card]
+    _ ≤ storageBound Symbol State k s := by
+        exact_mod_cast card_boundedStorage_le hsum


Suggested change

calc {x : UnboundedStorage Symbol State k | x.FitsIn w}.encard

= ((Storage.toBounded · w) '' {x | x.FitsIn w}).encard :=

((Storage.toBounded_injOn w).encard_image).symm

_ ≤ (Set.univ : Set (BoundedStorage Symbol State w)).encard :=

Set.encard_le_encard (Set.subset_univ _)

_ = Fintype.card (BoundedStorage Symbol State w) := by

simp [Set.encard_univ, ENat.card_eq_coe_fintype_card]

_ ≤ storageBound Symbol State k s := by

exact_mod_cast card_boundedStorage_le hsum

rw [← (Storage.toBounded_injOn w).encard_image]

refine Set.encard_le_card.trans ?_

rw [ENat.card_eq_coe_fintype_card]

exact_mod_cast card_boundedStorage_le hsum

barni120400 · 2026-08-29T10:59:44Z

+  refine ⟨?_, ?_⟩
+  · intro j
+    simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited
+      (tm.mem_visitedByTapeHead_self (tm.initCfg input) t j)
+  · intro j
+    exact content_natAbs_le_spaceUsedByTape t


Suggested change

refine ⟨?_, ?_⟩

· intro j

simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited

(tm.mem_visitedByTapeHead_self (tm.initCfg input) t j)

· intro j

exact content_natAbs_le_spaceUsedByTape t

refine ⟨fun j => ?_, fun j => content_natAbs_le_spaceUsedByTape t⟩

simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited

(tm.mem_visitedByTapeHead_self (tm.initCfg input) t j)

barni120400 · 2026-08-29T10:59:44Z

+        refine Set.encard_le_encard ?_
+        rintro _ ⟨t, rfl⟩
+        exact ⟨Set.mem_univ _, t, rfl⟩


Suggested change

refine Set.encard_le_encard ?_

rintro _ ⟨t, rfl⟩

exact ⟨Set.mem_univ _, t, rfl⟩

exact Set.encard_le_encard (Set.range_subset_iff.2 fun t => ⟨Set.mem_univ _, t, rfl⟩)

barni120400 · 2026-08-29T10:59:44Z

+  have : Fintype Symbol := Fintype.ofFinite Symbol
+  have : Fintype State := Fintype.ofFinite State
+  obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k)
+  refine ⟨a, c, fun input s hs => (tm.encard_cores_le hs).trans ?_⟩
+  calc ((input.length + 2) * storageBound Symbol State k s : ℕ∞)
+      ≤ ((input.length + 2) * (a * 2 ^ (c * s)) : ℕ) := by
+        exact_mod_cast Nat.mul_le_mul_left _ (hpow s)
+    _ = (input.length + 2) * a * 2 ^ (c * s) := by push_cast; ring


Suggested change

have : Fintype Symbol := Fintype.ofFinite Symbol

have : Fintype State := Fintype.ofFinite State

obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k)

refine ⟨a, c, fun input s hs => (tm.encard_cores_le hs).trans ?_⟩

calc ((input.length + 2) * storageBound Symbol State k s : ℕ∞)

≤ ((input.length + 2) * (a * 2 ^ (c * s)) : ℕ) := by

exact_mod_cast Nat.mul_le_mul_left _ (hpow s)

_ = (input.length + 2) * a * 2 ^ (c * s) := by push_cast; ring

cases nonempty_fintype Symbol

cases nonempty_fintype State

obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k)

refine ⟨a, c, fun input s hs => (tm.encard_cores_le hs).trans ?_⟩

rw [mul_assoc]

gcongr

exact_mod_cast hpow s

barni120400 · 2026-08-29T10:59:44Z

+  have hmono : ∀ j, tm.spaceUsedByTape cfg T j ≤ tm.spaceUsedByTape cfg (max t T) j :=
+    fun j => tm.spaceUsedByTape_mono cfg j (le_max_right t T)
+  have hsup : tm.spaceUsed cfg (max t T) ≤ tm.spaceUsed cfg T :=
+    (le_csSup hbdd ⟨max t T, rfl⟩).trans hT.ge
+  have hsum : ∑ j, tm.spaceUsedByTape cfg T j = ∑ j, tm.spaceUsedByTape cfg (max t T) j :=
+    le_antisymm (Finset.sum_le_sum fun j _ => hmono j) hsup
+  have heq := (Finset.sum_eq_sum_iff_of_le fun j _ => hmono j).mp hsum i (Finset.mem_univ i)
+  exact heq ▸ tm.spaceUsedByTape_mono cfg i (le_max_left t T)


Suggested change

have hmono : ∀ j, tm.spaceUsedByTape cfg T j ≤ tm.spaceUsedByTape cfg (max t T) j :=

fun j => tm.spaceUsedByTape_mono cfg j (le_max_right t T)

have hsup : tm.spaceUsed cfg (max t T) ≤ tm.spaceUsed cfg T :=

(le_csSup hbdd ⟨max t T, rfl⟩).trans hT.ge

have hsum : ∑ j, tm.spaceUsedByTape cfg T j = ∑ j, tm.spaceUsedByTape cfg (max t T) j :=

le_antisymm (Finset.sum_le_sum fun j _ => hmono j) hsup

have heq := (Finset.sum_eq_sum_iff_of_le fun j _ => hmono j).mp hsum i (Finset.mem_univ i)

exact heq ▸ tm.spaceUsedByTape_mono cfg i (le_max_left t T)

have hmono : ∀ j ∈ Finset.univ,

tm.spaceUsedByTape cfg T j ≤ tm.spaceUsedByTape cfg (max t T) j :=

fun j _ => tm.spaceUsedByTape_mono cfg j (le_max_right t T)

have heq := (Finset.sum_eq_sum_iff_of_le hmono).mp

(le_antisymm (Finset.sum_le_sum hmono) ((le_csSup hbdd ⟨max t T, rfl⟩).trans hT.ge))

exact heq i (Finset.mem_univ i) ▸ tm.spaceUsedByTape_mono cfg i (le_max_left t T)

barni120400 · 2026-08-29T11:09:14Z

+def window (s : ℕ) : Finset ℤ := Finset.Icc (-(s : ℤ)) s
+
+@[scoped grind =]
+lemma Storage.mem_window {s : ℕ} {z : ℤ} : z ∈ window s ↔ z.natAbs ≤ s := by


Why are lemmas about window in "Storage" namespace?

barni120400 · 2026-08-29T11:09:47Z

 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound


Insert in alphabetical order of imports

barni120400 · 2026-08-29T11:44:48Z

+/-- The state and work-tape data of a machine, with the cells and head position of tape `i` indexed
+by an arbitrary type `ι i`. -/
+@[ext]
+structure Storage (Symbol State : Type*) {k : ℕ} (ι : Fin k → Type*) where


I think that (ι : Fin k → Type*) is an overkill for what you want to achieve here.
It is instanciated twice, once at ℤ and once at the subtype ↥(window (w i)).
Consider defining Storage over ℤ directly, and replacing Storage.toBounded with a Storage.restrict that lands straight in the product type:

structure Storage (Symbol State : Type*) (k : ℕ) where /-- the state of the TM (cf. `Cfg.state`) -/ state : Option State /-- the contents of work tape `i` (cf. `Cfg.workTapes`) -/ workTapes : Fin k → ℤ → Option Symbol /-- the position of the head on work tape `i` (cf. `Cfg.workTapePos`) -/ workTapePos : Fin k → ℤ /-- Restriction of a storage to the finite windows `w` (with heads outside their window clamped to `0`). -/ def Storage.restrict (x : Storage Symbol State k) (w : Fin k → ℕ) : Option State × ((i : Fin k) → window (w i) → Option Symbol) × ((i : Fin k) → window (w i)) := (x.state, fun j z => x.workTapes j z.1, fun j => if h : x.workTapePos j ∈ window (w j) then ⟨_, h⟩ else ⟨0, Storage.mem_window.mpr (Nat.zero_le _)⟩)

It saves a lot of code

…ded version.

barni120400 · 2026-08-29T13:24:50Z

+
+/-- The part of a configuration that the machine can still read: the input head position together
+with the `Storage`, i.e. the configuration without the write-only output tape. -/
+def Cfg.core (c : Cfg k Symbol State input) :


I don't how good the terms "Storage" and "Core". I don't see any standard name for specifically these stuff, so maybe just call them ore explicitely instead of assigning new terms?

barni120400 · 2026-08-29T13:27:43Z

+open Cslib
+


Suggested change

open Cslib

barni120400 · 2026-08-29T13:27:43Z

+/-- The restriction is injective on storages that fit in the windows. -/
+lemma Storage.toBounded_injOn (w : Fin k → ℕ) :
+    Set.InjOn (Storage.toBounded (Symbol := Symbol) (State := State) · w) {x | x.FitsIn w} := by
+  rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy


Suggested change

rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy

rintro x ⟨_, _⟩ y ⟨_, _⟩ hxy

barni120400 · 2026-08-29T13:33:19Z

+
+/-! ## The storage and the core of a configuration
+
+Now we relate `Cfg` and `Storage` by givin the projection.


Suggested change

Now we relate `Cfg` and `Storage` by givin the projection.

Now we relate `Cfg` and `Storage` by giving the projection.

Prove an exponential upper bound in the number of configurations reac…

5bc455a

…hable in bounded space.

crei requested review from chenson2018 and fmontesi as code owners August 3, 2026 10:12

SamuelSchlesinger approved these changes Aug 14, 2026

View reviewed changes

Merge branch 'main' into configs_reachable_in_bounded_space

2bb3f3b

crei marked this pull request as draft August 27, 2026 10:28

crei added 3 commits August 27, 2026 12:28

Changes required by including the output tape in Cfg.

69b097b

cleanup

4876d03

Merge remote-tracking branch 'origin/main' into configs_reachable_in_…

417d7b1

…bounded_space

crei marked this pull request as ready for review August 29, 2026 09:56

barni120400 reviewed Aug 29, 2026

View reviewed changes

crei added 2 commits August 29, 2026 13:49

Review comments.

fa7ed1d

Define Storage only for \Int-indexed tapes and use tuple for the boun…

2ac2da5

…ded version.

barni120400 reviewed Aug 29, 2026

View reviewed changes

	rintro x ⟨hxp, hxc⟩ y ⟨hyp, hyc⟩ hxy
	rintro x ⟨_, _⟩ y ⟨_, _⟩ hxy


		/-! ## The storage and the core of a configuration

		Now we relate `Cfg` and `Storage` by givin the projection.

Uh oh!

Conversation

crei commented Aug 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

crei commented Aug 19, 2026

Uh oh!

crei commented Aug 29, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

crei commented Aug 3, 2026 •

edited

Loading