Repository navigation
refactor(MultiTape): simulate machines through adapters - #41
Closed
barni120400 wants to merge 1 commit into
Closed
barni120400 wants to merge 1 commit into
barni120400 wants to merge 1 commit into
Conversation
barni120400
force-pushed
the
refactor/multitape-tape-adapter
branch
6 times, most recently
from
October 24, 2026 19:20
9c4f041 to
fd3a762
Compare
barni120400
changed the title
barni120400
force-pushed
the
refactor/multitape-tape-adapter
branch
2 times, most recently
from
October 24, 2026 20:17
93fa123 to
b6f0da4
Compare
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-tape-adapter
branch
from
October 24, 2026 20:45
b6f0da4 to
192855e
Compare
Owner
Author
|
Moved to #32 (upstream leanprover#1151). |
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.adaptruns a machine through an adapter, andFollows.runningStepHomandFollows.stepHomturn a configuration map that agrees with the adapter into a homomorphism of step relations, so it maps run paths.Defines
extendTapes,outputToTapeandinputFromTapeastmrun through their adapters, 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.Working version of #32 (upstream leanprover#1151), which stays unchanged until this is ready.
Depends on #31.
Composed with Claude Code.