Skip to content

fix(MultiTapeTM): Remove output from the configuration type of a Turing machine - #745

Merged
fmontesi merged 2 commits into
leanprover:mainfrom
crei:tm_remove_output_from_Cfg
Jul 25, 2026
Merged

fix(MultiTapeTM): Remove output from the configuration type of a Turing machine#745
fmontesi merged 2 commits into
leanprover:mainfrom
crei:tm_remove_output_from_Cfg

Conversation

@crei

@crei crei commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

The configuration should only contain data that influences the future behaviour of the Turing machine. While it is convenient to put the "output so far" in the configuration, it leads to more problems down the line, for example when the number of reachable configurations is determined or if we want to reason about loops in the configuration graph.

NB: claude was used for a review of this PR and it did some refactoring.

crei added 2 commits July 24, 2026 19:49
The configuration should only contain data that influences the future
behaviour of the Turing machine. While it is convenient to put the
"output so far" in the configuration, it leads to more problems down the
line, for example when the number of reachable configurations is
determined or if we want to reason about loops in the configuration
graph.
@crei crei changed the title Remove output from the configuration type of a Turing machine. fix(MultiTapeTM): Remove output from the configuration type of a Turing machine. Jul 24, 2026
@crei
crei marked this pull request as ready for review July 24, 2026 20:59

@SamuelSchlesinger SamuelSchlesinger left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, just remove the period from the PR title.

@crei crei changed the title fix(MultiTapeTM): Remove output from the configuration type of a Turing machine. fix(MultiTapeTM): Remove output from the configuration type of a Turing machine Jul 24, 2026
@fmontesi
fmontesi added this pull request to the merge queue Jul 25, 2026
Merged via the queue into leanprover:main with commit 2867c46 Jul 25, 2026
2 of 5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants