refactor(MultiTape): express simulations and tape specifications through run paths by barni120400 · Pull Request #1117 · leanprover/cslib

barni120400 · 2026-10-10T22:10:27Z

Expresses the tape simulations, tape specifications and sequential composition through run paths. stepHom reads a semiconjugation of step as a homomorphism of the step relations, which maps run paths, and each of extendTapes, outputToTape and inputFromTape bounds the space of the mapped path through RunPath.space_map_le, replacing the per-file iteration and space proofs.

spaceUsed becomes an abbreviation for the space of the path of the first t steps, so TransformsTapes keeps its statement. Sequential composition derives its space bound from the existing state-free invariant. The deterministic space lemmas used only by these proofs and the unused Cfg.withOutput are removed.

The stack continues in #1133.

Composed with Claude Code.

…1116) Adds `RunPath.ofDeterministic` and `ComputationPath.ofDeterministic`, built directly from `step`, and proves that every deterministic path is the canonical path from its head. The halted-run and output-to-tape proofs reuse the shared path API. First step toward counting time and space only on run and computation paths. The stack continues in leanprover#1117. Composed with Codex; description written with Claude Code. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

crei

I love the homomorphism formalism, just some questions and docstring clarifications.

crei · 2026-10-13T07:31:29Z

    Cfg k Symbol State input :=
  Cfg.init ntm.q₀ input

+/-- The one-step relation on configurations for `input`, as a set of pairs. A map of configurations


I think the second sentence is more confusing than helpful.

crei · 2026-10-13T08:08:24Z

 attains its per-tape space usage at a single step, which makes a bound that holds at every point
 in time usable as a bound for the whole run.

+A simulation maps every run path of one machine to a run path of another with `RunPath.map`.


This reads like it would introduce the term simulation - could you put MultiTapeNTM.RunPath.space_map_le at the front, so it's clear that this paragraph is about explaining that lemma?

crei · 2026-10-13T08:15:49Z

+the tapes `j` of the source path, and the head of every other tape `l` stays in `S l`, then the
+mapped path uses the space of the source path plus the cells of `S l` for every other tape `l`. -/
+lemma space_map_le (p : ntm.RunPath input) (f : (ntm.stepRel input).Hom (ntm'.stepRel input'))
+    (e : Fin k ↪ Fin k') (S : Fin k' → Finset ℤ)


S should be lowercase and could also use more than one letter - this lemma has a lot of variables.

crei · 2026-10-13T08:19:01Z

  exact Finset.card_le_card (tm.visitedByTapeHead_mono cfg i h)

-/-- The total space used is monotone in the number of steps. -/
-lemma spaceUsed_mono (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) :


Why did you delete this? I see that a proof that used it before does not need it any more - is it somehow obvious with the new definitions?

I think that because we switched to RunPath the proof that used it don't need anymore to compare runs of different lengths.

crei · 2026-10-13T08:20:47Z

-    exact tm.mem_visitedByTapeHead_self cfg τ i
-
-/-- After the machine has halted the heads no longer move, so the space usage stops growing. -/
-lemma spaceUsed_eq_of_halt (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t)


The halting lemmas are also gone - is that obvious with the homomorphism formalism?

Not because of the homomorphism, it's because we use RunPath which make it very simple.

crei · 2026-10-13T08:24:24Z

        wordsCfg input none ws' (out ++ emitted) ∧
      Q input ws ws' emitted ∧
-      tm.spaceUsed (wordsCfg input (some tm.q₀) ws out) t ≤ s
+      (RunPath.ofDeterministic tm (wordsCfg input (some tm.q₀) ws out) t).space ≤ s


This is a bit difficult to read, do we not have the spaceUsed definition any more? Or is this a matter of it just being defeq and easier to use in this form?

Thats a good point. Now spaceUsed is a duplicated definition we don't want, but I change it to be a convenient wrapper for (RunPath.ofDeterministic tm cfg t).space which makes it readable

To be consistent with the naming I'll just call it space. But it will be in the next PR as there are still consumers of spaceUsed I haven't changed

Package the configuration maps of `extendTapes`, `outputToTape` and `inputFromTape` as step-preserving maps that transport run paths, and state their space bounds on the mapped path. Runs of the simulating machine follow from `runFrom_map` instead of per-file iteration proofs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Generate the hom apply lemmas with `simps`, derive the deterministic `spaceUsedByTape_le_card` from the shared path lemma, and drop the unused `space_map_noTapes_le` and the single-use projection lemma. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Nothing used `withOutputHom`. Remove it together with the lemmas and definitions only it relied on: `step_outputToTape_withOutput`, `RunPath.space_map_eq` and `Cfg.withOutput`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

State the space clause of `TransformsTapes` like `RunsInSpace`: every run from the start visits at most `s` cells. Sequential composition then bounds its space through the existing state-free invariant, without splitting the run at the first halt, and the deterministic space lemmas used only by the plumbing are removed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

State the space clause of `TransformsTapes` on the path of its first `t` steps, the path counterpart of the old `spaceUsed`. The halting argument moves into `TransformsTapes.imp`, through `runFrom_mem_ofDeterministic` and `RunPath.space_le_of_subset`, and the other specifications return to their original shape. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

`stepHom` reads a `Function.Semiconj` of the step functions as a homomorphism of the step relations; state the simulation step lemmas in that form and explain the construction in `embedHom`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

`RunPath.space_map_le` now takes sets containing the head positions of the extra tapes instead of a space bound for each of them, so the simulations state where their extra heads stay and the conversion to space happens once. `spaceUsedByTape_map_le_card` is removed. Explain `embedHom` in its docstring. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Define `spaceUsed` as an abbreviation for the space of the path of the first `t` steps, so `TransformsTapes` keeps its original statement while space is counted on paths. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

`ConfinedRun` now states that every head stays within `[-r, r]` at each step, so a round splits its run with `runFrom_add` and the final space bound comes from `RunPath.space_le_sum_card`. This removes the uses of the deterministic splitting, monotonicity and halting space lemmas, and the now unused `spaceUsed_le_of_visited_subset_Icc`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

`ConfinedRun` now reads the canonical path of the run: its last configuration and `RunPath.InWindow`, which says every head stays in `window r`. Runs compose with `ConfinedRun.trans` through the new `RunPath.ofDeterministic_add` (the path analogue of `runFrom_add`), and a halted run extends with `ConfinedRun.add_of_halted`, so the final space bound is `InWindow.space_le`. Moves `window` from `ConfigBound` to `TapeLemmas` and replaces `visitedByTapeHead_subset_Icc` with `inWindow_ofDeterministic`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

`ConfinedRun` was the canonical path of a run together with its last configuration and `InWindow`, which for a deterministic machine is just a run path in a window. The rounds of `repeatUntilBlank` are now run paths joined with `smash`, and the joined path gives the run and its space through `runFrom_head_eq_last` and `spaceUsed_head_le`. This removes `ConfinedRun` and `RunPath.ofDeterministic_add`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…paths `TransformsTapes` now asks for a run path to the halted normal form, with its time and space bounded. Combinators compose these paths: `seq` and `repeatUntilBlank` map the running steps of their parts with `runningStepHom` and join them with `smash`, and `tapeEmb` and the output generality map whole paths. `RunPath.exists_running` cuts a path at its first halted configuration, which replaces `HaltsAt`, `exists_haltsAt` and `existsUnique_haltsAt`. Mapping running steps replaces `runFrom_runCfg`, `runFrom_leftCfg`, `runFrom_rightCfg`, `HaltsAt.runFrom_seq`, `runFrom_seq` and `forgetState_runFrom_seq`, now `exists_runPath_seq`. This also removes `runFrom_succ`, `runFrom_add`, `runFrom_mem_ofDeterministic`, `runFrom_head_eq_last` and `spaceUsed_head_le`, and states the window bound as `RunPath.inWindow_of_space_le`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Adapt Tidy/Defs to upstream changes: rename `spaceUsed` to `space` (#1133) and state `computesTidily_iff` through run paths, following the `TransformsTapes` refactor in #1117.

Renames `MultiTapeTM.spaceUsed` to `space`, matching `RunPath.space` and `ComputationPath.space`: `tm.space cfg t` is the space of the path of the first `t` steps from `cfg`. The lemmas named after it follow. Depends on leanprover#1117: its commits are included temporarily and will leave this diff when that PR merges. The stack continues in leanprover#1122. Composed with Claude Code. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

barni120400 requested review from SamuelSchlesinger, arademaker, chenson2018, crei, fmontesi and sorrachai as code owners October 10, 2026 22:10

This was referenced Oct 10, 2026

refactor(MultiTape): add deterministic path constructors #1116

Merged

refactor(MultiTape): remove the deterministic space measures #1122

Open

SamuelSchlesinger reviewed Oct 10, 2026

View reviewed changes

Comment thread Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean Outdated

SamuelSchlesinger reviewed Oct 10, 2026

View reviewed changes

Comment thread Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean Outdated

barni120400 force-pushed the refactor/multitape-path-simulations branch from 0940347 to 9b2cf9a Compare October 11, 2026 13:56

barni120400 force-pushed the refactor/multitape-path-simulations branch from 9b2cf9a to 66e9d12 Compare October 12, 2026 08:50

barni120400 requested a review from SamuelSchlesinger October 12, 2026 09:20

barni120400 force-pushed the refactor/multitape-path-simulations branch from 66e9d12 to be5e7fa Compare October 12, 2026 16:09

crei requested changes Oct 13, 2026

View reviewed changes

barni120400 mentioned this pull request Oct 13, 2026

refactor(MultiTape): rename spaceUsed to space #1133

Merged

barni120400 force-pushed the refactor/multitape-path-simulations branch from d4d32b2 to c32d63c Compare October 13, 2026 21:43

barni120400 and others added 12 commits October 14, 2026 01:07

doc(MultiTape): keep the simulation module docs close to the original

6921170

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

style(MultiTape): drop an unneeded classical

ba4188d

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

doc(MultiTape): clarify the path-map docs and name the window sets

cfc7f30

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

refactor(MultiTape): read spaceUsed off the canonical path

0b768c3

Define `spaceUsed` as an abbreviation for the space of the path of the first `t` steps, so `TransformsTapes` keeps its original statement while space is counted on paths. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

barni120400 force-pushed the refactor/multitape-path-simulations branch from b7713cc to 4e0fecf Compare October 13, 2026 22:10

barni120400 and others added 3 commits October 14, 2026 01:21

refactor(MultiTape): run a round of the loop from its specification

9055753

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

crei approved these changes Oct 14, 2026

View reviewed changes

crei added this pull request to the merge queue Oct 14, 2026

Merged via the queue into leanprover:main with commit 19a3f67 Oct 14, 2026
2 checks passed

crei added a commit that referenced this pull request Oct 15, 2026

Merge leanprover/cslib main into crei/tidy

59c2258

Adapt Tidy/Defs to upstream changes: rename `spaceUsed` to `space` (#1133) and state `computesTidily_iff` through run paths, following the `TransformsTapes` refactor in #1117.

Conversation

barni120400 commented Oct 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

crei left a comment

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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

barni120400 Oct 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

barni120400 Oct 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

barni120400 commented Oct 10, 2026 •

edited

Loading

barni120400 Oct 13, 2026 •

edited

Loading

barni120400 Oct 13, 2026 •

edited

Loading