feat(MultiTapeTM): input shortening by barni120400 · Pull Request #12 · barni120400/cslib

barni120400 · 2026-09-12T18:21:41Z

Adds visit sequences of run paths and an input-shortening theorem for multi-tape Turing machines: when two input cells carry the same symbol and a halting computation path visits them with the same storages, deleting the cells after the first through the second preserves every storage reached by a step on either retained side. A long enough input to a space-bounded machine has such a pair of cells.

Collapsing the cut is a homomorphism from the steps on one retained side to the steps of the machine with its output erased, MultiTapeNTM.eraseOutput, built with adapt. Segments of the path between boundary visits map with RelSeries.map and join with smash, and all statements are about computation paths. Replaces the unused not_halts_of_repeat_nonhalt with its path version, RunPath.injOn_running.

Depends on #32.

Composed with Claude Code.

Adds visit sequences of run paths and an input-shortening theorem for multi-tape Turing machines: when two input cells carry the same symbol and a halting computation path visits them with the same storages, deleting the cells after the first through the second preserves every storage reached by a step on either retained side. A long enough input to a space-bounded machine has such a pair of cells. Collapsing the cut is a homomorphism from the steps on one retained side to the steps of the machine with its output erased, `MultiTapeTM.eraseOutput`, built with `adapt`. It comes from the single-step lemma `Follows.step`, which now also gives `stepHom` and `runningStepHom`. Segments of the path between boundary visits map with `RelSeries.map` and join with `smash`, and all statements are about computation paths. Replaces the unused `not_halts_of_repeat_nonhalt` with its path version, `RunPath.injOn_running`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…cut avoids Add `InputCut.Retains` and `InputCut.Avoids` for positions on a retained side of the cut, the latter also away from its endpoints. `exists_storage_eq` now preserves the storage of every configuration of the path that the cut avoids. `exists_shorter_input_storage` takes the space of the halting path only and chooses a cut that avoids the given configuration, so its induction over the path and `exists_inputCut` are gone. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Replace `InputCut.Retains` and `InputCut.Avoids` with `∉ Set.Ioo cut.left cut.right` and `∉ Set.Icc cut.left cut.right`. Make the output erasure and the collapse map private, since no public statement mentions them. Give `ComputationPath` `CoeFun` and `Membership` instances through its run path, so `p i` and `c ∈ p` no longer need `toRunPath`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

`Reached c` now says that the run of the output-erased machine on the shortened input reaches the image of `c` at some time, instead of that some computation path ends there. A side step becomes the lemma `step_cfg`, replacing `sideStepRel` and `stepHom`, and `Reached.slice` is an induction over the path indices, so `Reached.path`, the re-typed run path and `RunPath.inputPos_side` are gone. Several proofs use `grind` with the head-move lemma instead of explicit instances. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Add MultiTapeTM.reachable, the configurations a machine reaches on an input, with step_mem_reachable. Reached is membership of the image in the erased machine's reachable set, and exists_storage_eq and exists_shorter_input_storage conclude that a storage lies in Cfg.storage '' tm.reachable, instead of the existence of a computation path. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Add MultiTapeTM.core_step, that the core of a step depends only on the core, and replace injOn_running by MultiTapeNTM.RunPath.core_injOn_running, both next to Cfg.core. The cut map keeps the output, so a side step maps to a step of the machine itself, and the simulation shows that the image's core is reached on the shortened input. This removes eraseOutput, eraseOutputHom and Reached. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Abbreviate the invariant that the image's core is reached on the shortened input as a private Reached, shortening the statements of the simulation lemmas. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…oofs State the side condition of reached_slice and reached_covBy as SameSide with an endpoint. In exists_shorter_input_storage, infer the signature type, close the side of the cut with grind, and drop the unneeded classical. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

barni120400 mentioned this pull request Sep 12, 2026

feat(MultiTapeTM): loglogn_equals_no_space #13

Open

barni120400 force-pushed the feat/tm-input-shortening branch 2 times, most recently from 23f79eb to 626903e Compare September 18, 2026 14:59

barni120400 changed the base branch from deps/tm-config-bound to main September 21, 2026 16:42