Taking and dropping list elements in linear time

Taking or dropping the first n elements of a list encoded by Turing.MultiTapeTM.encList, with n in unary, has cost and output degree one. Both are computed by the one-tape machine Turing.MultiTapeTM.TakeDropUnary.toTM, which copies the count to its work tape and then streams the encoded list once, moving the work head at every element boundary. Folding over the count or over the list would cost quadratic time.

Main results

• Turing.MultiTapeTM.ComputableInDegree.takeUnary: the first n elements.
• Turing.MultiTapeTM.ComputableInDegree.dropUnary: all but the first n elements.

theorem Turing.MultiTapeTM.ComputableInDegree.takeUnary {α : Type} (enc : α ↪ List Bool) : ComputableInDegree (fun (p : List α × ℕ) => List.take p.2 p.1) (encPair (encList enc) encUnary) (encList enc) 1 1

Taking the first n elements, with n in unary, in linear time.

theorem Turing.MultiTapeTM.ComputableInDegree.dropUnary {α : Type} (enc : α ↪ List Bool) : ComputableInDegree (fun (p : List α × ℕ) => List.drop p.2 p.1) (encPair (encList enc) encUnary) (encList enc) 1 1

Dropping the first n elements, with n in unary, in linear time.