Repository navigation
refactor(MultiTape): remove the deterministic space measures - #31
Merged
Merged
Conversation
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
2 times, most recently
from
October 10, 2026 22:38
e66f0e7 to
6bfb712
Compare
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 11, 2026 13:56
6aa5add to
c9382aa
Compare
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
2 times, most recently
from
October 13, 2026 20:29
18fe0f6 to
875ec7a
Compare
barni120400
changed the base branch from
refactor/multitape-path-simulations
to
refactor/multitape-space-name
October 13, 2026 20:30
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 13, 2026 22:10
875ec7a to
66ff34a
Compare
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 13, 2026 22:23
66ff34a to
4c3900a
Compare
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 13, 2026 22:31
4c3900a to
6ff0a24
Compare
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 14, 2026 13:28
6ff0a24 to
75ff684
Compare
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 14, 2026 16:00
75ff684 to
7c96b26
Compare
barni120400
changed the base branch from
refactor/multitape-space-name
to
main
October 14, 2026 16:09
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 14, 2026 16:09
7c96b26 to
e129036
Compare
barni120400
commented
Oct 14, 2026
| ext z | ||
| simp [RelSeries.mem_snoc, or_and_right, exists_or, eq_comm, or_comm] | ||
|
|
||
| /-! ### Windows -/ |
Owner
Author
There was a problem hiding this comment.
Is this a cslib convension? If not, don't use it
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
2 times, most recently
from
October 18, 2026 14:48
c07d358 to
a73142b
Compare
barni120400
changed the base branch from
main
to
refactor/multitape-space-api-home
October 18, 2026 14:49
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 18, 2026 15:05
a73142b to
09736d7
Compare
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 19, 2026 21:40
09736d7 to
516b637
Compare
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 21, 2026 08:09
516b637 to
43fdfd4
Compare
barni120400
changed the base branch from
refactor/multitape-space-api-home
to
main
October 21, 2026 08:09
…achine (leanprover#904) This PR showcases how HML can be applied to CCS, by distinguishing the classical deterministic and nondeterministic vending machines with the formula `d[Coin](d⟨Tea⟩⊤ ∧ d⟨Coffee⟩⊤)`. Depends on leanprover#863.
…ver#1122) Removes `MultiTapeTM.visitedByTapeHead`, `spaceUsedByTape` and `space`, so space is counted only on run and computation paths. The visitation and displacement lemmas move to run paths and hold for nondeterministic machines. Counts the storages and cores in `ConfigBound` at the ends of computation paths, bounded by `RunsInSpace`, with unchanged numerical bounds. The computation paths of a deterministic machine are prefixes of one another (`RunPath.eq_take`), so the one visiting the most cells contains the windows of every other. Depends on leanprover#1145: its commit is included temporarily and will leave this diff when it merges. Composed with Claude Code. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
barni120400
force-pushed
the
refactor/multitape-single-space-api
branch
from
October 27, 2026 00:29
43fdfd4 to
ff7a819
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
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.
Removes
MultiTapeTM.visitedByTapeHead,spaceUsedByTapeandspace, so space is counted only on run and computation paths. The visitation and displacement lemmas move to run paths and hold for nondeterministic machines.Counts the storages and cores in
ConfigBoundat the ends of computation paths, bounded byRunsInSpace, with unchanged numerical bounds. The computation paths of a deterministic machine are prefixes of one another (RunPath.eq_take), so the one visiting the most cells contains the windows of every other.Depends on #37 (upstream leanprover#1145): its commit is included temporarily and will leave this diff when it merges.
Composed with Claude Code.