Repository navigation
refactor(MultiTape): simulate machines through adapters - #1151
Open
barni120400 wants to merge 2 commits into
Open
barni120400 wants to merge 2 commits into
barni120400 wants to merge 2 commits into
Conversation
barni120400
requested review from
SamuelSchlesinger,
arademaker,
chenson2018,
crei,
fmontesi and
sorrachai
as code owners
October 19, 2026 13:39
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
2 times, most recently
from
October 19, 2026 21:40
21b4e08 to
f33ed1b
Compare
Space is counted only on run and computation paths. The visitation and displacement lemmas hold for the run paths of nondeterministic machines, and the configuration bounds take `RunsInSpace` and count the storages and cores at the ends of computation paths: the computation paths of a deterministic machine are prefixes of one another, so the one visiting the most cells contains the windows of every other. The deterministic `visitedByTapeHead`, `spaceUsedByTape` and `space` go, with their lemmas and the unused `core_step_eq_of_core_eq`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 21, 2026 08:09
f33ed1b to
7c214a5
Compare
SamuelSchlesinger
approved these changes
Oct 23, 2026
A machine follows another when it performs each of its transitions through an adapter: what the inner machine reads, computed from the symbols under the heads of the outer machine (`HeadSymbols`), and the outer action performing each inner action. `adapt` runs a machine through an adapter, and `Follows.runningStepHom` and `Follows.stepHom` turn a configuration map that agrees with the adapter into a homomorphism of step relations. `extendTapes`, `outputToTape` and `inputFromTape` run `tm` through their adapters, so their homomorphisms come from `follows_adapt`. `seq` and `repeatUntilBlank` relabel the actions of their inner machines with `Action.mapState` and follow them by definition, and `prependOutputHom` follows the machine itself. This replaces the step lemmas of each simulation and the deterministic `stepHom` and `runningStepHom`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 24, 2026 20:50
7c214a5 to
192855e
Compare
barni120400
changed the title
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
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.
Lets a machine follow another: it performs each transition of the inner machine through an adapter, which computes what the inner machine reads from the symbols under the outer heads (
HeadSymbols) and gives the outer action performing each inner action.Follows.runningStepHomandFollows.stepHomturn a configuration map that agrees with the adapter into a homomorphism of step relations, so it maps run paths.Defines
extendTapes,outputToTapeandinputFromTapeas the machine run through an adapter (MultiTapeTM.adapt), so their homomorphisms come fromfollows_adapt.seqandrepeatUntilBlankrelabel the actions of their inner machines withAction.mapStateand follow them by definition, andprependOutputHomfollows the machine itself. This replaces the step lemmas of each simulation and the deterministicstepHomandrunningStepHom, and shortens the proofs that use them.Depends on #1122: its commit is included temporarily and will leave this diff when it merges.
Composed with Claude Code.