Emitting finite-alphabet codewords

Reading a source letter emits its opening delimiter. Finite control then emits its unary index and closing delimiter. A complete output costs exactly its binary encoded length plus one final halting transition.

structure Complexity.MathlibTM0.AlphabetMachine.Emitting {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (tape : Turing.Tape M.simulatorSource.binary.Alphabet) (emitted : List Bool) (d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w) : Prop

Output emission from the represented source tape.

• state : d.state = some (Phase.source Control.emit)

  Ready to read the next source letter.

• output : d.output = emitted

  Previously emitted bits.

• tape (i : Fin (Fintype.card M.simulatorSource.binary.Alphabet)) (z : ℤ) : d.workTapes i (d.workTapePos i + z) = SymbolTracks.encode (tape.nth z) ((trackEquiv M.simulatorSource.binary) i)

  Remaining source tape relative to the work heads.

structure Complexity.MathlibTM0.AlphabetMachine.Pending {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (n : Fin (co.size + 1)) (tape : Turing.Tape M.simulatorSource.binary.Alphabet) (emitted : List Bool) (d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w) : Prop

A symbol's opening delimiter has been emitted; its index and closing delimiter remain.

• state : d.state = some (Phase.emit n)

  Remaining unary index bits.

• output : d.output = emitted

  Previously emitted bits.

• tape (i : Fin (Fintype.card M.simulatorSource.binary.Alphabet)) (z : ℤ) : d.workTapes i (d.workTapePos i + z) = SymbolTracks.encode (tape.nth z) ((trackEquiv M.simulatorSource.binary) i)

  Source tracks are already positioned at the following letter.

theorem Complexity.MathlibTM0.AlphabetMachine.Emitting.read {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} {tape : Turing.Tape M.simulatorSource.binary.Alphabet} {emitted : List Bool} {d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w} (h : M.Emitting ci co tape emitted d) : (SymbolTracks.decode fun (a : M.simulatorSource.binary.Alphabet) => d.workTapeSymbols ((trackEquiv M.simulatorSource.binary).symm a)) = tape.head

theorem Complexity.MathlibTM0.AlphabetMachine.pending_run {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (n : ℕ) (hn : n < co.size + 1) {w : List Bool} {tape : Turing.Tape M.simulatorSource.binary.Alphabet} {emitted : List Bool} {d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w} (h : M.Pending ci co ⟨n, hn⟩ tape emitted d) : M.Emitting ci co tape (emitted ++ List.replicate n true ++ [false]) (Turing.MultiTapeTM.runFrom d (n + 1))

theorem Complexity.MathlibTM0.AlphabetMachine.Emitting.start {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} {tape : Turing.Tape M.simulatorSource.binary.Alphabet} {emitted : List Bool} {d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w} (h : M.Emitting ci co tape emitted d) (a : Output) (ha : M.readSymbol (MarkedMachine.Symbol.value tape.head) = some a) : M.Pending ci co ⟨↑(co.index a), ⋯⟩ (Turing.Tape.move Turing.Dir.right tape) (emitted ++ [false]) (Turing.MultiTapeTM.step d)

theorem Complexity.MathlibTM0.AlphabetMachine.Emitting.halt {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} {tape : Turing.Tape M.simulatorSource.binary.Alphabet} {emitted : List Bool} {d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w} (h : M.Emitting ci co tape emitted d) (ha : M.readSymbol (MarkedMachine.Symbol.value tape.head) = none) : (Turing.MultiTapeTM.step d).state = none ∧ (Turing.MultiTapeTM.step d).output = emitted

theorem Complexity.MathlibTM0.AlphabetMachine.Emitting.run {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (output : List Output) {tape : Turing.Tape M.simulatorSource.binary.Alphabet} {emitted : List Bool} {d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w} (h : M.Emitting ci co tape emitted d) (ho : ∀ (j : ℕ), M.readSymbol (MarkedMachine.Symbol.value (tape.nth ↑j)) = output[j]?) : (Turing.MultiTapeTM.runFrom d ((co.encode output).length + 1)).state = none ∧ (Turing.MultiTapeTM.runFrom d ((co.encode output).length + 1)).output = emitted ++ co.encode output