Finding, filtering and mapping with parameters

One left fold over list x applies a test or function to the parameter par x and the current element. The time bound charges each round for the parameter, the list, the accumulator and the largest cost of the test or function on an element.

Main results

• Turing.MultiTapeTM.ComputableInO.findWith: the first element passing a test.
• Turing.MultiTapeTM.ComputableInO.filterWith: the elements passing a test.
• Turing.MultiTapeTM.ComputableInO.mapWith: the images of the elements.

References

Derived from Christian Reitwiessner's original list-combinator construction, using the plain fold rules and independent time and workspace bounds.

theorem Turing.MultiTapeTM.ComputableInO.findWith {γ α π : Type} {encIn : γ ↪ List Bool} {enc : α ↪ List Bool} {encP : π ↪ List Bool} {par : γ → π} {list : γ → List α} {Tp Tl Sp Sl : γ → ℕ} {t : π × α → Bool} {Tt St : π × α → ℕ} (ht : ComputableInO t (encPair encP enc) encBool Tt St) (hpar : ComputableInO par encIn encP Tp Sp) (hlist : ComputableInO list encIn (encList enc) Tl Sl) : ComputableInO (fun (x : γ) => List.find? (fun (a : α) => t (par x, a)) (list x)) encIn (encOption enc) (fun (x : γ) => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * ((encP (par x)).length + ((encList enc) (list x)).length + listMax (fun (a : α) => Tt (par x, a)) (list x))) fun (x : γ) => (encIn x).length + Sp x + Sl x + (encP (par x)).length + ((encList enc) (list x)).length + listMax (fun (a : α) => St (par x, a)) (list x)

The first element of list x passing the test t with the parameter par x.

theorem Turing.MultiTapeTM.ComputableInO.filterWith {γ α π : Type} {encIn : γ ↪ List Bool} {enc : α ↪ List Bool} {encP : π ↪ List Bool} {par : γ → π} {list : γ → List α} {Tp Tl Sp Sl : γ → ℕ} {t : π × α → Bool} {Tt St : π × α → ℕ} (ht : ComputableInO t (encPair encP enc) encBool Tt St) (hpar : ComputableInO par encIn encP Tp Sp) (hlist : ComputableInO list encIn (encList enc) Tl Sl) : ComputableInO (fun (x : γ) => List.filter (fun (a : α) => t (par x, a)) (list x)) encIn (encList enc) (fun (x : γ) => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * ((encP (par x)).length + ((encList enc) (list x)).length + listMax (fun (a : α) => Tt (par x, a)) (list x))) fun (x : γ) => (encIn x).length + Sp x + Sl x + (encP (par x)).length + ((encList enc) (list x)).length + listMax (fun (a : α) => St (par x, a)) (list x)

The elements of list x passing the test t with the parameter par x.

theorem Turing.MultiTapeTM.ComputableInO.mapWith {γ α β π : Type} {encIn : γ ↪ List Bool} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {encP : π ↪ List Bool} {par : γ → π} {list : γ → List α} {Tp Tl Sp Sl : γ → ℕ} {f : π × α → β} {Tf Sf : π × α → ℕ} (hf : ComputableInO f (encPair encP enc) encB Tf Sf) (hpar : ComputableInO par encIn encP Tp Sp) (hlist : ComputableInO list encIn (encList enc) Tl Sl) : ComputableInO (fun (x : γ) => List.map (fun (a : α) => f (par x, a)) (list x)) encIn (encList encB) (fun (x : γ) => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * ((encP (par x)).length + ((encList enc) (list x)).length + ((encList encB) (List.map (fun (a : α) => f (par x, a)) (list x))).length + listMax (fun (a : α) => Tf (par x, a)) (list x))) fun (x : γ) => (encIn x).length + Sp x + Sl x + (encP (par x)).length + ((encList enc) (list x)).length + ((encList encB) (List.map (fun (a : α) => f (par x, a)) (list x))).length + listMax (fun (a : α) => Sf (par x, a)) (list x)

Mapping f with the parameter par x over list x.