feat(MultiTapeTM): redirect input and output through work tapes by SamuelSchlesinger · Pull Request #872 · leanprover/cslib

SamuelSchlesinger · 2026-09-05T21:30:35Z

Add transformations that write output to a fresh work tape and use a work tape in place of native input. Prove execution correspondence, including empty input, boundary clamping, and output emitted on the halting transition.

Part 3/6 of the TM composition stack. Depends on #871. Next: #873.

Validation: strict build, import checks, full tests, and linters.

This PR was composed with Astra via Codex.

crei · 2026-09-06T09:48:35Z

+# Substituting a work tape for the input tape
+
+The first work tape contains the virtual input. The remaining tapes are the native work tapes.
+A classifier distinguishes the two blank boundaries, preserving native head clamping without
+extending the alphabet. One native step takes two steps, and the real input head stays parked.


Suggested change

# Substituting a work tape for the input tape

The first work tape contains the virtual input. The remaining tapes are the native work tapes.

A classifier distinguishes the two blank boundaries, preserving native head clamping without

extending the alphabet. One native step takes two steps, and the real input head stays parked.

# Substituting a work tape for the input tape

This file concerns a Turing machine transformation that returns a modified Turing machine which

uses the first work tape as a virtual input tape, the remaining tapes are the original work tapes.

A classifier distinguishes the two blank boundaries of the original input tape, preserving input

head clamping without extending the alphabet. One original step takes two steps, and the real

input head stays parked.

crei · 2026-09-06T09:53:41Z

+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+
+/-!
+# Substituting a work tape for the input tape


I think this file (or alternatively InputFromWorkTape.lean) deserves a bit more documentation. I don't fully understand what is going on here and why we need two steps in the simulation.

Would it make sense to split the simulation in two parts: First, modify a TM so that the input head never tries to go "out of bounds" and second, the input-tape-to-work-tape substitution?

Also, would it be easier to add the virtual in put tape at the end?

crei · 2026-09-06T09:54:59Z

+/-!
+# Redirecting output to a fresh work tape
+
+`outputToWorkTape` adds one work tape, at index `Fin.last k`, and writes the native output there.


Suggested change

`outputToWorkTape` adds one work tape, at index `Fin.last k`, and writes the native output there.

The function `outputToWorkTape` modifies a Turing machine: It adds one work tape, at index `Fin.last k`, and writes the native output there.

crei · 2026-09-06T09:56:07Z

+  q₀ := tm.q₀
+  tr q input work :=
+    let out := tm.tr q input (fun i => work i.castSucc)
+    ⟨out.inputMove,


Same comment as in the previous PR applies here: please rename out to action

crei · 2026-09-06T09:57:00Z

+variable {Symbol : Type*}
+
+/-- A tape containing exactly the symbols of `xs` at positions `0, ..., xs.length - 1`. -/
+def listTape (xs : List Symbol) : ℤ → Option Symbol


Suggested change

def listTape (xs : List Symbol) : ℤ → Option Symbol

def listToTape (xs : List Symbol) : ℤ → Option Symbol

?

crei · 2026-09-06T10:04:29Z

+      · simp [embed]
+
+/-- Output redirection preserves arbitrary runs, including padded halting times. -/
+lemma runFrom_embed (cfg : Cfg k Symbol State input) (n : ℕ) :


I was wondering if we could generalize this - I think we had the same pattern in the previous PR:

If we have (f tm).step (g cfg) = g (tm.step cfg) for certain f, g and all cfg then (f tm).runFrom (g cfg) n = g (tm.runFrom cfg n)?

This should be it: #878

The interface through which the combinators will use machines: a machine reads words from its work tapes and leaves words on them, never touching the output. Configurations are described by equalities. `listTape` (due to Samuel Schlesinger, leanprover#872 — kept name-identical so the copies dedupe when that lands) turns a word into the tape holding exactly it; `wordsCfg` is the configuration whose tapes hold given words, heads at the start; and the postcondition of `TransformsTapes` is a single configuration equality `runFrom … τ = wordsCfg input none ws' out`, which packages halting, word-holding tapes, the rewound input head and the untouched output in one rewritable equation. Specifications then compose by rewriting rather than by per-tape case analyses. `exists_transformsTapes_nop` — halt in one step, every word unchanged, one visited cell per tape — is the first machine through the interface and the check that the format is inhabited exactly as intended. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Mathlib's naming convention for a constructor of an X from a Y. The name now differs from leanprover#872's `listTape`; the credit note says so. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`seq tm₀ tm₁` behaves like `tm₀` until it would halt and then continues as `tm₁`. The design is due to Samuel Schlesinger (leanprover#872): the state space is the sum, and the halting transition of the first phase is mapped to the initial state of the second, so the handoff costs no step. `transformsTapes_seq` composes two transformations with the bounds adding, and is where the interface's single-equality postcondition pays off: the first machine halts in a full `wordsCfg`, which is on the nose a starting configuration for the second. The proof splits the run at the first machine's minimal halting time (`exists_minimal_halting_time`, new in Deterministic.lean along with `runFrom_eq_of_halt`), mirrors phase one through the left embedding (a bounded induction — the embedding commutes with `step` only while the first machine is live), and phase two through the right embedding, which is a genuine step-semiconjugation, so its run lemma is one application of `runFrom_comm_of_step` from leanprover#878 (cherry-picked; this branch now builds on that PR). Space adds via `spaceUsed_add_le`/`spaceUsed_eq_of_workTapePos`, new in TapeLemmas.lean: space depends only on head positions, which both embeddings preserve. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`outputToTape tm` writes what tm would output onto a fresh last work tape whose head stands at the write frontier — design due to Samuel Schlesinger (leanprover#872). The frontier is the output's length, a function of the configuration, so the redirection is an unconditional step-semiconjugation: the run lemma is one `runFrom_comm_of_step`, and the space cost is exactly the written output (spaceUsed_outputToTape), via the new `length_output_mono`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`inputFromTape tm mark` reads its input from a virtual input work tape instead of the real input tape, which it never touches. Redirecting the input through a work tape is due to Samuel Schlesinger (leanprover#872); there the ambiguity between the two input boundaries — both blank, but the head clamps differently at each — is resolved by a boundary classification in the finite control. Here a flag tape carries a single mark at cell -1, in the spirit of the tidy normal form's footprint anchors, so the left boundary is recognised by reading the flag; the simulated configuration then determines the simulating one and the redirection is an unconditional step-semiconjugation. This commit establishes the machine, the embedding `inCfg`, the projections, and the three facts the semiconjugation rests on: the virtual head reads what the input head reads (`vip_read`), the flag marks exactly the left boundary (`flag_read`), and the clamped move tracks the input head (`clampMove_correct`). The clamp reasoning goes through `val_moveInputPos_eq`, a new `omega`-friendly form of the input head's post-move position as a clamped integer, added to Configuration.lean along with `inputSymbol_eq_none_of_boundary`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

feat(MultiTapeTM): redirect input and output through work tapes

2a15f3a

SamuelSchlesinger requested review from chenson2018 and fmontesi as code owners September 5, 2026 21:30

This was referenced Sep 5, 2026

feat(MultiTapeTM): add input and work tape rewinding #873

Closed

feat(MultiTapeTM): add sequential composition and tape extension #871

Closed

crei reviewed Sep 6, 2026

View reviewed changes

chore(MultiTapeTM): sync reviewed plumbing base

44cc38d

crei mentioned this pull request Sep 11, 2026

feat(MultiTapeTM): TransformsTapes interface and sequential composition #897

Open

SamuelSchlesinger closed this Sep 11, 2026

Navigation Menu

Uh oh!

feat(MultiTapeTM): redirect input and output through work tapes - #872

feat(MultiTapeTM): redirect input and output through work tapes#872
SamuelSchlesinger wants to merge 2 commits into
samschles/tm-02-basic-plumbingfrom
samschles/tm-03-tape-adapters

SamuelSchlesinger commented Sep 5, 2026 •

edited

Loading

Uh oh!

crei Sep 6, 2026

Uh oh!

crei Sep 6, 2026

Uh oh!

crei Sep 6, 2026

Uh oh!

crei Sep 6, 2026

Uh oh!

crei Sep 6, 2026

Uh oh!

crei Sep 6, 2026

Uh oh!

crei Sep 6, 2026 •

edited

Loading

Uh oh!

crei Sep 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	`outputToWorkTape` adds one work tape, at index `Fin.last k`, and writes the native output there.
	The function `outputToWorkTape` modifies a Turing machine: It adds one work tape, at index `Fin.last k`, and writes the native output there.

	def listTape (xs : List Symbol) : ℤ → Option Symbol
	def listToTape (xs : List Symbol) : ℤ → Option Symbol

Uh oh!

Conversation

SamuelSchlesinger commented Sep 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

crei Sep 6, 2026

Choose a reason for hiding this comment

Uh oh!

crei Sep 6, 2026

Choose a reason for hiding this comment

Uh oh!

crei Sep 6, 2026

Choose a reason for hiding this comment

Uh oh!

crei Sep 6, 2026

Choose a reason for hiding this comment

Uh oh!

crei Sep 6, 2026

Choose a reason for hiding this comment

Uh oh!

crei Sep 6, 2026

Choose a reason for hiding this comment

Uh oh!

crei Sep 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

crei Sep 7, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

SamuelSchlesinger commented Sep 5, 2026 •

edited

Loading

crei Sep 6, 2026 •

edited

Loading