Sequential composition after function computation

This file fixes the tape layout and executable phase pipeline used to feed one deterministic function computation into a second machine. Proofs of correctness and time bounds live in the internal and public theorem layers.

For a function-computing tmF : TM nf and a second machine tmG : TM ng, the composite has nf + 1 + (ng + 1) work tapes:

• 0 .. nf - 1: work tapes of tmF
• nf: raw redirected output of tmF
• nf + 1 .. nf + ng: work tapes of tmG
• nf + ng + 1: canonical virtual input of tmG

The raw output is rewound and copied to the fresh virtual-input tape before tmG resumes after its compulsory first transition off the left-end markers.

@[reducible, inline]

abbrev Complexity.TM.compositionTapeCount (nf ng : ℕ) : ℕ

Work-tape count of the sequential composition machine.

Equations

• Complexity.TM.compositionTapeCount nf ng = 0 + (nf + 1) + (ng + 1)

def Complexity.TM.compositionRawOutputIdx (nf ng : ℕ) : Fin (compositionTapeCount nf ng)

Physical work tape holding the raw redirected output of the first machine.

Equations

• Complexity.TM.compositionRawOutputIdx nf ng = ⟨nf, ⋯⟩

@[simp]

theorem Complexity.TM.compositionRawOutputIdx_val (nf ng : ℕ) : ↑(compositionRawOutputIdx nf ng) = nf

def Complexity.TM.compositionVirtualInputIdx (nf ng : ℕ) : Fin (compositionTapeCount nf ng)

Physical work tape holding the canonical virtual input of the second machine.

Equations

• Complexity.TM.compositionVirtualInputIdx nf ng = ⟨nf + 1 + ng, ⋯⟩

@[simp]

theorem Complexity.TM.compositionVirtualInputIdx_val (nf ng : ℕ) : ↑(compositionVirtualInputIdx nf ng) = nf + 1 + ng

theorem Complexity.TM.compositionRawOutputIdx_ne_virtualInputIdx (nf ng : ℕ) : compositionRawOutputIdx nf ng ≠ compositionVirtualInputIdx nf ng

The two pipeline tapes occupy distinct physical coordinates.

theorem Complexity.TM.compositionRawOutputIdx_eq_firstPlacedLast (nf ng : ℕ) : compositionRawOutputIdx nf ng = placeWorkIdx 0 (ng + 1) (Fin.last nf)

The raw-output coordinate is the placed last work tape of tmF.retargetOutput.

theorem Complexity.TM.compositionVirtualInputIdx_eq_secondPlacedLast (nf ng : ℕ) : compositionVirtualInputIdx nf ng = placeWorkIdx (0 + (nf + 1)) 0 (Fin.last ng)

The virtual-input coordinate is the placed last work tape of retargetInputStarted tmG.

def Complexity.TM.compositionPrefixIdx (nf ng : ℕ) (i : Fin nf) : Fin (compositionTapeCount nf ng)

Physical coordinate of work tape i of the first computation.

Equations

• Complexity.TM.compositionPrefixIdx nf ng i = ⟨↑i, ⋯⟩

@[simp]

theorem Complexity.TM.compositionPrefixIdx_val (nf ng : ℕ) (i : Fin nf) : ↑(compositionPrefixIdx nf ng i) = ↑i

def Complexity.TM.compositionSecondWorkIdx (nf ng : ℕ) (j : Fin ng) : Fin (compositionTapeCount nf ng)

Physical coordinate of source work tape j of the second computation.

Equations

• Complexity.TM.compositionSecondWorkIdx nf ng j = Complexity.TM.placeWorkIdx (0 + (nf + 1)) 0 j.castSucc

@[simp]

theorem Complexity.TM.compositionSecondWorkIdx_val (nf ng : ℕ) (j : Fin ng) : ↑(compositionSecondWorkIdx nf ng j) = nf + 1 + ↑j

def Complexity.TM.compositionFirstTM {nf : ℕ} (tmF : TM nf) (ng : ℕ) : TM (compositionTapeCount nf ng)

The first phase redirects tmF's output into the raw-output tape and parks the work-tape suffix reserved for the second computation.

Equations

• tmF.compositionFirstTM ng = Complexity.TM.placeWorkTM 0 (ng + 1) tmF.retargetOutput

def Complexity.TM.compositionSecondTM {ng : ℕ} (nf : ℕ) (tmG : TM ng) : TM (compositionTapeCount nf ng)

The last phase places the already-started virtual-input wrapper for tmG after the first computation's work and raw-output tapes.

Equations

• Complexity.TM.compositionSecondTM nf tmG = Complexity.TM.placeWorkTM (0 + (nf + 1)) 0 tmG.retargetInputStarted

def Complexity.TM.compositionTailTM (nf ng : ℕ) (tmG : TM ng) : TM (compositionTapeCount nf ng)

Pipeline after the first computation: rewind its raw output, copy it onto a clean virtual-input tape, rewind that tape, and run the second computation.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.compositionTM {nf ng : ℕ} (tmF : TM nf) (tmG : TM ng) : TM (compositionTapeCount nf ng)

Executable sequential composition of a function computation with a second deterministic machine.

Equations

• tmF.compositionTM tmG = (tmF.compositionFirstTM ng).seqTM (Complexity.TM.compositionTailTM nf ng tmG)