feat(MultiTapeTM): compose machines using tape transformations

[SamuelSchlesinger]

Construct machine composition from output redirection, work-tape rewind, and input substitution using the sequential combinator. Prove that the composite halts with the second machine's output on the first machine's result.

Part 5/6 of the TM composition stack. Depends on #873. Next: #875.

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

This PR was composed with Astra via Codex.

[crei]

I haven't read all of this PR yet, but I'm a bit surprised that there is still so much code to it. Maybe the plumbing is not abstract enough or does not have enough lemmas?

[crei]

I think it would be better to first explain what it does and then how it does it. It reads like we already know where this is going.

[crei]

Suggested change

	{input out₀ out₁ : List Symbol} {u v : ℕ}
	{input out₀ out₁ : List Symbol} {t\0 t\1 : ℕ}

[crei]

This could also be a bit more stand-alone. What is "the composite machine"?

[crei]

I think what this sequence of pull requests could be missing is returning to some normal form between computation sub-segments, i.e. the proofs are arguing on the Cfg level, but I think there should be an abstraction one level higher.

My AI has come up with the following, in which configurations are simplified to words (as in your model) but in addition, the tape heads are required to move to the initial position. On top of that, there is some Hoare-like logic, which allows us to compose the sub-segments:

/-- The configuration whose work tape `i` holds exactly the word `ws i` with its head at the
start, whose input head is at the start of the input, in state `q` with output `out`. -/
@[expose, simps]
public def wordsCfg (input : List Symbol) (q : Option State)
    (ws : Fin k → List Symbol) (out : List Symbol) : Cfg k Symbol State input :=
  ⟨q, 1, fun i => tapeOfList (ws i), fun _ => 0, out⟩

/-- The initial configuration is the word configuration with blank tapes and no output. -/
public lemma initCfg_eq_wordsCfg (tm : MultiTapeTM k Symbol State) (input : List Symbol) :
    tm.initCfg input = wordsCfg input (some tm.q₀) (fun _ => []) [] := by
  refine Cfg.ext rfl rfl ?_ rfl rfl
  funext i
  simp [Cfg.init, wordsCfg]

/-- `TransformsTapes tm P Q t s`: started in its initial state on tapes holding words `ws` that
satisfy the precondition `P`, the machine halts after at most `t` steps in the configuration whose
tapes hold words `ws'` with `Q input ws ws'`, with the input head back at the start and the output
unchanged, having used at most `s` work-tape cells.

The postcondition is a single configuration equality, so a machine satisfying it has re-normalised
everything: heads at the start, tapes blank outside their words, nothing written to the output.
The bounds are numbers; a specification whose bounds depend on the data is a *family*
`∀ j, TransformsTapes tm (P j) (Q j) (t j) (s j)` over one fixed machine. -/
@[expose] public def TransformsTapes (tm : MultiTapeTM k Symbol State)
    (P : (input : List Symbol) → (Fin k → List Symbol) → Prop)
    (Q : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop)
    (t s : ℕ) : Prop :=
  ∀ (input : List Symbol) (ws : Fin k → List Symbol) (out : List Symbol), P input ws →
    ∃ τ ≤ t, ∃ ws',
      tm.runFrom (wordsCfg input (some tm.q₀) ws out) τ = wordsCfg input none ws' out ∧
      Q input ws ws' ∧
      tm.spaceUsed (wordsCfg input (some tm.q₀) ws out) τ ≤ s

I'm trying this out now on a new branch and see how complicated function composition would be, but also already aiming towards a "loop combinator".