Strict PPT list traversal

An ordinary List.mapM traversal of a strict PPT program is strict PPT on framed list encodings. One polynomial coin budget, chosen from the complete encoded input list, bounds the budget of every element. Independent blocks of one random tape realize all calls. The existing deterministic list calculus charges the traversal, row extraction and complete output encoding.

Main results

• Cslib.Probability.IsPPTOn.mapM: strict PPT is closed under list traversal.
• Cslib.Probability.IsPPTOn.mapMWith: the traversal may capture its complete input.

theorem Cslib.Probability.IsPPTOn.mapM {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} (hprogram : IsPPTOn input output program) : IsPPTOn (Turing.MultiTapeTM.encList input) (Turing.MultiTapeTM.encList output) fun (list : List α) => List.mapM program list

Traverse a framed input list with a strict PPT program. One machine and polynomial clock work for all lists, including the empty list, and charge the complete encoded output list.

theorem Cslib.Probability.IsPPTOn.mapMWith {α β γ : Type} {input : α ↪ List Bool} {element : β ↪ List Bool} {output : γ ↪ List Bool} {list : α → List β} {program : α → β → ProbComp γ} (hprogram : IsPPTOn (Turing.MultiTapeTM.encPair input element) output fun (p : α × β) => program p.1 p.2) (hlist : Turing.MultiTapeTM.ComputableTidilyInPolyTime list input (Turing.MultiTapeTM.encList element)) : IsPPTOn input (Turing.MultiTapeTM.encList output) fun (a : α) => List.mapM (program a) (list a)

A list traversal may use the complete original input in every call. Preparing the pairs charges for repeated captured data as well as all elements of the computed list.