Repository navigation
refactor(MultiTape): rename spaceUsed to space - #1133
Open
barni120400 wants to merge 17 commits into
Open
barni120400 wants to merge 17 commits into
barni120400 wants to merge 17 commits into
Conversation
barni120400
requested review from
SamuelSchlesinger,
arademaker,
chenson2018,
crei,
fmontesi and
sorrachai
as code owners
October 13, 2026 20:30
This was referenced Oct 13, 2026
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>
barni120400
force-pushed
the
refactor/multitape-space-name
branch
from
October 13, 2026 22:10
9d2b691 to
4ea0078
Compare
`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>
barni120400
force-pushed
the
refactor/multitape-space-name
branch
from
October 13, 2026 22:23
4ea0078 to
555ad2b
Compare
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Match the space vocabulary of `Space.lean`, where the cells visited by all tapes of a path are its `space`: `tm.space cfg t` is the space of the path of the first `t` steps from `cfg`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…nfined runs Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
barni120400
force-pushed
the
refactor/multitape-space-name
branch
from
October 13, 2026 22:31
555ad2b to
3677dac
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Renames
MultiTapeTM.spaceUsedtospace, matchingRunPath.spaceandComputationPath.space:tm.space cfg tis the space of the path of the firsttsteps fromcfg. The lemmas named after it follow.Depends on #1117: its commits are included temporarily and will leave this diff when that PR merges. The stack continues in #1122.
Composed with Claude Code.