Composing closed probabilistic machines through a buffered word

The first machine writes to a fresh buffer. A deterministic handoff rewinds the buffer and marks its left boundary. The second machine then reads this word as its input, starting with separate blank work tapes. Preparation costs the intermediate word length plus four transitions.

Main definitions

• Turing.MultiTapePTM.comp: feed one closed machine's output to another.

Main results

• Turing.MultiTapePTM.eval_comp: the compiled output distribution is monadic composition.

References

Adapted from MultiTape/Oracle/Composition.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common machine compilers. As for upstream deterministic composition, second.comp first mark executes first and then second.

@[reducible, inline]

abbrev Turing.MultiTapePTM.Composition.source {k₀ : ℕ} {Symbol State₀ : Type} (machine : MultiTapePTM k₀ Symbol State₀) (k₁ : ℕ) : MultiTapePTM (k₁ + k₀ + 2) Symbol State₀

The shared output-buffer compiler, specialized to fair-coin machines.

@[reducible, inline]

abbrev Turing.MultiTapePTM.Composition.consumer {k₁ : ℕ} {Symbol State₁ : Type} (machine : MultiTapePTM k₁ Symbol State₁) (k₀ : ℕ) : MultiTapePTM (k₁ + k₀ + 2) Symbol State₁

The shared virtual-input compiler, specialized to fair-coin machines.

noncomputable def Turing.MultiTapePTM.Composition.continuation {k₁ : ℕ} {Symbol State₁ : Type} (machine : MultiTapePTM k₁ Symbol State₁) (k₀ : ℕ) (mark : Symbol) : MultiTapePTM (k₁ + k₀ + 2) Symbol ((MultiTapeTM.MarkWorkState ⊕ MultiTapeTM.RewindWorkState) ⊕ State₁)

Rewind and mark the intermediate word before starting the continuation.

theorem Turing.MultiTapePTM.Composition.runClosedConfigFrom_source {k₀ : ℕ} {Symbol State₀ : Type} (machine : MultiTapePTM k₀ Symbol State₀) (k₁ fuel : ℕ) (input : List Symbol) : (source machine k₁).runClosedConfigFrom fuel (MultiTapeMachine.initialConfig (source machine k₁) input) = MultiTapeMachine.Composition.buffer k₁ <$> machine.runClosedConfigFrom fuel (MultiTapeMachine.initialConfig machine input)

Buffering the source preserves its complete configuration program.

theorem Turing.MultiTapePTM.Composition.runClosedConfigFrom_consumer {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (machine : MultiTapePTM k₁ Symbol State₁) (mark : Symbol) (cfg₀ : MultiTapeMachine.Config k₀ Symbol State₀ Empty input) (cfg₁ : MultiTapeMachine.Config k₁ Symbol State₁ Empty cfg₀.tapes.output) (fuel : ℕ) : (consumer machine k₀).runClosedConfigFrom fuel (MultiTapeMachine.Composition.consumerConfig mark cfg₀ cfg₁) = MultiTapeMachine.Composition.consumerConfig mark cfg₀ <$> machine.runClosedConfigFrom fuel cfg₁

The consumer preserves the continuation's complete configuration program.

theorem Turing.MultiTapePTM.Composition.consumer_halted {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (machine : MultiTapePTM k₁ Symbol State₁) (mark : Symbol) (cfg : MultiTapeMachine.Config k₀ Symbol State₀ Empty input) (fuel : ℕ) (hhalt : ∀ final ∈ (machine.runClosedConfigFrom fuel (MultiTapeMachine.initialConfig machine cfg.tapes.output)).eval.support, final.tapes.state = none) (final : MultiTapeMachine.Config (k₁ + k₀ + 2) Symbol State₁ Empty input) : final ∈ ((consumer machine k₀).runClosedConfigFrom fuel (MultiTapeMachine.Composition.consumerConfig mark cfg (MultiTapeMachine.initialConfig machine cfg.tapes.output))).eval.support → final.tapes.state = none

Virtual-input redirection preserves a halting bound.

theorem Turing.MultiTapePTM.Composition.eval_runClosedConfigFrom_continuation {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (machine : MultiTapePTM k₁ Symbol State₁) (mark : Symbol) (cfg : MultiTapeMachine.Config k₀ Symbol State₀ Empty input) (prepareTime runTime : ℕ) (hprepare : cfg.tapes.output.length + 4 ≤ prepareTime) (hrun : ∀ final ∈ (machine.runClosedConfigFrom runTime (MultiTapeMachine.initialConfig machine cfg.tapes.output)).eval.support, final.tapes.state = none) : ((continuation machine k₀ mark).runClosedConfigFrom (prepareTime + runTime) (MultiTapeMachine.Sequential.start (continuation machine k₀ mark) (MultiTapeMachine.Composition.buffer k₁ cfg))).eval = PMF.map (fun (final : MultiTapeMachine.Config k₁ Symbol State₁ Empty cfg.tapes.output) => MultiTapeMachine.Sequential.right (MultiTapeMachine.Composition.consumerConfig mark cfg final)) (machine.runClosedConfigFrom runTime (MultiTapeMachine.initialConfig machine cfg.tapes.output)).eval

Once preparation and execution have been paid for, the continuation has its source law.

theorem Turing.MultiTapePTM.Composition.continuation_halted {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (machine : MultiTapePTM k₁ Symbol State₁) (mark : Symbol) (cfg : MultiTapeMachine.Config k₀ Symbol State₀ Empty input) (prepareTime runTime : ℕ) (hprepare : cfg.tapes.output.length + 4 ≤ prepareTime) (hrun : ∀ final ∈ (machine.runClosedConfigFrom runTime (MultiTapeMachine.initialConfig machine cfg.tapes.output)).eval.support, final.tapes.state = none) (final : MultiTapeMachine.Config (k₁ + k₀ + 2) Symbol ((MultiTapeTM.MarkWorkState ⊕ MultiTapeTM.RewindWorkState) ⊕ State₁) Empty input) : final ∈ ((continuation machine k₀ mark).runClosedConfigFrom (prepareTime + runTime) (MultiTapeMachine.Sequential.start (continuation machine k₀ mark) (MultiTapeMachine.Composition.buffer k₁ cfg))).eval.support → final.tapes.state = none

The handoff and continuation actually halt within the combined bound.

theorem Turing.MultiTapePTM.Composition.output_mem {k₀ : ℕ} {Symbol State₀ : Type} (machine : MultiTapePTM k₀ Symbol State₀) (fuel : ℕ) (input : List Symbol) (final : MultiTapeMachine.Config k₀ Symbol State₀ Empty input) (hfinal : final ∈ (machine.runClosedConfigFrom fuel (MultiTapeMachine.initialConfig machine input)).eval.support) : final.tapes.output ∈ (machine.runClosed fuel input).eval.support

A supported final configuration supplies a supported output word.

noncomputable def Turing.MultiTapePTM.comp {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} (second : MultiTapePTM k₁ Symbol State₁) (first : MultiTapePTM k₀ Symbol State₀) (mark : Symbol) : MultiTapePTM (k₁ + k₀ + 2) Symbol (State₀ ⊕ (MultiTapeTM.MarkWorkState ⊕ MultiTapeTM.RewindWorkState) ⊕ State₁)

Feed first's output to second, with separate work tapes and a charged input handoff.

theorem Turing.MultiTapePTM.eval_runClosedConfigFrom_comp {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapePTM k₀ Symbol State₀) (second : MultiTapePTM k₁ Symbol State₁) (mark : Symbol) (input : List Symbol) (firstTime secondTime : ℕ) (hfirst : ∀ final ∈ (first.runClosedConfigFrom firstTime (MultiTapeMachine.initialConfig first input)).eval.support, final.tapes.state = none) (hsecond : ∀ word ∈ (first.runClosed firstTime input).eval.support, ∀ final ∈ (second.runClosedConfigFrom secondTime (MultiTapeMachine.initialConfig second word)).eval.support, final.tapes.state = none) : ((second.comp first mark).runClosedConfigFrom (firstTime + (firstTime + 4 + secondTime)) (MultiTapeMachine.initialConfig (second.comp first mark) input)).eval = do let sourceFinal ← (first.runClosedConfigFrom firstTime (MultiTapeMachine.initialConfig first input)).eval PMF.map (MultiTapeMachine.Composition.finalConfig mark sourceFinal) (second.runClosedConfigFrom secondTime (MultiTapeMachine.initialConfig second sourceFinal.tapes.output)).eval

Composition preserves the full configuration distribution and charges the intermediate word. The first phase takes firstTime, preparation at most firstTime + 4, and the second phase secondTime. Both source bounds concern actual halting, including random stopping times.

theorem Turing.MultiTapePTM.eval_comp {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapePTM k₀ Symbol State₀) (second : MultiTapePTM k₁ Symbol State₁) (mark : Symbol) (input : List Symbol) (firstTime secondTime : ℕ) (hfirst : ∀ final ∈ (first.runClosedConfigFrom firstTime (MultiTapeMachine.initialConfig first input)).eval.support, final.tapes.state = none) (hsecond : ∀ word ∈ (first.runClosed firstTime input).eval.support, ∀ final ∈ (second.runClosedConfigFrom secondTime (MultiTapeMachine.initialConfig second word)).eval.support, final.tapes.state = none) : ((second.comp first mark).runClosed (firstTime + (firstTime + 4 + secondTime)) input).eval = do let word ← (first.runClosed firstTime input).eval (second.runClosed secondTime word).eval

At the output level, the compiled machine realizes ordinary monadic composition.

theorem Turing.MultiTapePTM.comp_halted {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapePTM k₀ Symbol State₀) (second : MultiTapePTM k₁ Symbol State₁) (mark : Symbol) (input : List Symbol) (firstTime secondTime : ℕ) (hfirst : ∀ final ∈ (first.runClosedConfigFrom firstTime (MultiTapeMachine.initialConfig first input)).eval.support, final.tapes.state = none) (hsecond : ∀ word ∈ (first.runClosed firstTime input).eval.support, ∀ final ∈ (second.runClosedConfigFrom secondTime (MultiTapeMachine.initialConfig second word)).eval.support, final.tapes.state = none) (final : MultiTapeMachine.Config (k₁ + k₀ + 2) Symbol (State₀ ⊕ (MultiTapeTM.MarkWorkState ⊕ MultiTapeTM.RewindWorkState) ⊕ State₁) Empty input) : final ∈ ((second.comp first mark).runClosedConfigFrom (firstTime + (firstTime + 4 + secondTime)) (MultiTapeMachine.initialConfig (second.comp first mark) input)).eval.support → final.tapes.state = none

Every supported execution of the composed machine has halted within the combined bound.