refactor(MultiTapeTM): Put the output tape into the configuration - #819
Open
barni120400 wants to merge 3 commits into
Open
refactor(MultiTapeTM): Put the output tape into the configuration#819barni120400 wants to merge 3 commits into
barni120400 wants to merge 3 commits into
Conversation
crei
reviewed
Aug 19, 2026
Comment on lines
+32
to
+33
| The transition function can optionally output one symbol, which is appended to the output tape held | ||
| in the configuration, so the output of a run can be read off its final configuration. |
Collaborator
There was a problem hiding this comment.
I think this can stay as it is. In this high-level design section we also don't mention how the other tapes are stored exactly.
crei
reviewed
Aug 19, 2026
crei
reviewed
Aug 19, 2026
Collaborator
There was a problem hiding this comment.
Just noticed this - we don't use BiTape any more here:
Suggested change
| is the blank tape symbol). Note that it is not required that `Symbol` or `State` are finite |
barni120400
force-pushed
the
multitape/run-from
branch
from
August 19, 2026 11:17
74eab40 to
871cd39
Compare
crei
approved these changes
Aug 19, 2026
The configuration gains an `output` field holding the symbols emitted so far, `step` appends to it and `initCfg` starts it empty. The output of a run can then be read off its final configuration, so `outputString` and its lemmas are replaced by `step_output` and existing facts about `configs`, and `ComputesInTimeAndSpace` reads the output from the configuration it already mentions. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`configs` returns the single configuration reached after `t` steps, not a sequence of configurations, so the plural name did not match the type. It also depends on `tm` only through its step function. Renamed to `runFrom`, along with its five lemmas. Pure rename, no change to any statement or proof. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Keep the design section free of storage details, list the output tape among a configuration's components, and drop the stale `BiTape` mention. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
barni120400
force-pushed
the
multitape/run-from
branch
from
August 20, 2026 15:43
871cd39 to
3f015fb
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
3 participants
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.
Two independent changes to the multi-tape Turing machine, one per commit.
The first puts the output tape into the configuration:
Cfggains anoutputfield,stepappends the symbol the transition emits, andinitCfgstarts it empty. The output of a run is then whatever is on its final configuration's tape. That makesoutputStringunnecessary, so it and its lemmas are removed:outputString_succbecomesstep_output,outputString_eq_of_haltis restated on configurations, andoutputString_haltandoutputString_add_eq_appendwere output-flavoured restatements of the existingconfigs_of_haltsandconfigs_add.ComputesInTimeAndSpacenow reads the output off the configuration it already mentions.The second renames
configstorunFrom. It returns the single configuration reached aftertsteps rather than a sequence, so the plural name did not match its type, and it depends on the machine only through its step function. Pure rename, no statement or proof changed.This is step 1 of the plan discussed on Zulip: with the output in the configuration, a
Listof configurations determines the output string, so a computation can be such a list and reuse the machinery inRelatesInSteps.lean.Note that the configuration space is now unbounded, so counting reachable configurations needs to happen on the storage configuration rather than on
Cfg.Supersedes #818.
NB: claude was used heavily throughout.