Walking along two lists

Turing.MultiTapeTM.zipFold f p l r walks along l, consuming r in step, and collects f p a b? for each element a of l and the matching element b? of r, if any — that is, (l.zipWithLeft (f p) r).reduceOption (Turing.MultiTapeTM.zipFold_eq_zipWithLeft). The function decides what happens at a missing partner and may drop an element, so that both zipping and padding are instances.

A linear f gives a machine in time the length of l times the length of the input and in linear space, provided that the results collected along the way are linear in the input. An f in linear space, at any time, gives a machine within the input and a bound on those results. The machine folds over l, keeping the rest of r and the results.

Main definitions

• Turing.MultiTapeTM.zipFold: walking along two lists.

Main results

• Turing.MultiTapeTM.zipFold_eq_zipWithLeft: zipFold is List.zipWithLeft followed by List.reduceOption.
• Turing.MultiTapeTM.zipFold_some: a walk that keeps every element is a List.mapIdx reading the second list at each index.
• Turing.MultiTapeTM.ComputableInO.zipFold: the cost of walking along two lists.
• Turing.MultiTapeTM.ComputableInSpace.zipFold: the space of walking along two lists.

def Turing.MultiTapeTM.zipFold {π α β γ : Type} (f : π → α → Option β → Option γ) (p : π) : List α → List β → List γ

Walk along l, consuming r in step, and collect f p a b? for each a in l and the matching element b? of r.

theorem Turing.MultiTapeTM.zipFold_eq_zipWithLeft {π α β γ : Type} (f : π → α → Option β → Option γ) (p : π) (l : List α) (r : List β) : zipFold f p l r = (List.zipWithLeft (f p) l r).reduceOption

Turing.MultiTapeTM.zipFold is List.zipWithLeft followed by List.reduceOption.

theorem Turing.MultiTapeTM.zipFold_some {π α β γ : Type} (g : π → α → Option β → γ) (p : π) (l : List α) (r : List β) : zipFold (fun (p : π) (a : α) (b : Option β) => some (g p a b)) p l r = List.mapIdx (fun (i : ℕ) (a : α) => g p a r[i]?) l

A walk that keeps every element is a List.mapIdx that reads the second list at each index.

theorem Turing.MultiTapeTM.ComputableInO.zipFold {π α β γ : Type} {encP : π ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {f : π → α → Option β → Option γ} [Inhabited β] [Inhabited γ] (hf : ComputableInO (fun (q : π × α × Option β) => f q.1 q.2.1 q.2.2) (encPair encP (encPair encA (encOption encB))) (encOption encC) (fun (q : π × α × Option β) => ((encPair encP (encPair encA (encOption encB))) q).length) fun (q : π × α × Option β) => ((encPair encP (encPair encA (encOption encB))) q).length) (k : ℕ) (hout : ∀ (q : π × List α × List β) (i : ℕ), ((encList encC) (MultiTapeTM.zipFold f q.1 (List.take i q.2.1) q.2.2)).length ≤ k * (((encPair encP (encPair (encList encA) (encList encB))) q).length + 1)) : ComputableInO (fun (q : π × List α × List β) => MultiTapeTM.zipFold f q.1 q.2.1 q.2.2) (encPair encP (encPair (encList encA) (encList encB))) (encList encC) (fun (q : π × List α × List β) => (q.2.1.length + 1) * (((encPair encP (encPair (encList encA) (encList encB))) q).length + 1)) fun (q : π × List α × List β) => ((encPair encP (encPair (encList encA) (encList encB))) q).length

Walking along two lists. For a linear f, whose results collected along the way are linear in the input, walking along two lists takes time the length of the first list times the length of the input, and linear space.

theorem Turing.MultiTapeTM.ComputableInSpace.zipFold {π α β γ : Type} {encP : π ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {f : π → α → Option β → Option γ} [Inhabited β] [Inhabited γ] (hf : ComputableInSpace (fun (q : π × α × Option β) => f q.1 q.2.1 q.2.2) (encPair encP (encPair encA (encOption encB))) (encOption encC) fun (q : π × α × Option β) => ((encPair encP (encPair encA (encOption encB))) q).length) {B : π × List α × List β → ℕ} (hout : ∀ (q : π × List α × List β) (i : ℕ), ((encList encC) (MultiTapeTM.zipFold f q.1 (List.take i q.2.1) q.2.2)).length ≤ B q) : ∃ (K : ℕ), ComputableInSpace (fun (q : π × List α × List β) => MultiTapeTM.zipFold f q.1 q.2.1 q.2.2) (encPair encP (encPair (encList encA) (encList encB))) (encList encC) fun (q : π × List α × List β) => K * (((encPair encP (encPair (encList encA) (encList encB))) q).length + B q + 1)

The space of walking along two lists. For f in linear space, walking along two lists takes space linear in the input and in a bound B on the results collected along the way.