feat(MultiTapeTM): Nondeterministic multi-tape Turing machines by barni120400 · Pull Request #820 · leanprover/cslib

barni120400 · 2026-08-19T11:20:11Z

Builds on #819 — only the last commit is new here, the first three are that PR.

Adds nondeterministic multi-tape Turing machines: the transition function is replaced by a transition relation, and a computation is a RelSeries of the step relation starting at the initial configuration, so its length, the configurations it visits and the one it halts in all come from Mathlib. MultiTapeTM.toNTM embeds the deterministic machine and preserves computation in bounded time and space.

Configurations and the effect of a transition move to a shared MultiTape/Basic.lean. No existing statement changes meaning.

NB: claude was used heavily throughout.

crei · 2026-08-19T14:58:14Z

+/-- `ntm` has a computation on `input` that starts at the initial configuration, halts, emits
+`output` and satisfies `P`. The notions below are its instances, so their constraints all refer to
+a single computation. -/
+def ComputesSuchThat (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol)


This kind of hides the fact that P only has to hold for some computation path. Maybe this should be a bit more visible in the name?

I did it on purpose, because by definition a computation of a non-deterministic machine is existance of a computation path.
So I didn't want to carry this existence in the name outside the "ComputesSuchThat".
I think the alternative is "ExistComputationPathSuchThat" but I think "ComputesSuchThat" is better

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>

A nondeterministic machine replaces the transition function by a transition relation. Configurations and the effect of an action move to a shared `MultiTape/Configuration.lean`; no existing statement changes meaning. A computation path is a `RelSeries` of the step relation starting at the initial configuration, so Mathlib supplies its length, the configurations it passes through, and the one it ends at. `MultiTapeTM.toNTM` embeds the deterministic machine and `toNTM_computes` shows the embedding preserves computation in bounded time and space. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

barni120400 requested review from chenson2018 and fmontesi as code owners August 19, 2026 11:20

barni120400 mentioned this pull request Aug 19, 2026

refactor(MultiTapeTM): Make the deterministic machine a nondeterministic one #821

Draft

crei reviewed Aug 19, 2026

View reviewed changes

chriseth mentioned this pull request Aug 20, 2026

feat(Data): Results about RelatesInSteps with bounds on the reachable set #779

Open

barni120400 force-pushed the multitape/ntm branch from ff38796 to 52f938a Compare August 20, 2026 08:58