A one-tape machine cutting a framed word at a unary count

The machine Turing.MultiTapeTM.TakeDropUnary.toTM keep reads frame u ++ List.replicate n true. It skips the frame, copies the count n to its work tape (leaving the head on the last true), rewinds the input head and then streams the framed word u, reading u itself as a sequence of frames: it remembers whether the next inner symbol is a marker or follows a marker true. At every inner terminator false the work head moves one cell to the left while it is on a true, so the head position counts the inner frames still to be taken or dropped. Inner symbols are emitted while the count is positive (keep = true) or once it is zero (keep = false).

On u = encList enc l this emits the encoded l.take n or l.drop n. The machine runs in time linear in its input and uses n + 2 work-tape cells. This is the realization behind Turing.MultiTapeTM.ComputableInDegree.takeUnary and .dropUnary; folding over the count or over the list would cost quadratic time.

Main definitions

• Turing.MultiTapeTM.TakeDropUnary.stream: the word emitted while streaming an inner word.
• Turing.MultiTapeTM.TakeDropUnary.toTM: the machine with one work tape.

Main results

• Turing.MultiTapeTM.TakeDropUnary.computesInTimeAndSpace_toTM: on frame u ++ List.replicate n true, toTM keep emits stream keep false n u within 3 * (frame u ++ List.replicate n true).length + 2 steps and n + 2 cells.
• Turing.MultiTapeTM.TakeDropUnary.stream_encList: on an encoded list, the stream is the encoded prefix or suffix.
• Turing.MultiTapeTM.TakeDropUnary.computableInTimeAndSpace: taking or dropping a unary number of encoded list elements within 3 * (input length) + 2 steps and n + 2 cells.

The streaming semantics

def Turing.MultiTapeTM.TakeDropUnary.emits (keep : Bool) (c : ℕ) : Bool

Whether inner symbols are emitted when the remaining count is c: while c is positive when taking (keep = true), once it is zero when dropping (keep = false).

def Turing.MultiTapeTM.TakeDropUnary.stream (keep : Bool) : Bool → ℕ → List Bool → List Bool

stream keep inBit c u: the word emitted while streaming the inner word u with remaining count c, where inBit says whether the next inner symbol follows a marker true (and so is a symbol of the current inner frame). Each inner terminator false decrements the count.

def Turing.MultiTapeTM.TakeDropUnary.nextKind (inBit b : Bool) : Bool

The kind of the next inner symbol after reading b in kind inBit.

def Turing.MultiTapeTM.TakeDropUnary.nextCount (inBit b : Bool) (c : ℕ) : ℕ

The count after reading b in kind inBit.

theorem Turing.MultiTapeTM.TakeDropUnary.stream_cons (keep inBit : Bool) (c : ℕ) (b : Bool) (u : List Bool) : stream keep inBit c (b :: u) = (if emits keep c = true then [b] else []) ++ stream keep (nextKind inBit b) (nextCount inBit b c) u

theorem Turing.MultiTapeTM.TakeDropUnary.stream_frame_append (keep : Bool) (c : ℕ) (w rest : List Bool) : stream keep false c (frame w ++ rest) = (if emits keep c = true then frame w else []) ++ stream keep false (c - 1) rest

Streaming one inner frame emits it when the count admits emission and then continues with the count decremented.

The machine

inductive Turing.MultiTapeTM.TakeDropUnary.State : Type

The control states of TakeDropUnary.toTM.

• skip : State

  Skipping the framed word: expecting a marker.

• skipBit : State

  Skipping the framed word: expecting a symbol.

• copy : State

  Copying the unary count to the work tape.

• rewind : State

  Moving the input head back to its start.

• marker (inBit : Bool) : State

  Streaming: expecting a marker of the outer frame.

• symbol (inBit : Bool) : State

  Streaming: expecting an inner symbol of kind inBit.

instance Turing.MultiTapeTM.TakeDropUnary.State.instFinite : Finite State

def Turing.MultiTapeTM.TakeDropUnary.toTM (keep : Bool) : MultiTapeTM 1 Bool State

The machine with one work tape cutting frame u ++ List.replicate n true: it emits the inner frames of u while the count n lasts (keep = true) or after it is used up (keep = false).

Configurations

The framed input

The phases of the machine

theorem Turing.MultiTapeTM.TakeDropUnary.computesInTimeAndSpace_toTM (keep : Bool) (u : List Bool) (n : ℕ) : (toTM keep).ComputesInTimeAndSpace (frame u ++ List.replicate n true) (stream keep false n u) (3 * (frame u ++ List.replicate n true).length + 2) (n + 2)

On frame u ++ List.replicate n true, toTM keep emits stream keep false n u within 3 * (frame u ++ List.replicate n true).length + 2 steps, visiting the n + 2 work-tape cells -1, …, n.

Encoded lists

theorem Turing.MultiTapeTM.TakeDropUnary.stream_encList {α : Type} (keep : Bool) (enc : α ↪ List Bool) (l : List α) (c : ℕ) : stream keep false c ((encList enc) l) = (encList enc) (if keep = true then List.take c l else List.drop c l)

Streaming an encoded list emits the encoded prefix (keep = true) or suffix (keep = false) at the count.

theorem Turing.MultiTapeTM.TakeDropUnary.computableInTimeAndSpace {α : Type} (keep : Bool) (enc : α ↪ List Bool) : ComputableInTimeAndSpace (fun (p : List α × ℕ) => if keep = true then List.take p.2 p.1 else List.drop p.2 p.1) (encPair (encList enc) encUnary) (encList enc) (fun (p : List α × ℕ) => 3 * ((encPair (encList enc) encUnary) p).length + 2) fun (p : List α × ℕ) => p.2 + 2

Taking (keep = true) or dropping (keep = false) a unary number of elements of an encoded list, by toTM keep, within 3 * (encPair (encList enc) encUnary p).length + 2 steps and p.2 + 2 work-tape cells.